Improve auto solving - 30% faster and hopefully proper errors if a type mismatch is blocking it.

port/Lib/CompileExp.newt

@@ -115,7 +115,7 @@ compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME
 compileTerm (Lam _ nm _ _ t) = CLam nm <$> compileTerm t
 compileTerm tm@(App _ _ _) = case funArgs tm of
   (Meta _ k, args) => do
-        -- this will be undefined, should only happen for use metas
+        info (getFC tm) "Compiling an unsolved meta \{show tm}"
         pure $ CApp (CRef "Meta\{show k}") Nil 0
   (t@(Ref fc nm _), args) => do
         args' <- traverse compileTerm args

port/Lib/Elab.newt

@@ -6,6 +6,7 @@ import Data.String
 import Data.IORef
 import Lib.Types
 import Lib.Eval
+import Lib.Util
 import Lib.TopContext
 import Lib.Syntax
 
@@ -137,7 +138,7 @@ findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
   -- FIXME we're restoring state, but the INFO logs have already been emitted
   -- Also redo this whole thing to run during elab, recheck constraints, etc.
   mc <- readIORef top.metaCtx
-  catchError(do
+  catchError (do
       -- TODO sort out the FC here
       let fc = getFC ty
       debug $ \ _ => "TRY \{show name} : \{rpprint Nil type} for \{show ty}"
@@ -145,6 +146,9 @@ findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
       -- tm <- check (mkCtx fc) (RVar fc name) ty
       -- FIXME RVar should optionally have qualified names
       let (QN ns nm) = name
+
+      let (cod, tele) = splitTele type
+      modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next CheckFirst
       tm <- check ctx (RVar fc nm) ty
       debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}"
       writeIORef top.metaCtx mc
@@ -276,7 +280,7 @@ updateMeta ix f = do
   top <- get
   mc <- readIORef top.metaCtx
   metas <- go mc.metas
-  writeIORef top.metaCtx $ MC metas mc.next
+  writeIORef top.metaCtx $ MC metas mc.next mc.mcmode
   where
     go : List MetaEntry -> M (List MetaEntry)
     go Nil = error' "Meta \{show ix} not found"
@@ -301,12 +305,14 @@ checkAutos ix (_ :: rest) = checkAutos ix rest
 
 addConstraint : Env -> Int -> SnocList Val -> Val -> M Unit
 addConstraint env ix sp tm = do
+  top <- get
+  mc <- readIORef top.metaCtx
+  let (CheckAll) = mc.mcmode | _ => pure MkUnit
   updateMeta ix $ \case
     (Unsolved pos k a b c cons) => do
       debug $ \ _ => "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
       pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons))
     (Solved _ k tm) => error' "Meta \{show k} already solved (addConstraint :: Nil)"
-  top <- get
   mc <- readIORef top.metaCtx
   checkAutos ix mc.metas
   -- this loops too
@@ -401,6 +407,18 @@ unify : Env -> UnifyMode -> Val -> Val  -> M UnifyResult
 .boundNames : Context -> List String
 ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ zip ctx.bds (map fst ctx.types)
 
+maybeCheck : M Unit -> M Unit
+maybeCheck action = do
+  top <- get
+  mc <- readIORef top.metaCtx
+  case mc.mcmode of
+    CheckAll => action
+    CheckFirst => do
+      modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next NoCheck
+      action
+      modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next CheckFirst
+    NoCheck => pure MkUnit
+
 solve env m sp t = do
   meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m
     | _ => error (getFC t) "Meta \{show m} already solved! (solve :: Nil)"
@@ -429,7 +447,7 @@ solve env m sp t = do
     updateMeta m $ \case
       (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
       (Solved _ k x) => error' "Meta \{show ix} already solved! (solve2 :: Nil)"
-    for cons $ \case
+    maybeCheck $ for_ cons $ \case
       MkMc fc env sp rhs => do
         val <- vappSpine soln sp
         debug $ \ _ => "discharge l=\{show $ length' env} \{(show val)} =?= \{(show rhs)}"
@@ -629,7 +647,7 @@ freshMeta ctx fc ty kind = do
   mc <- readIORef top.metaCtx
   debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
   let newmeta = Unsolved fc mc.next ctx ty kind Nil
-  writeIORef top.metaCtx $ MC (newmeta :: mc.metas) (1 + mc.next)
+  writeIORef top.metaCtx $ MC (newmeta :: mc.metas) (1 + mc.next) mc.mcmode
   -- infinite loop - keeps trying Ord a => Ord (a \x a)
   -- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta
   pure $ applyBDs 0 (Meta fc mc.next) ctx.bds

port/Lib/TopContext.newt

@@ -30,7 +30,7 @@ instance Show TopContext where
 -- TODO need to get class dependencies working
 emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext
 emptyTop = do
-  mcctx <- newIORef (MC Nil 0)
+  mcctx <- newIORef (MC Nil 0 CheckAll)
   errs <- newIORef $ the (List Error) Nil
   pure $ MkTop EmptyMap mcctx False errs Nil EmptyMap
 

port/Lib/Types.newt

@@ -307,10 +307,17 @@ data MConstraint = MkMc FC Env (SnocList Val) Val
 
 data MetaEntry = Unsolved FC Int Context Val MetaKind (List MConstraint) | Solved FC Int Val
 
+-- The purpose of this is to only check one level of constraints when trying an Auto solution
+-- The idea being we narrow it down to the likely solution, and let any consequent type error
+-- bubble up to the user, rather than have a type error wipe out all solutions.
+-- We also don't bother adding constraints if not in CheckAll mode
+data MetaMode = CheckAll | CheckFirst | NoCheck
+
 record MetaContext where
   constructor MC
   metas : List MetaEntry
   next : Int
+  mcmode : MetaMode
 
 data Def = Axiom | TCon (List QName) | DCon Int QName | Fn Tm | PrimTCon
          | PrimFn String (List String)
@@ -485,21 +492,6 @@ error fc msg = throwError $ E fc msg
 error' : ∀ a. String -> M a
 error' msg = throwError $ E emptyFC msg
 
--- freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
--- freshMeta ctx fc ty kind = do
---   top <- get
---   mc <- readIORef top.metaCtx
---   debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
---   writeIORef top.metaCtx $ MC (Unsolved fc mc.next ctx ty kind Nil :: mc.metas) (1 + mc.next)
---   pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
---   where
---     -- hope I got the right order here :)
---     applyBDs : Int -> Tm -> List BD -> Tm
---     applyBDs k t Nil = t
---     -- review the order here
---     applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k)
---     applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs
-
 lookupMeta : Int -> M MetaEntry
 lookupMeta ix = do
   top <- get
@@ -511,8 +503,5 @@ lookupMeta ix = do
     go (meta@(Unsolved _ k ys _ _ _) :: xs) = if k == ix then pure meta else go xs
     go (meta@(Solved _ k x) :: xs) = if k == ix then pure meta else go xs
 
--- we need more of topcontext later - Maybe switch it up so we're not passing
--- around top
-
 mkCtx : FC -> Context
 mkCtx fc = MkCtx 0 Nil Nil Nil fc