defer skolem issue from unsolved meta application

TODO.md

@@ -1,6 +1,7 @@
 
 ## TODO
 
+- [ ] forall / ∀ sugar
 - [ ] Bad module name error has FC 0,0 instead of the module or name
 - [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this.
 - [ ] Remove context lambdas when printing solutions (show names from context)
@@ -8,6 +9,7 @@
 - [ ] Check for shadowing when declaring dcon
 - [ ] Require infix decl before declaring names (helps find bugs)
 - [ ] sugar for typeclasses
+- [ ] maybe add implicits in core to help resugar operators?
 - [x] Allow unicode operators/names
 - Web playground
   - [x] editor
@@ -17,6 +19,7 @@
   - [x] need to shim out Buffer
 - [x] get rid of stray INFO from auto resolution
 - [ ] handle `if_then_else_` style mixfix
+  - [ ] equational reasoning sample (maybe PLFA "Lists")
 - [x] Search should look at context
 - [ ] records
 - [ ] copattern matching

playground/samples/Concat.newt

@@ -28,11 +28,33 @@ infixl 1 _≡_
 data _≡_ : {A : U} -> A -> A -> U where
     Refl : {A : U} {a : A} -> a ≡ a
 
+sym : {A : U} {a b : A} -> a ≡ b -> b ≡ a
+sym Refl = Refl
+
 replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
 replace p Refl x = x
 
 cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
 
-thm : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
+length-++ : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
-thm Nil ys = Refl
+length-++ Nil ys = Refl
-thm (x :: xs) ys = cong S (thm xs ys)
+length-++ (x :: xs) ys = cong S (length-++ xs ys)
+
+-- PLFA definition
+reverse : {A : U} -> (xs : List A) -> List A
+reverse Nil = Nil
+reverse (x :: xs) = reverse xs ++ (x :: Nil)
+
+++-identity : {A : U} -> (xs : List A) -> xs ++ Nil ≡ xs
+++-identity Nil = Refl
+++-identity (x :: xs) = cong (_::_ x) (++-identity xs)
+
+++-associative : {A : U} (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
+
+-- TODO port equational reasoning
+reverse-++-distrib : {A : U} -> (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+reverse-++-distrib Nil ys = replace (\ z => reverse ys ≡ z) (sym (++-identity (reverse ys))) Refl
+reverse-++-distrib {A} (x :: xs) ys =
+  replace (\ z => (reverse (xs ++ ys) ++ (x :: Nil)) ≡ z)
+          (sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
+          (replace (\ z => (reverse (xs ++ ys)) ++ (x :: Nil) ≡ z ++ (x :: Nil)) (reverse-++-distrib xs ys) Refl)

src/Lib/Common.idr

@@ -19,7 +19,9 @@ emptyFC = (0,0)
 
 -- Error of a parse
 public export
-data Error = E FC String
+data Error
+  = E FC String
+  | Postpone FC Nat String
 %name Error err
 
 public export
@@ -33,6 +35,15 @@ showError src (E (line, col) msg) = "ERROR at \{show (line,col)}: \{msg}\n" ++ g
         "  \{x}\n  \{replicate (cast col) ' '}^\n"
       else if line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
       else go (l + 1) xs
+showError src (Postpone (line, col) ix msg) = "ERROR at \{show (line,col)}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src)
+  where
+    go : Int -> List String -> String
+    go l [] = ""
+    go l (x :: xs) =
+      if l == line then
+        "  \{x}\n  \{replicate (cast col) ' '}^\n"
+      else if line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
+      else go (l + 1) xs
 
 public export
 data Fixity = InfixL | InfixR | Infix

src/Lib/Elab.idr

@@ -120,20 +120,29 @@ parameters (ctx: Context)
   rename meta ren lvl v = go ren lvl v
     where
       go : List Nat -> Nat -> Val  -> M  Tm
-      goSpine : List Nat -> Nat -> Tm -> SnocList Val  -> M  Tm
+      goSpine : List Nat -> Nat -> Tm -> SnocList Val  -> M Tm
       goSpine ren lvl tm [<] = pure tm
       goSpine ren lvl tm (xs :< x) = do
         xtm <- go ren lvl x
         pure $ App emptyFC !(goSpine ren lvl tm xs) xtm
 
       go ren lvl (VVar fc k sp) = case findIndex (== k) ren of
-        Nothing => error fc "scope/skolem thinger"
+        Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}"
         Just x => goSpine ren lvl (Bnd fc $ cast x) sp
       go ren lvl (VRef fc nm def sp) = goSpine ren lvl (Ref fc nm def) sp
-      go ren lvl (VMeta fc ix sp) = if ix == meta
+      go ren lvl (VMeta fc ix sp) = do
+        -- So sometimes we have an unsolved meta in here which reference vars out of scope.
+        debug "rename Meta \{show ix} spine \{show sp}"
+        if ix == meta
         -- REVIEW is this the right fc?
-        then error fc "meta occurs check"
+          then error fc "meta occurs check"
-        else goSpine ren lvl (Meta fc ix) sp
+          else case !(lookupMeta ix) of
+            Solved fc _ val => do
+              debug "rename: \{show ix} is solved"
+              go ren lvl !(vappSpine val sp)
+            _ => do
+              debug "rename: \{show ix} is unsolved"
+              catchError {e=Error} (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err))
       go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<])))
       go ren lvl (VPi fc n icit ty tm) = pure (Pi fc n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<])))
       go ren lvl (VU fc) = pure (U fc)
@@ -169,19 +178,29 @@ parameters (ctx: Context)
 
     debug "meta \{show meta}"
     ren <- invert l sp
-    tm <- rename m ren l t
+    catchError {e=Error} (do
-    let tm = lams (length sp) tm
+
-    top <- get
+      tm <- rename m ren l t
-    soln <- eval [] CBN tm
+
+      let tm = lams (length sp) tm
+      top <- get
+      soln <- eval [] CBN tm
+
+      updateMeta ctx m $ \case
+        (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
+        (Solved _ k x) => error' "Meta \{show ix} already solved!"
+      for_ cons $ \case
+        MkMc fc ctx sp rhs => do
+          val <- vappSpine soln sp
+          debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}"
+          unify ctx.lvl Normal val rhs)
+      (\case
+        Postpone fc ix msg => do
+          -- let someone else solve this and then check again.
+          addConstraint ctx m sp t
+          pure ()
+        err => throwError err)
 
-    updateMeta ctx m $ \case
-      (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
-      (Solved _ k x) => error' "Meta \{show ix} already solved!"
-    for_ cons $ \case
-      MkMc fc ctx sp rhs => do
-        val <- vappSpine soln sp
-        debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}"
-        unify ctx.lvl Normal val rhs
 
   unifySpine : Nat -> UnifyMode -> Bool -> SnocList Val -> SnocList Val  -> M UnifyResult
   unifySpine l mode False _ _ = error emptyFC "unify failed at head" -- unreachable now
@@ -305,12 +324,12 @@ parameters (ctx: Context)
 export
 unifyCatch : FC -> Context -> Val -> Val -> M ()
 unifyCatch fc ctx ty' ty = do
-    res <- catchError (unify ctx ctx.lvl Normal ty' ty) $ \(E x str) => do
+    res <- catchError (unify ctx ctx.lvl Normal ty' ty) $ \err => do
       let names = toList $ map fst ctx.types
       debug "fail \{show ty'} \{show ty}"
       a <- quote ctx.lvl ty'
       b <- quote ctx.lvl ty
-      let msg = "unification failure: \{str}\n  failed to unify \{pprint names a}\n    with \{pprint names b}\n  "
+      let msg = "unification failure: \{errorMsg err}\n  failed to unify \{pprint names a}\n    with \{pprint names b}\n  "
       throwError (E fc msg)
     case res of
       MkResult [] => pure ()
@@ -503,8 +522,8 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
   -- codomain with the scrutinee type
   debug "unify dcon cod with scrut\n  \{show ty'}\n  \{show scty}"
   Just res <- catchError {e = Error} (Just <$> unify ctx' (length ctx'.env) Pattern ty' scty)
-              (\(E _ msg) => do
+              (\err => do
-                  debug "SKIP \{dcName} because unify error \{msg}"
+                  debug "SKIP \{dcName} because unify error \{errorMsg err}"
                   pure Nothing)
     | _ => pure Nothing
 
@@ -534,8 +553,8 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
 
     _ => do
         Right res <- tryError {e = Error} (unify ctx' (length ctx'.env) Pattern ty' scty)
-          | Left (E _ msg) => do
+          | Left err => do
-            debug "SKIP \{dcName} because unify error \{msg}"
+            debug "SKIP \{dcName} because unify error \{errorMsg err}"
             pure Nothing
 
         -- Constrain the scrutinee's variable to be dcon applied to args

src/Lib/ProcessDecl.idr

@@ -197,7 +197,7 @@ processDecl (Def fc nm clauses) = do
   mc <- readIORef top.metas
   let mstart = length mc.metas
   let Just entry = lookup nm top
-    | Nothing => throwError $ E fc "skip def \{nm} without Decl"
+    | Nothing => throwError $ E fc "No declaration for \{nm}"
   let (MkEntry name ty Axiom) := entry
     | _ => throwError $ E fc "\{nm} already defined"
 

src/Lib/Types.idr

@@ -471,6 +471,16 @@ export partial
 Show Context where
   show ctx = "Context \{show $ map fst $ ctx.types}"
 
+export
+errorMsg : Error -> String
+errorMsg (E x str) = str
+errorMsg (Postpone x k str) = str
+
+export
+HasFC Error where
+  getFC (E x str) = x
+  getFC (Postpone x k str) = x
+
 export
 error : FC -> String -> M a
 error fc msg = throwError $ E fc msg

src/Main.idr

@@ -146,7 +146,7 @@ main = do
   -- we'll need to reset for each file, etc.
   ctx <- empty
   Right _  <- runEitherT $ runStateT ctx $ main'
-    | Left (E (c, r) str) => do
+    | Left err => do
-        putStrLn "ERROR at (\{show c}, \{show r}): \{show str}"
+        putStrLn "ERROR at \{show $ getFC err}: \{errorMsg err}"
         exitFailure
   putStrLn "done"