[ refactor ] split Core.TT (#3151)

idris2api.ipkg

@@ -73,6 +73,7 @@ modules =
     Core.Metadata,
     Core.Name,
     Core.Name.Namespace,
+    Core.Name.Scoped,
     Core.Normalise,
     Core.Normalise.Convert,
     Core.Normalise.Eval,
@@ -90,8 +91,14 @@ modules =
     Core.Termination,
     Core.Transform,
     Core.TT,
-    Core.TT.Views,
+    Core.TT.Binder,
+    Core.TT.Primitive,
+    Core.TT.Subst,
+    Core.TT.Term,
+    Core.TT.Term.Subst,
     Core.TT.Traversals,
+    Core.TT.Var,
+    Core.TT.Views,
     Core.TTC,
     Core.Unify,
     Core.UnifyState,
@@ -164,21 +171,28 @@ modules =
 
     Libraries.Data.ANameMap,
     Libraries.Data.DList,
+    Libraries.Data.Erased,
     Libraries.Data.Fin,
     Libraries.Data.Graph,
     Libraries.Data.IMaybe,
     Libraries.Data.IntMap,
     Libraries.Data.IOArray,
     Libraries.Data.IOMatrix,
-    Libraries.Data.LengthMatch,
     Libraries.Data.List.Extra,
-    Libraries.Data.List.Quantifiers.Extra,
+    Libraries.Data.List.HasLength,
     Libraries.Data.List.Lazy,
+    Libraries.Data.List.LengthMatch,
+    Libraries.Data.List.Quantifiers.Extra,
+    Libraries.Data.List.SizeOf,
     Libraries.Data.List1,
     Libraries.Data.NameMap,
     Libraries.Data.NameMap.Traversable,
+    Libraries.Data.Ordering.Extra,
     Libraries.Data.PosMap,
     Libraries.Data.Primitives,
+    Libraries.Data.SnocList.HasLength,
+    Libraries.Data.SnocList.LengthMatch,
+    Libraries.Data.SnocList.SizeOf,
     Libraries.Data.Span,
     Libraries.Data.SortedMap,
     Libraries.Data.SortedSet,

libs/base/System/Concurrency.idr

@@ -215,4 +215,3 @@ channelGet chan = primIO (prim__channelGet chan)
 export
 channelPut : HasIO io => (chan : Channel a) -> (val : a) -> io ()
 channelPut chan val = primIO (prim__channelPut chan val)
-

src/Compiler/CaseOpts.idr

@@ -37,15 +37,14 @@ shiftUnder : {args : _} ->
 shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
 shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
 
-shiftVar : {outer, args : _} ->
+shiftVar : {outer, args : Scope} ->
-           {idx : _} ->
+           NVar n (outer ++ (x :: args ++ vars)) ->
-           (0 p : IsVar n idx (outer ++ (x :: args ++ vars))) ->
            NVar n (outer ++ (args ++ x :: vars))
-shiftVar {outer = []} p = shiftUnder p
+shiftVar nvar
-shiftVar {outer = (n::xs)} First = MkNVar First
+  = let out = mkSizeOf outer in
-shiftVar {outer = (y::xs)} (Later p)
+    case locateNVar out nvar of
-    = case shiftVar p of
+      Left nvar => embed nvar
-           MkNVar p' => MkNVar (Later p')
+      Right (MkNVar p) => weakenNs out (shiftUnder p)
 
 mutual
   shiftBinder : {outer, args : _} ->
@@ -53,7 +52,7 @@ mutual
                 CExp (outer ++ old :: (args ++ vars)) ->
                 CExp (outer ++ (args ++ new :: vars))
   shiftBinder new (CLocal fc p)
-      = case shiftVar p of
+      = case shiftVar (MkNVar p) of
              MkNVar p' => CLocal fc (renameVar p')
     where
       renameVar : IsVar x i (outer ++ (args ++ (old :: rest))) ->

src/Compiler/CompileExpr.idr

@@ -39,14 +39,14 @@ numArgs defs (Ref _ _ n)
            _ => pure (Arity 0)
 numArgs _ tm = pure (Arity 0)
 
-mkSub : Nat -> (ns : List Name) -> List Nat -> (ns' ** SubVars ns' ns)
+mkSub : Nat -> (ns : List Name) -> List Nat -> (ns' ** Thin ns' ns)
-mkSub i _ [] = (_ ** SubRefl)
+mkSub i _ [] = (_ ** Refl)
-mkSub i [] ns = (_ ** SubRefl)
+mkSub i [] ns = (_ ** Refl)
 mkSub i (x :: xs) es
     = let (ns' ** p) = mkSub (S i) xs es in
           if i `elem` es
-             then (ns' ** DropCons p)
+             then (ns' ** Drop p)
-             else (x :: ns' ** KeepCons p)
+             else (x :: ns' ** Keep p)
 
 weakenVar : Var ns -> Var (a :: ns)
 weakenVar (MkVar p) = (MkVar (Later p))
@@ -134,13 +134,13 @@ eraseConArgs arity epos fn args
 mkDropSubst : Nat -> List Nat ->
               (rest : List Name) ->
               (vars : List Name) ->
-              (vars' ** SubVars (vars' ++ rest) (vars ++ rest))
+              (vars' ** Thin (vars' ++ rest) (vars ++ rest))
-mkDropSubst i es rest [] = ([] ** SubRefl)
+mkDropSubst i es rest [] = ([] ** Refl)
 mkDropSubst i es rest (x :: xs)
     = let (vs ** sub) = mkDropSubst (1 + i) es rest xs in
           if i `elem` es
-             then (vs ** DropCons sub)
+             then (vs ** Drop sub)
-             else (x :: vs ** KeepCons sub)
+             else (x :: vs ** Keep sub)
 
 -- Rewrite applications of Nat-like constructors and functions to more optimal
 -- versions using Integer
@@ -338,7 +338,7 @@ toCExpTm n (Bind fc x (Lam _ _ _ _) sc)
     = pure $ CLam fc x !(toCExp n sc)
 toCExpTm n (Bind fc x (Let _ rig val _) sc)
     = do sc' <- toCExp n sc
-         pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
+         pure $ branchZero (shrinkCExp (Drop Refl) sc')
                         (CLet fc x YesInline !(toCExp n val) sc')
                         rig
 toCExpTm n (Bind fc x (Pi _ c e ty) sc)
@@ -454,31 +454,32 @@ mutual
                      if noworld -- just substitute the scrutinee into
                                 -- the RHS
                         then
-                             let env : SubstCEnv args vars
+                             let (s, env) : (SizeOf args, SubstCEnv args vars)
                                      = mkSubst 0 scr pos args in
                               do log "compiler.newtype.world" 50 "Inlining case on \{show n} (no world)"
-                                 pure $ Just (substs env !(toCExpTree n sc))
+                                 pure $ Just (substs s env !(toCExpTree n sc))
                         else -- let bind the scrutinee, and substitute the
                              -- name into the RHS
-                             let env : SubstCEnv args (MN "eff" 0 :: vars)
+                             let (s, env) : (_, SubstCEnv args (MN "eff" 0 :: vars))
                                      = mkSubst 0 (CLocal fc First) pos args in
                              do sc' <- toCExpTree n sc
                                 let scope = insertNames {outer=args}
                                                         {inner=vars}
                                                         {ns = [MN "eff" 0]}
                                                         (mkSizeOf _) (mkSizeOf _) sc'
-                                let tm = CLet fc (MN "eff" 0) NotInline scr (substs env scope)
+                                let tm = CLet fc (MN "eff" 0) NotInline scr (substs s env scope)
                                 log "compiler.newtype.world" 50 "Kept the scrutinee \{show tm}"
                                 pure (Just tm)
                 _ => pure Nothing -- there's a normal match to do
     where
       mkSubst : Nat -> CExp vs ->
-                Nat -> (args : List Name) -> SubstCEnv args vs
+                Nat -> (args : List Name) -> (SizeOf args, SubstCEnv args vs)
-      mkSubst _ _ _ [] = Nil
+      mkSubst _ _ _ [] = (zero, [])
       mkSubst i scr pos (a :: as)
-          = if i == pos
+          = let (s, env) = mkSubst (1 + i) scr pos as in
-               then scr :: mkSubst (1 + i) scr pos as
+            if i == pos
-               else CErased fc :: mkSubst (1 + i) scr pos as
+               then (suc s, scr :: env)
+               else (suc s, CErased fc :: env)
   getNewType fc scr n (_ :: ns) = getNewType fc scr n ns
 
   getDef : {vars : _} ->
@@ -678,10 +679,11 @@ getCFTypes args (NBind fc _ (Pi _ _ _ ty) sc)
 getCFTypes args t
     = pure (reverse args, !(nfToCFType (getLoc t) False t))
 
-lamRHSenv : Int -> FC -> (ns : List Name) -> SubstCEnv ns []
+lamRHSenv : Int -> FC -> (ns : List Name) -> (SizeOf ns, SubstCEnv ns [])
-lamRHSenv i fc [] = []
+lamRHSenv i fc [] = (zero, [])
 lamRHSenv i fc (n :: ns)
-    = CRef fc (MN "x" i) :: lamRHSenv (i + 1) fc ns
+    = let (s, env) = lamRHSenv (i + 1) fc ns in
+      (suc s, CRef fc (MN "x" i) :: env)
 
 mkBounds : (xs : _) -> Bounds xs
 mkBounds [] = None
@@ -699,8 +701,8 @@ getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
 -- function, they had arity 0.
 lamRHS : (ns : List Name) -> CExp ns -> CExp []
 lamRHS ns tm
-    = let env = lamRHSenv 0 (getFC tm) ns
+    = let (s, env) = lamRHSenv 0 (getFC tm) ns
-          tmExp = substs env (rewrite appendNilRightNeutral ns in tm)
+          tmExp = substs s env (rewrite appendNilRightNeutral ns in tm)
           newArgs = reverse $ getNewArgs env
           bounds = mkBounds newArgs
           expLocs = mkLocals zero {vars = []} bounds tmExp in

src/Compiler/Inline.idr

@@ -17,7 +17,7 @@ import Core.TT
 import Data.Maybe
 import Data.List
 import Data.Vect
-import Libraries.Data.LengthMatch
+import Libraries.Data.List.LengthMatch
 import Libraries.Data.NameMap
 import Libraries.Data.WithDefault
 
@@ -139,7 +139,7 @@ mutual
                | Nothing => pure Nothing
            res <- eval rec env' stk'
                      (rewrite sym (appendAssociative args vars free) in
-                              embed {vars = vars ++ free} exp)
+                              embed {outer = vars ++ free} exp)
            pure (Just res)
   tryApply rec stk env _ = pure Nothing
 
@@ -414,12 +414,12 @@ fixArity (MkError exp) = pure $ MkError !(fixArityTm exp [])
 fixArity d = pure d
 
 -- TODO: get rid of this `done` by making the return `args'` runtime irrelevant?
-getLams : {done : _} ->
+getLams : {done : _} -> SizeOf done ->
           Int -> SubstCEnv done args -> CExp (done ++ args) ->
-          (args' ** (SubstCEnv args' args, CExp (args' ++ args)))
+          (args' ** (SizeOf args', SubstCEnv args' args, CExp (args' ++ args)))
-getLams {done} i env (CLam fc x sc)
+getLams {done} d i env (CLam fc x sc)
-    = getLams {done = x :: done} (i + 1) (CRef fc (MN "ext" i) :: env) sc
+    = getLams {done = x :: done} (suc d) (i + 1) (CRef fc (MN "ext" i) :: env) sc
-getLams {done} i env sc = (done ** (env, sc))
+getLams {done} d i env sc = (done ** (d, env, sc))
 
 mkBounds : (xs : _) -> Bounds xs
 mkBounds [] = None
@@ -437,8 +437,8 @@ getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
 -- not the highest, as you'd expect if they were all lambdas).
 mergeLambdas : (args : List Name) -> CExp args -> (args' ** CExp args')
 mergeLambdas args (CLam fc x sc)
-    = let (args' ** (env, exp')) = getLams 0 [] (CLam fc x sc)
+    = let (args' ** (s, env, exp')) = getLams zero 0 [] (CLam fc x sc)
-          expNs = substs env exp'
+          expNs = substs s env exp'
           newArgs = reverse $ getNewArgs env
           expLocs = mkLocals (mkSizeOf args) {vars = []} (mkBounds newArgs)
                              (rewrite appendNilRightNeutral args in expNs) in

src/Compiler/LambdaLift.idr

@@ -31,7 +31,7 @@ mutual
   ||| @ vars is the list of names accessible within the current scope of the
   |||   lambda-lifted code.
   public export
-  data Lifted : (vars : List Name) -> Type where
+  data Lifted : Scoped where
 
        ||| A local variable in the lambda-lifted syntax tree.
        |||
@@ -424,6 +424,7 @@ mutual
            update Lifts { defs $= ((n, MkLFun (dropped vars unused) bound scl') ::) }
            pure $ LUnderApp fc n (length bound) (allVars fc vars unused)
     where
+
         allPrfs : (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Var vs)
         allPrfs [] _ = []
         allPrfs (v :: vs) (False::uvs) = MkVar First :: map weaken (allPrfs vs uvs)

src/Compiler/Opts/ConstantFold.idr

@@ -50,7 +50,8 @@ record WkCExp (vars : List Name) where
   expr : CExp supp
 
 Weaken WkCExp where
-  weaken (MkWkCExp s Refl e) = MkWkCExp (suc s) Refl e
+  weakenNs s' (MkWkCExp {outer, supp} s Refl e)
+    = MkWkCExp (s' + s) (appendAssociative ns outer supp)  e
 
 lookup : FC -> Var ds -> Subst ds vars -> CExp vars
 lookup fc (MkVar p) rho = case go p rho of

src/Compiler/Opts/Identity.idr

@@ -17,8 +17,8 @@ parameters (fn1 : Name) (idIdx : Nat)
   mutual
     -- special case for matching on 'Nat'-shaped things
     isUnsucc : Var vars -> CExp vars -> Maybe (Constant, Var (x :: vars))
-    isUnsucc (MkVar {i} _) (COp _ (Sub _) [CLocal {idx} _ _, CPrimVal _ c]) =
+    isUnsucc var (COp _ (Sub _) [CLocal _ p, CPrimVal _ c]) =
-        if i == idx
+        if var == MkVar p
             then Just (c, MkVar First)
             else Nothing
     isUnsucc _ _ = Nothing
@@ -29,7 +29,7 @@ parameters (fn1 : Name) (idIdx : Nat)
 
     -- does the CExp evaluate to the var, the constructor or the constant?
     cexpIdentity : Var vars -> Maybe (Name, List (Var vars)) -> Maybe Constant -> CExp vars -> Bool
-    cexpIdentity (MkVar {i} _) _ _ (CLocal {idx} fc p) = idx == i
+    cexpIdentity var _ _ (CLocal fc p) = var == MkVar p
     cexpIdentity var _ _ (CRef _ _) = False
     cexpIdentity var _ _ (CLam _ _ _) = False
     cexpIdentity var con const (CLet _ _ NotInline val sc) = False

src/Core/AutoSearch.idr

@@ -186,7 +186,7 @@ getUsableEnv fc rigc p [] = []
 getUsableEnv {vars = v :: vs} {done} fc rigc p (b :: env)
    = let rest = getUsableEnv fc rigc (sucR p) env in
          if (multiplicity b == top || isErased rigc)
-            then let MkVar var = weakenVar p (MkVar First) in
+            then let 0 var = mkIsVar (hasLength p) in
                      (Local (binderLoc b) Nothing _ var,
                        rewrite appendAssociative done [v] vs in
                           weakenNs (sucR p) (binderType b)) ::

src/Core/Case/CaseBuilder.idr

@@ -16,7 +16,7 @@ import Idris.Pretty.Annotations
 import Data.List
 import Data.String
 import Data.Vect
-import Libraries.Data.LengthMatch
+import Libraries.Data.List.LengthMatch
 import Libraries.Data.SortedSet
 
 import Decidable.Equality
@@ -176,7 +176,7 @@ getPat (Later p) (x :: xs) = getPat p xs
 
 dropPat : {idx : Nat} ->
           (0 el : IsVar nm idx ps) ->
-          NamedPats ns ps -> NamedPats ns (dropVar ps el)
+          NamedPats ns ps -> NamedPats ns (dropIsVar ps el)
 dropPat First (x :: xs) = xs
 dropPat (Later p) (x :: xs) = x :: dropPat p xs
 
@@ -218,7 +218,7 @@ Weaken ArgType where
   weakenNs s Unknown = Unknown
 
 Weaken (PatInfo p) where
-  weaken (MkInfo p el fty) = MkInfo p (Later el) (weaken fty)
+  weakenNs s (MkInfo p el fty) = MkInfo p (weakenIsVar s el) (weakenNs s fty)
 
 -- FIXME: perhaps 'vars' should be second argument so we can use Weaken interface
 weaken : {x, vars : _} ->
@@ -941,11 +941,11 @@ pickNextViable {ps = q :: qs} fc phase fn npss
                             pure (_ ** MkNVar (Later var))
 
 moveFirst : {idx : Nat} -> (0 el : IsVar nm idx ps) -> NamedPats ns ps ->
-            NamedPats ns (nm :: dropVar ps el)
+            NamedPats ns (nm :: dropIsVar ps el)
 moveFirst el nps = getPat el nps :: dropPat el nps
 
 shuffleVars : {idx : Nat} -> (0 el : IsVar nm idx todo) -> PatClause vars todo ->
-              PatClause vars (nm :: dropVar todo el)
+              PatClause vars (nm :: dropIsVar todo el)
 shuffleVars First orig@(MkPatClause pvars lhs pid rhs) = orig -- no-op
 shuffleVars el (MkPatClause pvars lhs pid rhs)
     = MkPatClause pvars (moveFirst el lhs) pid rhs
@@ -1165,11 +1165,11 @@ mkPatClause fc fn args ty pid (ps, rhs)
                      Nothing => pure (Nothing, CaseBuilder.Unknown)
                      Just (NBind pfc _ (Pi _ c _ farg) fsc) =>
                         pure (Just !(fsc defs (toClosure defaultOpts [] (Ref pfc Bound arg))),
-                                Known c (embed {more = arg :: args}
+                                Known c (embed {outer = arg :: args}
                                           !(quote empty [] farg)))
                      Just t =>
                         pure (Nothing,
-                                Stuck (embed {more = arg :: args}
+                                Stuck (embed {outer = arg :: args}
                                         !(quote empty [] t)))
              pure (MkInfo p First (Builtin.snd fa_tys)
                       :: weaken !(mkNames args ps eq (Builtin.fst fa_tys)))
@@ -1197,7 +1197,7 @@ patCompile fc fn phase ty (p :: ps) def
          i <- newRef PName (the Int 0)
          cases <- match fc fn phase pats
                         (rewrite sym (appendNilRightNeutral ns) in
-                                 map (TT.weakenNs n) def)
+                                 map (weakenNs n) def)
          pure (_ ** cases)
   where
     mkPatClausesFrom : Int -> (args : List Name) ->
@@ -1375,17 +1375,6 @@ getPMDef fc phase fn ty clauses
     labelPat i [] = []
     labelPat i (x :: xs) = ("pat" ++ show i ++ ":", x) :: labelPat (i + 1) xs
 
-    mkSubstEnv : Int -> String -> Env Term vars -> SubstEnv vars []
-    mkSubstEnv i pname [] = Nil
-    mkSubstEnv i pname (v :: vs)
-       = Ref fc Bound (MN pname i) :: mkSubstEnv (i + 1) pname vs
-
-    close : {vars : _} ->
-            Env Term vars -> String -> Term vars -> ClosedTerm
-    close {vars} env pname tm
-        = substs (mkSubstEnv 0 pname env)
-              (rewrite appendNilRightNeutral vars in tm)
-
     toClosed : Defs -> (String, Clause) -> (ClosedTerm, ClosedTerm)
     toClosed defs (pname, MkClause env lhs rhs)
-          = (close env pname lhs, close env pname rhs)
+          = (close fc pname env lhs, close fc pname env rhs)

src/Core/CompileExpr.idr

@@ -9,6 +9,8 @@ import Core.TT
 import Data.List
 import Data.Vect
 
+import Libraries.Data.SnocList.SizeOf
+
 %default covering
 
 -- Backends might be able to treat some 'shapes' of data type specially,
@@ -472,56 +474,24 @@ mutual
                         CConstAlt (outer ++ (ns ++ inner))
   insertNamesConstAlt outer ns (MkConstAlt x sc) = MkConstAlt x (insertNames outer ns sc)
 
-mutual
+export
-  export
+FreelyEmbeddable CExp where
-  embed : CExp args -> CExp (args ++ vars)
-  embed cexp = believe_me cexp
-  -- It is identity at run time, but it would be implemented as below
-  -- (not sure theere's much performance benefit, mind...)
-  {-
-  embed (CLocal fc prf) = CLocal fc (varExtend prf)
-  embed (CRef fc n) = CRef fc n
-  embed (CLam fc x sc) = CLam fc x (embed sc)
-  embed (CLet fc x inl val sc) = CLet fc x inl (embed val) (embed sc)
-  embed (CApp fc f args) = CApp fc (embed f) (assert_total (map embed args))
-  embed (CCon fc n t args) = CCon fc n t (assert_total (map embed args))
-  embed (COp fc p args) = COp fc p (assert_total (map embed args))
-  embed (CExtPrim fc p args) = CExtPrim fc p (assert_total (map embed args))
-  embed (CForce fc e) = CForce fc (embed e)
-  embed (CDelay fc e) = CDelay fc (embed e)
-  embed (CConCase fc sc alts def)
-      = CConCase fc (embed sc) (assert_total (map embedAlt alts))
-                 (assert_total (map embed def))
-  embed (CConstCase fc sc alts def)
-      = CConstCase fc (embed sc) (assert_total (map embedConstAlt alts))
-                   (assert_total (map embed def))
-  embed (CPrimVal fc c) = CPrimVal fc c
-  embed (CErased fc) = CErased fc
-  embed (CCrash fc msg) = CCrash fc msg
-
-  embedAlt : CConAlt args -> CConAlt (args ++ vars)
-  embedAlt {args} {vars} (MkConAlt n t as sc)
-     = MkConAlt n t as (rewrite appendAssociative as args vars in embed sc)
-
-  embedConstAlt : CConstAlt args -> CConstAlt (args ++ vars)
-  embedConstAlt (MkConstAlt c sc) = MkConstAlt c (embed sc)
-  -}
 
 mutual
   -- Shrink the scope of a compiled expression, replacing any variables not
   -- in the remaining set with Erased
   export
-  shrinkCExp : SubVars newvars vars -> CExp vars -> CExp newvars
+  shrinkCExp : Thin newvars vars -> CExp vars -> CExp newvars
   shrinkCExp sub (CLocal fc prf)
-      = case subElem prf sub of
+      = case shrinkIsVar prf sub of
              Nothing => CErased fc
              Just (MkVar prf') => CLocal fc prf'
   shrinkCExp _ (CRef fc x) = CRef fc x
   shrinkCExp sub (CLam fc x sc)
-      = let sc' = shrinkCExp (KeepCons sub) sc in
+      = let sc' = shrinkCExp (Keep sub) sc in
             CLam fc x sc'
   shrinkCExp sub (CLet fc x inl val sc)
-      = let sc' = shrinkCExp (KeepCons sub) sc in
+      = let sc' = shrinkCExp (Keep sub) sc in
             CLet fc x inl (shrinkCExp sub val) sc'
   shrinkCExp sub (CApp fc x xs)
       = CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))
@@ -545,11 +515,11 @@ mutual
   shrinkCExp _ (CErased fc) = CErased fc
   shrinkCExp _ (CCrash fc x) = CCrash fc x
 
-  shrinkConAlt : SubVars newvars vars -> CConAlt vars -> CConAlt newvars
+  shrinkConAlt : Thin newvars vars -> CConAlt vars -> CConAlt newvars
   shrinkConAlt sub (MkConAlt x ci tag args sc)
-        = MkConAlt x ci tag args (shrinkCExp (subExtend args sub) sc)
+        = MkConAlt x ci tag args (shrinkCExp (keeps args sub) sc)
 
-  shrinkConstAlt : SubVars newvars vars -> CConstAlt vars -> CConstAlt newvars
+  shrinkConstAlt : Thin newvars vars -> CConstAlt vars -> CConstAlt newvars
   shrinkConstAlt sub (MkConstAlt x sc) = MkConstAlt x (shrinkCExp sub sc)
 
 export
@@ -560,103 +530,59 @@ export
 Weaken CConAlt where
   weakenNs ns tm = insertNamesConAlt zero ns tm
 
--- Substitute some explicit terms for names in a term, and remove those
+public export
--- names from the scope
+SubstCEnv : Scope -> Scoped
-namespace SubstCEnv
+SubstCEnv = Subst CExp
-  public export
-  data SubstCEnv : List Name -> List Name -> Type where
-       Nil : SubstCEnv [] vars
-       (::) : CExp vars ->
-              SubstCEnv ds vars -> SubstCEnv (d :: ds) vars
-
-findDrop : FC -> Var (dropped ++ vars) ->
-           SubstCEnv dropped vars -> CExp vars
-findDrop fc (MkVar p) [] = CLocal fc p
-findDrop fc (MkVar First) (tm :: env) = tm
-findDrop fc (MkVar (Later p)) (tm :: env) = findDrop fc (MkVar p) env
-
-find : FC ->
-       SizeOf outer ->
-       Var (outer ++ (dropped ++ vars)) ->
-       SubstCEnv dropped vars ->
-       CExp (outer ++ vars)
-find fc outer var env = case sizedView outer of
-  Z       => findDrop fc var env
-  S outer => case var of
-    MkVar First     => CLocal fc First
-    MkVar (Later p) => weaken (find fc outer (MkVar p) env)
-    -- TODO: refactor to weaken only once?
 
 mutual
-  substEnv : SizeOf outer ->
+  substEnv : Substitutable CExp CExp
-             SubstCEnv dropped vars ->
+  substEnv outer dropped env (CLocal fc prf)
-             CExp (outer ++ (dropped ++ vars)) ->
+      = find (\ (MkVar p) => CLocal fc p) outer dropped (MkVar prf) env
-             CExp (outer ++ vars)
+  substEnv _ _ _ (CRef fc x) = CRef fc x
-  substEnv outer env (CLocal fc prf)
+  substEnv outer dropped env (CLam fc x sc)
-      = find fc outer (MkVar prf) env
+      = let sc' = substEnv (suc outer) dropped env sc in
-  substEnv _ _ (CRef fc x) = CRef fc x
-  substEnv outer env (CLam fc x sc)
-      = let sc' = substEnv (suc outer) env sc in
             CLam fc x sc'
-  substEnv outer env (CLet fc x inl val sc)
+  substEnv outer dropped env (CLet fc x inl val sc)
-      = let sc' = substEnv (suc outer) env sc in
+      = let sc' = substEnv (suc outer) dropped env sc in
-            CLet fc x inl (substEnv outer env val) sc'
+            CLet fc x inl (substEnv outer dropped env val) sc'
-  substEnv outer env (CApp fc x xs)
+  substEnv outer dropped env (CApp fc x xs)
-      = CApp fc (substEnv outer env x) (assert_total (map (substEnv outer env) xs))
+      = CApp fc (substEnv outer dropped env x) (assert_total (map (substEnv outer dropped env) xs))
-  substEnv outer env (CCon fc x ci tag xs)
+  substEnv outer dropped env (CCon fc x ci tag xs)
-      = CCon fc x ci tag (assert_total (map (substEnv outer env) xs))
+      = CCon fc x ci tag (assert_total (map (substEnv outer dropped env) xs))
-  substEnv outer env (COp fc x xs)
+  substEnv outer dropped env (COp fc x xs)
-      = COp fc x (assert_total (map (substEnv outer env) xs))
+      = COp fc x (assert_total (map (substEnv outer dropped env) xs))
-  substEnv outer env (CExtPrim fc p xs)
+  substEnv outer dropped env (CExtPrim fc p xs)
-      = CExtPrim fc p (assert_total (map (substEnv outer env) xs))
+      = CExtPrim fc p (assert_total (map (substEnv outer dropped env) xs))
-  substEnv outer env (CForce fc lr x) = CForce fc lr (substEnv outer env x)
+  substEnv outer dropped env (CForce fc lr x) = CForce fc lr (substEnv outer dropped env x)
-  substEnv outer env (CDelay fc lr x) = CDelay fc lr (substEnv outer env x)
+  substEnv outer dropped env (CDelay fc lr x) = CDelay fc lr (substEnv outer dropped env x)
-  substEnv outer env (CConCase fc sc xs def)
+  substEnv outer dropped env (CConCase fc sc xs def)
-      = CConCase fc (substEnv outer env sc)
+      = CConCase fc (substEnv outer dropped env sc)
-                 (assert_total (map (substConAlt outer env) xs))
+                 (assert_total (map (substConAlt outer dropped env) xs))
-                 (assert_total (map (substEnv outer env) def))
+                 (assert_total (map (substEnv outer dropped env) def))
-  substEnv outer env (CConstCase fc sc xs def)
+  substEnv outer dropped env (CConstCase fc sc xs def)
-      = CConstCase fc (substEnv outer env sc)
+      = CConstCase fc (substEnv outer dropped env sc)
-                   (assert_total (map (substConstAlt outer env) xs))
+                   (assert_total (map (substConstAlt outer dropped env) xs))
-                   (assert_total (map (substEnv outer env) def))
+                   (assert_total (map (substEnv outer dropped env) def))
-  substEnv _ _ (CPrimVal fc x) = CPrimVal fc x
+  substEnv _ _ _ (CPrimVal fc x) = CPrimVal fc x
-  substEnv _ _ (CErased fc) = CErased fc
+  substEnv _ _ _ (CErased fc) = CErased fc
-  substEnv _ _ (CCrash fc x) = CCrash fc x
+  substEnv _ _ _ (CCrash fc x) = CCrash fc x
 
-  substConAlt : SizeOf outer ->
+  substConAlt : Substitutable CExp CConAlt
-                SubstCEnv dropped vars ->
+  substConAlt {vars} {outer} {dropped} p q env (MkConAlt x ci tag args sc)
-                CConAlt (outer ++ (dropped ++ vars)) ->
-                CConAlt (outer ++ vars)
-  substConAlt {vars} {outer} {dropped} p env (MkConAlt x ci tag args sc)
       = MkConAlt x ci tag args
            (rewrite appendAssociative args outer vars in
-                    substEnv (mkSizeOf args + p) env
+                    substEnv (mkSizeOf args + p) q env
                       (rewrite sym (appendAssociative args outer (dropped ++ vars)) in
                                sc))
 
-  substConstAlt : SizeOf outer ->
+  substConstAlt : Substitutable CExp CConstAlt
-                  SubstCEnv dropped vars ->
+  substConstAlt outer dropped env (MkConstAlt x sc) = MkConstAlt x (substEnv outer dropped env sc)
-                  CConstAlt (outer ++ (dropped ++ vars)) ->
-                  CConstAlt (outer ++ vars)
-  substConstAlt outer env (MkConstAlt x sc) = MkConstAlt x (substEnv outer env sc)
 
 export
 substs : {dropped, vars : _} ->
+         SizeOf dropped ->
          SubstCEnv dropped vars -> CExp (dropped ++ vars) -> CExp vars
-substs env tm = substEnv zero env tm
+substs = substEnv zero
-
-resolveRef : SizeOf outer ->
-             SizeOf done ->
-             Bounds bound -> FC -> Name ->
-             Maybe (CExp (outer ++ (done ++ bound ++ vars)))
-resolveRef _ _ None _ _ = Nothing
-resolveRef {outer} {vars} {done} p q (Add {xs} new old bs) fc n
-    = if n == old
-         then rewrite appendAssociative outer done (new :: xs ++ vars) in
-              let MkNVar p = weakenNVar (p + q) (MkNVar First) in
-                    Just (CLocal fc p)
-         else rewrite appendAssociative done [new] (xs ++ vars)
-                in resolveRef p (sucR q) bs fc n
 
 mutual
   export
@@ -667,7 +593,9 @@ mutual
   mkLocals later bs (CLocal {idx} {x} fc p)
       = let MkNVar p' = addVars later bs (MkNVar p) in CLocal {x} fc p'
   mkLocals later bs (CRef fc var)
-      = maybe (CRef fc var) id (resolveRef later zero bs fc var)
+      = fromMaybe (CRef fc var) $ do
+          MkVar p <- resolveRef later [<] bs fc var
+          pure (CLocal fc p)
   mkLocals later bs (CLam fc x sc)
       = let sc' = mkLocals (suc later) bs sc in
             CLam fc x sc'

src/Core/CompileExpr/Pretty.idr

@@ -23,18 +23,13 @@ import Libraries.Data.String.Extra
 
 %hide Core.Name.prettyOp
 
-%hide Core.TT.Bound
-%hide Core.TT.App
-
 %hide CompileExpr.(::)
 %hide CompileExpr.Nil
 %hide String.(::)
 %hide String.Nil
 %hide Doc.Nil
-%hide SubstEnv.(::)
+%hide Subst.(::)
-%hide SubstEnv.Nil
+%hide Subst.Nil
-%hide SubstCEnv.(::)
-%hide SubstCEnv.Nil
 %hide CList.(::)
 %hide CList.Nil
 %hide Stream.(::)

src/Core/Context/Data.idr

@@ -53,11 +53,7 @@ getPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
         Core (Maybe (List (Maybe (Term vars))))
 getPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
       = do scPs <- getPs (map (map (map weaken)) acc) tyn sc
-           pure $ map (map shrink) scPs
+           pure $ map (map (>>= \ tm => shrink tm (Drop Refl))) scPs
-  where
-    shrink : Maybe (Term (x :: vars)) -> Maybe (Term vars)
-    shrink Nothing = Nothing
-    shrink (Just tm) = shrinkTerm tm (DropCons SubRefl)
 getPs acc tyn tm
     = case getFnArgs tm of
            (Ref _ _ n, args) =>

src/Core/Context/Pretty.idr

@@ -20,8 +20,8 @@ import Libraries.Data.String.Extra
 %hide String.(::)
 %hide String.Nil
 %hide Doc.Nil
-%hide SubstEnv.(::)
+%hide Subst.(::)
-%hide SubstEnv.Nil
+%hide Subst.Nil
 %hide CList.(::)
 %hide CList.Nil
 %hide Stream.(::)

src/Core/Coverage.idr

@@ -200,9 +200,9 @@ showK : {ns : _} ->
         Show a => KnownVars ns a -> String
 showK {a} xs = show (map aString xs)
   where
-    aString : {vars : _} ->
+    aString : {vars : Scope} ->
               (Var vars, a) -> (Name, a)
-    aString (MkVar v, t) = (getName v, t)
+    aString (MkVar v, t) = (nameAt v, t)
 
 weakenNs : SizeOf args -> KnownVars vars a -> KnownVars (args ++ vars) a
 weakenNs args [] = []
@@ -213,7 +213,7 @@ findTag : {idx, vars : _} ->
           (0 p : IsVar n idx vars) -> KnownVars vars a -> Maybe a
 findTag v [] = Nothing
 findTag v ((v', t) :: xs)
-    = if sameVar (MkVar v) v'
+    = if MkVar v == v'
          then Just t
          else findTag v xs
 
@@ -222,7 +222,7 @@ addNot : {idx, vars : _} ->
          KnownVars vars (List Int)
 addNot v t [] = [(MkVar v, [t])]
 addNot v t ((v', ts) :: xs)
-    = if sameVar (MkVar v) v'
+    = if MkVar v == v'
          then ((v', t :: ts) :: xs)
          else ((v', ts) :: addNot v t xs)
 
@@ -436,20 +436,8 @@ clauseMatches : {vars : _} ->
                 Env Term vars -> Term vars ->
                 ClosedTerm -> Core Bool
 clauseMatches env tm trylhs
-    = let lhs = !(eraseApps (close (getLoc tm) env tm)) in
+    = let lhs = !(eraseApps (close (getLoc tm) "cov" env tm)) in
           pure $ match !(toResolvedNames lhs) !(toResolvedNames trylhs)
-  where
-    mkSubstEnv : {vars : _} ->
-                 FC -> Int -> Env Term vars -> SubstEnv vars []
-    mkSubstEnv fc i [] = Nil
-    mkSubstEnv fc i (v :: vs)
-       = Ref fc Bound (MN "cov" i) :: mkSubstEnv fc (i + 1) vs
-
-    close : {vars : _} ->
-            FC -> Env Term vars -> Term vars -> ClosedTerm
-    close {vars} fc env tm
-        = substs (mkSubstEnv fc 0 env)
-              (rewrite appendNilRightNeutral vars in tm)
 
 export
 checkMatched : {auto c : Ref Ctxt Defs} ->

src/Core/Env.idr

@@ -227,21 +227,21 @@ isUsed n (v :: vs) = n == varIdx v || isUsed n vs
 
 mkShrinkSub : {n : _} ->
               (vars : _) -> List (Var (n :: vars)) ->
-              (newvars ** SubVars newvars (n :: vars))
+              (newvars ** Thin newvars (n :: vars))
 mkShrinkSub [] els
     = if isUsed 0 els
-         then (_ ** KeepCons SubRefl)
+         then (_ ** Keep Refl)
-         else (_ ** DropCons SubRefl)
+         else (_ ** Drop Refl)
 mkShrinkSub (x :: xs) els
     = let (_ ** subRest) = mkShrinkSub xs (dropFirst els) in
       if isUsed 0 els
-        then (_ ** KeepCons subRest)
+        then (_ ** Keep subRest)
-        else (_ ** DropCons subRest)
+        else (_ ** Drop subRest)
 
 mkShrink : {vars : _} ->
            List (Var vars) ->
-           (newvars ** SubVars newvars vars)
+           (newvars ** Thin newvars vars)
-mkShrink {vars = []} xs = (_ ** SubRefl)
+mkShrink {vars = []} xs = (_ ** Refl)
 mkShrink {vars = v :: vs} xs = mkShrinkSub _ xs
 
 -- Find the smallest subset of the environment which is needed to type check
@@ -249,14 +249,14 @@ mkShrink {vars = v :: vs} xs = mkShrinkSub _ xs
 export
 findSubEnv : {vars : _} ->
              Env Term vars -> Term vars ->
-             (vars' : List Name ** SubVars vars' vars)
+             (vars' : List Name ** Thin vars' vars)
 findSubEnv env tm = mkShrink (findUsedLocs env tm)
 
 export
-shrinkEnv : Env Term vars -> SubVars newvars vars -> Maybe (Env Term newvars)
+shrinkEnv : Env Term vars -> Thin newvars vars -> Maybe (Env Term newvars)
-shrinkEnv env SubRefl = Just env
+shrinkEnv env Refl = Just env
-shrinkEnv (b :: env) (DropCons p) = shrinkEnv env p
+shrinkEnv (b :: env) (Drop p) = shrinkEnv env p
-shrinkEnv (b :: env) (KeepCons p)
+shrinkEnv (b :: env) (Keep p)
     = do env' <- shrinkEnv env p
          b' <- assert_total (shrinkBinder b p)
          pure (b' :: env')
@@ -304,16 +304,16 @@ uniqifyEnv env = uenv [] env
     uenv : {vars : _} ->
            List Name -> Env Term vars ->
            (vars' ** (Env Term vars', CompatibleVars vars vars'))
-    uenv used [] = ([] ** ([], CompatPre))
+    uenv used [] = ([] ** ([], Pre))
     uenv used {vars = v :: vs} (b :: bs)
         = if v `elem` used
              then let v' = uniqueLocal used v
                       (vs' ** (env', compat)) = uenv (v' :: used) bs
-                      b' = map (renameVars compat) b in
+                      b' = map (compatNs compat) b in
-                  (v' :: vs' ** (b' :: env', CompatExt compat))
+                  (v' :: vs' ** (b' :: env', Ext compat))
              else let (vs' ** (env', compat)) = uenv (v :: used) bs
-                      b' = map (renameVars compat) b in
+                      b' = map (compatNs compat) b in
-                  (v :: vs' ** (b' :: env', CompatExt compat))
+                  (v :: vs' ** (b' :: env', Ext compat))
 
 export
 allVars : {vars : _} -> Env Term vars -> List (Var vars)
@@ -325,3 +325,17 @@ allVarsNoLet : {vars : _} -> Env Term vars -> List (Var vars)
 allVarsNoLet [] = []
 allVarsNoLet (Let _ _ _ _ :: vs) = map weaken (allVars vs)
 allVarsNoLet (v :: vs) = MkVar First :: map weaken (allVars vs)
+
+export
+close : FC -> String -> Env Term vars -> Term vars -> ClosedTerm
+close fc nm env tm
+  = let (s, env) = mkSubstEnv 0 env in
+    substs s env (rewrite appendNilRightNeutral vars in tm)
+
+  where
+
+    mkSubstEnv : Int -> Env Term vs -> (SizeOf vs, SubstEnv vs [])
+    mkSubstEnv i [] = (zero, [])
+    mkSubstEnv i (v :: vs)
+       = let (s, env) = mkSubstEnv (i + 1) vs in
+         (suc s, Ref fc Bound (MN nm i) :: env)

src/Core/Hash.idr

@@ -146,7 +146,7 @@ Hashable ty => Hashable (Binder ty) where
       = h `hashWithSalt` 5 `hashWithSalt` c `hashWithSalt` ty
 
 Hashable (Var vars) where
-  hashWithSalt h (MkVar {i} _) = hashWithSalt h i
+  hashWithSalt h (MkVar {varIdx = i} _) = hashWithSalt h i
 
 mutual
   export

src/Core/LinearCheck.idr

@@ -13,6 +13,8 @@ import Core.TT
 
 import Data.List
 
+import Libraries.Data.SnocList.SizeOf
+
 %default covering
 
 -- List of variable usages - we'll count the contents of specific variables
@@ -43,14 +45,8 @@ count p [] = 0
 count p (v :: xs)
     = if p == varIdx v then 1 + count p xs else count p xs
 
-localPrf : {later : _} -> Var (later ++ n :: vars)
-localPrf {later = []} = MkVar First
-localPrf {n} {vars} {later = (x :: xs)}
-    = let MkVar p = localPrf {n} {vars} {later = xs} in
-          MkVar (Later p)
-
 mutual
-  updateHoleUsageArgs : {vars : _} ->
+  updateHoleUsageArgs : {0 vars : _} ->
                         {auto c : Ref Ctxt Defs} ->
                         {auto u : Ref UST UState} ->
                         (useInHole : Bool) ->
@@ -65,7 +61,7 @@ mutual
   -- The assumption here is that hole types are abstracted over the entire
   -- environment, so that they have the appropriate number of function
   -- arguments and there are no lets
-  updateHoleType : {vars : _} ->
+  updateHoleType : {0 vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    {auto u : Ref UST UState} ->
                    (useInHole : Bool) ->
@@ -124,7 +120,7 @@ mutual
       findLocal (_ :: els) (S k) = findLocal els k
       findLocal _ _ = Nothing
 
-  updateHoleUsage : {vars : _} ->
+  updateHoleUsage : {0 vars : _} ->
                     {auto c : Ref Ctxt Defs} ->
                     {auto u : Ref UST UState} ->
                     (useInHole : Bool) ->
@@ -526,14 +522,15 @@ mutual
       -- As checkEnvUsage in general, but it's okay for local variables to
       -- remain unused (since in that case, they must be used outside the
       -- case block)
-      checkEnvUsage : {done, vars : _} ->
+      checkEnvUsage : {vars : _} ->
+                      SizeOf done ->
                       RigCount ->
-                      Env Term vars -> Usage (done ++ vars) ->
+                      Env Term vars -> Usage (done <>> vars) ->
-                      List (Term (done ++ vars)) ->
+                      List (Term (done <>> vars)) ->
-                      Term (done ++ vars) -> Core ()
+                      Term (done <>> vars) -> Core ()
-      checkEnvUsage rig [] usage args tm = pure ()
+      checkEnvUsage s rig [] usage args tm = pure ()
-      checkEnvUsage rig {done} {vars = nm :: xs} (b :: env) usage args tm
+      checkEnvUsage s rig {done} {vars = nm :: xs} (b :: env) usage args tm
-          = do let pos = localPrf {later = done}
+          = do let pos = mkVarChiply s
                let used_in = count (varIdx pos) usage
 
                holeFound <- if isLinear (multiplicity b)
@@ -546,10 +543,7 @@ mutual
                checkUsageOK (getLoc (binderType b))
                             used nm (isLocArg pos args)
                                     ((multiplicity b) |*| rig)
-               checkEnvUsage {done = done ++ [nm]} rig env
+               checkEnvUsage (s :< nm) rig env usage args tm
-                     (rewrite sym (appendAssociative done [nm] xs) in usage)
-                     (rewrite sym (appendAssociative done [nm] xs) in args)
-                     (rewrite sym (appendAssociative done [nm] xs) in tm)
 
       getPUsage : ClosedTerm -> (vs ** (Env Term vs, Term vs, Term vs)) ->
                   Core (List (Name, ArgUsage))
@@ -560,7 +554,7 @@ mutual
                (rhs', _, used) <- lcheck rig False penv rhs
                log "quantity" 10 $ "Used: " ++ show used
                let args = getArgs lhs
-               checkEnvUsage {done = []} rig penv used args rhs'
+               checkEnvUsage [<] rig penv used args rhs'
                ause <- getCaseUsage ty penv args used rhs
                log "quantity" 10 $ "Arg usage: " ++ show ause
                pure ause
@@ -652,18 +646,19 @@ mutual
                Name -> Int -> Def -> List (Term vars) ->
                Core (Term vars, Glued vars, Usage vars)
   expandMeta rig erase env n idx (PMDef _ [] (STerm _ fn) _ _) args
-      = do tm <- substMeta (embed fn) args []
+      = do tm <- substMeta (embed fn) args zero []
            lcheck rig erase env tm
     where
       substMeta : {drop, vs : _} ->
-                  Term (drop ++ vs) -> List (Term vs) -> SubstEnv drop vs ->
+                  Term (drop ++ vs) -> List (Term vs) ->
+                  SizeOf drop -> SubstEnv drop vs ->
                   Core (Term vs)
-      substMeta (Bind bfc n (Lam _ c e ty) sc) (a :: as) env
+      substMeta (Bind bfc n (Lam _ c e ty) sc) (a :: as) drop env
-          = substMeta sc as (a :: env)
+          = substMeta sc as (suc drop) (a :: env)
-      substMeta (Bind bfc n (Let _ c val ty) sc) as env
+      substMeta (Bind bfc n (Let _ c val ty) sc) as drop env
-          = substMeta (subst val sc) as env
+          = substMeta (subst val sc) as drop env
-      substMeta rhs [] env = pure (substs env rhs)
+      substMeta rhs [] drop env = pure (substs drop env rhs)
-      substMeta rhs _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show fn))
+      substMeta rhs _ _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show fn))
   expandMeta rig erase env n idx def _
       = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show def))
 
@@ -699,16 +694,16 @@ mutual
            pure (Meta fc n idx (reverse chk), glueBack defs env nty, [])
 
 
-checkEnvUsage : {vars, done : _} ->
+checkEnvUsage : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
-                FC -> RigCount ->
+                FC -> SizeOf done -> RigCount ->
-                Env Term vars -> Usage (done ++ vars) ->
+                Env Term vars -> Usage (done <>> vars) ->
-                Term (done ++ vars) ->
+                Term (done <>> vars) ->
                 Core ()
-checkEnvUsage fc rig [] usage tm = pure ()
+checkEnvUsage fc s rig [] usage tm = pure ()
-checkEnvUsage fc rig {done} {vars = nm :: xs} (b :: env) usage tm
+checkEnvUsage fc s rig {vars = nm :: xs} (b :: env) usage tm
-    = do let pos = localPrf {later = done}
+    = do let pos = mkVarChiply s
          let used_in = count (varIdx pos) usage
 
          holeFound <- if isLinear (multiplicity b)
@@ -719,9 +714,7 @@ checkEnvUsage fc rig {done} {vars = nm :: xs} (b :: env) usage tm
                        then 1
                        else used_in
          checkUsageOK used ((multiplicity b) |*| rig)
-         checkEnvUsage {done = done ++ [nm]} fc rig env
+         checkEnvUsage fc (s :< nm) rig env usage tm
-               (rewrite sym (appendAssociative done [nm] xs) in usage)
-               (rewrite sym (appendAssociative done [nm] xs) in tm)
   where
     checkUsageOK : Nat -> RigCount -> Core ()
     checkUsageOK used r = when (isLinear r && used /= 1)
@@ -743,5 +736,5 @@ linearCheck fc rig erase env tm
          logEnv "quantity" 5 "In env" env
          (tm', _, used) <- lcheck rig erase env tm
          log "quantity" 5 $ "Used: " ++ show used
-         when (not erase) $ checkEnvUsage {done = []} fc rig env used tm'
+         when (not erase) $ checkEnvUsage fc [<] rig env used tm'
          pure tm'

src/Core/Name.idr

@@ -447,7 +447,7 @@ nameEq (Resolved x) (Resolved y) with (decEq x y)
 nameEq _ _ = Nothing
 
 export
-namesEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)
+namesEq : (xs, ys : List Name) -> Maybe (xs = ys)
 namesEq [] [] = Just Refl
 namesEq (x :: xs) (y :: ys)
     = do p <- nameEq x y
@@ -456,3 +456,11 @@ namesEq (x :: xs) (y :: ys)
          rewrite ps
          Just Refl
 namesEq _ _ = Nothing
+
+||| Generate the next machine name
+export
+next : Name -> Name
+next (MN n i) = MN n (i + 1)
+next (UN n) = MN (show n) 0
+next (NS ns n) = NS ns (next n)
+next n = MN (show n) 0

src/Core/Name/Scoped.idr

@@ -0,0 +1,260 @@
+module Core.Name.Scoped
+
+import Core.Name
+
+import public Libraries.Data.List.HasLength
+import public Libraries.Data.List.SizeOf
+
+%default total
+
+------------------------------------------------------------------------
+-- Basic type definitions
+
+||| A scope is represented by a list of names. E.g. in the following
+||| rule, the scope Γ is extended with x when going under the λx.
+||| binder:
+|||
+|||    Γ, x ⊢ t : B
+|||  -----------------------------
+|||    Γ    ⊢ λx. t : A → B
+public export
+Scope : Type
+Scope = List Name
+-- TODO: make that a SnocList
+
+||| A scoped definition is one indexed by a scope
+public export
+Scoped : Type
+Scoped = Scope -> Type
+
+------------------------------------------------------------------------
+-- Semi-decidable equality
+
+export
+scopeEq : (xs, ys : Scope) -> Maybe (xs = ys)
+scopeEq [] [] = Just Refl
+scopeEq (x :: xs) (y :: ys)
+    = do Refl <- nameEq x y
+         Refl <- scopeEq xs ys
+         Just Refl
+scopeEq _ _ = Nothing
+
+------------------------------------------------------------------------
+-- Generate a fresh name (for a given scope)
+
+export
+mkFresh : Scope -> Name -> Name
+mkFresh vs n
+  = if n `elem` vs
+    then assert_total $ mkFresh vs (next n)
+    else n
+
+
+------------------------------------------------------------------------
+-- Compatible variables
+
+public export
+data CompatibleVars : (xs, ys : List a) -> Type where
+   Pre : CompatibleVars xs xs
+   Ext : CompatibleVars xs ys -> CompatibleVars (n :: xs) (m :: ys)
+
+export
+invertExt : CompatibleVars (n :: xs) (m :: ys) -> CompatibleVars xs ys
+invertExt Pre = Pre
+invertExt (Ext p) = p
+
+export
+extendCompats : (args : List a) ->
+                CompatibleVars xs ys ->
+                CompatibleVars (args ++ xs) (args ++ ys)
+extendCompats args Pre = Pre
+extendCompats args prf = go args prf where
+
+  go : (args : List a) ->
+       CompatibleVars xs ys ->
+       CompatibleVars (args ++ xs) (args ++ ys)
+  go [] prf = prf
+  go (x :: xs) prf = Ext (go xs prf)
+
+export
+decCompatibleVars : (xs, ys : List a) -> Dec (CompatibleVars xs ys)
+decCompatibleVars [] [] = Yes Pre
+decCompatibleVars [] (x :: xs) = No (\case p impossible)
+decCompatibleVars (x :: xs) [] = No (\case p impossible)
+decCompatibleVars (x :: xs) (y :: ys) = case decCompatibleVars xs ys of
+  Yes prf => Yes (Ext prf)
+  No nprf => No (nprf . invertExt)
+
+export
+areCompatibleVars : (xs, ys : List a) ->
+                    Maybe (CompatibleVars xs ys)
+areCompatibleVars [] [] = pure Pre
+areCompatibleVars (x :: xs) (y :: ys)
+    = do compat <- areCompatibleVars xs ys
+         pure (Ext compat)
+areCompatibleVars _ _ = Nothing
+
+------------------------------------------------------------------------
+-- Thinnings
+
+public export
+data Thin : List a -> List a -> Type where
+  Refl : Thin xs xs
+  Drop : Thin xs ys -> Thin xs (y :: ys)
+  Keep : Thin xs ys -> Thin (x :: xs) (x :: ys)
+
+export
+none : {xs : List a} -> Thin [] xs
+none {xs = []} = Refl
+none {xs = _ :: _} = Drop none
+
+{- UNUSED: we actually sometimes want Refl vs. Keep!
+||| Smart constructor. We should use this to maximise the length
+||| of the Refl segment thus getting more short-circuiting behaviours
+export
+Keep : Thin xs ys -> Thin (x :: xs) (x :: ys)
+Keep Refl = Refl
+Keep p = Keep p
+-}
+
+export
+keeps : (args : List a) -> Thin xs ys -> Thin (args ++ xs) (args ++ ys)
+keeps [] th = th
+keeps (x :: xs) th = Keep (keeps xs th)
+
+||| Compute the thinning getting rid of the listed de Bruijn indices.
+-- TODO: is the list of erased arguments guaranteed to be sorted?
+-- Should it?
+export
+removeByIndices :
+  (erasedArgs : List Nat) ->
+  (args : Scope) ->
+  (args' ** Thin args' args)
+removeByIndices es = go 0 where
+
+  go : (currentIdx : Nat) -> (args : Scope) ->
+    (args' ** Thin args' args)
+  go idx [] = ([] ** Refl)
+  go idx (x :: xs) =
+    let (vs ** th) = go (S idx) xs in
+    if idx `elem` es
+      then (vs ** Drop th)
+      else (x :: vs ** Keep th)
+
+
+------------------------------------------------------------------------
+-- Concepts
+
+public export
+0 Weakenable : Scoped -> Type
+Weakenable tm = {0 vars, ns : Scope} ->
+  SizeOf ns -> tm vars -> tm (ns ++ vars)
+
+public export
+0 Strengthenable : Scoped -> Type
+Strengthenable tm = {0 vars, ns : Scope} ->
+  SizeOf ns -> tm (ns ++ vars) -> Maybe (tm vars)
+
+public export
+0 GenWeakenable : Scoped -> Type
+GenWeakenable tm = {0 outer, ns, local : Scope} ->
+  SizeOf local -> SizeOf ns -> tm (local ++ outer) -> tm (local ++ (ns ++ outer))
+
+public export
+0 Thinnable : Scoped -> Type
+Thinnable tm = {0 xs, ys : Scope} -> tm xs -> Thin xs ys -> tm ys
+
+public export
+0 Shrinkable : Scoped -> Type
+Shrinkable tm = {0 xs, ys : Scope} -> tm xs -> Thin ys xs -> Maybe (tm ys)
+
+public export
+0 Embeddable : Scoped -> Type
+Embeddable tm = {0 outer, vars : Scope} -> tm vars -> tm (vars ++ outer)
+
+------------------------------------------------------------------------
+-- IsScoped interface
+
+public export
+interface Weaken (0 tm : Scoped) where
+  constructor MkWeaken
+  -- methods
+  weaken : tm vars -> tm (nm :: vars)
+  weakenNs : Weakenable tm
+  -- default implementations
+  weaken = weakenNs (suc zero)
+
+-- This cannot be merged with Weaken because of WkCExp
+public export
+interface GenWeaken (0 tm : Scoped) where
+  constructor MkGenWeaken
+  genWeakenNs : GenWeakenable tm
+
+export
+genWeaken : GenWeaken tm =>
+  SizeOf local -> tm (local ++ outer) -> tm (local ++ n :: outer)
+genWeaken l = genWeakenNs l (suc zero)
+
+public export
+interface Strengthen (0 tm : Scoped) where
+  constructor MkStrengthen
+  -- methods
+  strengthenNs : Strengthenable tm
+
+export
+strengthen : Strengthen tm => tm (nm :: vars) -> Maybe (tm vars)
+strengthen = strengthenNs (suc zero)
+
+public export
+interface FreelyEmbeddable (0 tm : Scoped) where
+  constructor MkFreelyEmbeddable
+  -- this is free for nameless representations
+  embed : Embeddable tm
+  embed = believe_me
+
+export
+FunctorFreelyEmbeddable : Functor f => FreelyEmbeddable tm => FreelyEmbeddable (f . tm)
+FunctorFreelyEmbeddable = MkFreelyEmbeddable believe_me
+
+export
+ListFreelyEmbeddable : FreelyEmbeddable tm => FreelyEmbeddable (List . tm)
+ListFreelyEmbeddable = FunctorFreelyEmbeddable
+
+export
+MaybeFreelyEmbeddable : FreelyEmbeddable tm => FreelyEmbeddable (Maybe . tm)
+MaybeFreelyEmbeddable = FunctorFreelyEmbeddable
+
+export
+GenWeakenWeakens : GenWeaken tm => Weaken tm
+GenWeakenWeakens = MkWeaken (genWeakenNs zero (suc zero)) (genWeakenNs zero)
+
+export
+FunctorGenWeaken : Functor f => GenWeaken tm => GenWeaken (f . tm)
+FunctorGenWeaken = MkGenWeaken (\ l, s => map (genWeakenNs l s))
+
+export
+FunctorWeaken : Functor f => Weaken tm => Weaken (f . tm)
+FunctorWeaken = MkWeaken (go (suc zero)) go where
+
+  go : Weakenable (f . tm)
+  go s = map (weakenNs s)
+
+export
+ListWeaken : Weaken tm => Weaken (List . tm)
+ListWeaken = FunctorWeaken
+
+export
+MaybeWeaken : Weaken tm => Weaken (Maybe . tm)
+MaybeWeaken = FunctorWeaken
+
+public export
+interface Weaken tm => IsScoped (0 tm : Scoped) where
+  -- methods
+  compatNs : CompatibleVars xs ys -> tm xs -> tm ys
+
+  thin : Thinnable tm
+  shrink : Shrinkable tm
+
+export
+compat : IsScoped tm => tm (m :: xs) -> tm (n :: xs)
+compat = compatNs (Ext Pre)

src/Core/Normalise.idr

@@ -141,7 +141,7 @@ etaContract tm = do
       case tm of
         (Bind _ x (Lam _ _ _ _) (App _ fn (Local _ _ Z _))) => do
           logTerm "eval.eta" 10 "  Shrinking candidate" fn
-          let shrunk = shrinkTerm fn (DropCons SubRefl)
+          let shrunk = shrink fn (Drop Refl)
           case shrunk of
             Nothing => do
               log "eval.eta" 10 "  Failure!"
@@ -278,19 +278,19 @@ replace' {vars} tmpi defs env lhs parg tm
              quote empty env (NApp fc hd [])
     repSub (NApp fc hd args)
         = do args' <- traverse (traversePair repArg) args
-             pure $ applyWithFC
+             pure $ applyStackWithFC
                         !(replace' tmpi defs env lhs parg (NApp fc hd []))
                         args'
     repSub (NDCon fc n t a args)
         = do args' <- traverse (traversePair repArg) args
              empty <- clearDefs defs
-             pure $ applyWithFC
+             pure $ applyStackWithFC
                         !(quote empty env (NDCon fc n t a []))
                         args'
     repSub (NTCon fc n t a args)
         = do args' <- traverse (traversePair repArg) args
              empty <- clearDefs defs
-             pure $ applyWithFC
+             pure $ applyStackWithFC
                         !(quote empty env (NTCon fc n t a []))
                         args'
     repSub (NAs fc s a p)
@@ -307,7 +307,7 @@ replace' {vars} tmpi defs env lhs parg tm
     repSub (NForce fc r tm args)
         = do args' <- traverse (traversePair repArg) args
              tm' <- repSub tm
-             pure $ applyWithFC (TForce fc r tm') args'
+             pure $ applyStackWithFC (TForce fc r tm') args'
     repSub (NErased fc (Dotted t))
         = do t' <- repSub t
              pure (Erased fc (Dotted t'))

src/Core/Normalise/Convert.idr

@@ -45,13 +45,13 @@ tryUpdate : {vars, vars' : _} ->
             List (Var vars, Var vars') ->
             Term vars -> Maybe (Term vars')
 tryUpdate ms (Local fc l idx p)
-    = do MkVar p' <- findIdx ms idx
+    = do MkVar p' <- findIdx ms (MkVar p)
          pure $ Local fc l _ p'
   where
-    findIdx : List (Var vars, Var vars') -> Nat -> Maybe (Var vars')
+    findIdx : List (Var vars, Var vars') -> Var vars -> Maybe (Var vars')
     findIdx [] _ = Nothing
-    findIdx ((MkVar {i} _, v) :: ps) n
+    findIdx ((old, v) :: ps) n
-        = if i == n then Just v else findIdx ps n
+        = if old == n then Just v else findIdx ps n
 tryUpdate ms (Ref fc nt n) = pure $ Ref fc nt n
 tryUpdate ms (Meta fc n i args) = pure $ Meta fc n i !(traverse (tryUpdate ms) args)
 tryUpdate ms (Bind fc x b sc)
@@ -154,7 +154,7 @@ mutual
                    pure (Just (mapMaybe (dropP cargs cargs') ms))
            else pure Nothing
     where
-      weakenP : {c, c', args, args' : _} ->
+      weakenP : {0 c, c' : _} -> {0 args, args' : Scope} ->
                 (Var args, Var args') ->
                 (Var (c :: args), Var (c' :: args'))
       weakenP (v, vs) = (weaken v, weaken vs)
@@ -248,7 +248,7 @@ mutual
                         List (Var vs, Var vs') ->
                         Core Bool
        convertMatches [] = pure True
-       convertMatches ((MkVar {i=ix} p, MkVar {i=iy} p') :: vs)
+       convertMatches ((MkVar {varIdx = ix} p, MkVar {varIdx = iy} p') :: vs)
           = do let Just varg = getArgPos ix nargs
                    | Nothing => pure False
                let Just varg' = getArgPos iy nargs'

src/Core/Normalise/Eval.idr

@@ -424,13 +424,13 @@ parameters (defs : Defs, topopts : EvalOpts)
                Stack free -> CaseTree args ->
                Core (CaseResult (TermWithEnv free))
     evalTree env loc opts fc stk (Case {name} idx x _ alts)
-      = do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
+      = do xval <- evalLocal env fc Nothing idx (embedIsVar x) [] loc
            -- we have not defined quote yet (it depends on eval itself) so we show the NF
            -- i.e. only the top-level constructor.
            logC "eval.casetree" 5 $ do
              xval <- toFullNames xval
              pure "Evaluated \{show name} to \{show xval}"
-           let loc' = updateLocal opts env idx (varExtend x) loc xval
+           let loc' = updateLocal opts env idx (embedIsVar x) loc xval
            findAlt env loc' opts fc stk xval alts
     evalTree env loc opts fc stk (STerm _ tm)
           = pure (Result $ MkTermEnv loc $ embed tm)

src/Core/Normalise/Quote.idr

@@ -107,7 +107,7 @@ mutual
                 MkVar (Later isv')
   quoteHead q opts defs fc bounds env (NRef Bound (MN n i))
       = pure $ case findName bounds of
-             Just (MkVar p) => Local fc Nothing _ (varExtend p)
+             Just (MkVar p) => Local fc Nothing _ (embedIsVar p)
              Nothing => Ref fc Bound (MN n i)
     where
       findName : Bounds bound' -> Maybe (Var bound')
@@ -189,17 +189,17 @@ mutual
                                quoteArgsWithFC q opts' empty bound env args
                                else quoteArgsWithFC q ({ topLevel := False } opts')
                                                     defs bound env args
-           pure $ applyWithFC f' args'
+           pure $ applyStackWithFC f' args'
     where
       isRef : NHead vars -> Bool
       isRef (NRef{}) = True
       isRef _ = False
   quoteGenNF q opts defs bound env (NDCon fc n t ar args)
       = do args' <- quoteArgsWithFC q opts defs bound env args
-           pure $ applyWithFC (Ref fc (DataCon t ar) n) args'
+           pure $ applyStackWithFC (Ref fc (DataCon t ar) n) args'
   quoteGenNF q opts defs bound env (NTCon fc n t ar args)
       = do args' <- quoteArgsWithFC q opts defs bound env args
-           pure $ applyWithFC (Ref fc (TyCon t ar) n) args'
+           pure $ applyStackWithFC (Ref fc (TyCon t ar) n) args'
   quoteGenNF q opts defs bound env (NAs fc s n pat)
       = do n' <- quoteGenNF q opts defs bound env n
            pat' <- quoteGenNF q opts defs bound env pat
@@ -225,9 +225,9 @@ mutual
            case arg of
                 NDelay fc _ _ arg =>
                    do argNF <- evalClosure defs arg
-                      pure $ applyWithFC !(quoteGenNF q opts defs bound env argNF) args'
+                      pure $ applyStackWithFC !(quoteGenNF q opts defs bound env argNF) args'
                 _ => do arg' <- quoteGenNF q opts defs bound env arg
-                        pure $ applyWithFC (TForce fc r arg') args'
+                        pure $ applyStackWithFC (TForce fc r arg') args'
   quoteGenNF q opts defs bound env (NPrimVal fc c) = pure $ PrimVal fc c
   quoteGenNF q opts defs bound env (NErased fc t)
     = Erased fc <$> traverse @{%search} @{CORE} (\ nf => quoteGenNF q opts defs bound env nf) t

src/Core/Ord.idr

@@ -6,171 +6,7 @@ import Core.Name
 import Core.TT
 import Data.Vect
 
-infixl 5 `thenCmp`
+import Libraries.Data.Ordering.Extra
-
-thenCmp : Ordering -> Lazy Ordering -> Ordering
-thenCmp LT _ = LT
-thenCmp EQ o = o
-thenCmp GT _ = GT
-
-export
-Ord PrimType where
-  compare = compare `on` tag
-    where
-      tag : PrimType -> Int
-      tag IntType     = 1
-      tag Int8Type    = 2
-      tag Int16Type   = 3
-      tag Int32Type   = 4
-      tag Int64Type   = 5
-      tag IntegerType = 6
-      tag Bits8Type   = 7
-      tag Bits16Type  = 8
-      tag Bits32Type  = 9
-      tag Bits64Type  = 10
-      tag StringType  = 11
-      tag CharType    = 12
-      tag DoubleType  = 13
-      tag WorldType   = 14
-
-export
-Ord Constant where
-    I x `compare` I y = compare x y
-    I8 x `compare` I8 y = compare x y
-    I16 x `compare` I16 y = compare x y
-    I32 x `compare` I32 y = compare x y
-    I64 x `compare` I64 y = compare x y
-    BI x `compare` BI y = compare x y
-    B8 x `compare` B8 y = compare x y
-    B16 x `compare` B16 y = compare x y
-    B32 x `compare` B32 y = compare x y
-    B64 x `compare` B64 y = compare x y
-    Str x `compare` Str y = compare x y
-    Ch x `compare` Ch y = compare x y
-    Db x `compare` Db y = compare x y
-    PrT x `compare` PrT y = compare x y
-    compare x y = compare (tag x) (tag y)
-      where
-        tag : Constant -> Int
-        tag (I _) = 0
-        tag (I8 _) = 1
-        tag (I16 _) = 2
-        tag (I32 _) = 3
-        tag (I64 _) = 4
-        tag (BI _) = 5
-        tag (B8 _) = 6
-        tag (B16 _) = 7
-        tag (B32 _) = 8
-        tag (B64 _) = 9
-        tag (Str _) = 10
-        tag (Ch _) = 11
-        tag (Db _) = 12
-        tag (PrT _) = 13
-        tag WorldVal = 14
-
-primFnEq : PrimFn a1 -> PrimFn a2 -> Maybe (a1 = a2)
-primFnEq (Add t1) (Add t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (Sub t1) (Sub t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (Mul t1) (Mul t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (Div t1) (Div t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (Mod t1) (Mod t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (Neg t1) (Neg t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (ShiftL t1) (ShiftL t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (ShiftR t1) (ShiftR t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (BAnd t1) (BAnd t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (BOr t1) (BOr t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (BXOr t1) (BXOr t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (LT t1) (LT t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (LTE t1) (LTE t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (EQ t1) (EQ t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (GTE t1) (GTE t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq (GT t1) (GT t2) = if t1 == t2 then Just Refl else Nothing
-primFnEq StrLength StrLength = Just Refl
-primFnEq StrHead StrHead = Just Refl
-primFnEq StrTail StrTail = Just Refl
-primFnEq StrIndex StrIndex = Just Refl
-primFnEq StrCons StrCons = Just Refl
-primFnEq StrAppend StrAppend = Just Refl
-primFnEq StrReverse StrReverse = Just Refl
-primFnEq StrSubstr StrSubstr = Just Refl
-primFnEq DoubleExp DoubleExp = Just Refl
-primFnEq DoubleLog DoubleLog = Just Refl
-primFnEq DoublePow DoublePow = Just Refl
-primFnEq DoubleSin DoubleSin = Just Refl
-primFnEq DoubleCos DoubleCos = Just Refl
-primFnEq DoubleTan DoubleTan = Just Refl
-primFnEq DoubleASin DoubleASin = Just Refl
-primFnEq DoubleACos DoubleACos = Just Refl
-primFnEq DoubleATan DoubleATan = Just Refl
-primFnEq DoubleSqrt DoubleSqrt = Just Refl
-primFnEq DoubleFloor DoubleFloor = Just Refl
-primFnEq DoubleCeiling DoubleCeiling = Just Refl
-primFnEq (Cast f1 t1) (Cast f2 t2) = if f1 == f2 && t1 == t2 then Just Refl else Nothing
-primFnEq BelieveMe BelieveMe = Just Refl
-primFnEq Crash Crash = Just Refl
-primFnEq _ _ = Nothing
-
-primFnCmp : PrimFn a1 -> PrimFn a2 -> Ordering
-primFnCmp (Add t1) (Add t2) = compare t1 t2
-primFnCmp (Sub t1) (Sub t2) = compare t1 t2
-primFnCmp (Mul t1) (Mul t2) = compare t1 t2
-primFnCmp (Div t1) (Div t2) = compare t1 t2
-primFnCmp (Mod t1) (Mod t2) = compare t1 t2
-primFnCmp (Neg t1) (Neg t2) = compare t1 t2
-primFnCmp (ShiftL t1) (ShiftL t2) = compare t1 t2
-primFnCmp (ShiftR t1) (ShiftR t2) = compare t1 t2
-primFnCmp (BAnd t1) (BAnd t2) = compare t1 t2
-primFnCmp (BOr t1) (BOr t2) = compare t1 t2
-primFnCmp (BXOr t1) (BXOr t2) = compare t1 t2
-primFnCmp (LT t1) (LT t2) = compare t1 t2
-primFnCmp (LTE t1) (LTE t2) = compare t1 t2
-primFnCmp (EQ t1) (EQ t2) = compare t1 t2
-primFnCmp (GTE t1) (GTE t2) = compare t1 t2
-primFnCmp (GT t1) (GT t2) = compare t1 t2
-primFnCmp (Cast f1 t1) (Cast f2 t2) = compare f1 f2 `thenCmp` compare t1 t2
-primFnCmp f1 f2 = compare (tag f1) (tag f2)
-  where
-    tag : forall ar. PrimFn ar -> Int
-    tag (Add _) = 0
-    tag (Sub _) = 1
-    tag (Mul _) = 2
-    tag (Div _) = 3
-    tag (Mod _) = 4
-    tag (Neg _) = 5
-    tag (ShiftL _) = 6
-    tag (ShiftR _) = 7
-    tag (BAnd _) = 8
-    tag (BOr _) = 9
-    tag (BXOr _) = 10
-    tag (LT _) = 11
-    tag (LTE _) = 12
-    tag (EQ _) = 13
-    tag (GTE _) = 14
-    tag (GT _) = 15
-    tag StrLength = 16
-    tag StrHead = 17
-    tag StrTail = 18
-    tag StrIndex = 19
-    tag StrCons = 20
-    tag StrAppend = 21
-    tag StrReverse = 22
-    tag StrSubstr = 23
-    tag DoubleExp = 24
-    tag DoubleLog = 25
-    tag DoublePow = 26
-    tag DoubleSin = 27
-    tag DoubleCos = 28
-    tag DoubleTan = 29
-    tag DoubleASin = 30
-    tag DoubleACos = 31
-    tag DoubleATan = 32
-    tag DoubleSqrt = 33
-    tag DoubleFloor = 34
-    tag DoubleCeiling = 35
-    tag (Cast _ _) = 36
-    tag BelieveMe = 37
-    tag Crash = 38
-
 
 lrTag : LazyReason -> Int
 lrTag LInf = 0
@@ -181,14 +17,6 @@ export
 Ord LazyReason where
     compare l1 l2 = compare (lrTag l1) (lrTag l2)
 
-export
-Eq (Var vars) where
-    MkVar {i=i1} _ == MkVar {i=i2} _ = i1 == i2
-
-export
-Ord (Var vars) where
-    MkVar {i=i1} _ `compare` MkVar {i=i2} _ = compare i1 i2
-
 mutual
     export
     covering

src/Core/SchemeEval/Quote.idr

@@ -76,7 +76,7 @@ mutual
                 MkVar (Later isv')
   quoteHead q fc bounds env (SRef nt n)
       = pure $ case findName bounds of
-             Just (MkVar p) => Local fc Nothing _ (varExtend p)
+             Just (MkVar p) => Local fc Nothing _ (embedIsVar p)
              Nothing => Ref fc nt n
     where
       findName : Bounds bound' -> Maybe (Var bound')

src/Core/TT/Binder.idr

@@ -0,0 +1,230 @@
+module Core.TT.Binder
+
+import Algebra
+
+import Core.FC
+
+%default total
+
+------------------------------------------------------------------------
+-- Pi information classifies the kind of pi type this is
+
+public export
+data PiInfo t =
+  ||| Implicit Pi types (e.g. {0 a : Type} -> ...)
+  ||| The argument is to be solved by unification
+  Implicit |
+  ||| Explicit Pi types (e.g. (x : a) -> ...)
+  ||| The argument is to be passed explicitly
+  Explicit |
+  ||| Auto Pi types (e.g. (fun : Functor f) => ...)
+  ||| The argument is to be solved by proof search
+  AutoImplicit |
+  ||| Default Pi types (e.g. {default True flag : Bool} -> ...)
+  ||| The argument is set to the default value if nothing is
+  ||| passed explicitly
+  DefImplicit t
+
+%name PiInfo pinfo
+
+namespace PiInfo
+
+  export
+  isImplicit : PiInfo t -> Bool
+  isImplicit Explicit = False
+  isImplicit _ = True
+
+||| Heterogeneous equality, provided an heterogeneous equality
+||| of default values
+export
+eqPiInfoBy : (t -> u -> Bool) -> PiInfo t -> PiInfo u -> Bool
+eqPiInfoBy eqT = go where
+
+  go : PiInfo t -> PiInfo u -> Bool
+  go Implicit Implicit = True
+  go Explicit Explicit = True
+  go AutoImplicit AutoImplicit = True
+  go (DefImplicit t) (DefImplicit t') = eqT t t'
+  go _ _ = False
+
+-- There's few places where we need the default - it's just when checking if
+-- there's a default during elaboration - so often it's easier just to erase it
+-- to a normal implicit
+export
+forgetDef : PiInfo t -> PiInfo t'
+forgetDef Explicit = Explicit
+forgetDef Implicit = Implicit
+forgetDef AutoImplicit = AutoImplicit
+forgetDef (DefImplicit t) = Implicit
+
+export
+Show t => Show (PiInfo t) where
+  show Implicit = "Implicit"
+  show Explicit = "Explicit"
+  show AutoImplicit = "AutoImplicit"
+  show (DefImplicit t) = "DefImplicit " ++ show t
+
+export
+Eq t => Eq (PiInfo t) where
+  (==) = eqPiInfoBy (==)
+
+------------------------------------------------------------------------
+-- Different types of binders we may encounter
+
+public export
+data Binder : Type -> Type where
+     -- Lambda bound variables with their implicitness
+     Lam : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
+     -- Let bound variables with their value
+     Let : FC -> RigCount -> (val : type) -> (ty : type) -> Binder type
+     -- Forall/pi bound variables with their implicitness
+     Pi : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
+     -- pattern bound variables. The PiInfo gives the implicitness at the
+     -- point it was bound (Explicit if it was explicitly named in the
+     -- program)
+     PVar : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
+     -- variable bound for an as pattern (Like a let, but no computational
+     -- force, and only used on the lhs. Converted to a let on the rhs because
+     -- we want the computational behaviour.)
+     PLet : FC -> RigCount -> (val : type) -> (ty : type) -> Binder type
+     -- the type of pattern bound variables
+     PVTy : FC -> RigCount -> (ty : type) -> Binder type
+
+%name Binder bd
+
+export
+isLet : Binder t -> Bool
+isLet (Let _ _ _ _) = True
+isLet _ = False
+
+export
+binderLoc : Binder tm -> FC
+binderLoc (Lam fc _ x ty) = fc
+binderLoc (Let fc _ val ty) = fc
+binderLoc (Pi fc _ x ty) = fc
+binderLoc (PVar fc _ p ty) = fc
+binderLoc (PLet fc _ val ty) = fc
+binderLoc (PVTy fc _ ty) = fc
+
+export
+binderType : Binder tm -> tm
+binderType (Lam _ _ x ty) = ty
+binderType (Let _ _ val ty) = ty
+binderType (Pi _ _ x ty) = ty
+binderType (PVar _ _ _ ty) = ty
+binderType (PLet _ _ val ty) = ty
+binderType (PVTy _ _ ty) = ty
+
+export
+multiplicity : Binder tm -> RigCount
+multiplicity (Lam _ c x ty) = c
+multiplicity (Let _ c val ty) = c
+multiplicity (Pi _ c x ty) = c
+multiplicity (PVar _ c p ty) = c
+multiplicity (PLet _ c val ty) = c
+multiplicity (PVTy _ c ty) = c
+
+export
+piInfo : Binder tm -> PiInfo tm
+piInfo (Lam _ c x ty) = x
+piInfo (Let _ c val ty) = Explicit
+piInfo (Pi _ c x ty) = x
+piInfo (PVar _ c p ty) = p
+piInfo (PLet _ c val ty) = Explicit
+piInfo (PVTy _ c ty) = Explicit
+
+export
+isImplicit : Binder tm -> Bool
+isImplicit = PiInfo.isImplicit . piInfo
+
+export
+setMultiplicity : Binder tm -> RigCount -> Binder tm
+setMultiplicity (Lam fc _ x ty) c = Lam fc c x ty
+setMultiplicity (Let fc _ val ty) c = Let fc c val ty
+setMultiplicity (Pi fc _ x ty) c = Pi fc c x ty
+setMultiplicity (PVar fc _ p ty) c = PVar fc c p ty
+setMultiplicity (PLet fc _ val ty) c = PLet fc c val ty
+setMultiplicity (PVTy fc _ ty) c = PVTy fc c ty
+
+Show ty => Show (Binder ty) where
+  show (Lam _ c _ t) = "\\" ++ showCount c ++ show t
+  show (Pi _ c _ t) = "Pi " ++ showCount c ++ show t
+  show (Let _ c v t) = "let " ++ showCount c ++ show v ++ " : " ++ show t
+  show (PVar _ c _ t) = "pat " ++ showCount c ++ show t
+  show (PLet _ c v t) = "plet " ++ showCount c ++ show v ++ " : " ++ show t
+  show (PVTy _ c t) = "pty " ++ showCount c ++ show t
+
+export
+setType : Binder tm -> tm -> Binder tm
+setType (Lam fc c x _) ty = Lam fc c x ty
+setType (Let fc c val _) ty = Let fc c val ty
+setType (Pi fc c x _) ty = Pi fc c x ty
+setType (PVar fc c p _) ty = PVar fc c p ty
+setType (PLet fc c val _) ty = PLet fc c val ty
+setType (PVTy fc c _) ty = PVTy fc c ty
+
+export
+Functor PiInfo where
+  map func Explicit = Explicit
+  map func Implicit = Implicit
+  map func AutoImplicit = AutoImplicit
+  map func (DefImplicit t) = (DefImplicit (func t))
+
+export
+Foldable PiInfo where
+  foldr f acc Implicit = acc
+  foldr f acc Explicit = acc
+  foldr f acc AutoImplicit = acc
+  foldr f acc (DefImplicit x) = f x acc
+
+export
+Traversable PiInfo where
+  traverse f Implicit = pure Implicit
+  traverse f Explicit = pure Explicit
+  traverse f AutoImplicit = pure AutoImplicit
+  traverse f (DefImplicit x) = map DefImplicit (f x)
+
+export
+Functor Binder where
+  map func (Lam fc c x ty) = Lam fc c (map func x) (func ty)
+  map func (Let fc c val ty) = Let fc c (func val) (func ty)
+  map func (Pi fc c x ty) = Pi fc c (map func x) (func ty)
+  map func (PVar fc c p ty) = PVar fc c (map func p) (func ty)
+  map func (PLet fc c val ty) = PLet fc c (func val) (func ty)
+  map func (PVTy fc c ty) = PVTy fc c (func ty)
+
+export
+Foldable Binder where
+  foldr f acc (Lam fc c x ty) = foldr f (f ty acc) x
+  foldr f acc (Let fc c val ty) = f val (f ty acc)
+  foldr f acc (Pi fc c x ty) = foldr f (f ty acc) x
+  foldr f acc (PVar fc c p ty) = foldr f (f ty acc) p
+  foldr f acc (PLet fc c val ty) = f val (f ty acc)
+  foldr f acc (PVTy fc c ty) = f ty acc
+
+export
+Traversable Binder where
+  traverse f (Lam fc c x ty) = Lam fc c <$> traverse f x <*> f ty
+  traverse f (Let fc c val ty) = Let fc c <$> f val <*> f ty
+  traverse f (Pi fc c x ty) = Pi fc c <$> traverse f x <*> f ty
+  traverse f (PVar fc c p ty) = PVar fc c <$> traverse f p <*> f ty
+  traverse f (PLet fc c val ty) = PLet fc c <$> f val <*> f ty
+  traverse f (PVTy fc c ty) = PVTy fc c <$> f ty
+
+
+export
+eqBinderBy : (t -> u -> Bool) -> (Binder t -> Binder u -> Bool)
+eqBinderBy eqTU = go where
+
+  go : Binder t -> Binder u -> Bool
+  go (Lam _ c p ty) (Lam _ c' p' ty') = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
+  go (Let _ c v ty) (Let _ c' v' ty') = c == c' && eqTU v v' && eqTU ty ty'
+  go (Pi _ c p ty) (Pi _ c' p' ty')   = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
+  go (PVar _ c p ty) (PVar _ c' p' ty') = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
+  go (PLet _ c v ty) (PLet _ c' v' ty') = c == c' && eqTU v v' && eqTU ty ty'
+  go (PVTy _ c ty) (PVTy _ c' ty') = c == c' && eqTU ty ty'
+  go _ _ = False
+
+export
+Eq a => Eq (Binder a) where
+  (==) = eqBinderBy (==)

src/Core/TT/Primitive.idr

@@ -0,0 +1,592 @@
+module Core.TT.Primitive
+
+import Core.Name
+
+import Data.String
+import Data.Vect
+
+import Decidable.Equality
+
+import Idris.Pretty.Annotations
+
+import Libraries.Data.Ordering.Extra
+import Libraries.Data.Primitives
+import Libraries.Data.String.Extra -- compatibility
+import Libraries.Text.PrettyPrint.Prettyprinter
+
+%default total
+
+public export
+data PrimType
+    = IntType
+    | Int8Type
+    | Int16Type
+    | Int32Type
+    | Int64Type
+    | IntegerType
+    | Bits8Type
+    | Bits16Type
+    | Bits32Type
+    | Bits64Type
+    | StringType
+    | CharType
+    | DoubleType
+    | WorldType
+
+%name PrimType pty
+
+public export
+data Constant
+    = I   Int
+    | I8  Int8
+    | I16 Int16
+    | I32 Int32
+    | I64 Int64
+    | BI  Integer
+    | B8  Bits8
+    | B16 Bits16
+    | B32 Bits32
+    | B64 Bits64
+    | Str String
+    | Ch  Char
+    | Db  Double
+    | PrT PrimType
+    | WorldVal
+
+%name Constant cst
+
+export
+isConstantType : Name -> Maybe PrimType
+isConstantType (UN (Basic n)) = case n of
+  "Int"     => Just IntType
+  "Int8"    => Just Int8Type
+  "Int16"   => Just Int16Type
+  "Int32"   => Just Int32Type
+  "Int64"   => Just Int64Type
+  "Integer" => Just IntegerType
+  "Bits8"   => Just Bits8Type
+  "Bits16"  => Just Bits16Type
+  "Bits32"  => Just Bits32Type
+  "Bits64"  => Just Bits64Type
+  "String"  => Just StringType
+  "Char"    => Just CharType
+  "Double"  => Just DoubleType
+  "%World"  => Just WorldType
+  _ => Nothing
+isConstantType _ = Nothing
+
+export
+isPrimType : Constant -> Bool
+isPrimType (PrT _) = True
+isPrimType _       = False
+
+export
+primTypeEq : (x, y : PrimType) -> Maybe (x = y)
+primTypeEq IntType IntType = Just Refl
+primTypeEq Int8Type Int8Type = Just Refl
+primTypeEq Int16Type Int16Type = Just Refl
+primTypeEq Int32Type Int32Type = Just Refl
+primTypeEq Int64Type Int64Type = Just Refl
+primTypeEq IntegerType IntegerType = Just Refl
+primTypeEq StringType StringType = Just Refl
+primTypeEq CharType CharType = Just Refl
+primTypeEq DoubleType DoubleType = Just Refl
+primTypeEq WorldType WorldType = Just Refl
+primTypeEq _ _ = Nothing
+
+-- TODO : The `TempXY` instances can be removed after the next release
+--        (see also `Libraries.Data.Primitives`)
+export
+constantEq : (x, y : Constant) -> Maybe (x = y)
+constantEq (I x) (I y) = case decEq x y of
+                              Yes Refl => Just Refl
+                              No contra => Nothing
+constantEq (I8 x) (I8 y) = case decEq @{TempI8} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (I16 x) (I16 y) = case decEq @{TempI16} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (I32 x) (I32 y) = case decEq @{TempI32} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (I64 x) (I64 y) = case decEq @{TempI64} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (B8 x) (B8 y) = case decEq @{TempB8} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (B16 x) (B16 y) = case decEq @{TempB16} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (B32 x) (B32 y) = case decEq @{TempB32} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (B64 x) (B64 y) = case decEq @{TempB64} x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (BI x) (BI y) = case decEq x y of
+                                Yes Refl => Just Refl
+                                No contra => Nothing
+constantEq (Str x) (Str y) = case decEq x y of
+                                  Yes Refl => Just Refl
+                                  No contra => Nothing
+constantEq (Ch x) (Ch y) = case decEq x y of
+                                Yes Refl => Just Refl
+                                No contra => Nothing
+constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!
+constantEq (PrT x) (PrT y) = (\xy => cong PrT xy) <$> primTypeEq x y
+constantEq WorldVal WorldVal = Just Refl
+
+constantEq _ _ = Nothing
+
+export
+Show PrimType where
+  show IntType = "Int"
+  show Int8Type = "Int8"
+  show Int16Type = "Int16"
+  show Int32Type = "Int32"
+  show Int64Type = "Int64"
+  show IntegerType = "Integer"
+  show Bits8Type = "Bits8"
+  show Bits16Type = "Bits16"
+  show Bits32Type = "Bits32"
+  show Bits64Type = "Bits64"
+  show StringType = "String"
+  show CharType = "Char"
+  show DoubleType = "Double"
+  show WorldType = "%World"
+
+export
+Show Constant where
+  show (I x) = show x
+  show (I8 x) = show x
+  show (I16 x) = show x
+  show (I32 x) = show x
+  show (I64 x) = show x
+  show (BI x) = show x
+  show (B8 x) = show x
+  show (B16 x) = show x
+  show (B32 x) = show x
+  show (B64 x) = show x
+  show (Str x) = show x
+  show (Ch x) = show x
+  show (Db x) = show x
+  show (PrT x) = show x
+  show WorldVal = "%MkWorld"
+
+Pretty IdrisSyntax PrimType where
+  pretty c = annotate (TCon Nothing) $ case c of
+    IntType => "Int"
+    Int8Type => "Int8"
+    Int16Type => "Int16"
+    Int32Type => "Int32"
+    Int64Type => "Int64"
+    IntegerType => "Integer"
+    Bits8Type => "Bits8"
+    Bits16Type => "Bits16"
+    Bits32Type => "Bits32"
+    Bits64Type => "Bits64"
+    StringType => "String"
+    CharType => "Char"
+    DoubleType => "Double"
+    WorldType => "%World"
+
+export
+Pretty IdrisSyntax Constant where
+  pretty (PrT x) = pretty x
+  pretty v = annotate (DCon Nothing) $ pretty0 $ show v
+
+
+export
+Eq PrimType where
+  IntType == IntType = True
+  Int8Type == Int8Type = True
+  Int16Type == Int16Type = True
+  Int32Type == Int32Type = True
+  Int64Type == Int64Type = True
+  IntegerType == IntegerType = True
+  Bits8Type == Bits8Type = True
+  Bits16Type == Bits16Type = True
+  Bits32Type == Bits32Type = True
+  Bits64Type == Bits64Type = True
+  StringType == StringType = True
+  CharType == CharType = True
+  DoubleType == DoubleType = True
+  WorldType == WorldType = True
+  _ == _ = False
+
+export
+Eq Constant where
+  (I x) == (I y) = x == y
+  (I8 x) == (I8 y) = x == y
+  (I16 x) == (I16 y) = x == y
+  (I32 x) == (I32 y) = x == y
+  (I64 x) == (I64 y) = x == y
+  (BI x) == (BI y) = x == y
+  (B8 x) == (B8 y) = x == y
+  (B16 x) == (B16 y) = x == y
+  (B32 x) == (B32 y) = x == y
+  (B64 x) == (B64 y) = x == y
+  (Str x) == (Str y) = x == y
+  (Ch x) == (Ch y) = x == y
+  (Db x) == (Db y) = x == y
+  (PrT x) == (PrT y) = x == y
+  WorldVal == WorldVal = True
+  _ == _ = False
+
+export
+Ord PrimType where
+  compare = compare `on` tag
+    where
+      tag : PrimType -> Int
+      tag IntType     = 1
+      tag Int8Type    = 2
+      tag Int16Type   = 3
+      tag Int32Type   = 4
+      tag Int64Type   = 5
+      tag IntegerType = 6
+      tag Bits8Type   = 7
+      tag Bits16Type  = 8
+      tag Bits32Type  = 9
+      tag Bits64Type  = 10
+      tag StringType  = 11
+      tag CharType    = 12
+      tag DoubleType  = 13
+      tag WorldType   = 14
+
+export
+Ord Constant where
+    I x `compare` I y = compare x y
+    I8 x `compare` I8 y = compare x y
+    I16 x `compare` I16 y = compare x y
+    I32 x `compare` I32 y = compare x y
+    I64 x `compare` I64 y = compare x y
+    BI x `compare` BI y = compare x y
+    B8 x `compare` B8 y = compare x y
+    B16 x `compare` B16 y = compare x y
+    B32 x `compare` B32 y = compare x y
+    B64 x `compare` B64 y = compare x y
+    Str x `compare` Str y = compare x y
+    Ch x `compare` Ch y = compare x y
+    Db x `compare` Db y = compare x y
+    PrT x `compare` PrT y = compare x y
+    compare x y = compare (tag x) (tag y)
+      where
+        tag : Constant -> Int
+        tag (I _) = 0
+        tag (I8 _) = 1
+        tag (I16 _) = 2
+        tag (I32 _) = 3
+        tag (I64 _) = 4
+        tag (BI _) = 5
+        tag (B8 _) = 6
+        tag (B16 _) = 7
+        tag (B32 _) = 8
+        tag (B64 _) = 9
+        tag (Str _) = 10
+        tag (Ch _) = 11
+        tag (Db _) = 12
+        tag (PrT _) = 13
+        tag WorldVal = 14
+
+-- for typecase
+export
+primTypeTag : PrimType -> Int
+-- 1 = ->, 2 = Type
+primTypeTag IntType = 3
+primTypeTag IntegerType = 4
+primTypeTag Bits8Type = 5
+primTypeTag Bits16Type = 6
+primTypeTag Bits32Type = 7
+primTypeTag Bits64Type = 8
+primTypeTag StringType = 9
+primTypeTag CharType = 10
+primTypeTag DoubleType = 11
+primTypeTag WorldType = 12
+primTypeTag Int8Type = 13
+primTypeTag Int16Type = 14
+primTypeTag Int32Type = 15
+primTypeTag Int64Type = 16
+
+||| Precision of integral types.
+public export
+data Precision = P Int | Unlimited
+
+%name Precision prec
+
+export
+Eq Precision where
+  (P m) == (P n)         = m == n
+  Unlimited == Unlimited = True
+  _         == _         = False
+
+export
+Ord Precision where
+  compare (P m) (P n)         = compare m n
+  compare Unlimited Unlimited = EQ
+  compare Unlimited _         = GT
+  compare _         Unlimited = LT
+
+-- so far, we only support limited precision
+-- unsigned integers
+public export
+data IntKind = Signed Precision | Unsigned Int
+
+public export
+intKind : PrimType -> Maybe IntKind
+intKind IntegerType = Just $ Signed Unlimited
+intKind Int8Type    = Just . Signed   $ P 8
+intKind Int16Type   = Just . Signed   $ P 16
+intKind Int32Type   = Just . Signed   $ P 32
+intKind Int64Type   = Just . Signed   $ P 64
+intKind IntType     = Just . Signed   $ P 64
+intKind Bits8Type   = Just $ Unsigned 8
+intKind Bits16Type  = Just $ Unsigned 16
+intKind Bits32Type  = Just $ Unsigned 32
+intKind Bits64Type  = Just $ Unsigned 64
+intKind _           = Nothing
+
+public export
+precision : IntKind -> Precision
+precision (Signed p)   = p
+precision (Unsigned p) = P p
+
+-- All the internal operators, parameterised by their arity
+public export
+data PrimFn : Nat -> Type where
+     Add : (ty : PrimType) -> PrimFn 2
+     Sub : (ty : PrimType) -> PrimFn 2
+     Mul : (ty : PrimType) -> PrimFn 2
+     Div : (ty : PrimType) -> PrimFn 2
+     Mod : (ty : PrimType) -> PrimFn 2
+     Neg : (ty : PrimType) -> PrimFn 1
+     ShiftL : (ty : PrimType) -> PrimFn 2
+     ShiftR : (ty : PrimType) -> PrimFn 2
+
+     BAnd : (ty : PrimType) -> PrimFn 2
+     BOr : (ty : PrimType) -> PrimFn 2
+     BXOr : (ty : PrimType) -> PrimFn 2
+
+     LT  : (ty : PrimType) -> PrimFn 2
+     LTE : (ty : PrimType) -> PrimFn 2
+     EQ  : (ty : PrimType) -> PrimFn 2
+     GTE : (ty : PrimType) -> PrimFn 2
+     GT  : (ty : PrimType) -> PrimFn 2
+
+     StrLength : PrimFn 1
+     StrHead : PrimFn 1
+     StrTail : PrimFn 1
+     StrIndex : PrimFn 2
+     StrCons : PrimFn 2
+     StrAppend : PrimFn 2
+     StrReverse : PrimFn 1
+     StrSubstr : PrimFn 3
+
+     DoubleExp : PrimFn 1
+     DoubleLog : PrimFn 1
+     DoublePow : PrimFn 2
+     DoubleSin : PrimFn 1
+     DoubleCos : PrimFn 1
+     DoubleTan : PrimFn 1
+     DoubleASin : PrimFn 1
+     DoubleACos : PrimFn 1
+     DoubleATan : PrimFn 1
+     DoubleSqrt : PrimFn 1
+     DoubleFloor : PrimFn 1
+     DoubleCeiling : PrimFn 1
+
+     Cast : PrimType -> PrimType -> PrimFn 1
+     BelieveMe : PrimFn 3
+     Crash : PrimFn 2
+
+%name PrimFn f
+
+export
+Show (PrimFn arity) where
+  show (Add ty) = "+" ++ show ty
+  show (Sub ty) = "-" ++ show ty
+  show (Mul ty) = "*" ++ show ty
+  show (Div ty) = "/" ++ show ty
+  show (Mod ty) = "%" ++ show ty
+  show (Neg ty) = "neg " ++ show ty
+  show (ShiftL ty) = "shl " ++ show ty
+  show (ShiftR ty) = "shr " ++ show ty
+  show (BAnd ty) = "and " ++ show ty
+  show (BOr ty) = "or " ++ show ty
+  show (BXOr ty) = "xor " ++ show ty
+  show (LT ty) = "<" ++ show ty
+  show (LTE ty) = "<=" ++ show ty
+  show (EQ ty) = "==" ++ show ty
+  show (GTE ty) = ">=" ++ show ty
+  show (GT ty) = ">" ++ show ty
+  show StrLength = "op_strlen"
+  show StrHead = "op_strhead"
+  show StrTail = "op_strtail"
+  show StrIndex = "op_strindex"
+  show StrCons = "op_strcons"
+  show StrAppend = "++"
+  show StrReverse = "op_strrev"
+  show StrSubstr = "op_strsubstr"
+  show DoubleExp = "op_doubleExp"
+  show DoubleLog = "op_doubleLog"
+  show DoublePow = "op_doublePow"
+  show DoubleSin = "op_doubleSin"
+  show DoubleCos = "op_doubleCos"
+  show DoubleTan = "op_doubleTan"
+  show DoubleASin = "op_doubleASin"
+  show DoubleACos = "op_doubleACos"
+  show DoubleATan = "op_doubleATan"
+  show DoubleSqrt = "op_doubleSqrt"
+  show DoubleFloor = "op_doubleFloor"
+  show DoubleCeiling = "op_doubleCeiling"
+  show (Cast x y) = "cast-" ++ show x ++ "-" ++ show y
+  show BelieveMe = "believe_me"
+  show Crash = "crash"
+
+export
+prettyOp : PrimFn arity -> Vect arity (Doc IdrisSyntax) -> Doc IdrisSyntax
+prettyOp op@(Add ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "+" <++> v2
+prettyOp op@(Sub ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "-" <++> v2
+prettyOp op@(Mul ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "*" <++> v2
+prettyOp op@(Div ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`div`" <++> v2
+prettyOp op@(Mod ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`mod`" <++> v2
+prettyOp op@(Neg ty) [v] = annotate (Fun $ UN $ Basic $ show op) "-" <++> v
+prettyOp op@(ShiftL ty) [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "shiftl" <++> v1 <++> v2
+prettyOp op@(ShiftR ty) [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "shiftr" <++> v1 <++> v2
+prettyOp op@(BAnd ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "&&" <++> v2
+prettyOp op@(BOr ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "||" <++> v2
+prettyOp op@(BXOr ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`xor`" <++> v2
+prettyOp op@(LT ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "<" <++> v2
+prettyOp op@(LTE ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "<=" <++> v2
+prettyOp op@(EQ ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "==" <++> v2
+prettyOp op@(GTE ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) ">=" <++> v2
+prettyOp op@(GT ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) ">" <++> v2
+prettyOp op@StrLength [v] = annotate (Fun $ UN $ Basic $ show op) "length" <++> v
+prettyOp op@StrHead [v] = annotate (Fun $ UN $ Basic $ show op) "head" <++> v
+prettyOp op@StrTail [v] = annotate (Fun $ UN $ Basic $ show op) "tail" <++> v
+prettyOp op@StrIndex [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "[" <+> v2 <+> annotate (Fun $ UN $ Basic $ show op) "]"
+prettyOp op@StrCons [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "::" <++> v2
+prettyOp op@StrAppend [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "++" <++> v2
+prettyOp op@StrReverse [v] = annotate (Fun $ UN $ Basic $ show op) "reverse" <++> v
+prettyOp op@StrSubstr [v1,v2,v3] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "[" <+> v2 <+> annotate (Fun $ UN $ Basic $ show op) "," <++> v3 <+> annotate (Fun $ UN $ Basic $ show op) "]"
+prettyOp op@DoubleExp [v] = annotate (Fun $ UN $ Basic $ show op) "exp" <++> v
+prettyOp op@DoubleLog [v] = annotate (Fun $ UN $ Basic $ show op) "log" <++> v
+prettyOp op@DoublePow [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`pow`" <++> v2
+prettyOp op@DoubleSin [v] = annotate (Fun $ UN $ Basic $ show op) "sin" <++> v
+prettyOp op@DoubleCos [v] = annotate (Fun $ UN $ Basic $ show op) "cos" <++> v
+prettyOp op@DoubleTan [v] = annotate (Fun $ UN $ Basic $ show op) "tan" <++> v
+prettyOp op@DoubleASin [v] = annotate (Fun $ UN $ Basic $ show op) "asin" <++> v
+prettyOp op@DoubleACos [v] = annotate (Fun $ UN $ Basic $ show op) "acos" <++> v
+prettyOp op@DoubleATan [v] = annotate (Fun $ UN $ Basic $ show op) "atan" <++> v
+prettyOp op@DoubleSqrt [v] = annotate (Fun $ UN $ Basic $ show op) "sqrt" <++> v
+prettyOp op@DoubleFloor [v] = annotate (Fun $ UN $ Basic $ show op) "floor" <++> v
+prettyOp op@DoubleCeiling [v] = annotate (Fun $ UN $ Basic $ show op) "ceiling" <++> v
+prettyOp op@(Cast x y) [v] = annotate (Fun $ UN $ Basic $ show op) "[" <+> pretty x <++> annotate (Fun $ UN $ Basic $ show op) "->" <++> pretty y <+> annotate (Fun $ UN $ Basic $ show op) "]" <++> v
+prettyOp op@BelieveMe [v1,v2,v3] = annotate (Fun $ UN $ Basic $ show op) "believe_me" <++> v1 <++> v2 <++> v3
+prettyOp op@Crash [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "crash" <++> v1 <++> v2
+
+export
+primFnEq : PrimFn a1 -> PrimFn a2 -> Maybe (a1 = a2)
+primFnEq (Add t1) (Add t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (Sub t1) (Sub t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (Mul t1) (Mul t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (Div t1) (Div t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (Mod t1) (Mod t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (Neg t1) (Neg t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (ShiftL t1) (ShiftL t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (ShiftR t1) (ShiftR t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (BAnd t1) (BAnd t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (BOr t1) (BOr t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (BXOr t1) (BXOr t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (LT t1) (LT t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (LTE t1) (LTE t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (EQ t1) (EQ t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (GTE t1) (GTE t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq (GT t1) (GT t2) = if t1 == t2 then Just Refl else Nothing
+primFnEq StrLength StrLength = Just Refl
+primFnEq StrHead StrHead = Just Refl
+primFnEq StrTail StrTail = Just Refl
+primFnEq StrIndex StrIndex = Just Refl
+primFnEq StrCons StrCons = Just Refl
+primFnEq StrAppend StrAppend = Just Refl
+primFnEq StrReverse StrReverse = Just Refl
+primFnEq StrSubstr StrSubstr = Just Refl
+primFnEq DoubleExp DoubleExp = Just Refl
+primFnEq DoubleLog DoubleLog = Just Refl
+primFnEq DoublePow DoublePow = Just Refl
+primFnEq DoubleSin DoubleSin = Just Refl
+primFnEq DoubleCos DoubleCos = Just Refl
+primFnEq DoubleTan DoubleTan = Just Refl
+primFnEq DoubleASin DoubleASin = Just Refl
+primFnEq DoubleACos DoubleACos = Just Refl
+primFnEq DoubleATan DoubleATan = Just Refl
+primFnEq DoubleSqrt DoubleSqrt = Just Refl
+primFnEq DoubleFloor DoubleFloor = Just Refl
+primFnEq DoubleCeiling DoubleCeiling = Just Refl
+primFnEq (Cast f1 t1) (Cast f2 t2) = if f1 == f2 && t1 == t2 then Just Refl else Nothing
+primFnEq BelieveMe BelieveMe = Just Refl
+primFnEq Crash Crash = Just Refl
+primFnEq _ _ = Nothing
+
+export
+primFnCmp : PrimFn a1 -> PrimFn a2 -> Ordering
+primFnCmp (Add t1) (Add t2) = compare t1 t2
+primFnCmp (Sub t1) (Sub t2) = compare t1 t2
+primFnCmp (Mul t1) (Mul t2) = compare t1 t2
+primFnCmp (Div t1) (Div t2) = compare t1 t2
+primFnCmp (Mod t1) (Mod t2) = compare t1 t2
+primFnCmp (Neg t1) (Neg t2) = compare t1 t2
+primFnCmp (ShiftL t1) (ShiftL t2) = compare t1 t2
+primFnCmp (ShiftR t1) (ShiftR t2) = compare t1 t2
+primFnCmp (BAnd t1) (BAnd t2) = compare t1 t2
+primFnCmp (BOr t1) (BOr t2) = compare t1 t2
+primFnCmp (BXOr t1) (BXOr t2) = compare t1 t2
+primFnCmp (LT t1) (LT t2) = compare t1 t2
+primFnCmp (LTE t1) (LTE t2) = compare t1 t2
+primFnCmp (EQ t1) (EQ t2) = compare t1 t2
+primFnCmp (GTE t1) (GTE t2) = compare t1 t2
+primFnCmp (GT t1) (GT t2) = compare t1 t2
+primFnCmp (Cast f1 t1) (Cast f2 t2) = compare f1 f2 `thenCmp` compare t1 t2
+primFnCmp f1 f2 = compare (tag f1) (tag f2)
+  where
+    tag : forall ar. PrimFn ar -> Int
+    tag (Add _) = 0
+    tag (Sub _) = 1
+    tag (Mul _) = 2
+    tag (Div _) = 3
+    tag (Mod _) = 4
+    tag (Neg _) = 5
+    tag (ShiftL _) = 6
+    tag (ShiftR _) = 7
+    tag (BAnd _) = 8
+    tag (BOr _) = 9
+    tag (BXOr _) = 10
+    tag (LT _) = 11
+    tag (LTE _) = 12
+    tag (EQ _) = 13
+    tag (GTE _) = 14
+    tag (GT _) = 15
+    tag StrLength = 16
+    tag StrHead = 17
+    tag StrTail = 18
+    tag StrIndex = 19
+    tag StrCons = 20
+    tag StrAppend = 21
+    tag StrReverse = 22
+    tag StrSubstr = 23
+    tag DoubleExp = 24
+    tag DoubleLog = 25
+    tag DoublePow = 26
+    tag DoubleSin = 27
+    tag DoubleCos = 28
+    tag DoubleTan = 29
+    tag DoubleASin = 30
+    tag DoubleACos = 31
+    tag DoubleATan = 32
+    tag DoubleSqrt = 33
+    tag DoubleFloor = 34
+    tag DoubleCeiling = 35
+    tag (Cast _ _) = 36
+    tag BelieveMe = 37
+    tag Crash = 38

src/Core/TT/Subst.idr

@@ -0,0 +1,52 @@
+module Core.TT.Subst
+
+import Core.Name
+import Core.Name.Scoped
+import Core.TT.Var
+
+%default total
+
+public export
+data Subst : Scoped -> Scope -> Scoped where
+  Nil : Subst tm [] vars
+  (::) : tm vars -> Subst tm ds vars -> Subst tm (d :: ds) vars
+
+namespace Var
+
+  export
+  index : Subst tm ds vars -> Var ds -> tm vars
+  index [] (MkVar p) impossible
+  index (t :: _) (MkVar First) = t
+  index (_ :: ts) (MkVar (Later p)) = index ts (MkVar p)
+
+export
+findDrop :
+  (Var vars -> tm vars) ->
+  SizeOf dropped ->
+  Var (dropped ++ vars) ->
+  Subst tm dropped vars ->
+  tm vars
+findDrop k s var sub = case locateVar s var of
+  Left var => index sub var
+  Right var => k var
+
+export
+find : Weaken tm =>
+       (forall vars. Var vars -> tm vars) ->
+       SizeOf outer -> SizeOf dropped ->
+       Var (outer ++ (dropped ++ vars)) ->
+       Subst tm dropped vars ->
+       tm (outer ++ vars)
+find k outer dropped var sub = case locateVar outer var of
+  Left var => k (embed var)
+  Right var => weakenNs outer (findDrop k dropped var sub)
+
+public export
+0 Substitutable : Scoped -> Scoped -> Type
+Substitutable val tm
+  = {0 outer, dropped, vars : Scope} ->
+    SizeOf outer ->
+    SizeOf dropped ->
+    Subst val dropped vars ->
+    tm (outer ++ (dropped ++ vars)) ->
+    tm (outer ++ vars)

src/Core/TT/Term.idr

@@ -0,0 +1,558 @@
+module Core.TT.Term
+
+import Algebra
+
+import Core.FC
+
+import Core.Name
+import Core.Name.Scoped
+import Core.TT.Binder
+import Core.TT.Primitive
+import Core.TT.Var
+
+import Data.List
+
+%default total
+
+------------------------------------------------------------------------
+-- Name types
+-- This information is cached in Refs (global variables) so as to avoid
+-- too many lookups
+
+public export
+data NameType : Type where
+     Bound   : NameType
+     Func    : NameType
+     DataCon : (tag : Int) -> (arity : Nat) -> NameType
+     TyCon   : (tag : Int) -> (arity : Nat) -> NameType
+
+%name NameType nt
+
+export
+covering
+Show NameType where
+  showPrec d Bound = "Bound"
+  showPrec d Func = "Func"
+  showPrec d (DataCon tag ar) = showCon d "DataCon" $ showArg tag ++ showArg ar
+  showPrec d (TyCon tag ar) = showCon d "TyCon" $ showArg tag ++ showArg ar
+
+export
+isCon : NameType -> Maybe (Int, Nat)
+isCon (DataCon t a) = Just (t, a)
+isCon (TyCon t a) = Just (t, a)
+isCon _ = Nothing
+
+-- Typechecked terms
+-- These are guaranteed to be well-scoped wrt local variables, because they are
+-- indexed by the names of local variables in scope
+public export
+data LazyReason = LInf | LLazy | LUnknown
+
+%name LazyReason lz
+
+-- For as patterns matching linear arguments, select which side is
+-- consumed
+public export
+data UseSide = UseLeft | UseRight
+
+%name UseSide side
+
+public export
+data WhyErased a
+  = Placeholder
+  | Impossible
+  | Dotted a
+
+export
+Show a => Show (WhyErased a) where
+  show Placeholder = "placeholder"
+  show Impossible = "impossible"
+  show (Dotted x) = "dotted \{show x}"
+
+%name WhyErased why
+
+export
+Functor WhyErased where
+  map f Placeholder = Placeholder
+  map f Impossible = Impossible
+  map f (Dotted x) = Dotted (f x)
+
+export
+Foldable WhyErased where
+  foldr c n (Dotted x) = c x n
+  foldr c n _ = n
+
+export
+Traversable WhyErased where
+  traverse f Placeholder = pure Placeholder
+  traverse f Impossible = pure Impossible
+  traverse f (Dotted x) = Dotted <$> f x
+
+
+------------------------------------------------------------------------
+-- Core Terms
+
+public export
+data Term : Scoped where
+     Local : FC -> (isLet : Maybe Bool) ->
+             (idx : Nat) -> (0 p : IsVar name idx vars) -> Term vars
+     Ref : FC -> NameType -> (name : Name) -> Term vars
+     -- Metavariables and the scope they are applied to
+     Meta : FC -> Name -> Int -> List (Term vars) -> Term vars
+     Bind : FC -> (x : Name) ->
+            (b : Binder (Term vars)) ->
+            (scope : Term (x :: vars)) -> Term vars
+     App : FC -> (fn : Term vars) -> (arg : Term vars) -> Term vars
+     -- as patterns; since we check LHS patterns as terms before turning
+     -- them into patterns, this helps us get it right. When normalising,
+     -- we just reduce the inner term and ignore the 'as' part
+     -- The 'as' part should really be a Name rather than a Term, but it's
+     -- easier this way since it gives us the ability to work with unresolved
+     -- names (Ref) and resolved names (Local) without having to define a
+     -- special purpose thing. (But it'd be nice to tidy that up, nevertheless)
+     As : FC -> UseSide -> (as : Term vars) -> (pat : Term vars) -> Term vars
+     -- Typed laziness annotations
+     TDelayed : FC -> LazyReason -> Term vars -> Term vars
+     TDelay : FC -> LazyReason -> (ty : Term vars) -> (arg : Term vars) -> Term vars
+     TForce : FC -> LazyReason -> Term vars -> Term vars
+     PrimVal : FC -> (c : Constant) -> Term vars
+     Erased : FC -> WhyErased (Term vars) -> -- True == impossible term, for coverage checker
+              Term vars
+     TType : FC -> Name -> -- universe variable
+             Term vars
+
+%name Term t, u
+
+public export
+ClosedTerm : Type
+ClosedTerm = Term []
+
+------------------------------------------------------------------------
+-- Weakening
+
+export covering
+insertNames : GenWeakenable Term
+insertNames out ns (Local fc r idx prf)
+   = let MkNVar prf' = insertNVarNames out ns (MkNVar prf) in
+     Local fc r _ prf'
+insertNames out ns (Ref fc nt name) = Ref fc nt name
+insertNames out ns (Meta fc name idx args)
+    = Meta fc name idx (map (insertNames out ns) args)
+insertNames out ns (Bind fc x b scope)
+    = Bind fc x (assert_total (map (insertNames out ns) b))
+           (insertNames (suc out) ns scope)
+insertNames out ns (App fc fn arg)
+    = App fc (insertNames out ns fn) (insertNames out ns arg)
+insertNames out ns (As fc s as tm)
+    = As fc s (insertNames out ns as) (insertNames out ns tm)
+insertNames out ns (TDelayed fc r ty) = TDelayed fc r (insertNames out ns ty)
+insertNames out ns (TDelay fc r ty tm)
+    = TDelay fc r (insertNames out ns ty) (insertNames out ns tm)
+insertNames out ns (TForce fc r tm) = TForce fc r (insertNames out ns tm)
+insertNames out ns (PrimVal fc c) = PrimVal fc c
+insertNames out ns (Erased fc Impossible) = Erased fc Impossible
+insertNames out ns (Erased fc Placeholder) = Erased fc Placeholder
+insertNames out ns (Erased fc (Dotted t)) = Erased fc (Dotted (insertNames out ns t))
+insertNames out ns (TType fc u) = TType fc u
+
+export
+compatTerm : CompatibleVars xs ys -> Term xs -> Term ys
+compatTerm compat tm = believe_me tm -- no names in term, so it's identity
+-- This is how we would define it:
+-- compatTerm CompatPre tm = tm
+-- compatTerm prf (Local fc r idx vprf)
+--     = let MkVar vprf' = compatIsVar prf vprf in
+--           Local fc r _ vprf'
+-- compatTerm prf (Ref fc x name) = Ref fc x name
+-- compatTerm prf (Meta fc n i args)
+--     = Meta fc n i (map (compatTerm prf) args)
+-- compatTerm prf (Bind fc x b scope)
+--     = Bind fc x (map (compatTerm prf) b) (compatTerm (CompatExt prf) scope)
+-- compatTerm prf (App fc fn arg)
+--     = App fc (compatTerm prf fn) (compatTerm prf arg)
+-- compatTerm prf (As fc s as tm)
+--     = As fc s (compatTerm prf as) (compatTerm prf tm)
+-- compatTerm prf (TDelayed fc r ty) = TDelayed fc r (compatTerm prf ty)
+-- compatTerm prf (TDelay fc r ty tm)
+--     = TDelay fc r (compatTerm prf ty) (compatTerm prf tm)
+-- compatTerm prf (TForce fc r x) = TForce fc r (compatTerm prf x)
+-- compatTerm prf (PrimVal fc c) = PrimVal fc c
+-- compatTerm prf (Erased fc i) = Erased fc i
+-- compatTerm prf (TType fc) = TType fc
+
+
+mutual
+  export
+  shrinkPi : Shrinkable (PiInfo . Term)
+  shrinkPi pinfo th
+    = assert_total
+    $ traverse (\ t => shrinkTerm t th) pinfo
+
+  export
+  shrinkBinder : Shrinkable (Binder . Term)
+  shrinkBinder binder th
+    = assert_total
+    $ traverse (\ t => shrinkTerm t th) binder
+
+  export
+  shrinkTerms : Shrinkable (List . Term)
+  shrinkTerms ts th
+    = assert_total
+    $ traverse (\ t => shrinkTerm t th) ts
+
+  shrinkTerm : Shrinkable Term
+  shrinkTerm (Local fc r idx loc) prf
+    = do MkVar loc' <- shrinkIsVar loc prf
+         pure (Local fc r _ loc')
+  shrinkTerm (Ref fc x name) prf = Just (Ref fc x name)
+  shrinkTerm (Meta fc x y xs) prf
+     = do Just (Meta fc x y !(shrinkTerms xs prf))
+  shrinkTerm (Bind fc x b scope) prf
+     = Just (Bind fc x !(shrinkBinder b prf) !(shrinkTerm scope (Keep prf)))
+  shrinkTerm (App fc fn arg) prf
+     = Just (App fc !(shrinkTerm fn prf) !(shrinkTerm arg prf))
+  shrinkTerm (As fc s as tm) prf
+     = Just (As fc s !(shrinkTerm as prf) !(shrinkTerm tm prf))
+  shrinkTerm (TDelayed fc x y) prf
+     = Just (TDelayed fc x !(shrinkTerm y prf))
+  shrinkTerm (TDelay fc x t y) prf
+     = Just (TDelay fc x !(shrinkTerm t prf) !(shrinkTerm y prf))
+  shrinkTerm (TForce fc r x) prf
+     = Just (TForce fc r !(shrinkTerm x prf))
+  shrinkTerm (PrimVal fc c) prf = Just (PrimVal fc c)
+  shrinkTerm (Erased fc Placeholder) prf = Just (Erased fc Placeholder)
+  shrinkTerm (Erased fc Impossible) prf = Just (Erased fc Impossible)
+  shrinkTerm (Erased fc (Dotted t)) prf = Erased fc . Dotted <$> shrinkTerm t prf
+  shrinkTerm (TType fc u) prf = Just (TType fc u)
+
+
+mutual
+  export
+  thinPi : Thinnable (PiInfo . Term)
+  thinPi pinfo th = assert_total $ map (\ t => thinTerm t th) pinfo
+
+  export
+  thinBinder : Thinnable (Binder . Term)
+  thinBinder binder th = assert_total $ map (\ t => thinTerm t th) binder
+
+  export
+  thinTerms : Thinnable (List . Term)
+  thinTerms ts th = assert_total $ map (\ t => thinTerm t th) ts
+
+  thinTerm : Thinnable Term
+  thinTerm (Local fc x idx y) th
+      = let MkVar y' = thinIsVar y th in Local fc x _ y'
+  thinTerm (Ref fc x name) th = Ref fc x name
+  thinTerm (Meta fc x y xs) th
+      = Meta fc x y (thinTerms xs th)
+  thinTerm (Bind fc x b scope) th
+      = Bind fc x (thinBinder b th) (thinTerm scope (Keep th))
+  thinTerm (App fc fn arg) th
+      = App fc (thinTerm fn th) (thinTerm arg th)
+  thinTerm (As fc s nm pat) th
+      = As fc s (thinTerm nm th) (thinTerm pat th)
+  thinTerm (TDelayed fc x y) th = TDelayed fc x (thinTerm y th)
+  thinTerm (TDelay fc x t y) th
+      = TDelay fc x (thinTerm t th) (thinTerm y th)
+  thinTerm (TForce fc r x) th = TForce fc r (thinTerm x th)
+  thinTerm (PrimVal fc c) th = PrimVal fc c
+  thinTerm (Erased fc Impossible) th = Erased fc Impossible
+  thinTerm (Erased fc Placeholder) th = Erased fc Placeholder
+  thinTerm (Erased fc (Dotted t)) th = Erased fc (Dotted (thinTerm t th))
+  thinTerm (TType fc u) th = TType fc u
+
+export
+GenWeaken Term where
+  genWeakenNs = assert_total $ insertNames
+
+export
+%hint
+WeakenTerm : Weaken Term
+WeakenTerm = GenWeakenWeakens
+
+export
+FreelyEmbeddable Term where
+
+export
+IsScoped Term where
+  shrink = shrinkTerm
+  thin = thinTerm
+  compatNs = compatTerm
+
+------------------------------------------------------------------------
+-- Smart constructors
+
+export
+apply : FC -> Term vars -> List (Term vars) -> Term vars
+apply loc fn [] = fn
+apply loc fn (a :: args) = apply loc (App loc fn a) args
+
+-- Creates a chain of `App` nodes, each with its own file context
+export
+applySpineWithFC : Term vars -> SnocList (FC, Term vars) -> Term vars
+applySpineWithFC fn [<] = fn
+applySpineWithFC fn (args :< (fc, arg)) = App fc (applySpineWithFC fn args) arg
+
+-- Creates a chain of `App` nodes, each with its own file context
+export
+applyStackWithFC : Term vars -> List (FC, Term vars) -> Term vars
+applyStackWithFC fn [] = fn
+applyStackWithFC fn ((fc, arg) :: args) = applyStackWithFC (App fc fn arg) args
+
+-- Build a simple function type
+export
+fnType : {vars : _} -> FC -> Term vars -> Term vars -> Term vars
+fnType fc arg scope = Bind emptyFC (MN "_" 0) (Pi fc top Explicit arg) (weaken scope)
+
+export
+linFnType : {vars : _} -> FC -> Term vars -> Term vars -> Term vars
+linFnType fc arg scope = Bind emptyFC (MN "_" 0) (Pi fc linear Explicit arg) (weaken scope)
+
+export
+getFnArgs : Term vars -> (Term vars, List (Term vars))
+getFnArgs tm = getFA [] tm
+  where
+    getFA : List (Term vars) -> Term vars ->
+            (Term vars, List (Term vars))
+    getFA args (App _ f a) = getFA (a :: args) f
+    getFA args tm = (tm, args)
+
+export
+getFn : Term vars -> Term vars
+getFn (App _ f a) = getFn f
+getFn tm = tm
+
+export
+getArgs : Term vars -> (List (Term vars))
+getArgs = snd . getFnArgs
+
+
+------------------------------------------------------------------------
+-- Namespace manipulations
+
+-- Remove/restore the given namespace from all Refs. This is to allow
+-- writing terms and case trees to disk without repeating the same namespace
+-- all over the place.
+public export
+interface StripNamespace a where
+  trimNS : Namespace -> a -> a
+  restoreNS : Namespace -> a -> a
+
+export
+StripNamespace Name where
+  trimNS ns nm@(NS tns n)
+    = if ns == tns then NS emptyNS n else nm
+      -- ^ A blank namespace, rather than a UN, so we don't catch primitive
+      -- names which are represented as UN.
+  trimNS ns nm = nm
+
+  restoreNS ns nm@(NS tns n)
+      = if isNil (unsafeUnfoldNamespace tns)
+            then NS ns n
+            else nm
+  restoreNS ns nm = nm
+
+export covering
+StripNamespace (Term vars) where
+  trimNS ns (Ref fc x nm)
+      = Ref fc x (trimNS ns nm)
+  trimNS ns (Meta fc x y xs)
+      = Meta fc x y (map (trimNS ns) xs)
+  trimNS ns (Bind fc x b scope)
+      = Bind fc x (map (trimNS ns) b) (trimNS ns scope)
+  trimNS ns (App fc fn arg)
+      = App fc (trimNS ns fn) (trimNS ns arg)
+  trimNS ns (As fc s p tm)
+      = As fc s (trimNS ns p) (trimNS ns tm)
+  trimNS ns (TDelayed fc x y)
+      = TDelayed fc x (trimNS ns y)
+  trimNS ns (TDelay fc x t y)
+      = TDelay fc x (trimNS ns t) (trimNS ns y)
+  trimNS ns (TForce fc r y)
+      = TForce fc r (trimNS ns y)
+  trimNS ns tm = tm
+
+  restoreNS ns (Ref fc x nm)
+      = Ref fc x (restoreNS ns nm)
+  restoreNS ns (Meta fc x y xs)
+      = Meta fc x y (map (restoreNS ns) xs)
+  restoreNS ns (Bind fc x b scope)
+      = Bind fc x (map (restoreNS ns) b) (restoreNS ns scope)
+  restoreNS ns (App fc fn arg)
+      = App fc (restoreNS ns fn) (restoreNS ns arg)
+  restoreNS ns (As fc s p tm)
+      = As fc s (restoreNS ns p) (restoreNS ns tm)
+  restoreNS ns (TDelayed fc x y)
+      = TDelayed fc x (restoreNS ns y)
+  restoreNS ns (TDelay fc x t y)
+      = TDelay fc x (restoreNS ns t) (restoreNS ns y)
+  restoreNS ns (TForce fc r y)
+      = TForce fc r (restoreNS ns y)
+  restoreNS ns tm = tm
+
+
+export
+isErased : Term vars -> Bool
+isErased (Erased _ _) = True
+isErased _ = False
+
+export
+getLoc : Term vars -> FC
+getLoc (Local fc _ _ _) = fc
+getLoc (Ref fc _ _) = fc
+getLoc (Meta fc _ _ _) = fc
+getLoc (Bind fc _ _ _) = fc
+getLoc (App fc _ _) = fc
+getLoc (As fc _ _ _) = fc
+getLoc (TDelayed fc _ _) = fc
+getLoc (TDelay fc _ _ _) = fc
+getLoc (TForce fc _ _) = fc
+getLoc (PrimVal fc _) = fc
+getLoc (Erased fc i) = fc
+getLoc (TType fc _) = fc
+
+export
+Eq LazyReason where
+  (==) LInf LInf = True
+  (==) LLazy LLazy = True
+  (==) LUnknown LUnknown = True
+  (==) _ _ = False
+
+export
+Show LazyReason where
+    show LInf = "Inf"
+    show LLazy = "Lazy"
+    show LUnknown = "Unkown"
+
+export
+compatible : LazyReason -> LazyReason -> Bool
+compatible LUnknown _ = True
+compatible _ LUnknown = True
+compatible x y = x == y
+
+export
+total
+Eq a => Eq (WhyErased a) where
+  Placeholder == Placeholder = True
+  Impossible == Impossible = True
+  Dotted t == Dotted u = t == u
+  _ == _ = False
+
+export
+eqWhyErasedBy : (a -> b -> Bool) -> WhyErased a -> WhyErased b -> Bool
+eqWhyErasedBy eq Impossible Impossible = True
+eqWhyErasedBy eq Placeholder Placeholder = True
+eqWhyErasedBy eq (Dotted t) (Dotted u) = eq t u
+eqWhyErasedBy eq _ _ = False
+
+export
+total
+eqTerm : Term vs -> Term vs' -> Bool
+eqTerm (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'
+eqTerm (Ref _ _ n) (Ref _ _ n') = n == n'
+eqTerm (Meta _ _ i args) (Meta _ _ i' args')
+    = i == i' && assert_total (all (uncurry eqTerm) (zip args args'))
+eqTerm (Bind _ _ b sc) (Bind _ _ b' sc')
+    = assert_total (eqBinderBy eqTerm b b') && eqTerm sc sc'
+eqTerm (App _ f a) (App _ f' a') = eqTerm f f' && eqTerm a a'
+eqTerm (As _ _ a p) (As _ _ a' p') = eqTerm a a' && eqTerm p p'
+eqTerm (TDelayed _ _ t) (TDelayed _ _ t') = eqTerm t t'
+eqTerm (TDelay _ _ t x) (TDelay _ _ t' x') = eqTerm t t' && eqTerm x x'
+eqTerm (TForce _ _ t) (TForce _ _ t') = eqTerm t t'
+eqTerm (PrimVal _ c) (PrimVal _ c') = c == c'
+eqTerm (Erased _ i) (Erased _ i') = assert_total (eqWhyErasedBy eqTerm i i')
+eqTerm (TType _ _) (TType _ _) = True
+eqTerm _ _ = False
+
+export
+total
+Eq (Term vars) where
+  (==) = eqTerm
+
+------------------------------------------------------------------------
+-- Scope checking
+
+mutual
+
+  resolveNamesBinder : (vars : List Name) -> Binder (Term vars) -> Binder (Term vars)
+  resolveNamesBinder vars b = assert_total $ map (resolveNames vars) b
+
+  resolveNamesTerms : (vars : List Name) -> List (Term vars) -> List (Term vars)
+  resolveNamesTerms vars ts = assert_total $ map (resolveNames vars) ts
+
+  -- Replace any Ref Bound in a type with appropriate local
+  export
+  resolveNames : (vars : List Name) -> Term vars -> Term vars
+  resolveNames vars (Ref fc Bound name)
+      = case isNVar name vars of
+             Just (MkNVar prf) => Local fc (Just False) _ prf
+             _ => Ref fc Bound name
+  resolveNames vars (Meta fc n i xs)
+      = Meta fc n i (resolveNamesTerms vars xs)
+  resolveNames vars (Bind fc x b scope)
+      = Bind fc x (resolveNamesBinder vars b) (resolveNames (x :: vars) scope)
+  resolveNames vars (App fc fn arg)
+      = App fc (resolveNames vars fn) (resolveNames vars arg)
+  resolveNames vars (As fc s as pat)
+      = As fc s (resolveNames vars as) (resolveNames vars pat)
+  resolveNames vars (TDelayed fc x y)
+      = TDelayed fc x (resolveNames vars y)
+  resolveNames vars (TDelay fc x t y)
+      = TDelay fc x (resolveNames vars t) (resolveNames vars y)
+  resolveNames vars (TForce fc r x)
+      = TForce fc r (resolveNames vars x)
+  resolveNames vars tm = tm
+
+------------------------------------------------------------------------
+-- Showing
+
+export
+withPiInfo : Show t => PiInfo t -> String -> String
+withPiInfo Explicit tm = "(" ++ tm ++ ")"
+withPiInfo Implicit tm = "{" ++ tm ++ "}"
+withPiInfo AutoImplicit tm = "{auto " ++ tm ++ "}"
+withPiInfo (DefImplicit t) tm = "{default " ++ show t ++ " " ++ tm ++ "}"
+
+export
+covering
+{vars : _} -> Show (Term vars) where
+  show tm = let (fn, args) = getFnArgs tm in showApp fn args
+    where
+      showApp : {vars : _} -> Term vars -> List (Term vars) -> String
+      showApp (Local _ c idx p) []
+         = show (nameAt p) ++ "[" ++ show idx ++ "]"
+
+      showApp (Ref _ _ n) [] = show n
+      showApp (Meta _ n _ args) []
+          = "?" ++ show n ++ "_" ++ show args
+      showApp (Bind _ x (Lam _ c info ty) sc) []
+          = "\\" ++ withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++
+            " => " ++ show sc
+      showApp (Bind _ x (Let _ c val ty) sc) []
+          = "let " ++ showCount c ++ show x ++ " : " ++ show ty ++
+            " = " ++ show val ++ " in " ++ show sc
+      showApp (Bind _ x (Pi _ c info ty) sc) []
+          = withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++
+            " -> " ++ show sc
+      showApp (Bind _ x (PVar _ c info ty) sc) []
+          = withPiInfo info ("pat " ++ showCount c ++ show x ++ " : " ++ show ty) ++
+            " => " ++ show sc
+      showApp (Bind _ x (PLet _ c val ty) sc) []
+          = "plet " ++ showCount c ++ show x ++ " : " ++ show ty ++
+            " = " ++ show val ++ " in " ++ show sc
+      showApp (Bind _ x (PVTy _ c ty) sc) []
+          = "pty " ++ showCount c ++ show x ++ " : " ++ show ty ++
+            " => " ++ show sc
+      showApp (App _ _ _) [] = "[can't happen]"
+      showApp (As _ _ n tm) [] = show n ++ "@" ++ show tm
+      showApp (TDelayed _ _ tm) [] = "%Delayed " ++ show tm
+      showApp (TDelay _ _ _ tm) [] = "%Delay " ++ show tm
+      showApp (TForce _ _ tm) [] = "%Force " ++ show tm
+      showApp (PrimVal _ c) [] = show c
+      showApp (Erased _ (Dotted t)) [] = ".(" ++ show t ++ ")"
+      showApp (Erased _ _) [] = "[__]"
+      showApp (TType _ u) [] = "Type"
+      showApp _ [] = "???"
+      showApp f args = "(" ++ assert_total (show f) ++ " " ++
+                        assert_total (showSep " " (map show args))
+                     ++ ")"

src/Core/TT/Term/Subst.idr

@@ -0,0 +1,55 @@
+module Core.TT.Term.Subst
+
+import Core.Name
+import Core.Name.Scoped
+
+import Core.TT.Binder
+import Core.TT.Subst
+import Core.TT.Term
+import Core.TT.Var
+
+%default total
+
+public export
+SubstEnv : Scope -> Scoped
+SubstEnv = Subst Term
+
+substTerm : Substitutable Term Term
+substTerms : Substitutable Term (List . Term)
+substBinder : Substitutable Term (Binder . Term)
+
+substTerm outer dropped env (Local fc r _ prf)
+    = find (\ (MkVar p) => Local fc r _ p) outer dropped (MkVar prf) env
+substTerm outer dropped env (Ref fc x name) = Ref fc x name
+substTerm outer dropped env (Meta fc n i xs)
+    = Meta fc n i (substTerms outer dropped env xs)
+substTerm outer dropped env (Bind fc x b scope)
+    = Bind fc x (substBinder outer dropped env b)
+                (substTerm (suc outer) dropped env scope)
+substTerm outer dropped env (App fc fn arg)
+    = App fc (substTerm outer dropped env fn) (substTerm outer dropped env arg)
+substTerm outer dropped env (As fc s as pat)
+    = As fc s (substTerm outer dropped env as) (substTerm outer dropped env pat)
+substTerm outer dropped env (TDelayed fc x y) = TDelayed fc x (substTerm outer dropped env y)
+substTerm outer dropped env (TDelay fc x t y)
+    = TDelay fc x (substTerm outer dropped env t) (substTerm outer dropped env y)
+substTerm outer dropped env (TForce fc r x) = TForce fc r (substTerm outer dropped env x)
+substTerm outer dropped env (PrimVal fc c) = PrimVal fc c
+substTerm outer dropped env (Erased fc Impossible) = Erased fc Impossible
+substTerm outer dropped env (Erased fc Placeholder) = Erased fc Placeholder
+substTerm outer dropped env (Erased fc (Dotted t)) = Erased fc (Dotted (substTerm outer dropped env t))
+substTerm outer dropped env (TType fc u) = TType fc u
+
+substTerms outer dropped env xs
+  = assert_total $ map (substTerm outer dropped env) xs
+
+substBinder outer dropped env b
+  = assert_total $ map (substTerm outer dropped env) b
+
+export
+substs : SizeOf dropped -> SubstEnv dropped vars -> Term (dropped ++ vars) -> Term vars
+substs dropped env tm = substTerm zero dropped env tm
+
+export
+subst : Term vars -> Term (x :: vars) -> Term vars
+subst val tm = substs (suc zero) [val] tm

src/Core/TT/Var.idr

@@ -0,0 +1,449 @@
+module Core.TT.Var
+
+import Data.Fin
+import Data.List
+import Data.Nat
+import Data.So
+import Data.SnocList
+import Data.Vect
+
+import Core.Name
+import Core.Name.Scoped
+
+import Libraries.Data.SnocList.HasLength
+import Libraries.Data.SnocList.SizeOf
+
+import Libraries.Data.Erased
+
+%default total
+
+------------------------------------------------------------------------
+-- IsVar Predicate
+
+||| IsVar n k ns is a proof that
+||| the name n
+||| is a position k
+||| in the snoclist ns
+public export
+data IsVar : a -> Nat -> List a -> Type where
+     First : IsVar n Z (n :: ns)
+     Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
+
+%name IsVar idx
+
+export
+finIdx : {idx : _} -> (0 prf : IsVar x idx vars) ->
+         Fin (length vars)
+finIdx First = FZ
+finIdx (Later l) = FS (finIdx l)
+
+||| Recover the value pointed at by an IsVar proof
+||| O(n) in the size of the index
+export
+nameAt : {vars : List a} -> {idx : Nat} -> (0 p : IsVar n idx vars) -> a
+nameAt {vars = n :: _} First = n
+nameAt (Later p) = nameAt p
+
+||| Inversion principle for Later
+export
+dropLater : IsVar nm (S idx) (n :: ns) -> IsVar nm idx ns
+dropLater (Later p) = p
+
+export
+0 mkIsVar : HasLength m inner -> IsVar nm m (inner ++ nm :: outer)
+mkIsVar Z = First
+mkIsVar (S x) = Later (mkIsVar x)
+
+export
+0 mkIsVarChiply : HasLength m inner -> IsVar nm m (inner <>> nm :: outer)
+mkIsVarChiply hl
+  = rewrite chipsAsListAppend inner (nm :: outer) in
+    rewrite sym $ plusZeroRightNeutral m in
+    mkIsVar (hlChips hl Z)
+
+||| Compute the remaining scope once the target variable has been removed
+public export
+dropIsVar :
+  (ns : List a) ->
+  {idx : Nat} -> (0 p : IsVar name idx ns) ->
+  List a
+dropIsVar (_ :: xs) First = xs
+dropIsVar (n :: xs) (Later p) = n :: dropIsVar xs p
+
+||| Throw in extra variables on the outer side of the context
+||| This is essentially the identity function
+||| This is slow so we ensure it's only used in a runtime irrelevant manner
+export
+0 embedIsVar : IsVar x idx xs -> IsVar x idx (xs ++ outer)
+embedIsVar First = First
+embedIsVar (Later p) = Later (embedIsVar p)
+
+||| Throw in extra variables on the local end of the context.
+||| This is slow so we ensure it's only used in a runtime irrelevant manner
+export
+0 weakenIsVar : (s : SizeOf ns) -> IsVar x idx xs -> IsVar x (size s + idx) (ns ++ xs)
+weakenIsVar (MkSizeOf Z Z) p =  p
+weakenIsVar (MkSizeOf (S k) (S l)) p =  Later (weakenIsVar (MkSizeOf k l) p)
+
+0 locateIsVarLT :
+  (s : SizeOf local) ->
+  So (idx < size s) ->
+  IsVar x idx (local ++ outer) ->
+  IsVar x idx local
+locateIsVarLT (MkSizeOf Z Z) so v = case v of
+  First impossible
+  Later v impossible
+locateIsVarLT (MkSizeOf (S k) (S l)) so v = case v of
+  First => First
+  Later v => Later (locateIsVarLT (MkSizeOf k l) so v)
+
+0 locateIsVarGE :
+  (s : SizeOf local) ->
+  So (idx >= size s) ->
+  IsVar x idx (local ++ outer) ->
+  IsVar x (idx `minus` size s) outer
+locateIsVarGE (MkSizeOf Z Z) so v = rewrite minusZeroRight idx in v
+locateIsVarGE (MkSizeOf (S k) (S l)) so v = case v of
+  Later v => locateIsVarGE (MkSizeOf k l) so v
+
+export
+locateIsVar : {idx : Nat} -> (s : SizeOf local) ->
+  (0 p : IsVar x idx (local ++ outer)) ->
+  Either (Erased (IsVar x idx local))
+         (Erased (IsVar x (idx `minus` size s) outer))
+locateIsVar s p = case choose (idx < size s) of
+  Left so => Left (MkErased (locateIsVarLT s so p))
+  Right so => Right (MkErased (locateIsVarGE s so p))
+
+------------------------------------------------------------------------
+-- Variable in scope
+
+||| A variable in a scope is a name, a De Bruijn index,
+||| and a proof that the name is at that position in the scope.
+||| Everything but the De Bruijn index is erased.
+public export
+record Var {0 a : Type} (vars : List a) where
+  constructor MkVar
+  {varIdx : Nat}
+  {0 varNm : a}
+  0 varPrf : IsVar varNm varIdx vars
+
+namespace Var
+
+  export
+  later : Var ns -> Var (n :: ns)
+  later (MkVar p) = MkVar (Later p)
+
+  export
+  isLater : Var (n :: vs) -> Maybe (Var vs)
+  isLater (MkVar First) = Nothing
+  isLater (MkVar (Later p)) = Just (MkVar p)
+
+export
+mkVar : SizeOf inner -> Var (inner ++ nm :: outer)
+mkVar (MkSizeOf s p) = MkVar (mkIsVar p)
+
+export
+mkVarChiply : SizeOf inner -> Var (inner <>> nm :: outer)
+mkVarChiply (MkSizeOf s p) = MkVar (mkIsVarChiply p)
+
+||| Generate all variables
+export
+allVars : (vars : Scope) -> List (Var vars)
+allVars = go [<] where
+
+  go : SizeOf local -> (vs : Scope) -> List (Var (local <>> vs))
+  go s [] = []
+  go s (v :: vs) = mkVarChiply s :: go (s :< v) vs
+
+export
+Eq (Var xs) where
+  v == w = varIdx v == varIdx w
+
+
+||| Removing var 0, strengthening all the other ones
+export
+dropFirst : List (Var (n :: vs)) -> List (Var vs)
+dropFirst = List.mapMaybe isLater
+
+||| Manufacturing a thinning from a list of variables to keep
+export
+thinFromVars :
+  (vars : _) -> List (Var vars) ->
+  (newvars ** Thin newvars vars)
+thinFromVars [] els
+    = (_ ** Refl)
+thinFromVars (x :: xs) els
+    = let (vs ** subRest) = thinFromVars xs (dropFirst els) in
+      if MkVar First `elem` els
+        then (x :: vs ** Keep subRest)
+        else (vs ** Drop subRest)
+
+export
+Show (Var ns) where
+  show v = show (varIdx v)
+
+------------------------------------------------------------------------
+-- Named variable in scope
+
+public export
+record NVar {0 a : Type} (nm : a) (vars : List a) where
+  constructor MkNVar
+  {nvarIdx : Nat}
+  0 nvarPrf : IsVar nm nvarIdx vars
+
+namespace NVar
+  export
+  later : NVar nm ns -> NVar nm (n :: ns)
+  later (MkNVar p) = MkNVar (Later p)
+
+  export
+  isLater : NVar nm (n :: ns) -> Maybe (NVar nm ns)
+  isLater (MkNVar First) = Nothing
+  isLater (MkNVar (Later p)) = Just (MkNVar p)
+
+export
+forgetName : NVar nm vars -> Var vars
+forgetName (MkNVar p) = MkVar p
+
+export
+recoverName : (v : Var vars) -> NVar (varNm v) vars
+recoverName (MkVar p) = MkNVar p
+
+export
+mkNVar : SizeOf inner -> NVar nm (inner ++ nm :: outer)
+mkNVar (MkSizeOf s p) = MkNVar (mkIsVar p)
+
+export
+mkNVarChiply : SizeOf inner -> NVar nm (inner <>> nm :: outer)
+mkNVarChiply (MkSizeOf s p) = MkNVar (mkIsVarChiply p)
+
+export
+locateNVar : SizeOf local -> NVar nm (local ++ outer) ->
+             Either (NVar nm local) (NVar nm outer)
+locateNVar s (MkNVar p) = case locateIsVar s p of
+  Left p => Left (MkNVar (runErased p))
+  Right p => Right (MkNVar (runErased p))
+
+public export
+dropNVar : {ns : List a} -> NVar nm ns -> List a
+dropNVar (MkNVar p) = dropIsVar ns p
+
+------------------------------------------------------------------------
+-- Scope checking
+
+export
+isDeBruijn : Nat -> (vars : List Name) -> Maybe (Var vars)
+isDeBruijn Z (_ :: _) = pure (MkVar First)
+isDeBruijn (S k) (_ :: vs) = later <$> isDeBruijn k vs
+isDeBruijn _ _ = Nothing
+
+export
+isNVar : (n : Name) -> (ns : List Name) -> Maybe (NVar n ns)
+isNVar n [] = Nothing
+isNVar n (m :: ms)
+    = case nameEq n m of
+           Nothing   => map later (isNVar n ms)
+           Just Refl => pure (MkNVar First)
+
+export
+isVar : (n : Name) -> (ns : List Name) -> Maybe (Var ns)
+isVar n ns = forgetName <$> isNVar n ns
+
+export
+locateVar : SizeOf local -> Var (local ++ outer) ->
+            Either (Var local) (Var outer)
+locateVar s v  = bimap forgetName forgetName
+  $ locateNVar s (recoverName v)
+
+------------------------------------------------------------------------
+-- Weakening
+
+export
+weakenNVar : SizeOf ns -> NVar name outer -> NVar name (ns ++ outer)
+weakenNVar s (MkNVar {nvarIdx} p)
+  = MkNVar {nvarIdx = plus (size s) nvarIdx} (weakenIsVar s p)
+
+export
+embedNVar : NVar name ns -> NVar name (ns ++ outer)
+embedNVar (MkNVar p) = MkNVar (embedIsVar p)
+
+export
+insertNVar : SizeOf local ->
+             NVar nm (local ++ outer) ->
+             NVar nm (local ++ n :: outer)
+insertNVar p v = case locateNVar p v of
+  Left v => embedNVar v
+  Right v => weakenNVar p (later v)
+
+export
+insertNVarChiply : SizeOf local ->
+  NVar nm (local <>> outer) ->
+  NVar nm (local <>> n :: outer)
+insertNVarChiply p v
+  = rewrite chipsAsListAppend local (n :: outer) in
+    insertNVar (p <>> zero)
+  $ replace {p = NVar nm} (chipsAsListAppend local outer) v
+
+export
+insertNVarNames : GenWeakenable (NVar name)
+insertNVarNames p q v = case locateNVar p v of
+  Left v => embedNVar v
+  Right v =>
+    rewrite appendAssociative local ns outer in
+    weakenNVar (p + q) v
+
+||| The (partial) inverse to insertNVar
+export
+removeNVar : SizeOf local ->
+         NVar nm (local ++ n :: outer) ->
+  Maybe (NVar nm (local ++      outer))
+removeNVar s var = case locateNVar s var of
+  Left v => pure (embedNVar v)
+  Right v => weakenNVar s <$> isLater v
+
+export
+insertVar : SizeOf local ->
+  Var (local ++ outer) ->
+  Var (local ++ n :: outer)
+insertVar p v = forgetName $ insertNVar p (recoverName v)
+
+weakenVar : SizeOf ns -> Var outer -> Var (ns ++ outer)
+weakenVar p v = forgetName $ weakenNVar p (recoverName v)
+
+insertVarNames : GenWeakenable Var
+insertVarNames p q v = forgetName $ insertNVarNames p q (recoverName v)
+
+||| The (partial) inverse to insertVar
+export
+removeVar : SizeOf local ->
+         Var (local ++ n :: outer) ->
+  Maybe (Var (local ++      outer))
+removeVar s var = forgetName <$> removeNVar s (recoverName var)
+
+------------------------------------------------------------------------
+-- Strengthening
+
+export
+strengthenIsVar : {n : Nat} -> (s : SizeOf inner) ->
+  (0 p : IsVar x n (inner ++ vars)) ->
+  Maybe (Erased (IsVar x (n `minus` size s) vars))
+strengthenIsVar s p = case locateIsVar s p of
+  Left _ => Nothing
+  Right p => pure p
+
+strengthenVar : SizeOf inner ->
+  Var (inner ++ vars) -> Maybe (Var vars)
+strengthenVar s (MkVar p)
+  = do MkErased p <- strengthenIsVar s p
+       pure (MkVar p)
+
+strengthenNVar : SizeOf inner ->
+  NVar x (inner ++ vars) -> Maybe (NVar x vars)
+strengthenNVar s (MkNVar p)
+  = do MkErased p <- strengthenIsVar s p
+       pure (MkNVar p)
+
+------------------------------------------------------------------------
+-- Reindexing
+
+0 lookup :
+  CompatibleVars xs ys ->
+  {idx : Nat} ->
+  (0 p : IsVar {a} name idx xs) ->
+  a
+lookup Pre p = name
+lookup (Ext {m} x) First = m
+lookup (Ext x) (Later p) = lookup x p
+
+0 compatIsVar :
+  (ns : CompatibleVars xs ys) ->
+  {idx : Nat} -> (0 p : IsVar name idx xs) ->
+  IsVar (lookup ns p) idx ys
+compatIsVar Pre p = p
+compatIsVar (Ext {n} x) First = First
+compatIsVar (Ext {n} x) (Later p) = Later (compatIsVar x p)
+
+compatVar : CompatibleVars xs ys -> Var xs -> Var ys
+compatVar prf (MkVar p) = MkVar (compatIsVar prf p)
+
+------------------------------------------------------------------------
+-- Thinning
+
+export
+thinIsVar : {idx : Nat} -> (0 p : IsVar name idx xs) ->
+  Thin xs ys -> Var ys
+thinIsVar p Refl = MkVar p
+thinIsVar p (Drop th) = later (thinIsVar p th)
+thinIsVar First (Keep th) = MkVar First
+thinIsVar (Later p) (Keep th) = later (thinIsVar p th)
+
+export
+shrinkIsVar : {idx : Nat} -> (0 p : IsVar name idx xs) ->
+  Thin ys xs -> Maybe (Var ys)
+shrinkIsVar prf Refl = Just (MkVar prf)
+shrinkIsVar First (Drop p) = Nothing
+shrinkIsVar (Later x) (Drop p) = shrinkIsVar x p
+shrinkIsVar First (Keep p) = Just (MkVar First)
+shrinkIsVar (Later x) (Keep p) = later <$> shrinkIsVar x p
+
+------------------------------------------------------------------------
+-- Putting it all together
+
+export
+%hint
+0 FreelyEmbeddableIsVar : FreelyEmbeddable (IsVar x k)
+FreelyEmbeddableIsVar = MkFreelyEmbeddable embedIsVar
+
+export
+GenWeaken (Var {a = Name}) where
+  genWeakenNs = insertVarNames
+
+%hint
+export
+WeakenVar : Weaken (Var {a = Name})
+WeakenVar = GenWeakenWeakens
+
+export
+Strengthen (Var {a = Name}) where
+  strengthenNs = strengthenVar
+
+export
+FreelyEmbeddable (Var {a = Name}) where
+  embed (MkVar p) = MkVar (embedIsVar p)
+
+export
+IsScoped (Var {a = Name}) where
+  compatNs = compatVar
+
+  thin (MkVar p) = thinIsVar p
+  shrink (MkVar p) = shrinkIsVar p
+
+export
+GenWeaken (NVar {a = Name} nm) where
+  genWeakenNs = insertNVarNames
+
+%hint
+export
+WeakenNVar : Weaken (NVar {a = Name} nm)
+WeakenNVar = GenWeakenWeakens
+
+export
+Strengthen (NVar {a = Name} nm) where
+  strengthenNs = strengthenNVar
+
+export
+FreelyEmbeddable (NVar {a = Name} nm) where
+  embed (MkNVar p) = MkNVar (embedIsVar p)
+
+------------------------------------------------------------------------
+-- Corollaries
+
+||| Moving the zeroth variable under a set number of variables
+export
+shiftUnderNs : SizeOf {a = Name} inner ->
+               {idx : _} ->
+               (0 p : IsVar n idx (x :: inner ++ outer)) ->
+               NVar n (inner ++ x :: outer)
+shiftUnderNs s First = weakenNs s (MkNVar First)
+shiftUnderNs s (Later p) = insertNVar s (MkNVar p)

src/Core/Unify.idr

@@ -300,24 +300,30 @@ getVars _ (_ :: xs) = Nothing
 -- Make a sublist representing the variables used in the application.
 -- We'll use this to ensure that local variables which appear in a term
 -- are all arguments to a metavariable application for pattern unification
-toSubVars : (vars : List Name) -> List (Var vars) ->
+toThin : (vars : List Name) -> List (Var vars) ->
-            (newvars ** SubVars newvars vars)
+            (newvars ** Thin newvars vars)
-toSubVars [] xs = ([] ** SubRefl)
+toThin [] xs = ([] ** Refl)
-toSubVars (n :: ns) xs
+toThin (n :: ns) xs
      -- If there's a proof 'First' in 'xs', then 'n' should be kept,
      -- otherwise dropped
      -- (Remember: 'n' might be shadowed; looking for 'First' ensures we
      -- get the *right* proof that the name is in scope!)
-     = let (_ ** svs) = toSubVars ns (dropFirst xs) in
+     = let (_ ** svs) = toThin ns (dropFirst xs) in
            if anyFirst xs
-              then (_ ** KeepCons svs)
+              then (_ ** Keep svs)
-              else (_ ** DropCons svs)
+              else (_ ** Drop svs)
   where
     anyFirst : List (Var (n :: ns)) -> Bool
     anyFirst [] = False
     anyFirst (MkVar First :: xs) = True
     anyFirst (MkVar (Later p) :: xs) = anyFirst xs
 
+-- Update the variable list to point into the sub environment
+-- (All of these will succeed because the Thin we have comes from
+-- the list of variable uses! It's not stated in the type, though.)
+updateVars : List (Var {a = Name} vars) -> Thin newvars vars -> List (Var newvars)
+updateVars vs th = mapMaybe (\ v => shrink v th) vs
+
 {- Applying the pattern unification rule is okay if:
    * Arguments are all distinct local variables
    * The metavariable name doesn't appear in the unifying term
@@ -338,7 +344,7 @@ patternEnv : {auto c : Ref Ctxt Defs} ->
              {vars : _} ->
              Env Term vars -> List (Closure vars) ->
              Core (Maybe (newvars ** (List (Var newvars),
-                                     SubVars newvars vars)))
+                                     Thin newvars vars)))
 patternEnv {vars} env args
     = do defs <- get Ctxt
          empty <- clearDefs defs
@@ -347,18 +353,8 @@ patternEnv {vars} env args
            case getVars [] args' of
              Nothing => Nothing
              Just vs =>
-               let (newvars ** svs) = toSubVars _ vs in
+               let (newvars ** svs) = toThin _ vs in
                  Just (newvars ** (updateVars vs svs, svs))
-  where
-    -- Update the variable list to point into the sub environment
-    -- (All of these will succeed because the SubVars we have comes from
-    -- the list of variable uses! It's not stated in the type, though.)
-    updateVars : List (Var vars) -> SubVars newvars vars -> List (Var newvars)
-    updateVars [] svs = []
-    updateVars (MkVar p :: ps) svs
-        = case subElem p svs of
-               Nothing => updateVars ps svs
-               Just p' => p' :: updateVars ps svs
 
 getVarsTm : List Nat -> List (Term vars) -> Maybe (List (Var vars))
 getVarsTm got [] = Just []
@@ -374,25 +370,15 @@ patternEnvTm : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Env Term vars -> List (Term vars) ->
                Core (Maybe (newvars ** (List (Var newvars),
-                                       SubVars newvars vars)))
+                                       Thin newvars vars)))
 patternEnvTm {vars} env args
     = do defs <- get Ctxt
          empty <- clearDefs defs
          pure $ case getVarsTm [] args of
            Nothing => Nothing
            Just vs =>
-             let (newvars ** svs) = toSubVars _ vs in
+             let (newvars ** svs) = toThin _ vs in
                  Just (newvars ** (updateVars vs svs, svs))
-  where
-    -- Update the variable list to point into the sub environment
-    -- (All of these will succeed because the SubVars we have comes from
-    -- the list of variable uses! It's not stated in the type, though.)
-    updateVars : List (Var vars) -> SubVars newvars vars -> List (Var newvars)
-    updateVars [] svs = []
-    updateVars (MkVar p :: ps) svs
-        = case subElem p svs of
-               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.
@@ -437,9 +423,8 @@ data IVars : List Name -> List Name -> Type where
              IVars (v :: vs) newvars
 
 Weaken (IVars vs) where
-  weaken INil = INil
+  weakenNs s INil = INil
-  weaken (ICons Nothing ts) = ICons Nothing (weaken ts)
+  weakenNs s (ICons t ts) = ICons (weakenNs @{MaybeWeaken} s t) (weakenNs s ts)
-  weaken (ICons (Just t) ts) = ICons (Just (weaken t)) (weaken ts)
 
 getIVars : IVars vs ns -> List (Maybe (Var ns))
 getIVars INil = []
@@ -522,23 +507,20 @@ tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
     isSimple (App _ f a) = noMeta f 6 && noMeta a 3
     isSimple tm = noMeta tm 0
 
-    updateIVar : {v : Nat} ->
+    updateIVar : forall vs, newvars . IVars vs newvars -> Var newvars ->
-                 forall vs, newvars . IVars vs newvars -> (0 p : IsVar nm v newvars) ->
                  Maybe (Var vs)
-    updateIVar {v} (ICons Nothing rest) prf
+    updateIVar (ICons Nothing rest) new
-        = do MkVar prf' <- updateIVar rest prf
+        = later <$> updateIVar rest new
-             Just (MkVar (Later prf'))
+    updateIVar (ICons (Just old) rest) new
-    updateIVar {v} (ICons (Just (MkVar {i} p)) rest) prf
+        = if new == old
-        = if v == i
              then Just (MkVar First)
-             else do MkVar prf' <- updateIVar rest prf
+             else later <$> updateIVar rest new
-                     Just (MkVar (Later prf'))
     updateIVar _ _ = Nothing
 
     updateIVars : {vs, newvars : _} ->
                   IVars vs newvars -> Term newvars -> Maybe (Term vs)
     updateIVars ivs (Local fc r idx p)
-        = do MkVar p' <- updateIVar ivs p
+        = do MkVar p' <- updateIVar ivs (MkVar p)
              Just (Local fc r _ p')
     updateIVars ivs (Ref fc nt n) = pure $ Ref fc nt n
     updateIVars ivs (Meta fc n i args)
@@ -599,7 +581,7 @@ tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
     mkDef vs vars soln (Bind bfc x b@(Let _ c val ty) sc)
        = do mbsc' <- mkDef vs (ICons Nothing vars) soln sc
             flip traverseOpt mbsc' $ \sc' =>
-              case shrinkTerm sc' (DropCons SubRefl) of
+              case shrink sc' (Drop Refl) of
                 Just scs => pure scs
                 Nothing => pure $ Bind bfc x b sc'
     mkDef [] vars soln _
@@ -621,7 +603,7 @@ updateSolution env (Meta fc mname idx args) soln
          case !(patternEnvTm env args) of
               Nothing => pure False
               Just (newvars ** (locs, submv)) =>
-                  case shrinkTerm soln submv of
+                  case shrink soln submv of
                        Nothing => pure False
                        Just stm =>
                           do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
@@ -827,7 +809,7 @@ mutual
               (margs : List (Closure vars)) ->
               (margs' : List (Closure vars)) ->
               List (Var newvars) ->
-              SubVars newvars vars ->
+              Thin newvars vars ->
               (solfull : Term vars) -> -- Original solution
               (soln : Term newvars) -> -- Solution with shrunk environment
               (solnf : NF vars) ->
@@ -918,11 +900,11 @@ mutual
                              postponeS swap loc mode "Can't instantiate" env
                                        (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tmnf
 
-                     case shrinkTerm tm submv of
+                     case shrink tm submv of
                           Just stm => solveOrElsePostpone stm
                           Nothing =>
                             do tm' <- quote defs env tmnf
-                               case shrinkTerm tm' submv of
+                               case shrink tm' submv of
                                     Nothing => postponeS swap loc mode "Can't shrink" env
                                                  (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
                                                  tmnf

src/Core/UnifyState.idr

@@ -17,6 +17,8 @@ import Libraries.Data.IntMap
 import Libraries.Data.NameMap
 import Libraries.Data.WithDefault
 
+import Libraries.Data.SnocList.HasLength
+
 %default covering
 
 public export
@@ -314,90 +316,86 @@ addPolyConstraint fc env arg x@(NApp _ (NMeta _ _ _) _) y
 addPolyConstraint fc env arg x y
     = pure ()
 
+mkLocal : {wkns : SnocList Name} -> FC -> Binder (Term vars) -> Term (wkns <>> x :: (vars ++ done))
+mkLocal fc b = Local fc (Just (isLet b)) _ (mkIsVarChiply (mkHasLength wkns))
+
 mkConstantAppArgs : {vars : _} ->
                     Bool -> FC -> Env Term vars ->
-                    (wkns : List Name) ->
+                    (wkns : SnocList Name) ->
-                    List (Term (wkns ++ (vars ++ done)))
+                    List (Term (wkns <>> (vars ++ done)))
 mkConstantAppArgs lets fc [] wkns = []
 mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns
-    = let rec = mkConstantAppArgs {done} lets fc env (wkns ++ [x]) in
+    = let rec = mkConstantAppArgs {done} lets fc env (wkns :< x) in
           if lets || not (isLet b)
-             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
+             then mkLocal fc b :: rec
-                  rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
+             else rec
-             else rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
 
 mkConstantAppArgsSub : {vars : _} ->
                        Bool -> FC -> Env Term vars ->
-                       SubVars smaller vars ->
+                       Thin smaller vars ->
-                       (wkns : List Name) ->
+                       (wkns : SnocList Name) ->
-                       List (Term (wkns ++ (vars ++ done)))
+                       List (Term (wkns <>> (vars ++ done)))
 mkConstantAppArgsSub lets fc [] p wkns = []
 mkConstantAppArgsSub {done} {vars = x :: xs}
-                        lets fc (b :: env) SubRefl wkns
+                        lets fc (b :: env) Refl wkns
-    = rewrite appendAssociative wkns [x] (xs ++ done) in
+    = mkConstantAppArgs lets fc env (wkns :< x)
-              mkConstantAppArgs lets fc env (wkns ++ [x])
 mkConstantAppArgsSub {done} {vars = x :: xs}
-                        lets fc (b :: env) (DropCons p) wkns
+                        lets fc (b :: env) (Drop p) wkns
-    = rewrite appendAssociative wkns [x] (xs ++ done) in
+    = mkConstantAppArgsSub lets fc env p (wkns :< x)
-              mkConstantAppArgsSub lets fc env p (wkns ++ [x])
 mkConstantAppArgsSub {done} {vars = x :: xs}
-                        lets fc (b :: env) (KeepCons p) wkns
+                        lets fc (b :: env) (Keep p) wkns
-    = let rec = mkConstantAppArgsSub {done} lets fc env p (wkns ++ [x]) in
+    = let rec = mkConstantAppArgsSub {done} lets fc env p (wkns :< x) in
           if lets || not (isLet b)
-             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
+             then mkLocal fc b :: rec
-                  rewrite appendAssociative wkns [x] (xs ++ done) in rec
+             else rec
-             else rewrite appendAssociative wkns [x] (xs ++ done) in rec
 
 mkConstantAppArgsOthers : {vars : _} ->
                           Bool -> FC -> Env Term vars ->
-                          SubVars smaller vars ->
+                          Thin smaller vars ->
-                          (wkns : List Name) ->
+                          (wkns : SnocList Name) ->
-                          List (Term (wkns ++ (vars ++ done)))
+                          List (Term (wkns <>> (vars ++ done)))
 mkConstantAppArgsOthers lets fc [] p wkns = []
 mkConstantAppArgsOthers {done} {vars = x :: xs}
-                        lets fc (b :: env) SubRefl wkns
+                        lets fc (b :: env) Refl wkns
-    = rewrite appendAssociative wkns [x] (xs ++ done) in
+    = mkConstantAppArgsOthers lets fc env Refl (wkns :< x)
-              mkConstantAppArgsOthers lets fc env SubRefl (wkns ++ [x])
 mkConstantAppArgsOthers {done} {vars = x :: xs}
-                        lets fc (b :: env) (KeepCons p) wkns
+                        lets fc (b :: env) (Keep p) wkns
-    = rewrite appendAssociative wkns [x] (xs ++ done) in
+    = mkConstantAppArgsOthers lets fc env p (wkns :< x)
-              mkConstantAppArgsOthers lets fc env p (wkns ++ [x])
 mkConstantAppArgsOthers {done} {vars = x :: xs}
-                        lets fc (b :: env) (DropCons p) wkns
+                        lets fc (b :: env) (Drop p) wkns
-    = let rec = mkConstantAppArgsOthers {done} lets fc env p (wkns ++ [x]) in
+    = let rec = mkConstantAppArgsOthers {done} lets fc env p (wkns :< x) in
           if lets || not (isLet b)
-             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
+             then mkLocal fc b :: rec
-                  rewrite appendAssociative wkns [x] (xs ++ done) in rec
+             else rec
-             else rewrite appendAssociative wkns [x] (xs ++ done) in rec
 
 export
 applyTo : {vars : _} ->
           FC -> Term vars -> Env Term vars -> Term vars
 applyTo fc tm env
-  = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
+  = let args = reverse (mkConstantAppArgs {done = []} False fc env [<]) in
         apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)
 
 export
 applyToFull : {vars : _} ->
               FC -> Term vars -> Env Term vars -> Term vars
 applyToFull fc tm env
-  = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
+  = let args = reverse (mkConstantAppArgs {done = []} True fc env [<]) in
         apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)
 
 export
 applyToSub : {vars : _} ->
              FC -> Term vars -> Env Term vars ->
-             SubVars smaller vars -> Term vars
+             Thin smaller vars -> Term vars
 applyToSub fc tm env sub
-  = let args = reverse (mkConstantAppArgsSub {done = []} True fc env sub []) in
+  = let args = reverse (mkConstantAppArgsSub {done = []} True fc env sub [<]) in
         apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)
 
 export
 applyToOthers : {vars : _} ->
                 FC -> Term vars -> Env Term vars ->
-                SubVars smaller vars -> Term vars
+                Thin smaller vars -> Term vars
 applyToOthers fc tm env sub
-  = let args = reverse (mkConstantAppArgsOthers {done = []} True fc env sub []) in
+  = let args = reverse (mkConstantAppArgsOthers {done = []} True fc env sub [<]) in
         apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)
 
 -- Create a new metavariable with the given name and return type,
@@ -425,7 +423,7 @@ newMetaLets {vars} fc rig env n ty def nocyc lets
          pure (idx, Meta fc n idx envArgs)
   where
     envArgs : List (Term vars)
-    envArgs = let args = reverse (mkConstantAppArgs {done = []} lets fc env []) in
+    envArgs = let args = reverse (mkConstantAppArgs {done = []} lets fc env [<]) in
                   rewrite sym (appendNilRightNeutral vars) in args
 
 export
@@ -471,7 +469,7 @@ newConstant {vars} fc rig env tm ty constrs
          pure (Meta fc cn idx envArgs)
   where
     envArgs : List (Term vars)
-    envArgs = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
+    envArgs = let args = reverse (mkConstantAppArgs {done = []} True fc env [<]) in
                   rewrite sym (appendNilRightNeutral vars) in args
 
 -- Create a new search with the given name and return type,
@@ -493,7 +491,7 @@ newSearch {vars} fc rig depth def env n ty
          pure (idx, Meta fc n idx envArgs)
   where
     envArgs : List (Term vars)
-    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
+    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env [<]) in
                   rewrite sym (appendNilRightNeutral vars) in args
 
 -- Add a hole which stands for a delayed elaborator
@@ -513,7 +511,7 @@ newDelayed {vars} fc rig env n ty
          pure (idx, Meta fc n idx envArgs)
   where
     envArgs : List (Term vars)
-    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
+    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env [<]) in
                   rewrite sym (appendNilRightNeutral vars) in args
 
 export

src/Idris/REPL.idr

@@ -795,7 +795,7 @@ execDecls decls = do
     execDecl decl = do
       i <- desugarDecl [] decl
       inidx <- resolveName (UN $ Basic "[defs]")
-      _ <- newRef EST (initEStateSub inidx [] SubRefl)
+      _ <- newRef EST (initEStateSub inidx [] Refl)
       processLocal [] (MkNested []) [] !getItDecls i
 
 export

src/Libraries/Data/Erased.idr

@@ -0,0 +1,24 @@
+module Libraries.Data.Erased
+
+%default total
+
+public export
+record Erased (a : Type) where
+  constructor MkErased
+  0 runErased : a
+
+export
+Functor Erased where
+  map f (MkErased x) = MkErased (f x)
+
+export
+Applicative Erased where
+  pure x = MkErased x
+  MkErased f <*> MkErased x = MkErased (f x)
+
+join : Erased (Erased a) -> Erased a
+join (MkErased mx) = MkErased (let MkErased x = mx in x)
+
+export
+Monad Erased where
+  mx >>= f = join (f <$> mx)

src/Libraries/Data/List/Extra.idr

@@ -134,3 +134,11 @@ suffixOfBy : (match : a -> b -> Maybe m) ->
 suffixOfBy match left right
   = do (ms, bs) <- Extra.prefixOfBy match (reverse left) (reverse right)
        pure (reverse bs, reverse ms)
+
+export
+lengthDistributesOverAppend
+  : (xs, ys : List a)
+  -> length (xs ++ ys) = length xs + length ys
+lengthDistributesOverAppend [] ys = Refl
+lengthDistributesOverAppend (x :: xs) ys =
+  cong S $ lengthDistributesOverAppend xs ys

src/Libraries/Data/List/HasLength.idr

@@ -0,0 +1,48 @@
+module Libraries.Data.List.HasLength
+
+import Data.Nat
+
+-- TODO: delete in favor of base lib's List.HasLength once next version _after_ v0.6.0 ships.
+public export
+data HasLength : Nat -> List a -> Type where
+  Z : HasLength Z []
+  S : HasLength n as -> HasLength (S n) (a :: as)
+
+-- TODO: Use List.HasLength.sucR from the base lib instead once next version _after_ v0.6.0 ships.
+export
+sucR : HasLength n xs -> HasLength (S n) (xs ++ [x])
+sucR Z     = S Z
+sucR (S n) = S (sucR n)
+
+-- TODO: Use List.HasLength.hasLengthAppend from the base lib instead once next version _after_ v0.6.0 ships.
+export
+hlAppend : HasLength m xs -> HasLength n ys -> HasLength (m + n) (xs ++ ys)
+hlAppend Z ys = ys
+hlAppend (S xs) ys = S (hlAppend xs ys)
+
+-- TODO: Use List.HasLength.hasLength from the base lib instead once next version _after_ v0.6.0 ships.
+export
+mkHasLength : (xs : List a) -> HasLength (length xs) xs
+mkHasLength [] = Z
+mkHasLength (_ :: xs) = S (mkHasLength xs)
+
+-- TODO: Use List.HasLength.take from the base lib instead once next vresion _after_ v0.6.0 ships.
+export
+take : (n : Nat) -> (xs : Stream a) -> HasLength n (take n xs)
+take Z _ = Z
+take (S n) (x :: xs) = S (take n xs)
+
+export
+cast : {ys : _} -> (0 _ : List.length xs = List.length ys) -> HasLength m xs -> HasLength m ys
+cast {ys = []}      eq Z = Z
+cast {ys = y :: ys} eq (S p) = S (cast (injective eq) p)
+
+-- TODO: Delete once version _after_ v0.6.0 ships.
+hlReverseOnto : HasLength m acc -> HasLength n xs -> HasLength (m + n) (reverseOnto acc xs)
+hlReverseOnto p Z = rewrite plusZeroRightNeutral m in p
+hlReverseOnto {n = S n} p (S q) = rewrite sym (plusSuccRightSucc m n) in hlReverseOnto (S p) q
+
+-- TODO: Use List.HasLength.hasLengthReverse from the base lib instead once next version _after_ v0.6.0 ships.
+export
+hlReverse : HasLength m acc -> HasLength m (reverse acc)
+hlReverse = hlReverseOnto Z

src/Libraries/Data/List/LengthMatch.idr

@@ -1,4 +1,4 @@
-module Libraries.Data.LengthMatch
+module Libraries.Data.List.LengthMatch
 
 %default total
 
@@ -19,4 +19,3 @@ export
 lengthsMatch : LengthMatch xs ys -> (length xs) = (length ys)
 lengthsMatch NilMatch = Refl
 lengthsMatch (ConsMatch x) = cong (S) (lengthsMatch x)
-

src/Libraries/Data/List/SizeOf.idr

@@ -0,0 +1,61 @@
+module Libraries.Data.List.SizeOf
+
+import Data.List
+import Libraries.Data.List.HasLength
+
+%default total
+
+public export
+record SizeOf {a : Type} (xs : List a) where
+  constructor MkSizeOf
+  size        : Nat
+  0 hasLength : HasLength size xs
+
+export
+0 theList : SizeOf {a} xs -> List a
+theList _ = xs
+
+public export
+zero : SizeOf []
+zero = MkSizeOf Z Z
+
+public export
+suc : SizeOf as -> SizeOf (a :: as)
+suc (MkSizeOf n p) = MkSizeOf (S n) (S p)
+
+-- ||| suc but from the right
+export
+sucR : SizeOf as -> SizeOf (as ++ [a])
+sucR (MkSizeOf n p) = MkSizeOf (S n) (sucR p)
+
+export
+(+) : SizeOf xs -> SizeOf ys -> SizeOf (xs ++ ys)
+MkSizeOf m p + MkSizeOf n q = MkSizeOf (m + n) (hlAppend p q)
+
+export
+mkSizeOf : (xs : List a) -> SizeOf xs
+mkSizeOf xs = MkSizeOf (length xs) (mkHasLength xs)
+
+export
+reverse : SizeOf xs -> SizeOf (reverse xs)
+reverse (MkSizeOf n p) = MkSizeOf n (hlReverse p)
+
+export
+map : SizeOf xs -> SizeOf (map f xs)
+map (MkSizeOf n p) = MkSizeOf n (cast (sym $ lengthMap xs) p)
+
+export
+take : {n : Nat} -> {0 xs : Stream a} -> SizeOf (take n xs)
+take = MkSizeOf n (take n xs)
+
+namespace SizedView
+
+  public export
+  data SizedView : SizeOf as -> Type where
+    Z : SizedView (MkSizeOf Z Z)
+    S : (n : SizeOf as) -> SizedView (suc {a} n)
+
+export
+sizedView : (p : SizeOf as) -> SizedView p
+sizedView (MkSizeOf Z Z)         = Z
+sizedView (MkSizeOf (S n) (S p)) = S (MkSizeOf n p)

src/Libraries/Data/Ordering/Extra.idr

@@ -0,0 +1,11 @@
+module Libraries.Data.Ordering.Extra
+
+%default total
+
+infixl 5 `thenCmp`
+
+export
+thenCmp : Ordering -> Lazy Ordering -> Ordering
+thenCmp LT _ = LT
+thenCmp EQ o = o
+thenCmp GT _ = GT

src/Libraries/Data/SnocList/HasLength.idr

@@ -0,0 +1,71 @@
+module Libraries.Data.SnocList.HasLength
+
+import Data.Nat
+
+---------------------------------------
+-- horrible hack
+import Libraries.Data.List.HasLength as L
+
+public export
+LHasLength : Nat -> List a -> Type
+LHasLength = L.HasLength
+%hide L.HasLength
+---------------------------------------
+
+public export
+data HasLength : Nat -> SnocList a -> Type where
+  Z : HasLength Z [<]
+  S : HasLength n sa -> HasLength (S n) (sa :< a)
+
+export
+hasLength : HasLength n sx -> length sx === n
+hasLength Z = Refl
+hasLength (S p) = cong S (hasLength p)
+
+export
+sucL : HasLength n sx -> HasLength (S n) ([<x] ++ sx)
+sucL Z     = S Z
+sucL (S n) = S (sucL n)
+
+export
+hlAppend : HasLength m sx -> HasLength n sy -> HasLength (n + m) (sx ++ sy)
+hlAppend sx Z = sx
+hlAppend sx (S sy) = S (hlAppend sx sy)
+
+export
+hlFish : HasLength m sx -> LHasLength n ys -> HasLength (n + m) (sx <>< ys)
+hlFish x Z = x
+hlFish {n = S n} x (S y) = rewrite plusSuccRightSucc n m in hlFish (S x) y
+
+export
+mkHasLength : (sx : SnocList a) -> HasLength (length sx) sx
+mkHasLength [<] = Z
+mkHasLength (sx :< _) = S (mkHasLength sx)
+
+export
+hlChips : HasLength m sx -> LHasLength n ys -> LHasLength (m + n) (sx <>> ys)
+hlChips Z y = y
+hlChips {m = S m} {n} (S x) y
+  = rewrite plusSuccRightSucc m n in
+    hlChips x (S y)
+
+{-
+export
+take : (n : Nat) -> (sx : Stream a) -> HasLength n (take n sx)
+take Z _ = Z
+take (S n) (x :: sx) = S (take n sx)
+-}
+
+export
+cast : {sy : _} -> (0 _ : SnocList.length sx = SnocList.length sy) ->
+       HasLength m sx -> HasLength m sy
+cast {sy = [<]} eq Z = Z
+cast {sy = sy :< _} eq (S p) = S (cast (injective eq) p)
+
+hlReverseOnto : HasLength m acc -> HasLength n sx -> HasLength (m + n) (reverseOnto acc sx)
+hlReverseOnto p Z = rewrite plusZeroRightNeutral m in p
+hlReverseOnto {n = S n} p (S q) = rewrite sym (plusSuccRightSucc m n) in hlReverseOnto (S p) q
+
+export
+hlReverse : HasLength m acc -> HasLength m (reverse acc)
+hlReverse = hlReverseOnto Z

src/Libraries/Data/SnocList/LengthMatch.idr

@@ -0,0 +1,32 @@
+module Libraries.Data.SnocList.LengthMatch
+
+%default total
+
+public export
+data LengthMatch : SnocList a -> SnocList b -> Type where
+     LinMatch : LengthMatch [<] [<]
+     SnocMatch : LengthMatch xs ys -> LengthMatch (xs :< x) (ys :< y)
+
+export
+checkLengthMatch : (xs : SnocList a) -> (ys : SnocList b) ->
+  Maybe (LengthMatch xs ys)
+checkLengthMatch [<] [<] = Just LinMatch
+checkLengthMatch [<] (_ :< _) = Nothing
+checkLengthMatch (_ :< _) [<] = Nothing
+checkLengthMatch (xs :< _) (ys :< _)
+    = Just (SnocMatch !(checkLengthMatch xs ys))
+
+export
+lengthsMatch : LengthMatch xs ys -> (length xs) = (length ys)
+lengthsMatch LinMatch = Refl
+lengthsMatch (SnocMatch x) = cong S (lengthsMatch x)
+
+export
+reverseOnto : LengthMatch sx sy -> LengthMatch sx' sy' ->
+  LengthMatch (reverseOnto sx sx') (reverseOnto sy sy')
+reverseOnto p LinMatch = p
+reverseOnto p (SnocMatch x) = reverseOnto (SnocMatch p) x
+
+export
+reverse : LengthMatch sx sy -> LengthMatch (reverse sx) (reverse sy)
+reverse = reverseOnto LinMatch

src/Libraries/Data/SnocList/SizeOf.idr

@@ -0,0 +1,92 @@
+module Libraries.Data.SnocList.SizeOf
+
+import Data.List
+import Data.SnocList
+import Libraries.Data.List.HasLength
+import Libraries.Data.SnocList.HasLength
+
+---------------------------------------
+-- horrible hack
+import Libraries.Data.List.SizeOf as L
+
+public export
+0 LSizeOf : {0 a : Type} -> List a -> Type
+LSizeOf xs = L.SizeOf xs
+
+%hide L.SizeOf
+---------------------------------------
+
+%default total
+
+public export
+record SizeOf {a : Type} (sx : SnocList a) where
+  constructor MkSizeOf
+  size        : Nat
+  0 hasLength : HasLength size sx
+
+export
+0 theList : SizeOf {a} sx -> SnocList a
+theList _ = sx
+
+public export
+Lin : SizeOf [<]
+Lin = MkSizeOf Z Z
+
+public export
+(:<) : SizeOf as -> (0 a : _) -> SizeOf (as :< a)
+MkSizeOf n p :< _ = MkSizeOf (S n) (S p)
+
+-- ||| suc but from the left
+export
+sucL : SizeOf as -> SizeOf ([<a] ++ as)
+sucL (MkSizeOf n p) = MkSizeOf (S n) (sucL p)
+
+public export
+(<><) : SizeOf {a} sx -> LSizeOf {a} ys -> SizeOf (sx <>< ys)
+MkSizeOf m p <>< MkSizeOf n q = MkSizeOf (n + m) (hlFish p q)
+
+public export
+(<>>) : SizeOf {a} sx -> LSizeOf {a} ys -> LSizeOf (sx <>> ys)
+MkSizeOf m p <>> MkSizeOf n q = MkSizeOf (m + n) (hlChips p q)
+
+export
+cast : LSizeOf {a} xs -> SizeOf {a} (cast xs)
+cast = ([<] <><)
+
+export
+(+) : SizeOf sx -> SizeOf sy -> SizeOf (sx ++ sy)
+MkSizeOf m p + MkSizeOf n q = MkSizeOf (n + m) (hlAppend p q)
+
+export
+mkSizeOf : (sx : SnocList a) -> SizeOf sx
+mkSizeOf sx = MkSizeOf (length sx) (mkHasLength sx)
+
+export
+reverse : SizeOf sx -> SizeOf (reverse sx)
+reverse (MkSizeOf n p) = MkSizeOf n (hlReverse p)
+
+export
+map : SizeOf sx -> SizeOf (map f sx)
+map (MkSizeOf n p) = MkSizeOf n (cast (sym $ lengthMap sx) p) where
+
+  lengthMap : (sx : _) -> SnocList.length (map f sx) === SnocList.length sx
+  lengthMap [<] = Refl
+  lengthMap (sx :< x) = cong S (lengthMap sx)
+
+{-
+export
+take : {n : Nat} -> {0 sx : Stream a} -> SizeOf (take n sx)
+take = MkSizeOf n (take n sx)
+-}
+
+namespace SizedView
+
+  public export
+  data SizedView : SizeOf as -> Type where
+    Z : SizedView [<]
+    S : (n : SizeOf as) -> SizedView (n :< a)
+
+export
+sizedView : (p : SizeOf as) -> SizedView p
+sizedView (MkSizeOf Z Z)         = Z
+sizedView (MkSizeOf (S n) (S p)) = S (MkSizeOf n p)

src/TTImp/Elab.idr

@@ -45,7 +45,7 @@ doPLetRenames ns drops (Bind fc n b sc)
     = case lookup n ns of
            Just (c, n') =>
              Bind fc n' (setMultiplicity b (c `lub` (multiplicity b)))
-                     (doPLetRenames ns (n' :: drops) (renameTop n' sc))
+                     (doPLetRenames ns (n' :: drops) (compat sc))
            Nothing => Bind fc n b (doPLetRenames ns drops sc)
 doPLetRenames ns drops sc = sc
 
@@ -100,7 +100,7 @@ elabTermSub : {inner, vars : _} ->
               {auto o : Ref ROpts REPLOpts} ->
               Int -> ElabMode -> List ElabOpt ->
               NestedNames vars -> Env Term vars ->
-              Env Term inner -> SubVars inner vars ->
+              Env Term inner -> Thin inner vars ->
               RawImp -> Maybe (Glued vars) ->
               Core (Term vars, Glued vars)
 elabTermSub {vars} defining mode opts nest env env' sub tm ty
@@ -222,7 +222,7 @@ elabTerm : {vars : _} ->
            RawImp -> Maybe (Glued vars) ->
            Core (Term vars, Glued vars)
 elabTerm defining mode opts nest env tm ty
-    = elabTermSub defining mode opts nest env env SubRefl tm ty
+    = elabTermSub defining mode opts nest env env Refl tm ty
 
 export
 checkTermSub : {inner, vars : _} ->
@@ -233,7 +233,7 @@ checkTermSub : {inner, vars : _} ->
                {auto o : Ref ROpts REPLOpts} ->
                Int -> ElabMode -> List ElabOpt ->
                NestedNames vars -> Env Term vars ->
-               Env Term inner -> SubVars inner vars ->
+               Env Term inner -> Thin inner vars ->
                RawImp -> Glued vars ->
                Core (Term vars)
 checkTermSub defining mode opts nest env env' sub tm ty
@@ -290,4 +290,4 @@ checkTerm : {vars : _} ->
             RawImp -> Glued vars ->
             Core (Term vars)
 checkTerm defining mode opts nest env tm ty
-    = checkTermSub defining mode opts nest env env SubRefl tm ty
+    = checkTermSub defining mode opts nest env env Refl tm ty

src/TTImp/Elab/Binders.idr

@@ -178,7 +178,7 @@ checkLambda rig_in elabinfo nest env fc rigl info n argTy scope (Just expty_in)
                     (scopev, scopet) <-
                        inScope fc env' (\e' =>
                           check {e=e'} rig elabinfo nest' env' scope
-                                (Just (gnf env' (renameTop n psc))))
+                                (Just (gnf env' (compat psc))))
                     logTermNF "elab.binder" 10 "Lambda type" env exptynf
                     logGlueNF "elab.binder" 10 "Got scope type" env' scopet
 

src/TTImp/Elab/Case.idr

@@ -32,8 +32,8 @@ import Libraries.Data.WithDefault
 
 export
 changeVar : (old : Var vs) -> (new : Var vs) -> Term vs -> Term vs
-changeVar (MkVar {i=x} old) (MkVar new) (Local fc r idx p)
+changeVar old (MkVar new) (Local fc r idx p)
-    = if x == idx
+    = if old == MkVar p
          then Local fc r _ new
          else Local fc r _ p
 changeVar old new (Meta fc nm i args)
@@ -105,7 +105,7 @@ merge : {vs : List Name} ->
         List (Var vs) -> List (Var vs) -> List (Var vs)
 merge [] xs = xs
 merge (v :: vs) xs
-    = merge vs (v :: filter (not . sameVar v) xs)
+    = merge vs (v :: filter (v /=) xs)
 
 -- Extend the list of variables we need in the environment so far, removing
 -- duplicates
@@ -119,10 +119,6 @@ extendNeeded (PLet _ _ ty val) env needed
 extendNeeded b env needed
     = merge (findUsedLocs env (binderType b)) needed
 
-isNeeded : Nat -> List (Var vs) -> Bool
-isNeeded x [] = False
-isNeeded x (MkVar {i} _ :: xs) = x == i || isNeeded x xs
-
 findScrutinee : {vs : _} ->
                 Env Term vs -> RawImp -> Maybe (Var vs)
 findScrutinee {vs = n' :: _} (b :: bs) (IVar loc' n)
@@ -151,7 +147,7 @@ bindCaseLocals fc ((n, mn, envns) :: rest) argns rhs
     getArg (x :: xs) (S k) = getArg xs k
 
     getNameFrom : Var vars -> Name
-    getNameFrom (MkVar {i} _)
+    getNameFrom (MkVar {varIdx = i} _)
         = case getArg argns i of
                Nothing => n
                Just n' => n'
@@ -333,7 +329,7 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp
               RawImp -> List RawImp ->
               List RawImp
     mkSplit Nothing lhs args = reverse (lhs :: args)
-    mkSplit (Just (MkVar {i} prf)) lhs args
+    mkSplit (Just (MkVar {varIdx = i} prf)) lhs args
         = reverse (replace i lhs args)
 
     -- Names used in the pattern we're matching on, so don't bind them

src/TTImp/Elab/Check.idr

@@ -121,7 +121,7 @@ record EState (vars : List Name) where
   -- be considered parametric as far as case expression elaboration goes, and are
   -- the only things that unbound implicits can depend on
   outerEnv : Env Term outer
-  subEnv : SubVars outer vars
+  subEnv : Thin outer vars
   boundNames : List (Name, ImplBinding vars)
                   -- implicit pattern/type variable bindings and the
                   -- term/type they elaborated to
@@ -132,7 +132,7 @@ record EState (vars : List Name) where
                   -- the RHS)
   bindIfUnsolved : List (Name, RigCount,
                           (vars' ** (Env Term vars', PiInfo (Term vars'),
-                                     Term vars', Term vars', SubVars outer vars')))
+                                     Term vars', Term vars', Thin outer vars')))
                   -- names to add as unbound implicits if they are still holes
                   -- when unbound implicits are added
   lhsPatVars : List Name
@@ -160,7 +160,7 @@ data EST : Type where
 
 export
 initEStateSub : {outer : _} ->
-                Int -> Env Term outer -> SubVars outer vars -> EState vars
+                Int -> Env Term outer -> Thin outer vars -> EState vars
 initEStateSub n env sub = MkEState
     { defining = n
     , outerEnv = env
@@ -180,7 +180,7 @@ initEStateSub n env sub = MkEState
 export
 initEState : {vars : _} ->
              Int -> Env Term vars -> EState vars
-initEState n env = initEStateSub n env SubRefl
+initEState n env = initEStateSub n env Refl
 
 export
 saveHole : {auto e : Ref EST (EState vars)} ->
@@ -193,7 +193,7 @@ weakenedEState : {n, vars : _} ->
 weakenedEState {e}
     = do est <- get EST
          eref <- newRef EST $
-                   { subEnv $= DropCons
+                   { subEnv $= Drop
                    , boundNames $= map wknTms
                    , toBind $= map wknTms
                    , linearUsed $= map weaken
@@ -227,8 +227,8 @@ strengthenedEState {n} {vars} c e fc env
                 } est
 
   where
-    dropSub : SubVars xs (y :: ys) -> Core (SubVars xs ys)
+    dropSub : Thin xs (y :: ys) -> Core (Thin xs ys)
-    dropSub (DropCons sub) = pure sub
+    dropSub (Drop sub) = pure sub
     dropSub _ = throw (InternalError "Badly formed weakened environment")
 
     -- Remove any instance of the top level local variable from an
@@ -246,7 +246,7 @@ strengthenedEState {n} {vars} c e fc env
     removeArgVars (Local fc r Z p :: args)
         = removeArgVars args
     removeArgVars (a :: args)
-        = do a' <- shrinkTerm a (DropCons SubRefl)
+        = do a' <- shrink a (Drop Refl)
              args' <- removeArgVars args
              pure (a' :: args')
 
@@ -255,7 +255,7 @@ strengthenedEState {n} {vars} c e fc env
         = case getFnArgs tm of
                (f, args) =>
                    do args' <- removeArgVars args
-                      f' <- shrinkTerm f (DropCons SubRefl)
+                      f' <- shrink f (Drop Refl)
                       pure (apply (getLoc f) f' args')
 
     strTms : Defs -> (Name, ImplBinding (n :: vars)) ->
@@ -263,9 +263,9 @@ strengthenedEState {n} {vars} c e fc env
     strTms defs (f, NameBinding c p x y)
         = do xnf <- normaliseHoles defs env x
              ynf <- normaliseHoles defs env y
-             case (shrinkPi p (DropCons SubRefl),
+             case (shrinkPi p (Drop Refl),
                    removeArg xnf,
-                   shrinkTerm ynf (DropCons SubRefl)) of
+                   shrink ynf (Drop Refl)) of
                (Just p', Just x', Just y') =>
                     pure (f, NameBinding c p' x' y')
                _ => throw (BadUnboundImplicit fc env f y)
@@ -273,10 +273,10 @@ strengthenedEState {n} {vars} c e fc env
         = do xnf <- normaliseHoles defs env x
              ynf <- normaliseHoles defs env y
              znf <- normaliseHoles defs env z
-             case (shrinkPi p (DropCons SubRefl),
+             case (shrinkPi p (Drop Refl),
-                   shrinkTerm xnf (DropCons SubRefl),
+                   shrink xnf (Drop Refl),
-                   shrinkTerm ynf (DropCons SubRefl),
+                   shrink ynf (Drop Refl),
-                   shrinkTerm znf (DropCons SubRefl)) of
+                   shrink znf (Drop Refl)) of
                (Just p', Just x', Just y', Just z') =>
                     pure (f, AsBinding c p' x' y' z')
                _ => throw (BadUnboundImplicit fc env f y)
@@ -321,10 +321,10 @@ concrete defs env _ = pure False
 
 export
 updateEnv : {new : _} ->
-            Env Term new -> SubVars new vars ->
+            Env Term new -> Thin new vars ->
             List (Name, RigCount,
                    (vars' ** (Env Term vars', PiInfo (Term vars'),
-                              Term vars', Term vars', SubVars new vars'))) ->
+                              Term vars', Term vars', Thin new vars'))) ->
             EState vars -> EState vars
 updateEnv env sub bif st
     = { outerEnv := env

src/TTImp/Elab/ImplicitBind.idr

@@ -39,13 +39,13 @@ mkOuterHole loc rig n topenv (Just expty_in)
     = do est <- get EST
          let sub = subEnv est
          expected <- getTerm expty_in
-         case shrinkTerm expected sub of
+         case shrink expected sub of
               -- Can't shrink so rely on unification with expected type later
               Nothing => mkOuterHole loc rig n topenv Nothing
               Just exp' =>
                   do let env = outerEnv est
                      tm <- implBindVar loc rig env n exp'
-                     pure (embedSub sub tm, embedSub sub exp')
+                     pure (thin tm sub, thin exp' sub)
 mkOuterHole loc rig n topenv Nothing
     = do est <- get EST
          let sub = subEnv est
@@ -54,9 +54,9 @@ mkOuterHole loc rig n topenv Nothing
          u <- uniVar loc
          ty <- metaVar loc erased env nm (TType loc u)
          log "elab.implicits" 10 $ "Made metavariable for type of " ++ show n ++ ": " ++ show nm
-         put EST (addBindIfUnsolved nm rig Explicit topenv (embedSub sub ty) (TType loc u) est)
+         put EST (addBindIfUnsolved nm rig Explicit topenv (thin ty sub) (TType loc u) est)
          tm <- implBindVar loc rig env n ty
-         pure (embedSub sub tm, embedSub sub ty)
+         pure (thin tm sub, thin ty sub)
 
 -- Make a hole standing for the pattern variable, which we'll instantiate
 -- with a bound pattern variable later.
@@ -83,23 +83,24 @@ mkPatternHole {vars'} loc rig n topenv imode (Just expty_in)
               Nothing => mkPatternHole loc rig n topenv imode Nothing
               Just exp' =>
                   do tm <- implBindVar loc rig env n exp'
-                     pure (apply loc (embedSub sub tm) (mkArgs sub),
+                     pure (apply loc (thin tm sub) (mkArgs sub),
                            expected,
-                           embedSub sub exp')
+                           thin exp' sub)
   where
-    mkArgs : {vs : _} -> SubVars newvars vs -> List (Term vs)
+    -- TODO: generalise and get rid of (map weaken)
-    mkArgs SubRefl = []
+    mkArgs : {vs : _} -> Thin newvars vs -> List (Term vs)
-    mkArgs (DropCons p) = Local loc Nothing 0 First :: map weaken (mkArgs p)
+    mkArgs Refl = []
+    mkArgs (Drop p) = Local loc Nothing 0 First :: map weaken (mkArgs p)
     mkArgs _ = []
 
     -- This is for the specific situation where we're pattern matching on
     -- function types, which is realistically the only time we'll legitimately
     -- encounter a type variable under a binder
     bindInner : {vs : _} ->
-                Env Term vs -> Term vs -> SubVars newvars vs ->
+                Env Term vs -> Term vs -> Thin newvars vs ->
                 Maybe (Term newvars)
-    bindInner env ty SubRefl = Just ty
+    bindInner env ty Refl = Just ty
-    bindInner {vs = x :: _} (b :: env) ty (DropCons p)
+    bindInner {vs = x :: _} (b :: env) ty (Drop p)
         = bindInner env (Bind loc x b ty) p
     bindInner _ _ _ = Nothing
 
@@ -136,10 +137,10 @@ bindUnsolved {vars} fc elabmode _
   where
     makeBoundVar : {outer, vs : _} ->
                    Name -> RigCount -> PiInfo (Term vs) -> Env Term outer ->
-                   SubVars outer vs -> SubVars outer vars ->
+                   Thin outer vs -> Thin outer vars ->
                    Term vs -> Core (Term vs)
     makeBoundVar n rig p env sub subvars expected
-        = case shrinkTerm expected sub of
+        = case shrink expected sub of
                Nothing => do tmn <- toFullNames expected
                              throw (GenericMsg fc ("Can't bind implicit " ++ show n ++ " of type " ++ show tmn))
                Just exp' =>
@@ -147,14 +148,14 @@ bindUnsolved {vars} fc elabmode _
                        tm <- metaVar fc rig env impn exp'
                        let p' : PiInfo (Term vars) = forgetDef p
                        update EST { toBind $= ((impn, NameBinding rig p'
-                                                        (embedSub subvars tm)
+                                                        (thin tm subvars)
-                                                        (embedSub subvars exp')) ::) }
+                                                        (thin exp' subvars)) ::) }
-                       pure (embedSub sub tm)
+                       pure (thin tm sub)
 
     mkImplicit : {outer : _} ->
-                 Defs -> Env Term outer -> SubVars outer vars ->
+                 Defs -> Env Term outer -> Thin outer vars ->
                  (Name, RigCount, (vars' **
-                     (Env Term vars', PiInfo (Term vars'), Term vars', Term vars', SubVars outer vars'))) ->
+                     (Env Term vars', PiInfo (Term vars'), Term vars', Term vars', Thin outer vars'))) ->
                  Core ()
     mkImplicit defs outerEnv subEnv (n, rig, (vs ** (env, p, tm, exp, sub)))
         = do Just (Hole _ _) <- lookupDefExact n (gamma defs)
@@ -213,7 +214,7 @@ swapVars (TType fc u) = TType fc u
 push : {vs : _} ->
        FC -> (n : Name) -> Binder (Term vs) -> Term (n :: vs) -> Term vs
 push ofc n b tm@(Bind fc (PV x i) (Pi fc' c Implicit ty) sc) -- only push past 'PV's
-    = case shrinkTerm ty (DropCons SubRefl) of
+    = case shrink ty (Drop Refl) of
            Nothing => -- needs explicit pi, do nothing
                       Bind ofc n b tm
            Just ty' => Bind fc (PV x i) (Pi fc' c Implicit ty')
@@ -549,7 +550,7 @@ checkBindHere rig elabinfo nest env fc bindmode tm exp
          let dontbind = map fst (toBind est)
          -- Set the binding environment in the elab state - unbound
          -- implicits should have access to whatever is in scope here
-         put EST (updateEnv env SubRefl [] est)
+         put EST (updateEnv env Refl [] est)
          constart <- getNextEntry
          (tmv, tmt) <- check rig ({ implicitMode := bindmode,
                                     bindingVars := True }

src/TTImp/Elab/Utils.idr

@@ -83,39 +83,39 @@ plicit _ = Explicit
 
 export
 bindNotReq : {vs : _} ->
-             FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->
+             FC -> Int -> Env Term vs -> (sub : Thin pre vs) ->
              List (PiInfo RawImp, Name) ->
              Term vs -> (List (PiInfo RawImp, Name), Term pre)
-bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)
+bindNotReq fc i [] Refl ns tm = (ns, embed tm)
-bindNotReq fc i (b :: env) SubRefl ns tm
+bindNotReq fc i (b :: env) Refl ns tm
    = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
-         (ns', btm) = bindNotReq fc (1 + i) env SubRefl ns tmptm in
+         (ns', btm) = bindNotReq fc (1 + i) env Refl ns tmptm in
          (ns', refToLocal (MN "arg" i) _ btm)
-bindNotReq fc i (b :: env) (KeepCons p) ns tm
+bindNotReq fc i (b :: env) (Keep p) ns tm
    = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
          (ns', btm) = bindNotReq fc (1 + i) env p ns tmptm in
          (ns', refToLocal (MN "arg" i) _ btm)
-bindNotReq {vs = n :: _} fc i (b :: env) (DropCons p) ns tm
+bindNotReq {vs = n :: _} fc i (b :: env) (Drop p) ns tm
    = bindNotReq fc i env p ((plicit b, n) :: ns)
        (Bind fc _ (Pi (binderLoc b) (multiplicity b) Explicit (binderType b)) tm)
 
 export
 bindReq : {vs : _} ->
-          FC -> Env Term vs -> (sub : SubVars pre vs) ->
+          FC -> Env Term vs -> (sub : Thin pre vs) ->
           List (PiInfo RawImp, Name) ->
           Term pre -> Maybe (List (PiInfo RawImp, Name), List Name, ClosedTerm)
-bindReq {vs} fc env SubRefl ns tm
+bindReq {vs} fc env Refl ns tm
     = pure (ns, notLets [] _ env, abstractEnvType fc env tm)
   where
     notLets : List Name -> (vars : List Name) -> Env Term vars -> List Name
     notLets acc [] _ = acc
     notLets acc (v :: vs) (b :: env) = if isLet b then notLets acc vs env
                                        else notLets (v :: acc) vs env
-bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm
+bindReq {vs = n :: _} fc (b :: env) (Keep p) ns tm
     = do b' <- shrinkBinder b p
          bindReq fc env p ((plicit b, n) :: ns)
             (Bind fc _ (Pi (binderLoc b) (multiplicity b) Explicit (binderType b')) tm)
-bindReq fc (b :: env) (DropCons p) ns tm
+bindReq fc (b :: env) (Drop p) ns tm
     = bindReq fc env p ns tm
 
 -- This machinery is to calculate whether any top level argument is used

src/TTImp/Interactive/ExprSearch.idr

@@ -151,7 +151,7 @@ getAllEnv : {vars : _} -> FC ->
 getAllEnv fc done [] = []
 getAllEnv {vars = v :: vs} {done} fc p (b :: env)
    = let rest = getAllEnv fc (sucR p) env
-         MkVar var = weakenVar p (MkVar First)
+         0 var = mkIsVar (hasLength p)
          usable = usableName v in
          if usable
             then (Local fc Nothing _ var,
@@ -504,14 +504,14 @@ searchLocalWith {vars} fc nofn rig opts hints env ((p, pty) :: rest) ty topty
                                 getSuccessful fc rig opts False env ty topty
                                   [(do xtynf <- evalClosure defs xty
                                        findPos defs prf
-                                         (\arg => applyWithFC (Ref fc Func fname)
+                                         (\arg => applyStackWithFC (Ref fc Func fname)
                                                           [(fc1, xtytm),
                                                            (fc2, ytytm),
                                                            (fc, f arg)])
                                          xtynf target),
                                    (do ytynf <- evalClosure defs yty
                                        findPos defs prf
-                                           (\arg => applyWithFC (Ref fc Func sname)
+                                           (\arg => applyStackWithFC (Ref fc Func sname)
                                                           [(fc1, xtytm),
                                                            (fc2, ytytm),
                                                            (fc, f arg)])
@@ -554,7 +554,7 @@ makeHelper fc rig opts env letty targetty ((locapp, ds) :: next)
          helpern <- inCurrentNS helpern_in
          let env' = Lam fc top Explicit letty :: env
          scopeMeta <- metaVar fc top env' helpern
-                             (weaken {n = intn} targetty)
+                             (weaken targetty)
          let scope = toApp scopeMeta
          updateDef helpern (const (Just None))
          -- Apply the intermediate result to the helper function we're
@@ -712,7 +712,7 @@ searchType {vars} fc rig opts hints env topty Z (Bind bfc n b@(Pi fc' c info ty)
             (do defs <- get Ctxt
                 let n' = UN $ Basic !(getArgName defs n [] vars !(nf defs env ty))
                 let env' : Env Term (n' :: _) = b :: env
-                let sc' = renameTop n' sc
+                let sc' = compat sc
                 log "interaction.search" 10 $ "Introduced lambda, search for " ++ show sc'
                 scVal <- searchType fc rig opts hints env' topty Z sc'
                 pure (map (\ (sc, ds) =>

src/TTImp/Interactive/MakeLemma.idr

@@ -50,10 +50,10 @@ getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc)
     = do defs <- get Ctxt
          ty' <- map (map rawName) $ unelab env !(normalise defs env ty)
          let x' = UN $ Basic !(uniqueBasicName defs (map nameRoot vars) (nameRoot x))
-         (sc', ty) <- getArgs (b :: env) k (renameTop x' sc)
+         (sc', ty) <- getArgs (b :: env) k (compat {n = x'} sc)
          -- Don't need to use the name if it's not used in the scope type
          let mn = if c == top
-                       then case shrinkTerm sc (DropCons SubRefl) of
+                       then case shrink sc (Drop Refl) of
                                     Nothing => Just x'
                                     _ => Nothing
                        else Just x'

src/TTImp/PartialEval.idr

@@ -256,7 +256,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk
                  = mapMaybe (\ (x, s) => case s of
                                               Dynamic => Nothing
                                               Static t => Just (x, t)) sargs
-           let peapp = applyWithFC (Ref fc Func pename) (dropSpec 0 staticargs stk)
+           let peapp = applyStackWithFC (Ref fc Func pename) (dropSpec 0 staticargs stk)
            Nothing <- lookupCtxtExact pename (gamma defs)
                | Just _ => -- already specialised
                            do log "specialise" 5 $ "Already specialised " ++ show pename
@@ -297,7 +297,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk
            setFlag fc (Resolved peidx) (PartialEval (specLimits ++ toList reds))
 
            let PMDef pminfo pmargs ct tr pats = definition gdef
-               | _ => pure (applyWithFC (Ref fc Func fn) stk)
+               | _ => pure (applyStackWithFC (Ref fc Func fn) stk)
            logC "specialise" 5 $
                    do inpats <- traverse unelabDef pats
                       pure $ "Attempting to specialise:\n" ++
@@ -305,7 +305,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk
 
            Just newpats <- getSpecPats fc pename fn stk !(nf defs [] (type gdef))
                                        sargs staticargs pats
-                | Nothing => pure (applyWithFC (Ref fc Func fn) stk)
+                | Nothing => pure (applyStackWithFC (Ref fc Func fn) stk)
            log "specialise" 5 $ "New patterns for " ++ show pename ++ ":\n" ++
                     showSep "\n" (map showPat newpats)
            processDecl [InPartialEval] (MkNested []) []
@@ -321,7 +321,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk
                  fn <- toFullNames fn
                  pure "Partial evaluation of \{show fn} failed:\n\{show err}"
               update Ctxt { peFailures $= insert pename () }
-              pure (applyWithFC (Ref fc Func fn) stk))
+              pure (applyStackWithFC (Ref fc Func fn) stk))
   where
 
     identityFlag : List (Nat, ArgMode) -> Nat -> Maybe Nat
@@ -423,13 +423,9 @@ specialise {vars} fc env gdef fn stk
                     Nothing => Just <$> mkSpecDef fc gdef pename sargs fn stk
                     Just _ => pure Nothing
   where
-    dropAll : {vs : _} -> SubVars [] vs
-    dropAll {vs = []} = SubRefl
-    dropAll {vs = v :: vs} = DropCons dropAll
-
     concrete : {vars : _} ->
                Term vars -> Maybe (Term [])
-    concrete tm = shrinkTerm tm dropAll
+    concrete tm = shrink tm none
 
     getSpecArgs : Nat -> List Nat -> List (FC, Term vars) ->
                   Core (Maybe (List (Nat, ArgMode)))
@@ -457,31 +453,31 @@ findSpecs : {vars : _} ->
 findSpecs env stk (Ref fc Func fn)
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact fn (gamma defs)
-              | Nothing => pure (applyWithFC (Ref fc Func fn) stk)
+              | Nothing => pure (applyStackWithFC (Ref fc Func fn) stk)
          Just r <- specialise fc env gdef fn stk
-              | Nothing => pure (applyWithFC (Ref fc Func fn) stk)
+              | Nothing => pure (applyStackWithFC (Ref fc Func fn) stk)
          pure r
 findSpecs env stk (Meta fc n i args)
     = do args' <- traverse (findSpecs env []) args
-         pure $ applyWithFC (Meta fc n i args') stk
+         pure $ applyStackWithFC (Meta fc n i args') stk
 findSpecs env stk (Bind fc x b sc)
     = do b' <- traverse (findSpecs env []) b
          sc' <- findSpecs (b' :: env) [] sc
-         pure $ applyWithFC (Bind fc x b' sc') stk
+         pure $ applyStackWithFC (Bind fc x b' sc') stk
 findSpecs env stk (App fc fn arg)
     = do arg' <- findSpecs env [] arg
          findSpecs env ((fc, arg') :: stk) fn
 findSpecs env stk (TDelayed fc r tm)
     = do tm' <- findSpecs env [] tm
-         pure $ applyWithFC (TDelayed fc r tm') stk
+         pure $ applyStackWithFC (TDelayed fc r tm') stk
 findSpecs env stk (TDelay fc r ty tm)
     = do ty' <- findSpecs env [] ty
          tm' <- findSpecs env [] tm
-         pure $ applyWithFC (TDelay fc r ty' tm') stk
+         pure $ applyStackWithFC (TDelay fc r ty' tm') stk
 findSpecs env stk (TForce fc r tm)
     = do tm' <- findSpecs env [] tm
-         pure $ applyWithFC (TForce fc r tm') stk
+         pure $ applyStackWithFC (TForce fc r tm') stk
-findSpecs env stk tm = pure $ applyWithFC tm stk
+findSpecs env stk tm = pure $ applyStackWithFC tm stk
 
 bName : {auto q : Ref QVar Int} -> String -> Core Name
 bName n
@@ -543,7 +539,7 @@ mutual
                 MkVar (Later isv')
   quoteHead q defs fc bounds env (NRef Bound (MN n i))
       = case findName bounds of
-             Just (MkVar p) => pure $ Local fc Nothing _ (varExtend p)
+             Just (MkVar p) => pure $ Local fc Nothing _ (embedIsVar p)
              Nothing => pure $ Ref fc Bound (MN n i)
     where
       findName : Bounds bound' -> Maybe (Var bound')
@@ -632,10 +628,10 @@ mutual
   quoteGenNF q defs bound env (NApp fc (NRef Func fn) args)
       = do Just gdef <- lookupCtxtExact fn (gamma defs)
                 | Nothing => do args' <- quoteArgsWithFC q defs bound env args
-                                pure $ applyWithFC (Ref fc Func fn) args'
+                                pure $ applyStackWithFC (Ref fc Func fn) args'
            case specArgs gdef of
                 [] => do args' <- quoteArgsWithFC q defs bound env args
-                         pure $ applyWithFC (Ref fc Func fn) args'
+                         pure $ applyStackWithFC (Ref fc Func fn) args'
                 _ => do empty <- clearDefs defs
                         args' <- quoteArgsWithFC q defs bound env args
                         Just r <- specialise fc (extendEnv bound env) gdef fn args'
@@ -643,7 +639,7 @@ mutual
                                   -- can't specialise, keep the arguments
                                   -- unreduced
                                   do args' <- quoteArgsWithFC q empty bound env args
-                                     pure $ applyWithFC (Ref fc Func fn) args'
+                                     pure $ applyStackWithFC (Ref fc Func fn) args'
                         pure r
      where
        extendEnv : Bounds bs -> Env Term vs -> Env Term (bs ++ vs)
@@ -655,13 +651,13 @@ mutual
   quoteGenNF q defs bound env (NApp fc f args)
       = do f' <- quoteHead q defs fc bound env f
            args' <- quoteArgsWithFC q defs bound env args
-           pure $ applyWithFC f' args'
+           pure $ applyStackWithFC f' args'
   quoteGenNF q defs bound env (NDCon fc n t ar args)
       = do args' <- quoteArgsWithFC q defs bound env args
-           pure $ applyWithFC (Ref fc (DataCon t ar) n) args'
+           pure $ applyStackWithFC (Ref fc (DataCon t ar) n) args'
   quoteGenNF q defs bound env (NTCon fc n t ar args)
       = do args' <- quoteArgsWithFC q defs bound env args
-           pure $ applyWithFC (Ref fc (TyCon t ar) n) args'
+           pure $ applyStackWithFC (Ref fc (TyCon t ar) n) args'
   quoteGenNF q defs bound env (NAs fc s n pat)
       = do n' <- quoteGenNF q defs bound env n
            pat' <- quoteGenNF q defs bound env pat
@@ -686,9 +682,9 @@ mutual
            case arg of
                 NDelay fc _ _ arg =>
                    do argNF <- evalClosure defs arg
-                      pure $ applyWithFC !(quoteGenNF q defs bound env argNF) args'
+                      pure $ applyStackWithFC !(quoteGenNF q defs bound env argNF) args'
                 _ => do arg' <- quoteGenNF q defs bound env arg
-                        pure $ applyWithFC (TForce fc r arg') args'
+                        pure $ applyStackWithFC (TForce fc r arg') args'
   quoteGenNF q defs bound env (NPrimVal fc c) = pure $ PrimVal fc c
   quoteGenNF q defs bound env (NErased fc Impossible) = pure $ Erased fc Impossible
   quoteGenNF q defs bound env (NErased fc Placeholder) = pure $ Erased fc Placeholder

src/TTImp/ProcessDef.idr

@@ -231,27 +231,27 @@ recoverableErr defs _ = pure False
 -- should check the RHS, the LHS and its type in that environment,
 -- and a function which turns a checked RHS into a
 -- pattern clause
--- The 'SubVars' proof contains a proof that refers to the *inner* environment,
+-- The 'Thin' proof contains a proof that refers to the *inner* environment,
--- so all the outer things are marked as 'DropCons'
+-- so all the outer things are marked as 'Drop'
 extendEnv : {vars : _} ->
-            Env Term vars -> SubVars inner vars ->
+            Env Term vars -> Thin inner vars ->
             NestedNames vars ->
             Term vars -> Term vars ->
             Core (vars' **
-                    (SubVars inner vars',
+                    (Thin inner vars',
                      Env Term vars', NestedNames vars',
                      Term vars', Term vars'))
 extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n' (PVTy _ _ _) tysc) with (nameEq n n')
   extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n' (PVTy _ _ _) tysc) | Nothing
       = throw (InternalError "Can't happen: names don't match in pattern type")
   extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n (PVTy _ _ _) tysc) | (Just Refl)
-      = extendEnv (PVar fc c pi tmty :: env) (DropCons p) (weaken nest) sc tysc
+      = extendEnv (PVar fc c pi tmty :: env) (Drop p) (weaken nest) sc tysc
 extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n' (PLet _ _ _ _) tysc) with (nameEq n n')
   extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n' (PLet _ _ _ _) tysc) | Nothing
       = throw (InternalError "Can't happen: names don't match in pattern type")
   -- PLet on the left becomes Let on the right, to give it computational force
   extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n (PLet _ _ _ _) tysc) | (Just Refl)
-      = extendEnv (Let fc c tmval tmty :: env) (DropCons p) (weaken nest) sc tysc
+      = extendEnv (Let fc c tmval tmty :: env) (Drop p) (weaken nest) sc tysc
 extendEnv env p nest tm ty
       = pure (_ ** (p, env, nest, tm, ty))
 
@@ -368,7 +368,7 @@ checkLHS : {vars : _} ->
            Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
            FC -> RawImp ->
            Core (RawImp, -- checked LHS with implicits added
-                 (vars' ** (SubVars vars vars',
+                 (vars' ** (Thin vars vars',
                            Env Term vars', NestedNames vars',
                            Term vars', Term vars')))
 checkLHS {vars} trans mult n opts nest env fc lhs_in
@@ -425,7 +425,7 @@ checkLHS {vars} trans mult n opts nest env fc lhs_in
          logTerm "declare.def.lhs" 5 "LHS type" lhsty_lin
          setHoleLHS (bindEnv fc env lhstm_lin)
 
-         ext <- extendEnv env SubRefl nest lhstm_lin lhsty_lin
+         ext <- extendEnv env Refl nest lhstm_lin lhsty_lin
          pure (lhs, ext)
 
 -- Return whether any of the pattern variables are in a trivially empty
@@ -539,9 +539,9 @@ checkClause {vars} mult vis totreq hashit n opts nest env
          logTerm "declare.def.clause.with" 5 "With value type" wvalTy
          log "declare.def.clause.with" 5 $ "Using vars " ++ show wevars
 
-         let Just wval = shrinkTerm wval withSub
+         let Just wval = shrink wval withSub
              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #1")
-         let Just wvalTy = shrinkTerm wvalTy withSub
+         let Just wvalTy = shrink wvalTy withSub
              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #2")
          -- Should the env be normalised too? If the following 'impossible'
          -- error is ever thrown, that might be the cause!
@@ -691,26 +691,26 @@ checkClause {vars} mult vis totreq hashit n opts nest env
 
       pure (wargs ** (scenv, var, binder))
 
-    -- If it's 'KeepCons/SubRefl' in 'outprf', that means it was in the outer
+    -- If it's 'Keep/Refl' in 'outprf', that means it was in the outer
     -- environment so we need to keep it in the same place in the 'with'
-    -- function. Hence, turn it to KeepCons whatever
+    -- function. Hence, turn it to Keep whatever
     keepOldEnv : {0 outer : _} -> {vs : _} ->
-                 (outprf : SubVars outer vs) -> SubVars vs' vs ->
+                 (outprf : Thin outer vs) -> Thin vs' vs ->
-                 (vs'' : List Name ** SubVars vs'' vs)
+                 (vs'' : List Name ** Thin vs'' vs)
-    keepOldEnv {vs} SubRefl p = (vs ** SubRefl)
+    keepOldEnv {vs} Refl p = (vs ** Refl)
-    keepOldEnv {vs} p SubRefl = (vs ** SubRefl)
+    keepOldEnv {vs} p Refl = (vs ** Refl)
-    keepOldEnv (DropCons p) (DropCons p')
+    keepOldEnv (Drop p) (Drop p')
         = let (_ ** rest) = keepOldEnv p p' in
-              (_ ** DropCons rest)
+              (_ ** Drop rest)
-    keepOldEnv (DropCons p) (KeepCons p')
+    keepOldEnv (Drop p) (Keep p')
         = let (_ ** rest) = keepOldEnv p p' in
-              (_ ** KeepCons rest)
+              (_ ** Keep rest)
-    keepOldEnv (KeepCons p) (DropCons p')
+    keepOldEnv (Keep p) (Drop p')
         = let (_ ** rest) = keepOldEnv p p' in
-              (_ ** KeepCons rest)
+              (_ ** Keep rest)
-    keepOldEnv (KeepCons p) (KeepCons p')
+    keepOldEnv (Keep p) (Keep p')
         = let (_ ** rest) = keepOldEnv p p' in
-              (_ ** KeepCons rest)
+              (_ ** Keep rest)
 
     -- Rewrite the clauses in the block to use an updated LHS.
     -- 'drop' is the number of additional with arguments we expect
@@ -735,6 +735,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env
              newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
              pure (ImpossibleClause ploc newlhs)
 
+-- TODO: remove
 nameListEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)
 nameListEq [] [] = Just Refl
 nameListEq (x :: xs) (y :: ys) with (nameEq x y)

src/TTImp/ProcessParams.idr

@@ -19,12 +19,12 @@ import TTImp.TTImp
 %default covering
 
 extend : {extvs : _} ->
-         Env Term extvs -> SubVars vs extvs ->
+         Env Term extvs -> Thin vs extvs ->
          NestedNames extvs ->
          Term extvs ->
-         (vars' ** (SubVars vs vars', Env Term vars', NestedNames vars'))
+         (vars' ** (Thin vs vars', Env Term vars', NestedNames vars'))
 extend env p nest (Bind _ n b@(Pi fc c pi ty) sc)
-    = extend (b :: env) (DropCons p) (weaken nest) sc
+    = extend (b :: env) (Drop p) (weaken nest) sc
 extend env p nest tm = (_ ** (p, env, nest))
 
 export
@@ -48,7 +48,7 @@ processParams {vars} {c} {m} {u} nest env fc ps ds
          u <- uniVar fc
          pty <- checkTerm (-1) InType []
                           nest env pty_imp (gType fc u)
-         let (vs ** (prf, env', nest')) = extend env SubRefl nest pty
+         let (vs ** (prf, env', nest')) = extend env Refl nest pty
          logEnv "declare.param" 5 "Param env" env'
 
          -- Treat the names in the block as 'nested names' so that we expand

src/TTImp/TTImp.idr

@@ -32,12 +32,12 @@ record NestedNames (vars : List Name) where
 
 export
 Weaken NestedNames where
-  weaken (MkNested ns) = MkNested (map wknName ns)
+  weakenNs {ns = wkns} s (MkNested ns) = MkNested (map wknName ns)
     where
       wknName : (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars)) ->
-                (Name, (Maybe Name, List (Var (n :: vars)), FC -> NameType -> Term (n :: vars)))
+                (Name, (Maybe Name, List (Var (wkns ++ vars)), FC -> NameType -> Term (wkns ++ vars)))
       wknName (n, (mn, vars, rep))
-          = (n, (mn, map weaken vars, \fc, nt => weaken (rep fc nt)))
+          = (n, (mn, map (weakenNs s) vars, \fc, nt => weakenNs s (rep fc nt)))
 
 -- replace nested name with full name
 export

src/TTImp/Unelab.idr

@@ -115,13 +115,10 @@ mutual
           = TForce fc r (substVars xs y)
       substVars xs tm = tm
 
-      embedVar : Var vs -> Var (vs ++ more)
-      embedVar (MkVar p) = MkVar (varExtend p)
-
       substArgs : SizeOf vs -> List (List (Var vs), Term vars) -> Term vs -> Term (vs ++ vars)
       substArgs p substs tm =
         let
-          substs' = map (bimap (map $ embedVar {more = vars}) (weakenNs p)) substs
+          substs' = map (bimap (map $ embed {outer = vars}) (weakenNs p)) substs
           tm' = embed tm
         in
           substVars substs' tm'
@@ -245,8 +242,8 @@ mutual
                 NoSugar True =>
                    let x' = uniqueLocal vars x in
                        unelabBinder umode nest fc env x' b
-                                    (renameVars (CompatExt CompatPre) sc) sc'
+                                    (compat sc) sc'
-                                    (renameVars (CompatExt CompatPre) !(getTerm scty))
+                                    (compat !(getTerm scty))
                 _ => unelabBinder umode nest fc env x b sc sc' !(getTerm scty)
     where
       next : Name -> Name