From 4f7b78f05607ba0171bd3a74a46c7adabf45f3f9 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Tue, 17 Sep 2024 22:11:23 -0700
Subject: [PATCH] add types to metas, find example that needs postpone

---
 newt/typeclass.newt     | 16 ++++++++++++++++
 src/Lib/Check.idr       | 25 +++++++++++++++----------
 src/Lib/CompileExp.idr  |  3 +--
 src/Lib/ProcessDecl.idr |  6 +++++-
 src/Lib/TT.idr          | 32 +++++++++++++++++++-------------
 src/Lib/Types.idr       | 14 +++++++++-----
 6 files changed, 65 insertions(+), 31 deletions(-)

diff --git a/newt/typeclass.newt b/newt/typeclass.newt
index f6a6889..07b8ed3 100644
--- a/newt/typeclass.newt
+++ b/newt/typeclass.newt
@@ -39,3 +39,19 @@ MaybeMonad = MkMonad {Maybe} (\ {A} ma amb =>
 bind : {m : U -> U} -> {x : Monad m} -> {a b : U} -> (m a) -> (a -> m b) -> m b
 bind {m} {MkMonad bind'} = bind'
 
+ptype Int
+
+-- For now, we may try to solve this at creation time, but it's possible postpone is needed
+
+/-
+
+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 : Int -> Maybe Int
+foo x = bind {_} {_} (Just x) (\ x => Just x)
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 84af462..d5facb0 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -22,7 +22,7 @@ data Pden = PR Nat Nat (List Nat)
 
 forceMeta : Val -> M Val
 forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
-  (Unsolved pos k xs) => pure (VMeta fc ix sp)
+  (Unsolved pos k xs _) => pure (VMeta fc ix sp)
   (Solved k t) => vappSpine t sp >>= forceMeta
 forceMeta x = pure x
 
@@ -33,7 +33,7 @@ forceType (VRef fc nm def sp) =
       (Just (MkEntry name type (Fn t))) => vappSpine !(eval [] CBN t) sp
       _ => pure (VRef fc nm def sp)
 forceType (VMeta fc ix sp) = case !(lookupMeta ix) of
-  (Unsolved x k xs) => pure (VMeta fc ix sp)
+  (Unsolved x k xs _) => pure (VMeta fc ix sp)
   (Solved k t) => vappSpine t sp >>= forceType
 forceType x = pure x
 
@@ -63,7 +63,7 @@ parameters (ctx: Context)
 
             error fc "non-linear pattern"
           else go xs (k :: acc)
-      go _ _ = error emptyFC "non-variable in pattern"
+      go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}"
 
   -- we have to "lift" the renaming when we go under a lambda
   -- I think that essentially means our domain ix are one bigger, since we're looking at lvl
@@ -221,7 +221,8 @@ insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
 insert ctx tm ty = do
   case !(forceMeta ty) of
     VPi fc x Implicit a b => do
-      m <- freshMeta ctx (getFC tm)
+      m <- freshMeta ctx (getFC tm) a
+      debug "INSERT \{pprint (names ctx) m} : \{show a}"
       mv <- eval ctx.env CBN m
       insert ctx (App emptyFC tm m) !(b $$ mv)
     va => pure (tm, va)
@@ -322,13 +323,17 @@ extendPi ctx ty nms sc = pure (ctx, ty, nms <>> [], sc)
 updateContext : Context -> List (Nat, Val) -> M Context
 updateContext ctx [] = pure ctx
 updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` 1 in
-  updateContext ({env $= replace ix val, bds $= replace ix Defined } ctx) cs
+  updateContext ({env $= replace ix val, bds $= replaceV ix Defined } ctx) cs
   where
     replace : Nat -> a -> List a -> List a
     replace k x [] = []
     replace 0 x (y :: xs) = x :: xs
     replace (S k) x (y :: xs) = y :: replace k x xs
 
+    replaceV : Nat -> a -> Vect n a -> Vect n a
+    replaceV k x [] = []
+    replaceV 0 x (y :: xs) = x :: xs
+    replaceV (S k) x (y :: xs) = y :: replaceV k x xs
 
 -- ok, so this is a single constructor, CaseAlt
 -- since we've gotten here, we assume it's possible and we better have at least
@@ -635,8 +640,8 @@ infer ctx (RApp fc t u icit) = do
     -- TODO test case to cover this.
     tty => do
       debug "unify PI for \{show tty}"
-      a <- eval ctx.env CBN !(freshMeta ctx fc)
-      b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc
+      a <- eval ctx.env CBN !(freshMeta ctx fc (VU emptyFC))
+      b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC)
       unifyCatch fc ctx tty (VPi fc ":ins" icit a b)
       pure (a,b)
 
@@ -666,7 +671,7 @@ infer ctx (RAnn fc tm rty) = do
   pure (tm, vty)
 
 infer ctx (RLam fc nm icit tm) = do
-  a <- freshMeta ctx fc >>= eval ctx.env CBN
+  a <- freshMeta ctx fc (VU emptyFC) >>= eval ctx.env CBN
   let ctx' = extend ctx nm a
   (tm', b) <- infer ctx' tm
   debug "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}"
@@ -674,9 +679,9 @@ infer ctx (RLam fc nm icit tm) = do
   -- error {ctx} [DS "can't infer lambda"]
 
 infer ctx (RImplicit fc) = do
-  ty <- freshMeta ctx fc
+  ty <- freshMeta ctx fc (VU emptyFC)
   vty <- eval ctx.env CBN ty
-  tm <- freshMeta ctx fc
+  tm <- freshMeta ctx fc vty
   pure (tm, vty)
 
 infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), !(primType fc "String"))
diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr
index 6240894..d872243 100644
--- a/src/Lib/CompileExp.idr
+++ b/src/Lib/CompileExp.idr
@@ -79,7 +79,6 @@ compileTerm (Bnd _ k) = pure $ CBnd k
 -- need to eta expand to arity
 compileTerm t@(Ref fc nm _) = apply (CRef nm) [] [<] !(arityForName fc nm)
 
--- need to zonk
 compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME
 compileTerm (Lam _ nm t) = pure $ CLam nm !(compileTerm t)
 compileTerm tm@(App _ _ _) with (funArgs tm)
@@ -93,7 +92,7 @@ compileTerm tm@(App _ _ _) with (funArgs tm)
         -- apply (CRef "Meta\{show k}") args' [<] 0
         arity <- case meta of
                 -- maybe throw
-                (Unsolved x j xs) => pure 0
+                (Unsolved x j ctx _) => pure 0 -- FIXME # of Bound in ctx.bds
                 (Solved j tm) => pure $ getArity !(quote 0 tm)
         apply (CRef "Meta\{show k}") args' [<] arity
   _ | (t@(Ref fc nm _), args) = do
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index 21d2599..af1c98a 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -76,9 +76,13 @@ processDecl (Def fc nm clauses) = do
   tm' <- zonk ctx 0 [] tm
   putStrLn "NF \{pprint[] tm'}"
   mc <- readIORef ctx.metas
+
+  -- Maybe here we try search?
+
+
   for_ mc.metas $ \case
     (Solved k x) => pure ()
-    (Unsolved (l,c) k xs) => 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}"
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index d36540f..af15b34 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -34,19 +34,25 @@ error' msg = throwError $ E (0,0) msg
 -- because of dependent types (if we want something well-typed back out)
 
 export
-freshMeta : Context -> FC -> M Tm
-freshMeta ctx fc = do
+freshMeta : Context -> FC -> Val -> M Tm
+freshMeta ctx fc ty = do
   mc <- readIORef ctx.metas
   putStrLn "INFO at \{show fc}: fresh meta \{show mc.next}"
-  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx.bds ::) } mc
+  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty ::) } mc
   pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds
   where
-  -- hope I got the right order here :)
-  applyBDs : Nat -> Tm -> List BD -> Tm
-  applyBDs k t [] = t
-  -- review the order here
-  applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k)
-  applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
+    -- hope I got the right order here :)
+    applyBDs : Nat -> Tm -> Vect k BD -> Tm
+    applyBDs k t [] = t
+    -- review the order here
+    applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k)
+    applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
+
+    -- makeType : Vect k (String, Val) -> Vect k BD -> Val
+    -- makeType [] [] = ?makeType_rhs_2
+    -- makeType ((nm, ty) :: types) (Defined :: bds) = makeType types bds
+    -- makeType ((nm, ty) :: types) (Bound :: bds) = VPi emptyFC nm Explicit ty
+
 
 export
 lookupMeta : Nat -> M MetaEntry
@@ -57,7 +63,7 @@ lookupMeta ix = do
   where
     go : List MetaEntry -> M MetaEntry
     go [] = error' "Meta \{show ix} not found"
-    go (meta@(Unsolved _ k ys) :: xs) = if k == ix then pure meta else go xs
+    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
 
 export partial
@@ -158,7 +164,7 @@ eval env mode (App _ t u) = vapp !(eval env mode t) !(eval env mode u)
 eval env mode (U fc) = pure (VU fc)
 eval env mode (Meta fc i) =
   case !(lookupMeta i) of
-        (Unsolved _ k xs) => pure $ VMeta fc i [<]
+        (Unsolved _ k xs _) => pure $ VMeta fc i [<]
         (Solved k t) => pure $ t
 eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t)
 eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b)
@@ -221,7 +227,7 @@ solveMeta ctx ix tm = do
   where
     go : List MetaEntry -> SnocList MetaEntry -> M (List MetaEntry)
     go [] _ = error' "Meta \{show ix} not found"
-    go (meta@(Unsolved pos k _) :: xs) lhs = if k == ix
+    go (meta@(Unsolved pos k _ _) :: xs) lhs = if k == ix
       then do
         -- empty context should be ok, because this needs to be closed
         putStrLn "INFO at \{show pos}: solve \{show k} as \{!(prval tm)}"
@@ -267,7 +273,7 @@ zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of
     foo <- vappSpine v ([<] <>< sp')
     debug "-> result is \{show foo}"
     quote l foo
-  (Unsolved x j xs) => pure $ appSpine t sp
+  (Unsolved x j xs _) => pure $ appSpine t sp
 zonkApp top l env t sp = pure $ appSpine !(zonk top l env t) sp
 
 zonkAlt : TopContext -> Nat -> Env -> CaseAlt -> M CaseAlt
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index fe17e2a..98dff26 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -164,9 +164,9 @@ pprint names tm = render 80 $ go names tm
     go names (App _ t u) = text "(" <+> go names t <+> go names u <+> ")"
     go names (U _) = "U"
     go names (Pi _ nm Implicit t u) =
-      text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "=>" <+> go (nm :: names) u <+> ")"
+      text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "->" <+> go (nm :: names) u <+> ")"
     go names (Pi _ nm Explicit t u) =
-      text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")"
+      text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "->" <+> go (nm :: names) u <+> ")"
     -- FIXME - probably way wrong on the names here.  There is implicit binding going on
     go names (Case _ sc alts) = text "case" <+> go names sc <+> text "of" </> (nest 2 (line ++ stack (map (goAlt names) alts)))
     go names (Lit _ lit) = text "\{show lit}"
@@ -237,6 +237,8 @@ Show Val where
 -- Not used - I was going to change context to have a List Binder
 -- instead of env, types, bds
 -- But when we get down into eval, we don't have types to put into the env
+-- It looks like Idris has a separate LocalEnv in eval, Kovacs peels off
+-- env from context and extends it.
 data Binder : Type where
   Bind : (nm : String) -> (bd : BD) -> (val : Val) -> (ty : Val) -> Binder
 
@@ -285,13 +287,15 @@ Can I get val back? Do we need to quote? What happens if we don't?
 
 -}
 
+record Context
+
 public export
-data MetaEntry = Unsolved FC Nat (List BD) | Solved Nat Val
+data MetaEntry = Unsolved FC Nat Context Val | Solved Nat Val
 
 export
 covering
 Show MetaEntry where
-  show (Unsolved pos k xs) = "Unsolved \{show pos} \{show k}"
+  show (Unsolved pos k xs ty) = "Unsolved \{show pos} \{show k} : \{show ty}"
   show (Solved k x) = "Solved \{show k} \{show x}"
 
 public export
@@ -356,7 +360,7 @@ record Context where
   env : Env                  -- Values in scope
   types : Vect lvl (String, Val) -- types and names in scope
   -- so we'll try "bds" determines length of local context
-  bds  : List BD          -- bound or defined
+  bds : Vect lvl BD          -- bound or defined
 
   -- We only need this here if we don't pass TopContext
   -- top : TopContext