Introduce names in contexts.

Introduce rows for n-ary sums and products.

Remove union types.

1 files changed, 508 insertions, 483 deletions

diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index f6e095c..d80ce77 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -2,60 +2,54 @@ module Inky.Term
 
 import Data.Bool.Decidable
 import Data.DPair
-import Data.List.Elem
 import Data.Maybe.Decidable
-import Data.These
-import Data.Vect
+import Data.List
+import Inky.Context
 import Inky.Thinning
 import Inky.Type
 
--- Redefine so I can prove stuff about it
-%hide
-Prelude.getAt
-
-getAt : Nat -> List a -> Maybe a
-getAt k [] = Nothing
-getAt 0 (x :: xs) = Just x
-getAt (S k) (x :: xs) = getAt k xs
-
 --------------------------------------------------------------------------------
 -- Definition ------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 public export
-data SynthTerm : Nat -> Nat -> Type
+data SynthTerm : (tyCtx, tmCtx : Context ()) -> Type
 public export
-data CheckTerm : Nat -> Nat -> Type
+data CheckTerm : (tyCtx, tmCtx : Context ()) -> Type
 
 data SynthTerm where
-  Var : Fin tm -> SynthTerm ty tm
-  Lit : Nat -> SynthTerm ty tm
-  Suc : CheckTerm ty tm -> SynthTerm ty tm
-  App : SynthTerm ty tm -> List1 (CheckTerm ty tm) -> SynthTerm ty tm
-  Prj : SynthTerm ty tm -> Nat -> SynthTerm ty tm
-  Expand : SynthTerm ty tm -> SynthTerm ty tm
-  Annot : CheckTerm ty tm -> Ty ty -> SynthTerm ty tm
+  Var : Var tmCtx v -> SynthTerm tyCtx tmCtx
+  Lit : Nat -> SynthTerm tyCtx tmCtx
+  Suc : CheckTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx
+  App :
+    SynthTerm tyCtx tmCtx ->
+    (args : List (CheckTerm tyCtx tmCtx)) ->
+    {auto 0 _ : NonEmpty args} ->
+    SynthTerm tyCtx tmCtx
+  Prj : SynthTerm tyCtx tmCtx -> String -> SynthTerm tyCtx tmCtx
+  Expand : SynthTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx
+  Annot : CheckTerm tyCtx tmCtx -> Ty tyCtx () -> SynthTerm tyCtx tmCtx
 
 data CheckTerm where
   Let :
-    SynthTerm ty tm ->
-    CheckTerm ty (S tm) ->
-    CheckTerm ty tm
-  Abs : (k : Nat) -> CheckTerm ty (S k + tm) -> CheckTerm ty tm
-  Inj : Nat -> CheckTerm ty tm -> CheckTerm ty tm
-  Tup : List (CheckTerm ty tm) -> CheckTerm ty tm
+    (x : String) -> SynthTerm tyCtx tmCtx ->
+    CheckTerm tyCtx (tmCtx :< (x :- ())) ->
+    CheckTerm tyCtx tmCtx
+  Abs : (bound : Context ()) -> CheckTerm tyCtx (tmCtx ++ bound) -> CheckTerm tyCtx tmCtx
+  Inj : String -> CheckTerm tyCtx tmCtx -> CheckTerm tyCtx tmCtx
+  Tup : Context (CheckTerm tyCtx tmCtx) -> CheckTerm tyCtx tmCtx
   Case :
-    SynthTerm ty tm ->
-    List (CheckTerm ty (S tm)) ->
-    CheckTerm ty tm
-  Contract : CheckTerm ty tm -> CheckTerm ty tm
+    SynthTerm tyCtx tmCtx ->
+    Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) ->
+    CheckTerm tyCtx tmCtx
+  Contract : CheckTerm tyCtx tmCtx -> CheckTerm tyCtx tmCtx
   Fold :
-    SynthTerm ty tm ->
-    CheckTerm ty (S tm) ->
-    CheckTerm ty tm
+    SynthTerm tyCtx tmCtx ->
+    (x : String) -> CheckTerm tyCtx (tmCtx :< (x :- ())) ->
+    CheckTerm tyCtx tmCtx
   Embed :
-    SynthTerm ty tm ->
-    CheckTerm ty tm
+    SynthTerm tyCtx tmCtx ->
+    CheckTerm tyCtx tmCtx
 
 %name SynthTerm e
 %name CheckTerm t, u, v
@@ -64,639 +58,670 @@ data CheckTerm where
 -- Well Formed -----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
-GetAt : Nat -> List a -> a -> Type
-GetAt k xs x = (n : Elem x xs ** elemToNat n = k)
+-- Lookup name in a row --------------------------------------------------------
+
+GetAt : String -> Row a -> a -> Type
+GetAt x ys y = VarPos (forget ys) x y
 
-CanProject : Ty ty -> List (Ty ty) -> Type
-CanProject (TUnion as) bs = forget as = bs
-CanProject (TProd as) bs = as = bs
-CanProject _ bs = Void
+getAtUnique :
+  (x : String) -> (ys : Row a) ->
+  GetAt x ys y -> GetAt x ys z -> y = z
+getAtUnique x (row :< (x :- b)) Here Here = Refl
+getAtUnique x ((:<) row (x :- a) {fresh}) Here (There pos2) = void $ varPosNotFresh pos2 fresh
+getAtUnique x ((:<) row (x :- b) {fresh}) (There pos1) Here = void $ varPosNotFresh pos1 fresh
+getAtUnique x (row :< (y :- v)) (There pos1) (There pos2) = getAtUnique x row pos1 pos2
+
+getAt : String -> Row a -> Maybe a
+getAt x as = fst <$> remove' x as
+
+0 reflectGetAt : (x : String) -> (ys : Row a) -> GetAt x ys `OnlyWhen` getAt x ys
+reflectGetAt x ys with (reflectRemove x ys) | (remove' x ys)
+  _ | RJust (Evidence fresh prf) | Just (y, _) = RJust (equivVarPos (sym prf) Here)
+  _ | RNothing nprf | _ =
+    RNothing (\y, pos =>
+      nprf (y, snd (removePos ys pos)) $
+      Evidence (removedIsFresh ys pos) (sym $ reflectRemovePos ys pos))
+
+-- Test if we have an arrow ----------------------------------------------------
+
+IsArrow : Ty tyCtx () -> Ty tyCtx () -> Ty tyCtx () -> Type
+IsArrow (TArrow a b) c d = (c = a, d = b)
+IsArrow _ c d = Void
+
+isArrowUnique : (a : Ty tyCtx ()) -> IsArrow a b c -> IsArrow a d e -> (b = d, c = e)
+isArrowUnique (TArrow a b) (Refl, Refl) (Refl, Refl) = (Refl, Refl)
+
+isArrow : Ty tyCtx () -> Maybe (Ty tyCtx (), Ty tyCtx ())
+isArrow (TArrow a b) = Just (a, b)
+isArrow _ = Nothing
+
+reflectIsArrow : (a : Ty tyCtx ()) -> uncurry (IsArrow a) `OnlyWhen` isArrow a
+reflectIsArrow (TArrow a b) = RJust (Refl, Refl)
+reflectIsArrow (TVar i) = RNothing (\(_, _), x => x)
+reflectIsArrow TNat = RNothing (\(_, _), x => x)
+reflectIsArrow (TProd as) = RNothing (\(_, _), x => x)
+reflectIsArrow (TSum as) = RNothing (\(_, _), x => x)
+reflectIsArrow (TFix x a) = RNothing (\(_, _), x => x)
+
+-- Test if we have a product ---------------------------------------------------
+
+IsProduct : Ty tyCtx () -> Row (Ty tyCtx ()) -> Type
+IsProduct (TProd as) bs = bs = as
+IsProduct _ bs = Void
 
-CanInject : Ty ty -> List (Ty ty) -> Type
-CanInject (TUnion as) bs = forget as = bs
-CanInject (TSum as) bs = as = bs
-CanInject _ bs = Void
+isProductUnique : (a : Ty tyCtx ()) -> IsProduct a as -> IsProduct a bs -> as = bs
+isProductUnique (TProd as) Refl Refl = Refl
 
-IsFixpoint : Ty ty -> Ty (S ty) -> Type
-IsFixpoint TNat b = b = TSum [TProd [], TVar FZ]
-IsFixpoint (TFix a) b = a = b
-IsFixpoint _ b = Void
+isProduct : Ty tyCtx () -> Maybe (Row (Ty tyCtx ()))
+isProduct (TProd as) = Just as
+isProduct _ = Nothing
 
-IsArrow : {ty : Nat} -> (k : Nat) -> Ty ty -> Vect k (Ty ty) -> Ty ty -> Type
-IsArrow 0 a as b = (as = [], b = a)
-IsArrow (S k) (TArrow dom cod) as b = (bs ** (as = dom :: bs, IsArrow k cod bs b))
-IsArrow (S k) _ as b = Void
+reflectIsProduct : (a : Ty tyCtx ()) -> IsProduct a `OnlyWhen` isProduct a
+reflectIsProduct (TVar i) = RNothing (\_, x => x)
+reflectIsProduct TNat = RNothing (\_, x => x)
+reflectIsProduct (TArrow a b) = RNothing (\_, x => x)
+reflectIsProduct (TProd as) = RJust Refl
+reflectIsProduct (TSum as) = RNothing (\_, x => x)
+reflectIsProduct (TFix x a) = RNothing (\_, x => x)
 
-IsProduct : Ty ty -> List (Ty ty) -> Type
-IsProduct (TProd as) bs = as = bs
-IsProduct _ bs = Void
+-- Test if we have a sum -------------------------------------------------------
 
-IsSum : Ty ty -> List (Ty ty) -> Type
-IsSum (TSum as) bs = as = bs
+IsSum : Ty tyCtx () -> Row (Ty tyCtx ()) -> Type
+IsSum (TSum as) bs = bs = as
 IsSum _ bs = Void
 
+isSumUnique : (a : Ty tyCtx ()) -> IsSum a as -> IsSum a bs -> as = bs
+isSumUnique (TSum as) Refl Refl = Refl
+
+isSum : Ty tyCtx () -> Maybe (Row (Ty tyCtx ()))
+isSum (TSum as) = Just as
+isSum _ = Nothing
+
+reflectIsSum : (a : Ty tyCtx ()) -> IsSum a `OnlyWhen` isSum a
+reflectIsSum (TVar i) = RNothing (\_, x => x)
+reflectIsSum TNat = RNothing (\_, x => x)
+reflectIsSum (TArrow a b) = RNothing (\_, x => x)
+reflectIsSum (TProd as) = RNothing (\_, x => x)
+reflectIsSum (TSum as) = RJust Refl
+reflectIsSum (TFix x a) = RNothing (\_, x => x)
+
+-- Test if we have a fixpoint --------------------------------------------------
+
+IsFixpoint : Ty tyCtx () -> (x ** Ty (tyCtx :< (x :- ())) ()) -> Type
+IsFixpoint TNat yb = (fst yb = "X", snd yb = TSum [<"Z" :- TProd [<], "S" :- TVar (%% fst yb)])
+IsFixpoint (TFix x a) yb = (prf : (fst yb = x) ** (snd yb = (rewrite prf in a)))
+IsFixpoint _ yb = Void
+
+isFixpointUnique : (a : Ty tyCtx ()) -> IsFixpoint a xb -> IsFixpoint a yc -> xb = yc
+isFixpointUnique TNat {xb = (_ ** _), yc = (_ ** _)} (Refl, Refl) (Refl, Refl) = Refl
+isFixpointUnique (TFix x a) {xb = (x ** a), yc = (x ** a)} (Refl ** Refl) (Refl ** Refl) = Refl
+
+isFixpoint : Ty tyCtx () -> Maybe (x ** Ty (tyCtx :< (x :- ())) ())
+isFixpoint TNat = Just ("X" ** TSum [<("Z" :- TProd [<]), ("S" :- TVar (%% "X"))])
+isFixpoint (TFix x a) = Just (x ** a)
+isFixpoint _ = Nothing
+
+reflectIsFixpoint : (a : Ty tyCtx ()) -> IsFixpoint a `OnlyWhen` isFixpoint a
+reflectIsFixpoint (TVar i) = RNothing (\_, x => x)
+reflectIsFixpoint TNat = RJust (Refl, Refl)
+reflectIsFixpoint (TArrow a b) = RNothing (\_, x => x)
+reflectIsFixpoint (TProd as) = RNothing (\_, x => x)
+reflectIsFixpoint (TSum as) = RNothing (\_, x => x)
+reflectIsFixpoint (TFix x a) = RJust (Refl ** Refl)
+
+-- Test if we have a function, collecting the bound types ----------------------
+
+IsFunction :
+  {tyCtx : Context ()} ->
+  (bound : Context ()) -> (fun : Ty tyCtx ()) ->
+  (dom : All (const $ Ty tyCtx ()) bound) -> (cod : Ty tyCtx ()) ->
+  Type
+IsFunction [<] fun dom cod = (dom = [<], cod = fun)
+IsFunction (bound :< (x :- ())) fun dom cod =
+  ( b ** c **
+  ( IsArrow fun b c
+  , ( dom' **
+    ( dom = dom' :< (x :- b)
+    , IsFunction bound c dom' cod
+    ))
+  ))
+
+
+isFunctionUnique :
+  (bound : Context ()) -> (a : Ty tyCtx ()) ->
+  forall dom1, dom2, cod1, cod2.
+  IsFunction bound a dom1 cod1 -> IsFunction bound a dom2 cod2 -> (dom1 = dom2, cod1 = cod2)
+isFunctionUnique [<] a (Refl, Refl) (Refl, Refl) = (Refl, Refl)
+isFunctionUnique (bound :< (x :- ())) a
+  (b1 ** c1 ** (isArrow1, (dom1' ** (Refl, isFunc1))))
+  (b2 ** c2 ** (isArrow2, (dom2' ** (Refl, isFunc2))))
+  with (isArrowUnique a isArrow1 isArrow2)
+  isFunctionUnique (bound :< (x :- ())) a
+    (b ** c ** (_, (dom1' ** (Refl, isFunc1))))
+    (b ** c ** (_, (dom2' ** (Refl, isFunc2))))
+    | (Refl, Refl)
+    with (isFunctionUnique bound c isFunc1 isFunc2)
+    isFunctionUnique (bound :< (x :- ())) a
+      (b ** c ** (_, (dom' ** (Refl, _))))
+      (b ** c ** (_, (dom' ** (Refl, _))))
+      | (Refl, Refl) | (Refl, Refl) = (Refl, Refl)
+
+isFunction :
+  (bound : Context ()) -> Ty tyCtx () ->
+  Maybe (All (const $ Ty tyCtx ()) bound, Ty tyCtx ())
+isFunction [<] a = Just ([<], a)
+isFunction (bound :< (x :- ())) a = do
+  (b, c) <- isArrow a
+  (dom, cod) <- isFunction bound c
+  Just (dom :< (x :- b), cod)
+
+reflectIsFunction :
+  (bound : Context ()) -> (a : Ty tyCtx ()) ->
+  uncurry (IsFunction bound a) `OnlyWhen` isFunction bound a
+reflectIsFunction [<] a = RJust (Refl, Refl)
+reflectIsFunction (bound :< (x :- ())) a with (reflectIsArrow a) | (isArrow a)
+  _ | RJust isArrow | Just (b, c) with (reflectIsFunction bound c) | (isFunction bound c)
+    _ | RJust isFunc | Just (dom, cod) = RJust (b ** c ** (isArrow , (dom ** (Refl, isFunc))))
+    _ | RNothing notFunc | _ =
+      RNothing (\(dom :< (x :- b'), cod), (b' ** c' ** (isArrow', (dom ** (Refl, isFunc)))) =>
+        let (eq1, eq2) = isArrowUnique a {b, c, d = b', e = c'} isArrow isArrow' in
+        let isFunc = rewrite eq2 in isFunc in
+        notFunc (dom, cod) isFunc)
+  _ | RNothing notArrow | _ =
+    RNothing (\(dom, cod), (b ** c ** (isArrow, _)) => notArrow (b, c) isArrow)
+
+-- Full type checking and synthesis --------------------------------------------
+
 Synths :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
-  SynthTerm ty tm -> Ty ty -> Type
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  SynthTerm tyCtx tmCtx -> Ty tyCtx () -> Type
 Checks :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
-  Ty ty -> CheckTerm ty tm -> Type
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Type
 CheckSpine :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
-  (fun : Ty ty) -> List (CheckTerm ty tm) -> (res : Ty ty) -> Type
-CheckSpine1 :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
-  (fun : Ty ty) -> List1 (CheckTerm ty tm) -> (res : Ty ty) -> Type
-AllCheck : {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> List (Ty ty) -> List (CheckTerm ty tm) -> Type
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> (res : Ty tyCtx ()) -> Type
+AllCheck :
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Row (Ty tyCtx ()) -> Context (CheckTerm tyCtx tmCtx) -> Type
 AllCheckBinding :
-  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> List (Ty ty) -> Ty ty -> List (CheckTerm ty (S tm)) -> Type
-
-Synths ctx (Var i) a = (a = index i ctx)
-Synths ctx (Lit k) a = (a = TNat)
-Synths ctx (Suc t) a = (Checks ctx TNat t, a = TNat)
-Synths ctx (App e ts) a =
+  {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Row (Ty tyCtx ()) -> Ty tyCtx () ->
+  Context (x : String ** CheckTerm tyCtx (tmCtx :< (x :- ()))) ->
+  Type
+
+Synths env (Var i) a = (a = indexAll i env)
+Synths env (Lit k) a = (a = TNat)
+Synths env (Suc t) a = (Checks env TNat t, a = TNat)
+Synths env (App e ts) a =
   ( fun **
-  ( Synths ctx e fun
-  , CheckSpine1 ctx fun ts a
+  ( Synths env e fun
+  , CheckSpine env fun ts a
   ))
-Synths ctx (Prj e k) a =
+Synths env (Prj e x) a =
   ( b **
-  ( Synths ctx e b
+  ( Synths env e b
   , ( as **
-    ( CanProject b as
-    , GetAt k as a
+    ( IsProduct b as
+    , GetAt x as a
     ))
   ))
-Synths ctx (Expand e) a =
+Synths env (Expand e) a =
   ( b **
-  ( Synths ctx e b
-  , ( c **
-    ( IsFixpoint b c
-    , a = sub (Base Id :< b) c))
+  ( Synths env e b
+  , ( xc **
+    ( IsFixpoint b xc
+    , a = sub (Base Id :< (fst xc :- b)) (snd xc)
+    ))
   ))
-Synths ctx (Annot t a) b =
+Synths env (Annot t a) b =
   ( Not (IllFormed a)
-  , Checks ctx a t
+  , Checks env a t
   , a = b
   )
 
-Checks ctx a (Let e t) =
+Checks env a (Let x e t) =
   ( b **
-  ( Synths ctx e b
-  , Checks (b :: ctx) a t
+  ( Synths env e b
+  , Checks (env :< (x :- b)) a t
   ))
-Checks ctx a (Abs k t) =
-  ( as : Vect (S k) _ ** b **
-  ( IsArrow (S k) a as b
-  , Checks (as ++ ctx) b t
+Checks env a (Abs bound t) =
+  ( as ** b **
+  ( IsFunction bound a as b
+  , Checks (env ++ as) b t
   ))
-Checks ctx a (Inj k t) =
+Checks env a (Inj x t) =
   ( as **
-  ( CanInject a as
+  ( IsSum a as
   , ( b **
-    ( GetAt k as b
-    , Checks ctx b t
+    ( GetAt x as b
+    , Checks env b t
     ))
   ))
-Checks ctx a (Tup ts) =
+Checks env a (Tup ts) =
   ( as **
   ( IsProduct a as
-  , AllCheck ctx as ts
+  , AllCheck env as ts
   ))
-Checks ctx a (Case e ts) =
+Checks env a (Case e ts) =
   ( b **
-  ( Synths ctx e b
+  ( Synths env e b
   , ( as **
     ( IsSum b as
-    , AllCheckBinding ctx as a ts
+    , AllCheckBinding env as a ts
     ))
   ))
-Checks ctx a (Contract t) =
-  ( b **
-  ( IsFixpoint a b
-  , Checks ctx (sub (Base Id :< a) b) t
+Checks env a (Contract t) =
+  ( xb **
+  ( IsFixpoint a xb
+  , Checks env (sub (Base Id :< (fst xb :- a)) (snd xb)) t
   ))
-Checks ctx a (Fold e t) =
+Checks env a (Fold e x t) =
   ( b **
-  ( Synths ctx e b
-  , ( c **
-    ( IsFixpoint b c
-    , Checks (sub (Base Id :< a) c :: ctx) a t
+  ( Synths env e b
+  , ( yc **
+    ( IsFixpoint b yc
+    , Checks (env :< (x :- sub (Base Id :< (fst yc :- a)) (snd yc))) a t
     ))
   ))
-Checks ctx a (Embed e) = Synths ctx e a
-
-CheckSpine ctx fun [] res = fun = res
-CheckSpine ctx fun (t :: ts) res =
-  ( a ** b **
-  ( IsArrow 1 fun [a] b
-  , Checks ctx a t
-  , CheckSpine ctx b ts res
+Checks env a (Embed e) =
+  ( b **
+  ( Synths env e b
+  , a `Eq` b
   ))
 
-CheckSpine1 ctx fun (t ::: ts) res =
+CheckSpine env fun [] res = fun = res
+CheckSpine env fun (t :: ts) res =
   ( a ** b **
-  ( IsArrow 1 fun [a] b
-  , Checks ctx a t
-  , CheckSpine ctx b ts res
+  ( IsArrow fun a b
+  , Checks env a t
+  , CheckSpine env b ts res
   ))
 
-AllCheck ctx [] [] = ()
-AllCheck ctx [] (t :: ts) = Void
-AllCheck ctx (a :: as) [] = Void
-AllCheck ctx (a :: as) (t :: ts) = (Checks ctx a t, AllCheck ctx as ts)
+AllCheck env as [<] = (as = [<])
+AllCheck env as (ts :< (x :- t)) =
+  ( a ** bs **
+  ( Remove x as a bs
+  , Checks env a t
+  , AllCheck env bs ts
+  ))
 
-AllCheckBinding ctx [] b [] = ()
-AllCheckBinding ctx [] b (t :: ts) = Void
-AllCheckBinding ctx (a :: as) b [] = Void
-AllCheckBinding ctx (a :: as) b (t :: ts) = (Checks (a :: ctx) b t, AllCheckBinding ctx as b ts)
+AllCheckBinding env as a [<] = (as = [<])
+AllCheckBinding env as a (ts :< (x :- (y ** t))) =
+  ( b ** bs **
+  ( Remove x as b bs
+  , Checks (env :< (y :- b)) a t
+  , AllCheckBinding env bs a ts
+  ))
 
--- Uniqueness
+-- Reordering
 
-getAtUnique :
-  (n : Nat) -> (xs : List a) ->
-  GetAt n xs x -> GetAt n xs y -> x = y
-getAtUnique 0     (x :: xs) (Here ** prf1)     (Here ** prf2)     = Refl
-getAtUnique (S k) (x :: xs) (There n1 ** prf1) (There n2 ** prf2) = getAtUnique k xs (n1 ** injective prf1) (n2 ** injective prf2)
-getAtUnique _     []        (n1 ** prf1)       (n2 ** prf2)       impossible
-
-canProjectUnique : (a : Ty ty) -> CanProject a as -> CanProject a bs -> as = bs
-canProjectUnique (TUnion as) Refl Refl = Refl
-canProjectUnique (TProd as)  Refl Refl = Refl
-
-canInjectUnique : (a : Ty ty) -> CanInject a as -> CanInject a bs -> as = bs
-canInjectUnique (TUnion as) Refl Refl = Refl
-canInjectUnique (TSum as)   Refl Refl = Refl
-
-isFixpointUnique : (a : Ty ty) -> IsFixpoint a b -> IsFixpoint a c -> b = c
-isFixpointUnique TNat Refl Refl = Refl
-isFixpointUnique (TFix a) Refl Refl = Refl
-
-isArrowUnique :
-  (k : Nat) -> (a : Ty ty) ->
-  forall bs, b, cs, c. IsArrow k a bs b -> IsArrow k a cs c -> (bs = cs, b = c)
-isArrowUnique 0 a (Refl, Refl) (Refl, Refl) = (Refl, Refl)
-isArrowUnique (S k) (TArrow dom cod) (as ** (Refl, prf1)) (bs ** (Refl, prf2)) =
-  let (eq1, eq2) = isArrowUnique k cod prf1 prf2 in
-  (cong (dom ::) eq1, eq2)
-
-isProductUnique : (a : Ty ty) -> IsProduct a as -> IsProduct a bs -> as = bs
-isProductUnique (TProd as) Refl Refl = Refl
+allCheckReorder :
+  as <~> bs -> (ts : Context (CheckTerm tyCtx tmCtx)) ->
+  AllCheck env as ts -> AllCheck env bs ts
+allCheckReorder [] [<] Refl = Refl
+allCheckReorder (_ :: _) [<] Refl impossible
+allCheckReorder prf (ts :< (x :- t)) (a ** bs ** (prf1, prf2, prf3)) =
+  (a ** bs ** (Evidence prf1.fst (trans (sym prf) prf1.snd), prf2, prf3))
 
-isSumUnique : (a : Ty ty) -> IsSum a as -> IsSum a bs -> as = bs
-isSumUnique (TSum as) Refl Refl = Refl
+allCheckBindingReorder :
+  as <~> bs -> (ts : Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) ->
+  AllCheckBinding env as a ts -> AllCheckBinding env bs a ts
+allCheckBindingReorder [] [<] Refl = Refl
+allCheckBindingReorder (_ :: _) [<] Refl impossible
+allCheckBindingReorder prf (ts :< (x :- (y ** t))) (b ** bs ** (prf1, prf2, prf3)) =
+  (b ** bs ** (Evidence prf1.fst (trans (sym prf) prf1.snd), prf2, prf3))
 
+-- Uniqueness
 
 synthsUnique :
-  (0 ctx : Vect tm (Ty ty)) -> (e : SynthTerm ty tm) ->
-  Synths ctx e a -> Synths ctx e b -> a = b
+  (0 env : All (const $ Ty tyCtx ()) tmCtx) -> (e : SynthTerm tyCtx tmCtx) ->
+  Synths env e a -> Synths env e b -> a = b
 checkSpineUnique :
-  (0 ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty tm)) ->
-  CheckSpine ctx a ts b -> CheckSpine ctx a ts c -> b = c
-checkSpine1Unique :
-  (0 ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List1 (CheckTerm ty tm)) ->
-  CheckSpine1 ctx a ts b -> CheckSpine1 ctx a ts c -> b = c
-
-synthsUnique ctx (Var i) prf1 prf2 = trans prf1 (sym prf2)
-synthsUnique ctx (Lit k) prf1 prf2 = trans prf1 (sym prf2)
-synthsUnique ctx (Suc t) (_, prf1) (_, prf2) = trans prf1 (sym prf2)
-synthsUnique ctx (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22))
-  with (synthsUnique ctx e prf11 prf21)
-  synthsUnique ctx (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl =
-    checkSpine1Unique ctx fun ts prf12 prf22
-synthsUnique ctx (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22))
-  with (synthsUnique ctx e prf11 prf21)
-  synthsUnique ctx (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl
-    with (canProjectUnique a prf11 prf21)
-    synthsUnique ctx (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl =
+  (0 env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) ->
+  CheckSpine env fun ts a -> CheckSpine env fun ts b -> a = b
+
+synthsUnique env (Var i) prf1 prf2 = trans prf1 (sym prf2)
+synthsUnique env (Lit k) prf1 prf2 = trans prf1 (sym prf2)
+synthsUnique env (Suc t) (_, prf1) (_, prf2) = trans prf1 (sym prf2)
+synthsUnique env (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22))
+  with (synthsUnique env e prf11 prf21)
+  synthsUnique env (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl =
+    checkSpineUnique env fun ts prf12 prf22
+synthsUnique env (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22))
+  with (synthsUnique env e prf11 prf21)
+  synthsUnique env (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl
+    with (isProductUnique a prf11 prf21)
+    synthsUnique env (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl =
       getAtUnique k as prf1 prf2
-synthsUnique ctx (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22))
-  with (synthsUnique ctx e prf11 prf21)
-  synthsUnique ctx (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl
+synthsUnique env (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22))
+  with (synthsUnique env e prf11 prf21)
+  synthsUnique env (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl
     with (isFixpointUnique a prf11 prf21)
-    synthsUnique ctx (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl =
+    synthsUnique env (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl =
       trans prf1 (sym prf2)
-synthsUnique ctx (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2)
-
-checkSpineUnique ctx a [] prf1 prf2 = trans (sym prf1) prf2
-checkSpineUnique ctx a (t :: ts) (b ** c ** (prf11, _ , prf12)) (d ** e ** (prf21, _ , prf22))
-  with (isArrowUnique 1 a prf11 prf21)
-  checkSpineUnique ctx a (t :: ts) (b ** c ** (_, _ , prf1)) (b ** c ** (_, _ , prf2)) | (Refl, Refl) =
-    checkSpineUnique ctx c ts prf1 prf2
-
-checkSpine1Unique ctx a (t ::: ts) (b ** c ** (prf11, _ , prf12)) (d ** e ** (prf21, _ , prf22))
-  with (isArrowUnique 1 a prf11 prf21)
-  checkSpine1Unique ctx a (t ::: ts) (b ** c ** (_, _ , prf1)) (b ** c ** (_, _ , prf2)) | (Refl, Refl) =
-    checkSpineUnique ctx c ts prf1 prf2
-
--- Decidable -------------------------------------------------------------------
-
-canProject : Ty ty -> Maybe (List (Ty ty))
-canProject (TUnion as) = Just (forget as)
-canProject (TProd as) = Just as
-canProject _ = Nothing
-
-canInject : Ty ty -> Maybe (List (Ty ty))
-canInject (TUnion as) = Just (forget as)
-canInject (TSum as) = Just as
-canInject _ = Nothing
-
-isFixpoint : Ty ty -> Maybe (Ty (S ty))
-isFixpoint TNat = Just (TSum [TProd [], TVar FZ])
-isFixpoint (TFix a) = Just a
-isFixpoint _ = Nothing
-
-isArrow : (k : Nat) -> Ty ty -> Maybe (Vect k (Ty ty), Ty ty)
-isArrow 0 a = Just ([], a)
-isArrow (S k) (TArrow a b) = do
-  (as, c) <- isArrow k b
-  Just (a :: as, c)
-isArrow (S k) _ = Nothing
+synthsUnique env (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2)
 
-isProduct : Ty ty -> Maybe (List (Ty ty))
-isProduct (TProd as) = Just as
-isProduct _ = Nothing
+checkSpineUnique env fun [] prf1 prf2 = trans (sym prf1) prf2
+checkSpineUnique env fun (t :: ts) (a ** b ** (prf11, _ , prf12)) (c ** d ** (prf21, _ , prf22))
+  with (isArrowUnique fun prf11 prf21)
+  checkSpineUnique env fun (t :: ts) (a ** b ** (_, _ , prf1)) (a ** b ** (_, _ , prf2)) | (Refl, Refl) =
+    checkSpineUnique env b ts prf1 prf2
 
-isSum : Ty ty -> Maybe (List (Ty ty))
-isSum (TSum as) = Just as
-isSum _ = Nothing
+-- Decision
 
 synths :
-  (ctx : Vect tm (Ty ty)) ->
-  SynthTerm ty tm -> Maybe (Ty ty)
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  SynthTerm tyCtx tmCtx -> Maybe (Ty tyCtx ())
 checks :
-  (ctx : Vect tm (Ty ty)) ->
-  Ty ty -> CheckTerm ty tm -> Bool
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Bool
 checkSpine :
-  (ctx : Vect tm (Ty ty)) ->
-  Ty ty -> List (CheckTerm ty tm) -> Maybe (Ty ty)
-checkSpine1 :
-  (ctx : Vect tm (Ty ty)) ->
-  Ty ty -> List1 (CheckTerm ty tm) -> Maybe (Ty ty)
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> Maybe (Ty tyCtx ())
 allCheck :
-  (ctx : Vect tm (Ty ty)) ->
-  List (Ty ty) -> List (CheckTerm ty tm) -> Bool
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Row (Ty tyCtx ()) -> Context (CheckTerm tyCtx tmCtx) -> Bool
 allCheckBinding :
-  (ctx : Vect tm (Ty ty)) ->
-  List (Ty ty) -> Ty ty -> List (CheckTerm ty (S tm)) -> Bool
-
-synths ctx (Var i) = Just (index i ctx)
-synths ctx (Lit k) = Just TNat
-synths ctx (Suc t) = do
-  guard (checks ctx TNat t)
+  (env : All (const (Ty tyCtx ())) tmCtx) ->
+  Row (Ty tyCtx ()) -> Ty tyCtx () ->
+  Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) ->
+  Bool
+
+synths env (Var i) = Just (indexAll i env)
+synths env (Lit k) = Just TNat
+synths env (Suc t) = do
+  guard (checks env TNat t)
   Just TNat
-synths ctx (App e ts) = do
-  a <- synths ctx e
-  checkSpine1 ctx a ts
-synths ctx (Prj e k) = do
-  a <- synths ctx e
-  as <- canProject a
+synths env (App e ts) = do
+  a <- synths env e
+  checkSpine env a ts
+synths env (Prj e k) = do
+  a <- synths env e
+  as <- isProduct a
   getAt k as
-synths ctx (Expand e) = do
-  a <- synths ctx e
-  b <- isFixpoint a
-  Just (sub (Base Id :< a) b)
-synths ctx (Annot t a) = do
+synths env (Expand e) = do
+  a <- synths env e
+  (x ** b) <- isFixpoint a
+  Just (sub (Base Id :< (x :- a)) b)
+synths env (Annot t a) = do
   guard (not $ illFormed a)
-  guard (checks ctx a t)
+  guard (checks env a t)
   Just a
 
-checks ctx a (Let e t) =
-  case synths ctx e of
-    Just b => checks (b :: ctx) a t
+checks env a (Let x e t) =
+  case synths env e of
+    Just b => checks (env :< (x :- b)) a t
     Nothing => False
-checks ctx a (Abs k t) =
-  case isArrow (S k) a of
-    Just (as, b) => checks (as ++ ctx) b t
+checks env a (Abs bound t) =
+  case isFunction bound a of
+    Just (dom, cod) => checks (env ++ dom) cod t
     Nothing => False
-checks ctx a (Inj k t) =
-  case canInject a of
+checks env a (Inj k t) =
+  case isSum a of
     Just as =>
       case getAt k as of
-        Just b => checks ctx b t
+        Just b => checks env b t
         Nothing => False
     Nothing => False
-checks ctx a (Tup ts) =
+checks env a (Tup ts) =
   case isProduct a of
-    Just as => allCheck ctx as ts
+    Just as => allCheck env as ts
     Nothing => False
-checks ctx a (Case e ts) =
-  case synths ctx e of
+checks env a (Case e ts) =
+  case synths env e of
     Just b =>
       case isSum b of
-        Just as => allCheckBinding ctx as a ts
+        Just as => allCheckBinding env as a ts
         Nothing => False
     Nothing => False
-checks ctx a (Contract t) =
+checks env a (Contract t) =
   case isFixpoint a of
-    Just b => checks ctx (sub (Base Id :< a) b) t
+    Just (x ** b) => checks env (sub (Base Id :< (x :- a)) b) t
     Nothing => False
-checks ctx a (Fold e t) =
-  case synths ctx e of
+checks env a (Fold e x t) =
+  case synths env e of
     Just b =>
       case isFixpoint b of
-        Just c => checks (sub (Base Id :< a) c :: ctx) a t
+        Just (y ** c) => checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t
         Nothing => False
     Nothing => False
-checks ctx a (Embed e) =
-  case synths ctx e of
+checks env a (Embed e) =
+  case synths env e of
     Just b => a == b
     Nothing => False
 
-checkSpine ctx a [] = Just a
-checkSpine ctx a (t :: ts) = do
-  ([dom], cod) <- isArrow 1 a
-  guard (checks ctx dom t)
-  checkSpine ctx cod ts
+checkSpine env a [] = Just a
+checkSpine env a (t :: ts) = do
+  (dom, cod) <- isArrow a
+  guard (checks env dom t)
+  checkSpine env cod ts
 
-checkSpine1 ctx a (t ::: ts) = do
-  ([dom], cod) <- isArrow 1 a
-  guard (checks ctx dom t)
-  checkSpine ctx cod ts
-
-allCheck ctx [] [] = True
-allCheck ctx [] (t :: ts) = False
-allCheck ctx (a :: as) [] = False
-allCheck ctx (a :: as) (t :: ts) = checks ctx a t && allCheck ctx as ts
+allCheck env as [<] = null as
+allCheck env as (ts :< (x :- t)) =
+  case remove' x as of
+    Just (a, bs) => checks env a t && allCheck env bs ts
+    Nothing => False
 
-allCheckBinding ctx [] b [] = True
-allCheckBinding ctx [] b (t :: ts) = False
-allCheckBinding ctx (a :: as) b [] = False
-allCheckBinding ctx (a :: as) b (t :: ts) = checks (a :: ctx) b t && allCheckBinding ctx as b ts
+allCheckBinding env as a [<] = null as
+allCheckBinding env as a (ts :< (x :- (y ** t))) =
+  case remove' x as of
+    Just (b, bs) => checks (env :< (y :- b)) a t && allCheckBinding env bs a ts
+    Nothing => False
 
 -- Proof
 
-reflectGetAt : (k : Nat) -> (xs : List a) -> GetAt k xs `OnlyWhen` getAt k xs
-reflectGetAt k [] = RNothing (\_, (n ** prf) => absurd n)
-reflectGetAt 0 (x :: xs) = RJust (Here ** Refl)
-reflectGetAt (S k) (x :: xs) with (reflectGetAt k xs) | (getAt k xs)
-  _ | RJust (n ** prf) | _ = RJust (There n ** cong S prf)
-  _ | RNothing not | _ = RNothing (\x => \case (There n ** prf) => not x (n ** injective prf))
-
-reflectCanProject : (a : Ty ty) -> CanProject a `OnlyWhen` canProject a
-reflectCanProject (TVar i) = RNothing (\x, y => y)
-reflectCanProject TNat = RNothing (\x, y => y)
-reflectCanProject (TArrow a b) = RNothing (\x, y => y)
-reflectCanProject (TUnion as) = RJust Refl
-reflectCanProject (TProd as) = RJust Refl
-reflectCanProject (TSum as) = RNothing (\x, y => y)
-reflectCanProject (TFix a) = RNothing (\x, y => y)
-
-reflectCanInject : (a : Ty ty) -> CanInject a `OnlyWhen` canInject a
-reflectCanInject (TVar i) = RNothing (\x, y => y)
-reflectCanInject TNat = RNothing (\x, y => y)
-reflectCanInject (TArrow a b) = RNothing (\x, y => y)
-reflectCanInject (TUnion as) = RJust Refl
-reflectCanInject (TProd as) = RNothing (\x, y => y)
-reflectCanInject (TSum as) = RJust Refl
-reflectCanInject (TFix a) = RNothing (\x, y => y)
-
-reflectIsFixpoint : (a : Ty ty) -> IsFixpoint a `OnlyWhen` isFixpoint a
-reflectIsFixpoint (TVar i) = RNothing (\x, y => y)
-reflectIsFixpoint TNat = RJust Refl
-reflectIsFixpoint (TArrow a b) = RNothing (\x, y => y)
-reflectIsFixpoint (TUnion as) = RNothing (\x, y => y)
-reflectIsFixpoint (TProd as) = RNothing (\x, y => y)
-reflectIsFixpoint (TSum as) = RNothing (\x, y => y)
-reflectIsFixpoint (TFix a) = RJust Refl
-
-reflectIsArrow : (k : Nat) -> (a : Ty ty) -> uncurry (IsArrow k a) `OnlyWhen` isArrow k a
-reflectIsArrow 0 a = RJust (Refl, Refl)
-reflectIsArrow (S k) (TVar i) = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) TNat = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) (TArrow a b) with (reflectIsArrow k b) | (isArrow k b)
-  _ | RJust arrow | Just (as, c) = RJust (as ** (Refl, arrow))
-  _ | RNothing notArrow | _ = RNothing (\(a :: as, c), (as ** (Refl, prf)) => notArrow (as, c) prf)
-reflectIsArrow (S k) (TUnion as) = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) (TProd as) = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) (TSum as) = RNothing (\(_, _), x => x)
-reflectIsArrow (S k) (TFix a) = RNothing (\(_, _), x => x)
-
-reflectIsProduct : (a : Ty ty) -> IsProduct a `OnlyWhen` isProduct a
-reflectIsProduct (TVar i) = RNothing (\x, y => y)
-reflectIsProduct TNat = RNothing (\x, y => y)
-reflectIsProduct (TArrow a b) = RNothing (\x, y => y)
-reflectIsProduct (TUnion as) = RNothing (\x, y => y)
-reflectIsProduct (TProd as) = RJust Refl
-reflectIsProduct (TSum as) = RNothing (\x, y => y)
-reflectIsProduct (TFix a) = RNothing (\x, y => y)
-
-reflectIsSum : (a : Ty ty) -> IsSum a `OnlyWhen` isSum a
-reflectIsSum (TVar i) = RNothing (\x, y => y)
-reflectIsSum TNat = RNothing (\x, y => y)
-reflectIsSum (TArrow a b) = RNothing (\x, y => y)
-reflectIsSum (TUnion as) = RNothing (\x, y => y)
-reflectIsSum (TProd as) = RNothing (\x, y => y)
-reflectIsSum (TSum as) = RJust Refl
-reflectIsSum (TFix a) = RNothing (\x, y => y)
-
 -- FIXME: these are total; the termination checker is unreasonably slow.
 
 partial
-reflectSynths :
-  (ctx : Vect tm (Ty ty)) -> (e : SynthTerm ty tm) ->
-  Synths ctx e `OnlyWhen` synths ctx e
-partial
-reflectChecks :
-  (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (t : CheckTerm ty tm) ->
-  Checks ctx a t `Reflects` checks ctx a t
+0 reflectSynths :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (e : SynthTerm tyCtx tmCtx) ->
+  Synths env e `OnlyWhen` synths env e
 partial
-reflectCheckSpine :
-  (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty tm)) ->
-  CheckSpine ctx a ts `OnlyWhen` checkSpine ctx a ts
+0 reflectChecks :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (a : Ty tyCtx ()) -> (t : CheckTerm tyCtx tmCtx) ->
+  Checks env a t `Reflects` checks env a t
 partial
-reflectCheckSpine1 :
-  (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List1 (CheckTerm ty tm)) ->
-  CheckSpine1 ctx a ts `OnlyWhen` checkSpine1 ctx a ts
+0 reflectCheckSpine :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) ->
+  CheckSpine env fun ts `OnlyWhen` checkSpine env fun ts
 partial
-reflectAllCheck :
-  (ctx : Vect tm (Ty ty)) -> (as : List (Ty ty)) -> (ts : List (CheckTerm ty tm)) ->
-  AllCheck ctx as ts `Reflects` allCheck ctx as ts
+0 reflectAllCheck :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (as : Row (Ty tyCtx ())) -> (ts : Context (CheckTerm tyCtx tmCtx)) ->
+  AllCheck env as ts `Reflects` allCheck env as ts
 partial
-reflectAllCheckBinding :
-  (ctx : Vect tm (Ty ty)) -> (as : List (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty (S tm))) ->
-  AllCheckBinding ctx as a ts `Reflects` allCheckBinding ctx as a ts
-
-reflectSynths ctx (Var i) = RJust Refl
-reflectSynths ctx (Lit k) = RJust Refl
-reflectSynths ctx (Suc t) with (reflectChecks ctx TNat t) | (checks ctx TNat t)
+0 reflectAllCheckBinding :
+  (env : All (const $ Ty tyCtx ()) tmCtx) ->
+  (as : Row (Ty tyCtx ())) -> (a : Ty tyCtx ()) ->
+  (ts : Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) ->
+  AllCheckBinding env as a ts `Reflects` allCheckBinding env as a ts
+
+reflectSynths env (Var i) = RJust Refl
+reflectSynths env (Lit k) = RJust Refl
+reflectSynths env (Suc t) with (reflectChecks env TNat t) | (checks env TNat t)
   _ | RTrue tNat | _ = RJust (tNat, Refl)
   _ | RFalse tNotNat | _ = RNothing (\_, (tNat, _) => tNotNat tNat)
-reflectSynths ctx (App e ts) with (reflectSynths ctx e) | (synths ctx e)
-  _ | RJust eTy | Just a with (reflectCheckSpine1 ctx a ts) | (checkSpine1 ctx a ts)
+reflectSynths env (App e ts) with (reflectSynths env e) | (synths env e)
+  _ | RJust eTy | Just a with (reflectCheckSpine env a ts) | (checkSpine env a ts)
     _ | RJust tsSpine | Just b = RJust (a ** (eTy, tsSpine))
     _ | RNothing tsBad | _ =
       RNothing
         (\c, (b ** (eTy', tsSpine)) =>
-          let tsSpine = rewrite synthsUnique ctx e {a, b} eTy eTy' in tsSpine in
+          let tsSpine = rewrite synthsUnique env e {a, b} eTy eTy' in tsSpine in
           tsBad c tsSpine)
   _ | RNothing eBad | _ =
     RNothing (\c, (b ** (eTy, _)) => eBad b eTy)
-reflectSynths ctx (Prj e k) with (reflectSynths ctx e) | (synths ctx e)
-  _ | RJust eTy | Just a with (reflectCanProject a) | (canProject a)
-    _ | RJust prf | Just as with (reflectGetAt k as) | (getAt k as)
+reflectSynths env (Prj e x) with (reflectSynths env e) | (synths env e)
+  _ | RJust eTy | Just a with (reflectIsProduct a) | (isProduct a)
+    _ | RJust prf | Just as with (reflectGetAt x as) | (getAt x as)
       _ | RJust got | Just b = RJust (a ** (eTy, (as ** (prf, got))))
       _ | RNothing not | _ =
         RNothing (\x, (a' ** (eTy', (as' ** (prf', got)))) =>
-          let prf' = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf' in
-          let got = rewrite canProjectUnique a {as, bs = as'} prf prf' in got in
+          let prf' = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf' in
+          let got = rewrite isProductUnique a {as, bs = as'} prf prf' in got in
           not x got)
     _ | RNothing nprf | _ =
       RNothing (\x, (a' ** (eTy', (as' ** (prf, _)))) =>
-        let prf = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf in
         nprf as' prf)
   _ | RNothing eBad | _ = RNothing (\x, (a' ** (eTy, _)) => eBad a' eTy)
-reflectSynths ctx (Expand e) with (reflectSynths ctx e) | (synths ctx e)
+reflectSynths env (Expand e) with (reflectSynths env e) | (synths env e)
   _ | RJust eTy | Just a with (reflectIsFixpoint a) | (isFixpoint a)
-    _ | RJust prf | Just b = RJust (a ** (eTy, (b ** (prf, Refl))))
+    _ | RJust prf | Just (x ** b) = RJust (a ** (eTy, ((x ** b) ** (prf, Refl))))
     _ | RNothing nprf | _ =
       RNothing (\x, (a' ** (eTy', (b ** (prf, eq)))) =>
-        let prf = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf in
         nprf b prf)
   _ | RNothing eBad | _ = RNothing (\x, (a ** (eTy, _)) => eBad a eTy)
-reflectSynths ctx (Annot t a) with (reflectIllFormed a) | (illFormed a)
-  _ | RFalse wf | _ with (reflectChecks ctx a t) | (checks ctx a t)
+reflectSynths env (Annot t a) with (reflectIllFormed a) | (illFormed a)
+  _ | RFalse wf | _ with (reflectChecks env a t) | (checks env a t)
     _ | RTrue tTy | _ = RJust (wf, tTy, Refl)
     _ | RFalse tBad | _ = RNothing (\x, (_, tTy, Refl) => tBad tTy)
   _ | RTrue notWf | _ = RNothing (\x, (wf, _) => wf notWf)
 
-reflectChecks ctx a (Let e t) with (reflectSynths ctx e) | (synths ctx e)
-  _ | RJust eTy | Just b with (reflectChecks (b :: ctx) a t) | (checks (b :: ctx) a t)
+reflectChecks env a (Let x e t) with (reflectSynths env e) | (synths env e)
+  _ | RJust eTy | Just b with (reflectChecks (env :< (x :- b)) a t) | (checks (env :< (x :- b)) a t)
     _ | RTrue tTy | _ = RTrue (b ** (eTy, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(b' ** (eTy', tTy)) =>
-        let tTy = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in tTy in
+        let tTy = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in tTy in
         tBad tTy)
   _ | RNothing eBad | Nothing = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks ctx a (Abs k t) with (reflectIsArrow (S k) a) | (isArrow (S k) a)
-  _ | RJust prf | Just (as, b) with (reflectChecks (as ++ ctx) b t) | (checks (as ++ ctx) b t)
+reflectChecks env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction bound a)
+  _ | RJust prf | Just (as, b) with (reflectChecks (env ++ as) b t) | (checks (env ++ as) b t)
     _ | RTrue tTy | _ = RTrue (as ** b ** (prf, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(as' ** b' ** (prf', tTy)) =>
         let
-          tTy =
-            rewrite fst $ isArrowUnique (S k) a {bs = as, b, cs = as', c = b'} prf prf' in
-            rewrite snd $ isArrowUnique (S k) a {bs = as, b, cs = as', c = b'} prf prf' in
-            tTy
+          (eq1, eq2) =
+            isFunctionUnique bound a
+              {dom1 = as, cod1 = b, dom2 = as', cod2 = b'}
+              prf prf'
+          tTy = rewrite eq1 in rewrite eq2 in tTy
         in
         tBad tTy)
   _ | RNothing nprf | _ = RFalse (\(as ** b ** (prf, _)) => nprf (as, b) prf)
-reflectChecks ctx a (Inj k t) with (reflectCanInject a) | (canInject a)
+reflectChecks env a (Inj k t) with (reflectIsSum a) | (isSum a)
   _ | RJust prf | Just as with (reflectGetAt k as) | (getAt k as)
-    _ | RJust got | Just b with (reflectChecks ctx b t) | (checks ctx b t)
+    _ | RJust got | Just b with (reflectChecks env b t) | (checks env b t)
       _ | RTrue tTy | _ = RTrue (as ** (prf, (b ** (got, tTy))))
       _ | RFalse tBad | _ =
         RFalse (\(as' ** (prf', (b' ** (got', tTy)))) =>
-          let got' = rewrite canInjectUnique a {as, bs = as'} prf prf' in got' in
-          let tTy = rewrite getAtUnique k as {x = b, y = b'} got got' in tTy in
-          tBad tTy)
+          let got' = rewrite isSumUnique a {as, bs = as'} prf prf' in got' in
+          let tTy = rewrite getAtUnique k as {y = b, z = b'} got got' in tTy in
+          tBad tTy
+          )
     _ | RNothing not | _ =
       RFalse (\(as' ** (prf', (b ** (got, _)))) =>
-        let got = rewrite canInjectUnique a {as, bs = as'} prf prf' in got in
+        let got = rewrite isSumUnique a {as, bs = as'} prf prf' in got in
         not b got)
   _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf)
-reflectChecks ctx a (Tup ts) with (reflectIsProduct a) | (isProduct a)
-  _ | RJust prf | Just as with (reflectAllCheck ctx as ts) | (allCheck ctx as ts)
+reflectChecks env a (Tup ts) with (reflectIsProduct a) | (isProduct a)
+  _ | RJust prf | Just as with (reflectAllCheck env as ts) | (allCheck env as ts)
     _ | RTrue tsTy | _ = RTrue (as ** (prf, tsTy))
     _ | RFalse tsBad | _ =
       RFalse (\(as' ** (prf', tsTy)) =>
         let tsTy = rewrite isProductUnique a {as, bs = as'} prf prf' in tsTy in
         tsBad tsTy)
   _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf)
-reflectChecks ctx a (Case e ts) with (reflectSynths ctx e) | (synths ctx e)
+reflectChecks env a (Case e ts) with (reflectSynths env e) | (synths env e)
   _ | RJust eTy | Just b with (reflectIsSum b) | (isSum b)
-    _ | RJust prf | Just as with (reflectAllCheckBinding ctx as a ts) | (allCheckBinding ctx as a ts)
+    _ | RJust prf | Just as with (reflectAllCheckBinding env as a ts) | (allCheckBinding env as a ts)
       _ | RTrue tsTy | _ = RTrue (b ** (eTy, (as ** (prf, tsTy))))
       _ | RFalse tsBad | _ =
         RFalse
           (\(b' ** (eTy', (as' ** (prf', tsTy)))) =>
-            let prf' = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf' in
+            let prf' = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf' in
             let tsTy = rewrite isSumUnique b {as, bs = as'} prf prf' in tsTy in
             tsBad tsTy)
     _ | RNothing nprf | _ =
       RFalse (\(b' ** (eTy', (as ** (prf, _)))) =>
-        let prf = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf in
         nprf as prf)
   _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks ctx a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a)
-  _ | RJust prf | Just b with (reflectChecks ctx (sub (Base Id :< a) b) t) | (checks ctx (sub (Base Id :< a) b) t)
-    _ | RTrue tTy | _ = RTrue (b ** (prf, tTy))
+reflectChecks env a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a)
+  _ | RJust prf | Just (x ** b) with (reflectChecks env (sub (Base Id :< (x :- a)) b) t) | (checks env (sub (Base Id :< (x :- a)) b) t)
+    _ | RTrue tTy | _ = RTrue ((x ** b) ** (prf, tTy))
     _ | RFalse tBad | _ =
       RFalse (\(b' ** (prf', tTy)) =>
-        let tTy = rewrite isFixpointUnique a {b, c = b'} prf prf' in tTy in
+        let
+          eq = isFixpointUnique a {xb = (x ** b), yc = b'} prf prf'
+          tTy =
+            replace {p = \xb => Checks env (sub (Base Id :< (xb.fst :- a)) xb.snd) t}
+              (sym eq) tTy
+        in
         tBad tTy)
   _ | RNothing nprf | _ = RFalse (\(b ** (prf, _)) => nprf b prf)
-reflectChecks ctx a (Fold e t) with (reflectSynths ctx e) | (synths ctx e)
+reflectChecks env a (Fold e x t) with (reflectSynths env e) | (synths env e)
   _ | RJust eTy | Just b with (reflectIsFixpoint b) | (isFixpoint b)
-    _ | RJust prf | Just c with (reflectChecks ((sub (Base Id :< a) c) :: ctx) a t) | (checks ((sub (Base Id :< a) c) :: ctx) a t)
-      _ | RTrue tTy | _ = RTrue (b ** (eTy, (c ** (prf, tTy))))
+    _ | RJust prf | Just (y ** c) with (reflectChecks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) | (checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t)
+      _ | RTrue tTy | _ = RTrue (b ** (eTy, ((y ** c) ** (prf, tTy))))
       _ | RFalse tBad | _ =
         RFalse (\(b' ** (eTy', (c' ** (prf', tTy)))) =>
-          let prf' = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf' in
-          let tTy = rewrite isFixpointUnique b {b = c, c = c'} prf prf' in tTy in
+          let
+            prf' = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf'
+            eq = isFixpointUnique b {xb = (y ** c), yc = c'} prf prf'
+            tTy =
+              replace {p = \yc => Checks (env :< (x :- sub (Base Id :< (yc.fst :- a)) yc.snd)) a t}
+                (sym eq) tTy
+          in
           tBad tTy)
     _ | RNothing nprf | _ =
       RFalse (\(b' ** (eTy', (c ** (prf, _)))) =>
-        let prf = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf in
+        let prf = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf in
         nprf c prf)
   _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
-reflectChecks ctx a (Embed e) with (reflectSynths ctx e) | (synths ctx e)
+reflectChecks env a (Embed e) with (reflectSynths env e) | (synths env e)
   _ | RJust eTy | Just b with (reflectEq a b) | (a == b)
-    reflectChecks ctx a (Embed e) | RJust eTy | Just .(a) | RTrue Refl | _ = RTrue eTy
-    _ | RFalse neq | _ = RFalse (\eTy' => neq $ synthsUnique ctx e eTy' eTy)
-  _ | RNothing eBad | _ = RFalse (\eTy => eBad a eTy)
-
-reflectCheckSpine ctx a [] = RJust Refl
-reflectCheckSpine ctx a (t :: ts) with (reflectIsArrow 1 a) | (isArrow 1 a)
-  _ | RJust prf | Just ([b], c) with (reflectChecks ctx b t) | (checks ctx b t)
-    _ | RTrue tTy | _ with (reflectCheckSpine ctx c ts) | (checkSpine ctx c ts)
-      _ | RJust tsTy | Just d = RJust (b ** c ** (prf, tTy, tsTy))
-      _ | RNothing tsBad | _ =
-        RNothing (\d, (_ ** c' ** (prf', _, tsTy)) =>
-          let tsTy = rewrite snd $ isArrowUnique 1 a {b = c, c = c'} prf prf' in tsTy in
-          tsBad d tsTy)
-    _ | RFalse tBad | _ =
-      RNothing (\d, (b' ** _ ** (prf', tTy, _)) =>
-        let
-          tTy =
-            rewrite fst $ biinj (::) $ fst $ isArrowUnique 1 a {bs = [b], cs = [b']} prf prf' in
-            tTy
-        in
-        tBad tTy)
-  _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf ([b], c) prf)
+    _ | RTrue eq | _ = RTrue (b ** (eTy, eq))
+    _ | RFalse neq | _ =
+      RFalse (\(b' ** (eTy', eq)) =>
+        let eq = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in eq in
+        neq eq)
+  _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy)
 
-reflectCheckSpine1 ctx a (t ::: ts) with (reflectIsArrow 1 a) | (isArrow 1 a)
-  _ | RJust prf | Just ([b], c) with (reflectChecks ctx b t) | (checks ctx b t)
-    _ | RTrue tTy | _ with (reflectCheckSpine ctx c ts) | (checkSpine ctx c ts)
+reflectCheckSpine env a [] = RJust Refl
+reflectCheckSpine env a (t :: ts) with (reflectIsArrow a) | (isArrow a)
+  _ | RJust prf | Just (b, c) with (reflectChecks env b t) | (checks env b t)
+    _ | RTrue tTy | _ with (reflectCheckSpine env c ts) | (checkSpine env c ts)
       _ | RJust tsTy | Just d = RJust (b ** c ** (prf, tTy, tsTy))
       _ | RNothing tsBad | _ =
         RNothing (\d, (_ ** c' ** (prf', _, tsTy)) =>
-          let tsTy = rewrite snd $ isArrowUnique 1 a {b = c, c = c'} prf prf' in tsTy in
+          let (eq1, eq2) = isArrowUnique a {c, e = c'} prf prf' in
+          let tsTy = rewrite eq2 in tsTy in
           tsBad d tsTy)
     _ | RFalse tBad | _ =
       RNothing (\d, (b' ** _ ** (prf', tTy, _)) =>
-        let
-          tTy =
-            rewrite fst $ biinj (::) $ fst $ isArrowUnique 1 a {bs = [b], cs = [b']} prf prf' in
-            tTy
-        in
+        let (eq1, eq2) = isArrowUnique a {b, d = b'} prf prf' in
+        let tTy = rewrite eq1 in tTy in
         tBad tTy)
-  _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf ([b], c) prf)
-
-reflectAllCheck ctx [] [] = RTrue ()
-reflectAllCheck ctx [] (t :: ts) = RFalse (\x => x)
-reflectAllCheck ctx (a :: as) [] = RFalse (\x => x)
-reflectAllCheck ctx (a :: as) (t :: ts) with (reflectChecks ctx a t) | (checks ctx a t)
-  _ | RTrue tTy | _ with (reflectAllCheck ctx as ts) | (allCheck ctx as ts)
-    _ | RTrue tsTy | _ = RTrue (tTy, tsTy)
-    _ | RFalse tsBad | _ = RFalse (\(_, tsTy) => tsBad tsTy)
-  _ | RFalse tBad | _ = RFalse (\(tTy, _) => tBad tTy)
-
-reflectAllCheckBinding ctx [] b [] = RTrue ()
-reflectAllCheckBinding ctx [] b (t :: ts) = RFalse (\x => x)
-reflectAllCheckBinding ctx (a :: as) b [] = RFalse (\x => x)
-reflectAllCheckBinding ctx (a :: as) b (t :: ts) with (reflectChecks (a :: ctx) b t) | (checks (a :: ctx) b t)
-  _ | RTrue tTy | _ with (reflectAllCheckBinding ctx as b ts) | (allCheckBinding ctx as b ts)
-    _ | RTrue tsTy | _ = RTrue (tTy, tsTy)
-    _ | RFalse tsBad | _ = RFalse (\(_, tsTy) => tsBad tsTy)
-  _ | RFalse tBad | _ = RFalse (\(tTy, _) => tBad tTy)
+  _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf (b, c) prf)
+
+reflectAllCheck env [<] [<] = RTrue Refl
+reflectAllCheck env (_ :< _) [<] = RFalse (\case Refl impossible)
+reflectAllCheck env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x as)
+  _ | RJust prf | Just (a, bs) with (reflectAnd (reflectChecks env a t) (reflectAllCheck env bs ts)) | (checks env a t && allCheck env bs ts)
+    _ | RTrue checks | _ = RTrue (a ** bs ** (prf, checks))
+    _ | RFalse notChecks | _ =
+      RFalse (\(a' ** bs' ** (prf', checks)) =>
+        let (eq, reorder) = removeUnique x as prf prf' in
+        notChecks $
+        bimap (\x => rewrite eq in x) (allCheckReorder (sym reorder) ts) checks)
+  _ | RNothing nprf | _ = RFalse (\(a ** bs ** (prf, _)) => nprf (a, bs) prf)
+
+reflectAllCheckBinding env [<] a [<] = RTrue Refl
+reflectAllCheckBinding env (_ :< _) a [<] = RFalse (\case Refl impossible)
+reflectAllCheckBinding env as a (ts :< (x :- (y ** t))) with (reflectRemove x as) | (remove' x as)
+  _ | RJust prf | Just (b, bs) with (reflectAnd (reflectChecks (env :< (y :- b)) a t) (reflectAllCheckBinding env bs a ts)) | (checks (env :< (y :- b)) a t && allCheckBinding env bs a ts)
+    _ | RTrue checks | _ = RTrue (b ** bs ** (prf, checks))
+    _ | RFalse notChecks | _ =
+      RFalse (\(b' ** bs' ** (prf', checks)) =>
+        let (eq, reorder) = removeUnique x as prf prf' in
+        notChecks $
+        bimap (\x => rewrite eq in x) (allCheckBindingReorder (sym reorder) ts) checks)
+  _ | RNothing nprf | _ = RFalse (\(b ** bs ** (prf, _)) => nprf (b, bs) prf)