[ unify ] Don't add constraints for vvar with spine. Constrain vvar instead of η expanding.

TODO.md

@@ -7,8 +7,10 @@
 - [ ] consider making meta application implicit in term, so its more readable when printed
   - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people
     leave that implicit for efficiency. I think it would also make printing more readable.
+  - When printing `Value`, I now print the spine size instead of spine.
 - [x] eval for case (see order.newt)
 - [ ] dynamic pattern unification (add test case first)
+  - Possibly the cause of issue in code commented out in `TestCase4.newt`
 - [x] switch from commit/mustWork to checking progress
 - [x] type constructors are no longer generated?  And seem to have 0 arity.
 - [x] raw let is not yet implemented (although define used by case tree building)

newt/Tree.newt

@@ -59,12 +59,13 @@ data T23 : Bnd -> Bnd -> Nat -> U where
 -- 56:
 
 infixl 5 _*_
-infixl 1 _,_
+infixr 1 _,_
+infixr 1 _**_
 data Sg : (A : U) -> (A -> U) -> U where
-  _,_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
+  _**_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
 
 data _*_ : (A B : U) -> U where
-   Foo : {A B : U} -> A -> B -> A * B
+   _,_ : {A B : U} -> A -> B -> A * B
 
 TooBig : Bnd -> Bnd -> Nat -> U
 TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
@@ -72,12 +73,11 @@ TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
 insert : {h : Nat} {l u : Bnd} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
 insert (MkI x lx xu) (leaf lu) = ?
 insert (MkI x lx xu) (node2 x1 t t1) = ?
--- TODO - unify error the typ
 insert (MkI x lx xu) (node3 y z tly tyz tzu) = case cmp x y of
   -- u := N y is not solved at this time
   inl xy => case insert (MkI {_} {N y} x lx xy) tly of
-    -- It's having trouble with Foo because of a spine length issue
-    -- Idris says this isn't covering, even with just `inl a` , `inr a`
-    inl (v , (Foo tlv tvy)) => inl (y, node2 v tlv tvy, node2 z tyz tzy)
+    -- NOW down to a non-linear issue now.
+    -- Possibly due to the meta being applied to an extra argument
+    inl (v ** (tlv , tvy)) => inl (y ** (node2 v tlv tvy, node2 z tyz tzu))
     inr x1 => ?
   inr x1 => ?

src/Lib/Elab.idr

@@ -93,7 +93,7 @@ parameters (ctx: Context)
           then do
             debug "\{show k} \{show acc}"
 
-            error fc "non-linear pattern"
+            error fc "non-linear pattern: \{show sp}"
           else go xs (k :: acc)
       go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}"
 
@@ -194,9 +194,6 @@ parameters (ctx: Context)
     debug "env \{show ctx.env}"
     debug "types \{show $ ctx.types}"
     case (t',u') of
-      (VLam _ _ t,  VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
-      (t,         VLam fc' _ t') => unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
-      (VLam fc _ t,  t'       ) => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<])
       (VMeta fc k sp,  VMeta fc' k' sp' ) =>
         if k == k' then unifySpine l (k == k') sp sp'
         -- TODO, might want to try the other way, too.
@@ -207,11 +204,14 @@ parameters (ctx: Context)
       (VVar fc k sp,   (VVar fc' k' sp')  ) =>
         if k == k' then unifySpine l (k == k') sp sp'
         else if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')]
-        -- else error ctx.fc "unify error: vvar mismatch \{show k} \{show k'} \{show ctx.env}"
 
       -- attempt at building constraints
-      (VVar fc k sp, u) => pure $ MkResult[(k, u)]
-      (t, VVar fc k sp) => pure $ MkResult[(k, t)]
+      (VVar fc k [<], u) => pure $ MkResult[(k, u)]
+      (t, VVar fc k [<]) => pure $ MkResult[(k, t)]
+
+      (VLam _ _ t,  VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
+      (t,         VLam fc' _ t') => unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
+      (VLam fc _ t,  t'       ) => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<])
 
       -- REVIEW - consider separate value for DCon/TCon
       (VRef fc k def sp,   VRef fc' k' def' sp'  ) =>
@@ -578,9 +578,7 @@ checkDone ctx [] body ty = do
   -- I'm running an eval here to run case statements that are
   -- unblocked by lets in the env. (Tree.newt:cmp)
   -- The case eval code only works in the Tm -> Val case at the moment.
-  -- we don't have anything like `vapp`
-  -- NOW In Tree.newt we have a case/case unification that might
-  -- have succeeded if it was left as a functino call.
+  -- we don't have anything like `vapp` for case
   ty <- quote (length ctx.env) ty
   ty <- eval ctx.env CBV ty
   debug "check at \{show ty}"
@@ -647,7 +645,8 @@ check ctx tm ty = case (tm, !(forceType ty)) of
     -- Maybe we can let the scrutinee and jump into the middle?
     (sc, scty) <- infer ctx rsc
     scty <- forceMeta scty
-    debug "SCTM/TY \{pprint (names ctx) sc} \{show scty}"
+    debug "SCTM \{pprint (names ctx) sc}"
+    debug "SCTY \{show scty}"
 
     let scnm = fresh "sc"
     top <- get
@@ -697,7 +696,6 @@ check ctx tm ty = case (tm, !(forceType ty)) of
   (t@(RLam fc nm icit tm), ty) =>
             error fc "Expected pi type, got \{!(prvalCtx ty)}"
 
-  -- NOW Test1.newt passes with Explicit, TestCase4.newt passes with Implicit
   (tm, ty@(VPi fc nm' Implicit a b)) => do
     let names = toList $ map fst ctx.types
     debug "XXX edge add implicit lambda {\{nm'} : \{show a}} to \{show tm} "

src/Lib/Types.idr

@@ -225,7 +225,7 @@ covering export
 Show Val where
   show (VVar _ k sp) = "(%var \{show k} \{show sp})"
   show (VRef _ nm _ sp) = "(%ref \{nm} \{show sp})"
-  show (VMeta _ ix sp) = "(%meta \{show ix} \{show sp})"
+  show (VMeta _ ix sp) = "(%meta \{show ix} \{show $ length sp})"
   show (VLam _ str x) = "(%lam \{str} \{show x})"
   show (VPi fc str Implicit x y) = "(%pi {\{str} : \{show  x}}. \{show  y})"
   show (VPi fc str Explicit x y) = "(%pi (\{str} : \{show  x}). \{show  y})"