From 38f01065eb5470612aa5bdfad0b678e4b0943c3c Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Wed, 18 Sep 2024 22:21:10 -0700
Subject: [PATCH] mechanism for multiple errors printed at end of file

---
 newt/typeclass.newt     | 22 ++++++++++++++++++----
 src/Lib/Check.idr       |  5 +++--
 src/Lib/ProcessDecl.idr |  6 ++++--
 src/Lib/TopContext.idr  |  8 ++++++--
 src/Lib/Types.idr       |  3 +--
 src/Main.idr            | 10 +++++++++-
 6 files changed, 41 insertions(+), 13 deletions(-)

diff --git a/newt/typeclass.newt b/newt/typeclass.newt
index 07b8ed3..35f5855 100644
--- a/newt/typeclass.newt
+++ b/newt/typeclass.newt
@@ -48,10 +48,24 @@ ptype Int
 So I think we need to solve meta 7 first, and then if we're lucky, it's var 0 and we're
 good to go.
 
-failed to unify ( Maybe ( ?m:9 x:0 ) )
-    with ( ( ?m:4 x:0 ) ( ?m:7 x:0 ) )
-  non-variable in pattern (%meta 7 [< (%var 0 [< ])])
+  foo x = bind {_} {_} {_} (Just x) (\ x => Just x)
+  failed to unify ( Maybe ( ?m:10 x:0 ) )
+    with ( ( ?m:4 x:0 ) ( ?m:8 x:0 ) )
+  non-variable in pattern (%meta 8 [< (%var 0 [< ])])
+
+  If I stick Int in third slot:
+  foo x = bind {_} {_} {Int} (Just x) (\ x => Just x)
+                                    ^
+  failed to unify ( Maybe ( ?m:8 x:0 ) )
+    with ( ( ?m:4 x:0 ) Int )
+  non-variable in pattern (%ref Int [< ])
+
+  -- If I slot in MaybeMonad, all is happy.
+  foo x = bind {_} {MaybeMonad} {_} (Just x) (\ x => Just x)
+
+  -- And a maybe up front has only the auto unsolved.
+
 -/
 
 foo : Int -> Maybe Int
-foo x = bind {_} {_} (Just x) (\ x => Just x)
+foo x = bind {Maybe} {_} {_} (Just x) (\ x => Just x)
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index d5facb0..809987b 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -223,8 +223,9 @@ insert ctx tm ty = do
     VPi fc x Implicit a b => do
       m <- freshMeta ctx (getFC tm) a
       debug "INSERT \{pprint (names ctx) m} : \{show a}"
+      debug "TM \{pprint (names ctx) tm}"
       mv <- eval ctx.env CBN m
-      insert ctx (App emptyFC tm m) !(b $$ mv)
+      insert ctx (App (getFC tm) tm m) !(b $$ mv)
     va => pure (tm, va)
 
 primType : FC -> String -> M Val
@@ -574,7 +575,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of
               let var = VVar fc (length ctx.env) [<]
               let ctx' = extend ctx nm a
               tm' <- check ctx' tm !(b $$ var)
-              pure $ Lam emptyFC nm tm'
+              pure $ Lam fc nm tm'
             else if icit' == Implicit then do
               let var = VVar fc (length ctx.env) [<]
               ty' <- b $$ var
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index af1c98a..b1b9b80 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -85,8 +85,10 @@ processDecl (Def fc nm clauses) = do
     (Unsolved (l,c) k xs ty) => do
       -- should just print, but it's too subtle in the sea of messages
       -- we'd also need the ability to mark the whole top context as failure if we continue
-      -- putStrLn "ERROR at (\{show l}, \{show c}): Unsolved meta \{show k}"
-      throwError $ E (l,c) "Unsolved meta \{show k}"
+      -- put a list of errors in TopContext
+      putStrLn $ showError "" $ E (l,c) "Unsolved meta \{show k}"
+      addError $ E (l,c) "Unsolved meta \{show k}"
+      -- throwError $ E (l,c) "Unsolved meta \{show k}"
   debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
   modify $ setDef nm ty (Fn tm')
 
diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr
index cbf35a3..976b181 100644
--- a/src/Lib/TopContext.idr
+++ b/src/Lib/TopContext.idr
@@ -19,11 +19,11 @@ lookup nm top = go top.defs
 export
 covering
 Show TopContext where
-  show (MkTop defs metas _) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]"
+  show (MkTop defs metas _ _) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]"
 
 public export
 empty : HasIO m => m TopContext
-empty = pure $ MkTop [] !(newIORef (MC [] 0)) False
+empty = pure $ MkTop [] !(newIORef (MC [] 0)) False !(newIORef [])
 
 ||| set or replace def. probably need to check types and Axiom on replace
 public export
@@ -35,3 +35,7 @@ setDef name ty def = { defs $= go }
     go (x@(MkEntry nm ty' def') :: defs) = if nm == name
       then MkEntry name ty def :: defs
       else x :: go defs
+
+public export
+addError : HasIO io => {auto top : TopContext} -> Error -> io ()
+addError err = modifyIORef top.errors (err ::)
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 98dff26..371414a 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -346,8 +346,7 @@ record TopContext where
   defs : List TopEntry
   metas : IORef MetaContext
   verbose : Bool
-  -- metas : TODO
-
+  errors : IORef (List Error)
 
 
 -- we'll use this for typechecking, but need to keep a TopContext around too.
diff --git a/src/Main.idr b/src/Main.idr
index b12b9fe..8b985b2 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -55,9 +55,17 @@ processFile fn = do
   Right _ <- tryError $ traverse_ processDecl (collectDecl res.decls)
     | Left y => fail (showError src y)
 
-  dumpContext !get
+  top <- get
+  dumpContext top
   dumpSource
 
+  [] <- readIORef top.errors
+    | errors => do
+      for_ errors $ \err =>
+        putStrLn (showError src err)
+      exitFailure
+  pure ()
+
 main' : M ()
 main' = do
   args <- getArgs