From 76fae34bcf578d943def8bc337f63f424321db4c Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 13 Jul 2024 09:32:49 -0700
Subject: [PATCH] unification seems to work for kovacs examples

---
 README.md                    |  48 +++++++---
 newt-vscode/src/extension.ts |   6 +-
 newt/zoo3.newt               |  22 +----
 src/Lib/Check.idr            | 169 ++++++++++++++++++++++++-----------
 src/Lib/Parser.idr           |   8 +-
 src/Lib/Parser/Impl.idr      |  22 ++---
 src/Lib/Prettier.idr         |   1 +
 src/Lib/TT.idr               |  29 +++---
 src/Lib/Types.idr            |  30 ++++---
 src/Main.idr                 |  15 ++--
 src/Syntax.idr               |   5 --
 11 files changed, 219 insertions(+), 136 deletions(-)

diff --git a/README.md b/README.md
index 6bd9b4f..a693c11 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,5 @@
 
-Parser is in place. 
+Parser is in place.
 Ditched well-scoped for now.
 
 Fixed more issues, started processing stuff, we need real example code.
@@ -12,45 +12,65 @@ So smalltt has TopVar with a Level. typechecking binders end up as top too.
 
 Also delayed unfolded values for top or solved metas. This looks like glue - all the bits for the top and a cached value (it's keeping top as values).
 
-We need metas next.  SmallTT has a metactx in context as a mutable array.
+REVIEW the delayed unfolding, we're being aggressive for now. This may have been necessary until unification was in place, now we can decide to further unfold during unification.
 
-We extend the context and then drop it, so we need soemthing mutable.
+metas are assoc list, can probably just be list, but we'd need to do level/index math for the lookup.
 
-It's in top context and he pulls stuff down to context as needed. I'm overthinking this. I'm reluctant to copy Idris because resolved names are not compatible with query based, but everybody is using an array...
+They are in separate MetaContext wrapped in an IORef. I'm reluctant to copy Idris because resolved names are not compatible with query based, but everybody is using an array...
 
-I'd kinda like to see array run in js...
+Idris has a common array for metas and defs but that might be a problem if I go query based someday.
 
-Idris does a common array for metas and defs. 
+Prettier was missing a Lazy.  I'm still fairly faithful to the paper, but might want to refactor that to push the computation down into the `if`.
 
-Prettier was missing a Lazy.
+Zoo3 runs now, I had to fix meta / meta unification.
 
-Zoo3, mostly runs aside from eqTest. 
+I've added a bunch of info logs for the editor support.
+
+Zoo4 examples run now.
+
+Maybe do `data` next.  There is a crude version in place, we'll want to fix that, typecheck the new stuff, and then add cases. (Maybe introduce eliminators.)
+
+When I generate code, I'll eventually run up against the erased thing. (I'll want to erase some of the stuff that is compile time.)  But we'll generate code and decide how far we need to take this.  It's probably pointless to just reproduce Idris.
+
+When I self host, I'll have to drop or implement typeclasses. I do understand auto enough to make it happen.
+
+Ok, for code gen, I think I'll need something like primitive values and definitely primitive functions. For v0, I could leave the holes as undefined and if there is a function with that name, it's magically FFI.
+
+
+Questions:
+- [ ] Code gen or data next?
+- [ ] Should I write this up properly?
 
 Parser:
-- [x] unify broken for zoo3 `cons`
 - [ ] parser for block comments
 - [x] import statement
 - [x] def
 - [x] simple decl
-- [x] List not in scope
+
+Misc:
 - [x] vscode support for .newt
-- [ ] Should I switch this back over to the App monad?
 - [x] Error object like pi-forall
-- [ ] Get implicits working
+  - [ ] I think I'll need to go with non-generic error type once I need to do something other than print them
+- [x] Get unification working (zoo3)
+- [x] Get implicits working (zoo4)
 - [x] Replace on define
 - [x] more sugar on lambdas
 - [ ] tests for parsing and pretty printing
+- [ ] white box tests for internals
+  - Maybe look at narya for examples of what I should be testing
 - [ ] inductive types
-  - [ ] read data definitions 1/2 done
+  - read data definitions 1/2 done
 - [x] read files
 - [x] process a file
 - [x] figure out context representation - Global context?
 - [x] type checking / elab
   - What does this represent? The basics, implicits? pattern unification?
 - [ ] symbolic execution
+  - why did I put this here? Is it just for `eval`?  We do have CBN in place, we could eval inferrable
 - [ ] compilation
-
+  - I'm thinking I get data working first
 - [ ] write tests
+- [ ] Split up code better
 
 Forward:
 
diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts
index 0d22a29..73d7a46 100644
--- a/newt-vscode/src/extension.ts
+++ b/newt-vscode/src/extension.ts
@@ -27,9 +27,9 @@ export function activate(context: vscode.ExtensionContext) {
 
       for (let i = 0; i < lines.length; i++) {
         const line = lines[i];
-        const match = line.match(/ERROR at \((\d+), (\d+)\): (.*)/);
+        const match = line.match(/(INFO|ERROR) at \((\d+), (\d+)\): (.*)/);
         if (match) {
-          let [_full, line, column, message] = match;
+          let [_full, kind, line, column, message] = match;
           let lnum = Number(line);
           let cnum = Number(column);
           let start = new vscode.Position(lnum, cnum);
@@ -47,7 +47,7 @@ export function activate(context: vscode.ExtensionContext) {
           ) {
             message += "\n" + lines[++i];
           }
-          const severity = vscode.DiagnosticSeverity.Error;
+          const severity = kind === 'ERROR' ? vscode.DiagnosticSeverity.Error : vscode.DiagnosticSeverity.Information
           const diag = new vscode.Diagnostic(range, message, severity);
           diagnostics.push(diag);
         }
diff --git a/newt/zoo3.newt b/newt/zoo3.newt
index 8276dad..5b146cf 100644
--- a/newt/zoo3.newt
+++ b/newt/zoo3.newt
@@ -54,23 +54,5 @@ hundred = mul ten ten
 thousand : Nat
 thousand = mul ten hundred
 
--- All of these fail, but are they funext?
--- works for zoo3, but maybe I'm expanding stuff too eagerly
-
--- eq : Eq _ true true
--- eq = refl
-
--- eqTest2 : Eq _ five five
--- eqTest2 = refl
-
--- -- This one breaks
--- eqTest : Eq _ hundred hundred
--- -- eqTest = refl _ _
-
--- Add the rest
-
-
--- unify (%pi _ E (%var 3 []) (%cl [(%var 6 []), (%var 3 []), (%var 0 []), (%var 2 []), (%var 1 []), (%var 0 [])] (Bnd 2))) with 
---       (%pi _ E (%var 2 []) (%cl [(%var 6 []), (%var 2 []), (%var 0 []), (%var 1 []), (%var 0 [])] (Bnd 2)))
--- ->    (%pi _ E (%var 3 []) (%cl [(%var 6 []), (%var 3 []), (%var 0 []), (%var 2 []), (%var 1 []), (%var 0 [])] (Bnd 2))) with 
---       (%pi _ E (%var 2 []) (%cl [(%var 6 []), (%var 2 []), (%var 0 []), (%var 1 []), (%var 0 [])] (Bnd 2)))
+eqTest : Eq _ hundred hundred
+eqTest = refl _ _
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 4754939..6d7d9f0 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -21,7 +21,7 @@ data PRen = PR Nat Nat (List Nat)
 forceMeta : Val -> M Val
 -- TODO - need to look up metas
 forceMeta (VMeta ix sp) = case !(lookupMeta ix) of
-  (Unsolved k xs) => pure (VMeta ix sp)
+  (Unsolved pos k xs) => pure (VMeta ix sp)
   (Solved k t) => vappSpine t sp
 forceMeta x = pure x
 
@@ -32,7 +32,7 @@ invert lvl sp = go sp []
     go : SnocList Val -> List Nat -> M (List Nat)
     go [<] acc = pure $ reverse acc
     go (xs :< VVar k [<]) acc = do
-      if elem k acc 
+      if elem k acc
         then throwError $ E (0,0) "non-linear pattern"
         else go xs (k :: acc)
     go _ _ = throwError $ E (0,0) "non-variable in pattern"
@@ -40,7 +40,7 @@ invert lvl sp = go sp []
 -- 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
 -- in the codomain, so maybe we can just keep that value
-rename : Nat ->  List Nat -> Nat -> Val  -> M  Tm
+rename : Nat -> List Nat -> Nat -> Val  -> M  Tm
 rename meta ren lvl v = go ren lvl v
   where
     go : List Nat -> Nat -> Val  -> M  Tm
@@ -63,7 +63,7 @@ rename meta ren lvl v = go ren lvl v
 
 lams : Nat -> Tm -> Tm
 lams 0 tm = tm
-lams (S k) tm = Lam "arg\{show k}" Explicit (lams k tm)
+lams (S k) tm = Lam "arg:\{show k}" Explicit (lams k tm)
 
 solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
 solve l m sp t = do
@@ -75,54 +75,89 @@ solve l m sp t = do
   solveMeta top m soln
   pure ()
 
-unify : (l : Nat) -> Val -> Val  -> M  ()
+parameters (ctx: Context)
+  unify : (l : Nat) -> Val -> Val  -> M  ()
 
-unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M  ()
-unifySpine l False _ _ = throwError $ E (0,0) "unify failed"
-unifySpine l True [<] [<] = pure ()
-unifySpine l True (xs :< x) (ys :< y) = unify l x y >> unifySpine l True xs ys
-unifySpine l True _ _ = throwError $ E (0,0) "meta spine length mismatch"
+  unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M  ()
+  unifySpine l False _ _ = error [DS "unify failed at head"] -- unreachable now
+  unifySpine l True [<] [<] = pure ()
+  unifySpine l True (xs :< x) (ys :< y) = unify l x y >> unifySpine l True xs ys
+  unifySpine l True _ _ = error [DS "meta spine length mismatch"]
 
-unify l t u = do
-  t' <- forceMeta t
-  u' <- forceMeta u
-  case (t',u') of
-    (VLam _ _ t,  VLam _ _ t'  ) => unify (l + 1) !(t $$ VVar l [<]) !(t' $$ VVar l [<])
-    (t,           VLam _ _ t'  ) => unify (l + 1) !(t `vapp` VVar l [<]) !(t' $$ VVar l [<])
-    (VLam _ _ t,  t'           ) => unify (l + 1) !(t $$ VVar l [<]) !(t' `vapp` VVar l [<])
-    (VPi _ _ a b, VPi _ _ a' b') => unify l a a' >> unify (S l) !(b $$ VVar l [<]) !(b' $$ VVar l [<])
-    (VVar k sp,   VVar k' sp'  ) => unifySpine l (k == k') sp sp'
-    (VRef n sp,   VRef n' sp'  ) => unifySpine l (n == n') sp sp'
-    (VMeta i sp,  VMeta i' sp' ) => unifySpine l (i == i') sp sp'
-
-    (t,           VMeta i' sp') => solve l i' sp' t
-    (VMeta i sp, t'           ) => solve l i sp t'
-    (VU, VU) => pure ()
-    _ => throwError $ E (0,0) "unify failed"
+  unify l t u = do
+    putStrLn "Unify \{show ctx.lvl}"
+    putStrLn "  \{show l} \{show t}"
+    putStrLn "  =?= \{show u}"
+    t' <- forceMeta t
+    u' <- forceMeta u
+    case (t',u') of
+      (VLam _ _ t,  VLam _ _ t'  ) => unify (l + 1) !(t $$ VVar l [<]) !(t' $$ VVar l [<])
+      (t,           VLam _ _ t'  ) => unify (l + 1) !(t `vapp` VVar l [<]) !(t' $$ VVar l [<])
+      (VLam _ _ t,  t'           ) => unify (l + 1) !(t $$ VVar l [<]) !(t' `vapp` VVar l [<])
+      (VPi _ _ a b, VPi _ _ a' b') => unify l a a' >> unify (S l) !(b $$ VVar l [<]) !(b' $$ VVar l [<])
+      (VVar k sp,   VVar k' sp'  ) =>
+        if k == k' then unifySpine l (k == k') sp sp'
+        else error [DS "vvar mismatch \{show k} \{show k'}"]
+      (VRef k sp,   VRef k' sp'  ) =>
+        if k == k' then unifySpine l (k == k') sp sp'
+        else error [DS "vref mismatch \{show k} \{show k'}"]
+      (VMeta k sp,  VMeta k' sp' ) =>
+        if k == k' then unifySpine l (k == k') sp sp'
+        else solve l k sp (VMeta k' sp')
+      (t,           VMeta i' sp') => solve l i' sp' t
+      (VMeta i sp, t'           ) => solve l i sp t'
+      (VU, VU) => pure ()
+      -- REVIEW consider quoting back
+      _ => error [DS "unify failed", DS (show t'), DS "=?=", DS (show u') ]
 
+insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
+insert ctx tm ty = do
+  case !(forceMeta ty) of
+    VPi x Implicit a b => do
+      m <- freshMeta ctx
+      mv <- eval ctx.env CBN m
+      insert ctx (App tm m) !(b $$ mv)
+    va => pure (tm, va)
 
 export
 infer : Context -> Raw  -> M  (Tm, Val)
 
 export
 check : Context -> Raw -> Val  -> M  Tm
-check ctx (RSrcPos x tm) ty = check ({pos := x} ctx) tm ty
-check ctx (RLam nm icit tm) ty = case ty of                    
-                  (VPi pinm icit a b) => do
-                    -- TODO icit
-                    let var = VVar (length ctx.env) [<]
-                    let ctx' = extend ctx nm a
-                    tm' <- check ctx' tm !(b $$ var)
-                    pure $ Lam nm icit tm'
-                  other => error [(DS "Expected pi type, got \{show !(quote 0 ty)}")]
-check ctx tm ty = do
-  (tm', ty') <- infer ctx tm
-  -- This is where the conversion check / pattern unification go
-  unify ctx.lvl ty' ty
-  -- if quote 0 ty /= quote 0 ty' then
-  --     error [DS "type mismatch got", DD (quote 0 ty'), DS "expected", DD (quote 0 ty)]
-  --   else pure tm'
-  pure tm'
+check ctx tm ty with (force ty)
+  check ctx (RSrcPos x tm) _ | ty = check ({pos := x} ctx) tm ty
+  check ctx t@(RLam nm icit tm) _ | ty = case ty of
+          (VPi nm' icit' a b) => do
+            putStrLn "icits \{nm} \{show icit} \{nm'} \{show icit'}"
+            if icit == icit' then do
+                let var = VVar (length ctx.env) [<]
+                let ctx' = extend ctx nm a
+                tm' <- check ctx' tm !(b $$ var)
+                pure $ Lam nm icit tm'
+              else if icit' == Implicit then do
+                let var = VVar (length ctx.env) [<]
+                ty' <- b $$ var
+                sc <- check (extend ctx nm' a) t ty'
+                pure $ Lam nm' icit' sc
+              else
+                error [(DS "Icity issue checking \{show t} at \{show ty}")]
+          other => error [(DS "Expected pi type, got \{show !(quote 0 ty)}")]
+  check ctx tm _ | (VPi nm' Implicit a b) = do
+    putStrLn "XXX edge \{show tm} against VPi"
+    let var = VVar (length ctx.env) [<]
+    ty' <- b $$ var
+    sc <- check (extend ctx nm' a) tm ty'
+    pure $ Lam nm' Implicit sc
+  check ctx tm _ | ty = do
+    -- We need to insert if it's not a Lam
+    -- TODO figure out why the exception is here (cribbed from kovacs)
+    (tm', ty') <- case !(infer ctx tm) of
+      (tm'@(Lam{}),ty') => pure (tm', ty')
+      (tm', ty') => insert ctx tm' ty'
+    putStrLn "infer \{show tm} to \{show tm'} : \{show ty'} expect \{show ty}"
+    when( ctx.lvl /= length ctx.env) $ error [DS "level mismatch \{show ctx.lvl} \{show ctx.env}"]
+    unify ctx ctx.lvl ty' ty
+    pure tm'
 
 infer ctx (RVar nm) = go 0 ctx.types
   where
@@ -131,17 +166,36 @@ infer ctx (RVar nm) = go 0 ctx.types
       Just (MkEntry name ty (Fn t)) => pure (Ref nm (Just t), !(eval [] CBN ty))
       Just (MkEntry name ty _) => pure (Ref nm Nothing, !(eval [] CBN ty))
       Nothing => error [DS "\{show nm} not in scope"]
-    go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty) 
+    go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty)
       else go (i + 1) xs
   -- need environment of name -> type..
-infer ctx (RApp t u icit) = do 
+infer ctx (RApp t u icit) = do
   -- icit will be used for insertion, lets get this working first...
-  (t, tty) <- infer ctx t
-  case tty of
-    (VPi str icit' a b) => do
-      u <- check ctx u a
-      pure (App t u, !(b $$ !(eval ctx.env CBN u)))
-    _ => error [DS "Expected Pi type"]
+
+  (icit, t, tty) <- case the Icit icit of
+      Explicit => do
+        (t, tty) <- infer ctx t
+        (t, tty) <- insert ctx t tty
+        pure (Explicit, t, tty)
+      Implicit => do
+        (t, tty) <- infer ctx t
+        pure (Implicit, t, tty)
+
+  (a,b) <- case !(forceMeta tty) of
+    (VPi str icit' a b) => if icit' == icit then pure (a,b)
+        else error [DS "IcitMismatch \{show icit} \{show icit'}"]
+
+    -- If it's not a VPi, try to unify it with a VPi
+    tty => do
+      putStrLn "unify PI for \{show tty}"
+      a <- eval ctx.env CBN !(freshMeta ctx)
+      b <- MkClosure ctx.env <$> freshMeta (extend ctx "x" ?hole)
+      unify ctx 0 tty (VPi "x" icit a b)
+      pure (a,b)
+
+  u <- check ctx u a
+  pure (App t u, !(b $$ !(eval ctx.env CBN u)))
+
 infer ctx RU = pure (U, VU) -- YOLO
 infer ctx (RPi nm icit ty ty2) = do
   ty' <- check ctx ty VU
@@ -153,17 +207,24 @@ infer ctx (RLet str tm tm1 tm2) = error [DS "implement RLet"]
 infer ctx (RSrcPos x tm) = infer ({pos := x} ctx) tm
 infer ctx (RAnn tm rty) = do
   ty <- check ctx rty VU
-  vty <- eval ctx.env CBN ty 
+  vty <- eval ctx.env CBN ty
   tm <- check ctx tm vty
   pure (tm, vty)
 
-infer ctx (RLam str icit tm) = error [DS "can't infer lambda"]
+infer ctx (RLam nm icit tm) = do
+  a <- freshMeta ctx >>= eval ctx.env CBN
+  let ctx' = extend ctx nm a
+  (tm', b) <- infer ctx' tm
+  putStrLn "make lam for \{show nm} scope \{show tm'} : \{show b}"
+  pure $ (Lam nm icit tm', VPi nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
+  -- error {ctx} [DS "can't infer lambda"]
+
 infer ctx RHole = do
   ty <- freshMeta ctx
   vty <- eval ctx.env CBN ty
   tm <- freshMeta ctx
   pure (tm, vty)
-  
+
 infer ctx tm = error [DS "Implement infer \{show tm}"]
 
 -- I don't have types for these yet...
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 901bdc1..b0e2965 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -14,6 +14,7 @@ import Lib.Token
 import Lib.Parser.Impl
 import Syntax
 import Data.List
+import Data.Maybe
 
 -- There is the whole core vs surface thing here.
 -- might be best to do core first/ Technically don't
@@ -186,10 +187,11 @@ ibind : Parser (List (String, Icit, Raw))
 ibind = do
   sym "{"
   names <- some ident
-  sym ":"
-  ty <- typeExpr
+  ty <- optional (sym ":" >> typeExpr)
+  pos <- getPos
   sym "}"
-  pure $ map (\name => (name, Explicit, ty)) names
+  -- getPos is a hack here, I would like to position at the name... 
+  pure $ map (\name => (name, Implicit, fromMaybe (RSrcPos pos RHole) ty)) names
 
 -- Collect a bunch of binders (A : U) {y : A} -> ...
 binders : Parser Raw
diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr
index a98bb53..cd40ded 100644
--- a/src/Lib/Parser/Impl.idr
+++ b/src/Lib/Parser/Impl.idr
@@ -14,7 +14,7 @@ SourcePos : Type
 SourcePos = (Int,Int)
 
 emptyPos : SourcePos
-emptyPos = (0,0) 
+emptyPos = (0,0)
 
 -- Error of a parse
 public export
@@ -27,17 +27,17 @@ showError src (E (line, col) msg) = "ERROR at \{show (line,col)}: \{msg}\n" ++ g
   where
     go : Int -> List String -> String
     go l [] = ""
-    go l (x :: xs) = 
+    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 if line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
       else go (l + 1) xs
 
 -- Result of a parse
 public export
 data Result : Type -> Type where
   OK : a -> (toks : TokenList) -> (com : Bool) -> Result a
-  Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool)  -> Result a  
+  Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool)  -> Result a
 
 export
 Functor Result where
@@ -92,13 +92,13 @@ Functor Parser where
   map f (P pa) = P $ \ toks, com, col => map f (pa toks com col)
 
 export
-Applicative Parser where 
+Applicative Parser where
   pure pa = P (\ toks, com, col => OK pa toks com)
   P pab <*> P pa = P $ \toks,com,col =>
     case pab toks com col of
       Fail fatal err toks com => Fail fatal err toks com
-      OK f toks com => 
-        case pa toks com col of 
+      OK f toks com =>
+        case pa toks com col of
           (OK x toks com) => OK (f x) toks com
           (Fail fatal err toks com) => Fail fatal err toks com
 
@@ -125,7 +125,7 @@ pred : (BTok -> Bool) -> String -> Parser String
 pred f msg = P $ \toks,com,col =>
   case toks of
     (t :: ts) => if f t then OK (value t) ts com else Fail False (error toks "\{msg} vt:\{value t}") toks com
-    [] => Fail False (error toks "eof") toks com
+    [] => Fail False (error toks "\{msg} at EOF") toks com
 
 export
 commit : Parser ()
@@ -138,7 +138,7 @@ defer f = P $ \toks,com,col => runP (f ()) toks com col
 mutual
   export some : Parser a -> Parser (List a)
   some p = defer $ \_ => [| p :: many p|] --(::) <$> p <*> many p)
-  
+
   export many : Parser a -> Parser (List a)
   many p = some p <|> pure []
 
@@ -169,8 +169,8 @@ export
 sameLevel : Parser a -> Parser a
 sameLevel (P p) = P $ \toks,com,(l,c) => case toks of
   [] => p toks com (l,c)
-  (t :: _) => 
-    let (tl,tc) = start t 
+  (t :: _) =>
+    let (tl,tc) = start t
     in if tc == c then p toks com (tl, c)
     else if c < tc then Fail False (error toks "unexpected indent") toks com
     else Fail False (error toks "unexpected indent") toks com
diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr
index b01212a..e282b34 100644
--- a/src/Lib/Prettier.idr
+++ b/src/Lib/Prettier.idr
@@ -13,6 +13,7 @@ export
 data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc
 
 ||| `DOC` is an intermediate form used during layout/rendering
+||| The capitalization is the opposite of the paper.
 data DOC = EMPTY | TEXT String DOC | LINE Nat DOC
 
 flatten : Doc -> Doc
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index 70e5067..f502857 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -3,6 +3,9 @@
 -- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q
 -- or drop the indices for now.
 
+-- ***
+-- Kovacs has icity on App, and passes it around, but I'm not sure where it is needed since the insertion happens based on Raw.
+
 module Lib.TT
 -- For SourcePos
 import Lib.Parser.Impl
@@ -34,17 +37,21 @@ export
 error' : String -> M a
 error' msg = throwError $ E (0,0) msg
 
+-- order does indeed matter on the meta arguments
+-- because of dependent types (if we want something well-typed back out)
 
 export
 freshMeta : Context -> M Tm
 freshMeta ctx = do
   mc <- readIORef ctx.metas
-  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved mc.next ctx.bds ::) } mc
-  pure $ applyBDs 0 (Meta mc.next) ctx.bds 
+  putStrLn "INFO at \{show ctx.pos}: fresh meta \{show mc.next}"
+  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved ctx.pos mc.next ctx.bds ::) } mc
+  pure $ applyBDs 0 (Meta 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 (applyBDs (S k) t xs) (Bnd k)
   applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
 
@@ -57,7 +64,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
@@ -69,10 +76,12 @@ solveMeta ctx ix tm = do
   where
     go : List MetaEntry -> SnocList MetaEntry -> M (List MetaEntry)
     go [] _ = error' "Meta \{show ix} not found"
-    go (meta@(Unsolved k _) :: xs) lhs = if k == ix 
-      then pure $ lhs <>> (Solved k tm :: xs)
+    go (meta@(Unsolved pos k _) :: xs) lhs = if k == ix
+      then do
+        putStrLn "INFO at \{show pos}: solve \{show k} as \{show tm}"
+        pure $ lhs <>> (Solved k tm :: xs)
       else go xs (lhs :< meta)
-    go (meta@(Solved k _) :: xs) lhs = if k == ix 
+    go (meta@(Solved k _) :: xs) lhs = if k == ix
       then error' "Meta \{show ix} already solved!"
       else go xs (lhs :< meta)
 
@@ -88,7 +97,7 @@ export
 extend : Context -> String -> Val -> Context
 extend ctx name ty =
     { lvl $= S, env $= (VVar ctx.lvl [<] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx
-    
+
 -- I guess we define things as values?
 export
 define : Context -> String -> Val -> Val -> Context
@@ -146,7 +155,7 @@ eval env mode (App t u) = vapp !(eval env mode t) !(eval env mode u)
 eval env mode U = pure VU
 eval env mode (Meta i) =
   case !(lookupMeta i) of
-        (Unsolved k xs) => pure $ VMeta i [<]
+        (Unsolved _ k xs) => pure $ VMeta i [<]
         (Solved k t) => pure $ t
 eval env mode (Lam x icit t) = pure $ VLam x icit (MkClosure env t)
 eval env mode (Pi x icit a b) = pure $ VPi x icit !(eval env mode a) (MkClosure env b)
@@ -154,13 +163,13 @@ eval env mode (Let x icit ty t u) = eval (!(eval env mode t) :: env) mode u
 eval env mode (Bnd i) = case getAt i env of
   Just rval => pure rval
   Nothing => error' "Bad deBruin index \{show i}"
-  
+
 export
 quote : (lvl : Nat) -> Val -> M Tm
 
 quoteSp : (lvl : Nat) -> Tm -> SnocList Val -> M Tm
 quoteSp lvl t [<] = pure t
-quoteSp lvl t (xs :< x) = 
+quoteSp lvl t (xs :< x) =
   pure $ App !(quoteSp lvl t xs) !(quote lvl x)
   -- quoteSp lvl (App t !(quote lvl x)) xs  -- snoc says previous is right
 
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 720a1e3..f69fbf5 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -28,6 +28,11 @@ data Icit = Implicit | Explicit
 
 %name Icit icit
 
+export
+Show Icit where
+  show Implicit = "Implicit"
+  show Explicit = "Explicit"
+
 public export
 data BD = Bound | Defined
 
@@ -41,6 +46,7 @@ data Tm : Type where
   -- kovacs optimization, I think we can App out meta instead
   -- InsMeta : Nat -> List BD -> Tm
   Lam : Name -> Icit -> Tm -> Tm
+  -- Do we need to remember Icit here?
   App : Tm -> Tm -> Tm
   U   : Tm
   Pi  : Name -> Icit -> Tm -> Tm -> Tm
@@ -57,13 +63,14 @@ Show Tm where
   show (App t u) = "(\{show t} \{show u})"
   show (Meta i) = "(Meta \{show i})"
   show U = "U"
-  show (Pi str icit t u) = "(∏ \{str} : \{show t} => \{show u})"
+  show (Pi str Implicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
+  show (Pi str Explicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
   show (Let str icit t u v) = "let \{str} : \{show t} = \{show u} in \{show v}"
 
 -- I can't really show val because it's HOAS...
 
 -- TODO derive
-export 
+export
 Eq Icit where
   Implicit == Implicit = True
   Explicit == Explicit = True
@@ -126,9 +133,6 @@ data Val : Type where
   VPi : Name -> Icit -> Lazy Val -> Closure -> Val
   VU : Val
 
-Show Icit where
-  show Implicit = "I"
-  show Explicit = "E"
 
 Show Closure
 
@@ -138,7 +142,8 @@ Show Val where
   show (VRef nm sp) = "(%ref \{nm} \{show sp})"
   show (VMeta ix sp) = "(%meta \{show ix} \{show sp})"
   show (VLam str icit x) = "(%lam \{str} \{show icit} \{show x})"
-  show (VPi str icit x y) = "(%pi \{str} \{show icit} \{show x} \{show y})"
+  show (VPi str Implicit x y) = "(%pi {\{str} : \{show  x}}. \{show  y})"
+  show (VPi str Explicit x y) = "(%pi (\{str} : \{show  x}). \{show  y})"
   show VU = "U"
 
 public export
@@ -174,7 +179,7 @@ So I guess we have top and local then?
 With haskell syntax. I think we can have Axiom for claims and rewrite to def later.
 
 Hmm, so given ezoo, if I'm going simple, I could keep BDs short, and use the normal
-context. (Zoo4.lean:222) I'd probably still need an undefined/axiom marker as a value? 
+context. (Zoo4.lean:222) I'd probably still need an undefined/axiom marker as a value?
 
 ok, so with just one context, Env is List Val and we're getting Tm back from type checking.
 
@@ -182,9 +187,14 @@ Can I get val back? Do we need to quote? What happens if we don't?
 
 -}
 
--- FIXME remove List BD
 public export
-data MetaEntry = Unsolved Nat (List BD) | Solved Nat Val
+data MetaEntry = Unsolved SourcePos Nat (List BD) | Solved Nat Val
+
+export
+covering
+Show MetaEntry where
+  show (Unsolved pos k xs) = "Unsolved \{show pos} \{show k}"
+  show (Solved k x) = "Solved \{show k} \{show x}"
 
 public export
 record MetaContext where
@@ -241,7 +251,7 @@ record Context where
   -- so we'll try "bds" determines length of local context
   bds  : List BD          -- bound or defined
   pos : SourcePos            -- the last SourcePos that we saw
-  
+
   -- We only need this here if we don't pass TopContext
   -- top : TopContext
   metas : IORef MetaContext
diff --git a/src/Main.idr b/src/Main.idr
index 366bf74..dda436b 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -48,6 +48,7 @@ dumpContext top = do
 processDecl : Decl -> M ()
 processDecl (TypeSig nm tm) = do
   top <- get
+  putStrLn "-----"
   putStrLn "TypeSig \{nm} \{show tm}"
   ty <- check (mkCtx top.metas) tm VU
   putStrLn "got \{show ty}"
@@ -55,6 +56,7 @@ processDecl (TypeSig nm tm) = do
 
 -- FIXME - this should be in another file
 processDecl (Def nm raw) = do
+  putStrLn "-----"
   putStrLn "def \{show nm}"
   ctx <- get
   let pos = case raw of
@@ -67,12 +69,13 @@ processDecl (Def nm raw) = do
     | _ => throwError $ E pos "\{nm} already defined"
   putStrLn "check \{nm} = \{show raw} at \{show $ ty}"
   vty <- eval empty CBN ty
+  putStrLn "vty is \{show vty}"
   tm <- check (mkCtx ctx.metas) raw vty
   putStrLn "Ok \{show tm}"
   put (addDef ctx nm tm ty)
 
 processDecl (DCheck tm ty) = do
-  
+
   top <- get
   putStrLn "check \{show tm} at \{show ty}"
   ty' <- check (mkCtx top.metas) tm VU
@@ -84,7 +87,7 @@ processDecl (DCheck tm ty) = do
   putStrLn "norm \{show norm}"
   -- top <- get
   -- ctx <- mkCtx top.metas
-  -- I need a type to check against 
+  -- I need a type to check against
   -- norm <- nf [] x
   putStrLn "NF "
 
@@ -108,7 +111,7 @@ processDecl (Data nm ty cons) = do
           dty <- check (mkCtx ctx.metas) tm VU
           modify $ claim nm' dty
       _ => throwError $ E (0,0) "expected TypeSig"
-  
+
   pure ()
   where
     checkDeclType : Tm -> M ()
@@ -128,9 +131,9 @@ processFile fn = do
   printLn "process Decls"
   Right _ <- tryError $ traverse_ processDecl res.decls
     | Left y => putStrLn (showError src y)
-  
+
   dumpContext !get
-  
+
 main' : M ()
 main' = do
   args <- getArgs
@@ -139,7 +142,7 @@ main' = do
     | _ => putStrLn "Usage: newt foo.newt"
   -- Right files <- listDir "eg"
   --   | Left err => printLn err
-  
+
   traverse_ processFile (filter (".newt" `isSuffixOf`) files)
 
 main : IO ()
diff --git a/src/Syntax.idr b/src/Syntax.idr
index b8c93ed..f0bccbe 100644
--- a/src/Syntax.idr
+++ b/src/Syntax.idr
@@ -114,11 +114,6 @@ Show Pattern where
 Show CaseAlt where
   show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
 
-Show Icit where
-  show Implicit = "Implicit"
-  show Explicit = "Explicit"
-  -- show Eq = "Eq"
-
 covering
 Show Raw where
   show RHole = "_"