mechanism for multiple errors printed at end of file

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 ) )
+  foo x = bind {_} {_} {_} (Just x) (\ x => Just x)
-    with ( ( ?m:4 x:0 ) ( ?m:7 x:0 ) )
+  failed to unify ( Maybe ( ?m:10 x:0 ) )
-  non-variable in pattern (%meta 7 [< (%var 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)

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

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}"
+      -- put a list of errors in TopContext
-      throwError $ E (l,c) "Unsolved meta \{show k}"
+      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')
 

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 ::)

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.

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