Implement occurs check properly (finally!)

Instead of the previous unreliable hack, actually look for occurrences of the solved metavariable. Block if there are any, and fail if there are any under a constructor. I had expected this to hurt performance quite a bit, but it seems it doesn't. This was prompted by #304, which is now partly fixed, but there's still a refinement to unification needed to fix it fully (and at least it doesn't segfault due to the cycle now!)
2024-11-22 18:52:39 +03:00 · 2020-04-27 11:21:50 +01:00 · 2020-04-27 11:21:50 +01:00 · ff86f6f834
commit ff86f6f834
parent 19426ecd14
19 changed files with 118 additions and 62 deletions
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@ -103,7 +103,7 @@ last : {n : _} -> Fin (S n)
 last {n=Z} = FZ
 last {n=S _} = FS last

-export total
+public export total
 FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
 FSinjective Refl = Refl

--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@ -27,7 +27,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 22
+ttcVersion = 23

 export
 checkTTCVersion : String -> Int -> Int -> Core ()
--- a/src/Core/Core.idr
+++ b/src/Core/Core.idr
@ -48,7 +48,7 @@ data Error
    | CantConvert FC (Env Term vars) (Term vars) (Term vars)
    | CantSolveEq FC (Env Term vars) (Term vars) (Term vars)
    | PatternVariableUnifies FC (Env Term vars) Name (Term vars)
-    | CyclicMeta FC Name
+    | CyclicMeta FC (Env Term vars) Name (Term vars)
    | WhenUnifying FC (Env Term vars) (Term vars) (Term vars) Error
    | ValidCase FC (Env Term vars) (Either (Term vars) Error)
    | UndefinedName FC Name
@ -124,8 +124,9 @@ Show Error where
      = show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal"
  show (PatternVariableUnifies fc env n x)
      = show fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x
-  show (CyclicMeta fc n)
+  show (CyclicMeta fc env n tm)
      = show fc ++ ":Cycle detected in metavariable solution " ++ show n
+             ++ " = " ++ show tm
  show (WhenUnifying fc _ x y err)
      = show fc ++ ":When unifying: " ++ show x ++ " and " ++ show y ++ "\n\t" ++ show err
  show (ValidCase fc _ prob)
@ -275,7 +276,7 @@ getErrorLoc (Fatal err) = getErrorLoc err
 getErrorLoc (CantConvert loc _ _ _) = Just loc
 getErrorLoc (CantSolveEq loc _ _ _) = Just loc
 getErrorLoc (PatternVariableUnifies loc _ _ _) = Just loc
-getErrorLoc (CyclicMeta loc _) = Just loc
+getErrorLoc (CyclicMeta loc _ _ _) = Just loc
 getErrorLoc (WhenUnifying loc _ _ _ _) = Just loc
 getErrorLoc (ValidCase loc _ _) = Just loc
 getErrorLoc (UndefinedName loc _) = Just loc
--- a/src/Core/Normalise.idr
+++ b/src/Core/Normalise.idr
@ -54,15 +54,16 @@ export
 toClosure : EvalOpts -> Env Term outer -> Term outer -> Closure outer
 toClosure opts env tm = MkClosure opts [] env tm

-useMeta : FC -> Name -> Defs -> EvalOpts -> Core EvalOpts
-useMeta fc (Resolved i) defs opts
+useMeta : Bool -> FC -> Name -> Defs -> EvalOpts -> Core (Maybe EvalOpts)
+useMeta False _ _ _ opts = pure $ Just opts
+useMeta True fc (Resolved i) defs opts
    = case lookup i (usedMetas opts) of
-           Nothing => pure (record { usedMetas $= insert i () } opts)
-           Just _ => throw (CyclicMeta fc (Resolved i))
-useMeta fc n defs opts
+           Nothing => pure (Just (record { usedMetas $= insert i () } opts))
+           Just _ => pure Nothing
+useMeta True fc n defs opts
    = do let Just i = getNameID n (gamma defs)
              | Nothing => throw (UndefinedName fc n)
-         useMeta fc (Resolved i) defs opts
+         useMeta True fc (Resolved i) defs opts

 parameters (defs : Defs, topopts : EvalOpts)
  mutual
@ -195,9 +196,8 @@ parameters (defs : Defs, topopts : EvalOpts)
                                        (visibility res)
             if redok
                then do
-                   opts' <- if noCycles res
-                               then useMeta fc n defs topopts
-                               else pure topopts
+                   Just opts' <- useMeta (noCycles res) fc n defs topopts
+                        | Nothing => pure def
                   evalDef env opts' meta fc
                           (multiplicity res) (definition res) (flags res) stk def
                else pure def
--- a/src/Core/Unify.idr
+++ b/src/Core/Unify.idr
@ -184,6 +184,29 @@ convertErrorS s loc env x y
    = if s then convertError loc env y x
           else convertError loc env x y

+-- Find all the metavariables required by each of the given names.
+-- We'll assume all meta solutions are of the form STerm exp.
+chaseMetas : {auto c : Ref Ctxt Defs} ->
+             List Name -> NameMap () -> Core (List Name)
+chaseMetas [] all = pure (keys all)
+chaseMetas (n :: ns) all
+    = case lookup n all of
+           Just _ => chaseMetas ns all
+           _ => do defs <- get Ctxt
+                   Just (PMDef _ _ (STerm soln) _ _) <-
+                                  lookupDefExact n (gamma defs)
+                        | _ => chaseMetas ns (insert n () all)
+                   let sns = keys (getMetas soln)
+                   chaseMetas (sns ++ ns) (insert n () all)
+
+-- Get all the metavariable names used by the term (recursively, so we
+-- can do the occurs check)
+getMetaNames : {auto c : Ref Ctxt Defs} ->
+               Term vars -> Core (List Name)
+getMetaNames tm
+    = let metas = getMetas tm in
+          chaseMetas (keys metas) empty
+
 postpone : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           (blockedMeta : Bool) ->
@ -199,6 +222,8 @@ postpone blockedMetas loc mode logstr env x y
                                    " =?= " ++ show !(toFullNames yq))
         xtm <- quote empty env x
         ytm <- quote empty env y
+         -- Need to find all the metas in the constraint since solving any one
+         -- of them might stop the constraint being blocked.
         metas <-
             if blockedMetas
                then let xmetas = getMetas xtm in
@ -214,21 +239,6 @@ postpone blockedMetas loc mode logstr env x y
         logTerm 10 "Y" ytm
         pure (constrain c)
  where
-    -- Need to find all the metas in the constraint since solving any one
-    -- of them might stop the constraint being blocked. We'll assume all
-    -- meta solutions are of the form STerm exp.
-    chaseMetas : List Name -> NameMap () -> Core (List Name)
-    chaseMetas [] all = pure (keys all)
-    chaseMetas (n :: ns) all
-        = case lookup n all of
-               Just _ => chaseMetas ns all
-               _ => do defs <- get Ctxt
-                       Just (PMDef _ _ (STerm soln) _ _) <-
-                                      lookupDefExact n (gamma defs)
-                            | _ => chaseMetas ns (insert n () all)
-                       let sns = keys (getMetas soln)
-                       chaseMetas (sns ++ ns) (insert n () all)
-
    undefinedN : Name -> Core Bool
    undefinedN n
        = do defs <- get Ctxt
@ -378,6 +388,44 @@ patternEnvTm {vars} env args
               Nothing => updateVars ps svs
               Just p' => p' :: updateVars ps svs

+-- Check that the metavariable name doesn't occur in the solution.
+-- If it does, normalising might help. If it still does, that's an error.
+
+-- Also block if there's an unsolved meta under a function application,
+-- because that might cause future problems to get stuck even if they're
+-- solvable.
+occursCheck : {auto c : Ref Ctxt Defs} ->
+              FC -> Env Term vars -> UnifyInfo ->
+              Name -> Term vars -> Core (Maybe (Term vars))
+occursCheck fc env mode mname tm
+    = do solmetas <- getMetaNames tm
+         let False = mname `elem` solmetas
+             | _ => do defs <- get Ctxt
+                       tmnf <- normalise defs env tm
+                       solmetas <- getMetaNames tmnf
+                       if mname `elem` solmetas
+                          then do failOnStrongRigid False
+                                     (throw (CyclicMeta fc env mname tmnf))
+                                     tmnf
+                                  pure Nothing
+                          else pure $ Just tmnf
+         pure $ Just tm
+  where
+    -- Throw an occurs check failure if the name appears 'strong rigid',
+    -- that is, under a constructor form rather than a function, in the
+    -- term
+    failOnStrongRigid : Bool -> Core () -> Term vars -> Core ()
+    failOnStrongRigid bad err (Meta _ n _ _)
+        = if bad && n == mname
+             then err
+             else pure ()
+    failOnStrongRigid bad err tm
+        = case getFnArgs tm of
+               (f, []) => pure ()
+               (Ref _ Func _, _) => pure () -- might reduce away, just block
+               (Ref _ _ _, args) => traverse_ (failOnStrongRigid True err) args
+               (f, args) => traverse_ (failOnStrongRigid bad err) args
+
 -- Instantiate a metavariable by binding the variables in 'newvars'
 -- and returning the term
 -- If the type of the metavariable doesn't have enough arguments, fail, because
@ -748,6 +796,11 @@ mutual
                                          (NApp loc (NMeta mname mref margs) margs')
                                          tmnf
                     tm <- quote empty env tmnf
+                     Just tm <- occursCheck loc env mode mname tm
+                         | _ => postponeS True swap loc mode "Occurs check failed" env
+                                          (NApp loc (NMeta mname mref margs) margs')
+                                          tmnf
+
                     case shrinkTerm tm submv of
                          Just stm => solveHole fc mode env mname mref
                                                margs margs' locs submv
--- a/src/Idris/Error.idr
+++ b/src/Idris/Error.idr
@ -46,8 +46,10 @@ perror (PatternVariableUnifies _ env n tm)
    showPVar : Name -> String
    showPVar (PV n _) = showPVar n
    showPVar n = show n
-perror (CyclicMeta _ n)
-    = pure $ "Cycle detected in solution of metavariable " ++ show n
+perror (CyclicMeta _ env n tm)
+    = pure $ "Cycle detected in solution of metavariable "
+               ++ show !(prettyName n) ++ " = "
+               ++ !(pshow env tm)
 perror (WhenUnifying _ env x y err)
    = pure $ "When unifying " ++ !(pshow env x) ++ " and " ++ !(pshow env y) ++ "\n"
       ++ !(perror err)
--- a/src/TTImp/ProcessDef.idr
+++ b/src/TTImp/ProcessDef.idr
@ -79,7 +79,7 @@ impossibleErrOK defs (CantSolveEq fc env l r)
         impossibleOK defs !(nf defs env l)
                           !(nf defs env r)
 impossibleErrOK defs (BadDotPattern _ _ ErasedArg _ _) = pure True
-impossibleErrOK defs (CyclicMeta _ _) = pure True
+impossibleErrOK defs (CyclicMeta _ _ _ _) = pure True
 impossibleErrOK defs (AllFailed errs)
    = anyM (impossibleErrOK defs) (map snd errs)
 impossibleErrOK defs (WhenUnifying _ _ _ _ err)
--- a/tests/ideMode/ideMode001/expected
+++ b/tests/ideMode/ideMode001/expected
@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:190} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:191}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:190}_[] ?{_:191}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:221} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:222}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:221}_[] ?{_:222}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:223}_[] ?{_:222}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:631:1--638:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:212}_[] ?{_:211}_[])")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:202} : (Main.Vect n[0] a[1])) -> (({arg:203} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:631:1--638:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
--- a/tests/ideMode/ideMode003/expected
+++ b/tests/ideMode/ideMode003/expected
@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:190} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:191}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:190}_[] ?{_:191}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:221} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:222}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:221}_[] ?{_:222}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:223}_[] ?{_:222}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:631:1--638:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:212}_[] ?{_:211}_[])")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:202} : (Main.Vect n[0] a[1])) -> (({arg:203} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:631:1--638:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
--- a/tests/idris2/basic030/expected
+++ b/tests/idris2/basic030/expected
@ -1,7 +1,7 @@
 1/1: Building arity (arity.idr)
 arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1:
-When unifying (1 {arg:169} : Nat) -> MyN and MyN
+When unifying (1 {arg:199} : Nat) -> MyN and MyN
 Mismatch between:
-	(1 {arg:169} : Nat) -> MyN
+	(1 {arg:199} : Nat) -> MyN
 and
 	MyN
--- a/tests/ttimp/basic003/expected
+++ b/tests/ttimp/basic003/expected
@ -1,8 +1,8 @@
 Processing as TTImp
 Written TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:25} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:25}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:25}) m)) a))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
 Yaffle> Bye for now!
 Processing as TTC
 Read TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:25} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:25}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:25}) m)) a))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
 Yaffle> Bye for now!
--- a/tests/ttimp/basic006/expected
+++ b/tests/ttimp/basic006/expected
@ -2,5 +2,5 @@ Processing as TTImp
 Written TTC
 Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
 Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
-Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved117 ?Main.{a:59}_[]), ($resolved98 ?Main.{a:59}_[])]
+Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved119 ?Main.{a:62}_[]), ($resolved99 ?Main.{a:62}_[])]
 Yaffle> Bye for now!
--- a/tests/ttimp/coverage002/expected
+++ b/tests/ttimp/coverage002/expected
@ -2,6 +2,6 @@ Processing as TTImp
 Written TTC
 Yaffle> Main.lookup: All cases covered
 Yaffle> Main.lookup':
-($resolved144 [__] [__] (Main.FZ [__]) {arg:3})
+($resolved146 [__] [__] (Main.FZ [__]) {arg:3})
 Yaffle> Main.lookup'': Calls non covering function Main.lookup'
 Yaffle> Bye for now!
--- a/tests/ttimp/eta001/expected
+++ b/tests/ttimp/eta001/expected
@ -1,5 +1,5 @@
 Processing as TTImp
 Written TTC
-Yaffle> ((Main.Refl [Just {b:9} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
+Yaffle> ((Main.Refl [Just {b:10} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
 Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))
 Yaffle> Bye for now!
--- a/tests/ttimp/eta002/expected
+++ b/tests/ttimp/eta002/expected
@ -1,5 +1,5 @@
 Processing as TTImp
 Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
-Eta.yaff:16:10--17:1:When unifying: ($resolved98 ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved106)) ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved106)) ?Main.{x:18}_[] ?Main.{x:18}_[]) and ($resolved98 ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved106)) (({arg:10} : Integer) -> (({arg:11} : Integer) -> $resolved106)) $resolved107 \x : Char => \y : ?Main.{_:14}_[x[0]] => ($resolved107 ?Main.{_:15}_[x[1], y[0]] ?Main.{_:16}_[x[1], y[0]]))
+Eta.yaff:16:10--17:1:When unifying: ($resolved98 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved107)) ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved107)) ?Main.{x:19}_[] ?Main.{x:19}_[]) and ($resolved98 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved107)) (({arg:11} : Integer) -> (({arg:12} : Integer) -> $resolved107)) $resolved108 \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved108 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
 	Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
 Yaffle> Bye for now!
--- a/tests/ttimp/qtt002/expected
+++ b/tests/ttimp/qtt002/expected
@ -1,6 +1,6 @@
 Processing as TTImp
 Written TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:19} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:19}) a) (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:19})) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:19}))) m)) a))))))))))
-Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:49} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:49}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:49})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:49})) m)) a)))))))))
-Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:80} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:80}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:80})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:80}) a) ((Main.Vect ((Main.plus (Main.S {k:80})) m)) a))))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:21} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:21}) a) (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:21})) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:21}))) m)) a))))))))))
+Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:52} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:52}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:52})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:52})) m)) a)))))))))
+Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:84} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:84}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:84})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:84}) a) ((Main.Vect ((Main.plus (Main.S {k:84})) m)) a))))))))))
 Yaffle> Bye for now!
--- a/tests/ttimp/search001/expected
+++ b/tests/ttimp/search001/expected
@ -1,6 +1,6 @@
 Processing as TTImp
 Written TTC
-Yaffle> (((((Main.There [Just {a:15} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:9} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
-Yaffle> (((Main.Here [Just {a:9} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
+Yaffle> (((((Main.There [Just {a:19} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:11} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
+Yaffle> (((Main.Here [Just {a:11} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
 Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94)
 Yaffle> Bye for now!
--- a/tests/ttimp/search005/expected
+++ b/tests/ttimp/search005/expected
@ -1,8 +1,8 @@
 Processing as TTImp
 Written TTC
 Yaffle> \0 m : Main.Nat => \0 a : Type => \ys : (Main.Vect m[1] a[0]) => \0 n : Main.Nat => ys[1]
-Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:29} : Main.Nat => \x : a[1] => \xs : (Main.Vect {k:29}[1] a[2]) => \ys : (Main.Vect m[4] a[3]) => \0 n : Main.Nat => (Main.Cons (Main.plus {k:29}[4] m[6]) a[5] x[3] (Main.append m[6] a[5] {k:29}[4] xs[2] ys[1]))
-Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:201}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:201}]) z) y))]
-Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:314}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:314}]) z) w))]
-Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:464}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:464}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
+Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:30} : Main.Nat => \x : a[1] => \xs : (Main.Vect {k:30}[1] a[2]) => \ys : (Main.Vect m[4] a[3]) => \0 n : Main.Nat => (Main.Cons (Main.plus {k:30}[4] m[6]) a[5] x[3] (Main.append m[6] a[5] {k:30}[4] xs[2] ys[1]))
+Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:203}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:203}]) z) y))]
+Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:319}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:319}]) z) w))]
+Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:481}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:481}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
 Yaffle> Bye for now!
--- a/tests/ttimp/with001/expected
+++ b/tests/ttimp/with001/expected
@ -3,5 +3,5 @@ Written TTC
 Yaffle> (Main.Odd (Main.S Main.Z))
 Yaffle> (Main.Even (Main.S Main.Z))
 Yaffle> (Main.Nothing [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) (Main.S Main.Z)) (Main.S (Main.S Main.Z))))])
-Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:9} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))]))
+Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:10} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))]))
 Yaffle> Bye for now!