[ auto ] try autos if a meta in their type is solved

Also cut tryEval if the result is a lambda

newt/Prelude.newt

@@ -382,6 +382,10 @@ instance Show String where
 instance Show Int where
   show = showInt
 
+instance Show Bool where
+  show True = "true"
+  show False = "false"
+
 pfunc ord : Char → Int := `(c) => c.charCodeAt(0)`
 pfunc chr : Int → Char := `(c) => String.fromCharCode(c)`
 

src/Lib/Elab.newt

@@ -117,7 +117,7 @@ setMetaMode : MetaMode → M Unit
 -- ideally we could do metaCtx.mcmode := CheckFirst
 setMetaMode mcmode = modifyTop $ \top => [ metaCtx := [mcmode := mcmode] (top.metaCtx) ] top
 
-findMatches : Context -> Val -> List (QName × Tm) -> M (List String)
+findMatches : Context -> Val -> List (QName × Tm) -> M (List QName)
 findMatches ctx ty Nil = pure Nil
 findMatches ctx ty ((name, type) :: xs) = do
   let (True) = isCandidate ty type
@@ -137,7 +137,7 @@ findMatches ctx ty ((name, type) :: xs) = do
       tm <- check ctx (RVar fc nm) ty
       debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}"
       modifyTop [ metaCtx := mc ]
-      (_::_ nm) <$> findMatches ctx ty xs)
+      (_::_ name) <$> findMatches ctx ty xs)
     (\ err => do
       debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}"
       modifyTop [ metaCtx := mc ]
@@ -189,27 +189,35 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
       top <- getTop
       Nil <- contextMatches ctx ty
           | ((tm, vty) :: Nil) => do
-              unifyCatch (getFC ty) ctx ty vty
               val <- eval ctx.env CBN tm
-              debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}"
+              debug $ \ _ => "LOCAL SOLUTION \{rpprint Nil tm} evaled to \{show val}"
               let sp = makeSpine ctx.lvl ctx.bds
               solve ctx.env k sp val
+              debug $ \ _ => "<-- AUTO LOCAL"
+              debug $ \ _ => ">UNIFY \{show k}"
+              -- Causes infinite loop if we do this before the solve
+              -- may be nice to push it into solve, but vty is not there..
+              unifyCatch (getFC ty) ctx ty vty
+              debug $ \ _ => "<UNIFY \{show k}"
               pure True
           | res => do
-              debug $ \ _ => "FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}"
+              debug $ \ _ => "LOCAL FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}"
               pure False
 
       let (VRef _ tyname _) = ty | _ => pure False
       let cands = fromMaybe Nil $ lookupMap' tyname top.hints
       (nm :: Nil) <- findMatches ctx ty cands
         | res => do
-          debug $ \ _ => "FAILED to solve \{show ty}, matches: \{show res}"
+          debug $ \ _ => "GLOBAL FAILED to solve \{show ty}, matches: \{show res}"
           pure False
-      tm <- check ctx (RVar fc nm) ty
+      let val = VRef fc nm Lin
-      val <- eval ctx.env CBN tm
+      debug $ \ _ => "GLOBAL SOLUTION \{show val}"
-      debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}"
       let sp = makeSpine ctx.lvl ctx.bds
       solve ctx.env k sp val
+      debug $ \ _ => ">CHECK \{show k}"
+      let (QN ns nm) = nm
+      ignore $ check ctx (RVar fc nm) ty
+      debug $ \ _ => "<CHECK \{show k}"
       pure True
 trySolveAuto _ = pure False
 
@@ -244,17 +252,23 @@ updateMeta ix f = do
     _ => mc.autos
   modifyTop [ metaCtx := MC (updateMap ix me mc.metas) autos mc.next mc.mcmode ]
 
-checkAutos : QName -> List MetaEntry -> M Unit
+-- Try to solve autos that reference the meta ix
+checkAutos : QName -> List QName -> M Unit
 checkAutos ix Nil = pure MkUnit
-checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do
+checkAutos ix (cand :: rest) = do
-  ty' <- quote ctx.lvl ty
+  entry@(Unsolved fc k ctx ty AutoSolve _) <- lookupMeta cand | _ => checkAutos ix rest
-  when (usesMeta ty') $ \ _ => ignore $ trySolveAuto entry
+  case ty of
+    VRef _ nm sp => if checkMeta sp
+        then trySolveAuto entry >> checkAutos ix rest
+        else pure MkUnit
+    _ => pure MkUnit
   checkAutos ix rest
   where
-    usesMeta : Tm -> Bool
+    checkMeta : SnocList Val → Bool
-    usesMeta (App _ (Meta _ k) u) = if k == ix then True else usesMeta u
+    checkMeta Lin = False
-    usesMeta (App _ _ u) = usesMeta u
+    checkMeta (sp :< VMeta _ nm _) = if nm == ix then True else checkMeta sp
-    usesMeta _ = False
+    checkMeta (sp :< _) = checkMeta sp
+
 checkAutos ix (_ :: rest) = checkAutos ix rest
 
 addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit
@@ -266,12 +280,8 @@ addConstraint env ix sp tm = do
     (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]"
+    (Solved fc k tm) => error fc "Meta \{show k} already solved [addConstraint]"
     (OutOfScope) => error' "Meta \{show ix} out of scope"
-  -- I broke this while dropping IORef and it seemed to have no effect
-  -- top <- getTop
-  -- let mc = top.metaCtx
-  -- checkAutos ix $ mapMaybe (flip lookupMap' mc.metas) mc.autos
 
 -- return renaming, the position is the new VVar
 invert : Int -> SnocList Val -> M (List Int)
@@ -353,6 +363,7 @@ 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)
 
+-- run action if mcmode allows it, ratcheting as necessary
 maybeCheck : M Unit -> M Unit
 maybeCheck action = do
   top <- getTop
@@ -392,13 +403,19 @@ 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]"
+      (Solved fc k x) => error fc "Meta \{show ix} already solved! [solve2]"
       OutOfScope => error' "Meta \{show ix} out of scope"
-    maybeCheck $ for_ cons $ \case
+    maybeCheck $ do
+      for_ cons $ \case
         MkMc fc env sp rhs => do
           val <- vappSpine soln sp
           debug $ \ _ => "discharge l=\{show $ length' env} \{(show val)} =?= \{(show rhs)}"
           unify env UNormal val rhs
+      -- check any autos
+      top <- getTop
+      let mc = top.metaCtx
+      debug $ \ _ => "check autos depending on \{show ix} \{debugStr mc.mcmode}"
+      checkAutos ix mc.autos
     pure MkUnit
     )
 
@@ -478,7 +495,7 @@ unify env mode t u = do
               | Just v => unify env mode t' v
             if k == k'
               then unifySpine env mode (k == k') sp sp'
-              else error fc "vref mismatch \{show t'} \{show u'}"
+              else error fc "vref mismatch \{show t'} =?= \{show u'}"
 
     -- Lennart.newt cursed type references itself
     -- We _could_ look up the ref, eval against Nil and vappSpine...
@@ -601,8 +618,7 @@ freshMeta ctx fc ty kind = do
       AutoSolve => qn :: mc.autos
       _ => mc.autos
   modifyTop $ \top => [metaCtx := MC (updateMap qn newmeta mc.metas) autos (1 + mc.next) mc.mcmode ] top
-  -- infinite loop - keeps trying Ord a => Ord (a \x a)
+  -- I tried checking Auto immediately if CheckAll, but there isn't enough information yet.
-  -- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta
   pure $ applyBDs 0 (Meta fc qn) ctx.bds
   where
     -- hope I got the right order here :)
@@ -1308,8 +1324,6 @@ undo prev ((DoArrow fc left right alts) :: xs) = do
     (RLam fc (BI fc nm Explicit Many) rest) Explicit
 
 
-
-
 -- REVIEW do we want to let arg?
 -- collect fields and default assignment
 -- subst in real assignment

src/Lib/Eval.newt

@@ -79,6 +79,7 @@ tryEval env (VRef fc k sp) = do
             val <- vappSpine vtm sp
             case val of
               VCase _ _ _ => pure Nothing
+              VLam _ _ _ _ _ => pure Nothing
               -- For now? There is a spot in Compile.newt that has
               -- two applications of fresh that is getting unfolded even
               -- though it has the same head and spine.  Possibly because it's

src/Lib/Parser.newt

@@ -367,6 +367,7 @@ doArrow = do
   (Just _) <- optional $ keyword "<-"
     | _ => pure $ DoExpr fc left
   right <- term
+  -- FIXME bad error for `| pure MkUnit`, we need to commit if indentation is correct.
   alts <- startBlock $ manySame $ symbol "|" *> caseAlt
   pure $ DoArrow fc left right alts
 

src/Lib/Types.newt

@@ -286,10 +286,19 @@ instance Show MetaKind where
   show User = "User"
   show AutoSolve = "Auto"
 
+instance Eq MetaKind where
+  Normal == Normal = True
+  User == User = True
+  AutoSolve == AutoSolve = True
+  _ == _ = False
+
 -- constrain meta applied to val to be a val
 
 data MConstraint = MkMc FC Env (SnocList Val) Val
 
+instance Show MConstraint where
+  show (MkMc fc env (args) ty) = "MkMC \{show fc} env \{show args} \{show ty}"
+
 data MetaEntry
   = Unsolved FC QName Context Val MetaKind (List MConstraint)
   | Solved FC QName Val
@@ -308,6 +317,12 @@ record MetaContext where
   next : Int
   mcmode : MetaMode
 
+instance Eq MetaMode where
+  CheckAll == CheckAll = True
+  CheckFirst == CheckFirst = True
+  NoCheck == NoCheck = True
+  _ == _ = False
+
 data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon
 
 instance Eq ConInfo where

tests/RunLength.newt

@@ -0,0 +1,64 @@
+-- This showed a couple of issues related to having ++ in types.
+
+module RunLength
+
+-- https://youtu.be/N4Z45Xg6_oc?t=1246
+
+import Prelude
+
+-- TODO this belongs in a library
+
+data Void : U where
+
+Not : U → U
+Not x = x → Void
+
+data Dec : U → U where
+  Yes : ∀ prop. (prf : prop) → Dec prop
+  No : ∀ prop. (contra : Not prop) → Dec prop
+
+class DecEq t where
+  decEq : (x₁ : t) → (x₂ : t) → Dec (x₁ ≡ x₂)
+
+-- end lib
+
+rep : ∀ a. Nat → a → List a
+rep Z x = Nil
+rep (S k) x = x :: rep k x
+
+data RunLength : ∀ ty. List ty → U where
+  Empty : ∀ ty. RunLength {ty} Nil
+  Run : ∀ ty more. (n : Nat) →
+        (x : ty) →
+        RunLength more →
+        RunLength (rep n x ++ more)
+
+-- Idris has `?` here, but we're allowing metas on signatures to be solved later
+testComp : RunLength {Char} _
+testComp = Run (S (S (S Z))) 'x' $ Run (S (S (S (S Z)))) 'y' $ Empty
+
+-- 24:20
+uncompress : ∀ ty xs. RunLength {ty} xs → List ty
+
+data Singleton : ∀ a. a → U where
+  Val : ∀ a. (x : a) → Singleton x
+
+-- Idris generates this
+-- uncompress' : ∀ ty xs. RunLength {ty} xs → Singleton xs
+-- uncompress' Empty = Val Nil
+-- uncompress' (Run n x y) = let (Val ys) = uncompress' y in Val (rep n x ++ _)
+
+solve : ∀ a. {{a}} -> a
+solve {{a}} = a
+
+-- adding ys back in, we still get a unification failure.
+-- I think because the meta for ++ is not yet solved.
+uncompress' : ∀ ty xs. RunLength {ty} xs → Singleton {List ty} xs
+uncompress' Empty = Val Nil
+uncompress' {ty} (Run n x y) = let (Val ys) = uncompress' y in Val (rep n x ++ ys)
+
+rle : ∀ a. {{DecEq a}} → (xs : List a) → RunLength xs
+
+
+
+