Add more names. Names are good.

3 files changed, 50 insertions, 130 deletions

diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 8ddcd8d..6027d68 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -69,7 +69,7 @@ synthsUnique (PrjS {as} prf i) (PrjS {as = bs} prf' j) =
   let j = rewrite inj TProd $ synthsUnique prf prf' in j in
   cong fst $ lookupUnique as i j
 synthsUnique (UnrollS {x, a} prf) (UnrollS {x = y, a = b} prf') =
-  cong (\(x ** a) => sub [<TFix x a `Over` Id] a) $
+  cong (\(x ** a) => sub [<x :- TFix x a] a) $
   fixInjective $
   synthsUnique prf prf'
 synthsUnique (MapS _ _ _) (MapS _ _ _) = Refl
@@ -176,11 +176,11 @@ checksSplit (RollC prf) (RollNC2 contra) = checksSplit prf contra
 checksSplit (FoldC prf1 prf2) (FoldNC1 contra) = synthsSplit prf1 contra
 checksSplit (FoldC {x, a} prf1 prf2) (FoldNC2 prf1' contra) =
   void $ contra x a $ synthsUnique prf1' prf1
-checksSplit (FoldC {t, b} prf1 prf2) (FoldNC3 prf1' contra) =
+checksSplit (FoldC {y, t, b} prf1 prf2) (FoldNC3 prf1' contra) =
   let
     contra =
       replace
-        {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t}
+        {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (y :- sub [<x :- b] a)) b t}
         (fixInjective $ synthsUnique prf1' prf1)
         contra
   in
@@ -212,7 +212,7 @@ allBranchesSplit fresh (Step {as, b, x, t, ts} i prf prfs) (Step2 j contras) =
       replace
         {p = \(a ** i) =>
           These
-            (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t)
+            (NotChecks tyEnv (tmEnv :< (x :- a)) b t)
             (AnyNotBranches tyEnv tmEnv (dropElem as i) b ts)}
         (lookupUnique (MkRow as fresh) j i)
         contras
@@ -234,37 +234,37 @@ fallbackCheck prf p a =
   (b := p) >=> alpha b a
 
 synths :
-  (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
-  (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+  (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+  (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
   (e : Term mode m tyCtx tmCtx) ->
   Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e)
 export
 checks :
-  (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
-  (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+  (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+  (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
   (a : Ty [<]) -> (t : Term mode m tyCtx tmCtx) ->
   LazyEither (Checks tyEnv tmEnv a t) (NotChecks tyEnv tmEnv a t)
 checkSpine :
-  (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
-  (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+  (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+  (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
   (a : Ty [<]) -> (ts : List (Term mode m tyCtx tmCtx)) ->
   Proof (Ty [<]) (CheckSpine tyEnv tmEnv a ts) (NotCheckSpine tyEnv tmEnv a ts)
 allSynths :
-  (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
-  (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+  (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+  (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
   (es : Context (Term mode m tyCtx tmCtx)) ->
   (0 fresh : AllFresh es.names) ->
   Proof (Subset (Row (Ty [<])) (\as => es.names = as.names))
     (AllSynths tyEnv tmEnv es . Subset.fst)
     (AnyNotSynths tyEnv tmEnv es)
 allChecks :
-  (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
-  (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+  (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+  (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
   (as : Context (Ty [<])) -> (ts : Context (Term mode m tyCtx tmCtx)) ->
   LazyEither (AllChecks tyEnv tmEnv as ts) (AnyNotChecks tyEnv tmEnv as ts)
 allBranches :
-  (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
-  (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
+  (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
+  (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
   (as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term mode m tyCtx (tmCtx :< x))) ->
   LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts)
 
@@ -272,15 +272,15 @@ synths tyEnv tmEnv (Annot _ t a) =
   pure (sub tyEnv a) $
   map (uncurry AnnotS) AnnotNS $
   all (wellFormed a) (checks tyEnv tmEnv (sub tyEnv a) t)
-synths tyEnv tmEnv (Var _ i) = Just (indexAll i.pos tmEnv).extract `Because` VarS
+synths tyEnv tmEnv (Var _ i) = Just (indexAll i.pos tmEnv).value `Because` VarS
 synths tyEnv tmEnv (Let _ e (x ** f)) =
   map snd
     (\(_, _), (prf1, prf2) => LetS prf1 prf2)
     (either LetNS1 (\xPrfs => uncurry LetNS2 (snd xPrfs))) $
-  (a := synths tyEnv tmEnv e) >=> synths tyEnv (tmEnv :< (a `Over` Id)) f
+  (a := synths tyEnv tmEnv e) >=> synths tyEnv (tmEnv :< (x :- a)) f
 synths tyEnv tmEnv (LetTy _ a (x ** e)) =
   map id (\_, (wf, prf) => LetTyS wf prf) LetTyNS $
-  all (wellFormed a) (synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e)
+  all (wellFormed a) (synths (tyEnv :< (x :- sub tyEnv a)) tmEnv e)
 synths tyEnv tmEnv (Abs _ (bound ** t)) = Nothing `Because` ChecksNS Abs
 synths tyEnv tmEnv (App _ e ts) =
   map snd
@@ -321,7 +321,7 @@ synths tyEnv tmEnv (Unroll _ e) =
   synths tyEnv tmEnv e `andThen` isFix
   where
   f : (Ty [<], (x ** Ty [<x])) -> Ty [<]
-  f (a, (x ** b)) = sub [<TFix x b `Over` Id] b
+  f (a, (x ** b)) = sub [<x :- TFix x b] b
 
   true :
     (axb : _) ->
@@ -348,19 +348,19 @@ checks tyEnv tmEnv a (Let _ e (x ** t)) =
   map
     (\(_ ** (prf1, prf2)) => LetC prf1 prf2)
     (either LetNC1 (\xPrfs => uncurry LetNC2 $ snd xPrfs)) $
-  (b := synths tyEnv tmEnv e) >=> checks tyEnv (tmEnv :< (b `Over` Id)) a t
+  (b := synths tyEnv tmEnv e) >=> checks tyEnv (tmEnv :< (x :- b)) a t
 checks tyEnv tmEnv a (LetTy _ b (x ** t)) =
   map (uncurry LetTyC) LetTyNC $
-  all (wellFormed b) (checks (tyEnv :< (sub tyEnv b `Over` Id)) tmEnv a t)
+  all (wellFormed b) (checks (tyEnv :< (x :- sub tyEnv b)) tmEnv a t)
 checks tyEnv tmEnv a (Abs meta (bound ** t)) =
   map
     (\((_, _) ** (prf1, prf2)) => AbsC prf1 prf2)
     (either AbsNC1 false) $
   (domCod := isFunction bound a) >=>
-  checks tyEnv (tmEnv <>< mapProperty (`Over` Id) (fst domCod)) (snd domCod) t
+  checks tyEnv (tmEnv <>< fst domCod) (snd domCod) t
   where
   false :
-    (x ** (Prelude.uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) (fst x)) (snd x) t)) ->
+    (x ** (Prelude.uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< fst x) (snd x) t)) ->
     NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
   false ((_,_) ** prf) = uncurry AbsNC2 prf
 checks tyEnv tmEnv a (App meta f ts) = fallbackCheck App (synths tyEnv tmEnv $ App meta f ts) a
@@ -436,7 +436,7 @@ checks tyEnv tmEnv a (Roll _ t) =
   (xb := isFix a) >=> checks tyEnv tmEnv (ty xb) t
   where
   ty : (x ** Ty [<x]) -> Ty [<]
-  ty (x ** b) = sub [<TFix x b `Over` Id] b
+  ty (x ** b) = sub [<x :- TFix x b] b
 
   true :
     forall a.
@@ -459,8 +459,8 @@ checks tyEnv tmEnv a (Fold _ e (x ** t)) =
   (yc := isFix b) >=>
   checks tyEnv (tmEnv' yc) a t
   where
-  tmEnv' : (y ** Ty [<y]) -> All (const $ Thinned Ty [<]) (tmCtx :< x)
-  tmEnv' (y ** c) = tmEnv :< (sub [<a `Over` Id] c `Over` Id)
+  tmEnv' : (y ** Ty [<y]) -> All (Assoc0 $ Ty [<]) (tmCtx :< x)
+  tmEnv' (y ** c) = tmEnv :< (x :- sub [<y :- a] c)
 
   true :
     (b ** (Synths tyEnv tmEnv e b,
@@ -534,5 +534,5 @@ allBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) =
     (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $
   (ai := (decLookup l as).forget) >=>
   all
-    (checks tyEnv (tmEnv :< (fst ai `Over` Id)) b t)
+    (checks tyEnv (tmEnv :< (x :- fst ai)) b t)
     (allBranches tyEnv tmEnv (dropElem as $ snd ai) b ts)
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 50676ce..1ce0e41 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -80,89 +80,6 @@ desugarMapCaseNames [<] [<] i [<] f = Refl
 desugarMapCaseNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
   cong (:< l) $ desugarMapCaseNames as fresh i prfs f
 
--- -- Well Formed
-
--- desugarMapChecks :
---   (0 meta : m) =>
---   (a : Ty (tyCtx :< arg ++ bound)) -> (len : LengthOf bound) ->
---   (0 prf : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveIn` a) ->
---   {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
---   {env2 : All (const $ Thinned Ty [<]) bound} ->
---   {b, c : Ty [<]} ->
---   Synths tyEnv tmEnv f (TArrow b c) ->
---   Synths tyEnv tmEnv t (sub (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) a) ->
---   SynthsOnly t ->
---   Checks tyEnv tmEnv
---     (sub (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) a)
---     (desugarMap {m} a (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prf f t)
--- desugarMapTupleChecks :
---   (0 meta : m) =>
---   (as : Context (Ty (tyCtx :< arg ++ bound))) -> (len' : LengthOf bs) ->
---   (0 fresh' : AllFresh (as <>< bs).names) ->
---   (0 fresh : AllFresh as.names) ->
---   (len : LengthOf bound) ->
---   (0 prfs : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveInAll` as) ->
---   {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
---   {env2 : All (const $ Thinned Ty [<]) bound} ->
---   {b, c : Ty [<]} ->
---   Synths tyEnv tmEnv f (TArrow b c) ->
---   Synths tyEnv tmEnv t
---     (sub (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) (TProd (MkRow (as <>< bs) fresh'))) ->
---   SynthsOnly t ->
---   AllChecks tyEnv tmEnv
---     (subAll (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) as)
---     (desugarMapTuple {m} as fresh (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prfs f t).context
--- desugarMapCaseBranches :
---   (0 meta : m) =>
---   (as : Context (Ty (tyCtx :< arg ++ bound))) -> (len' : LengthOf bs) ->
---   (0 fresh' : AllFresh (as <>< bs).names) ->
---   (0 fresh : AllFresh as.names) ->
---   (len : LengthOf bound) ->
---   (0 prfs : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveInAll` as) ->
---   {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
---   {env2 : All (const $ Thinned Ty [<]) bound} ->
---   {b, c : Ty [<]} ->
---   Synths tyEnv tmEnv f (TArrow b c) ->
---   AllBranches tyEnv tmEnv
---     (subAll (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) as)
---     (sub (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) (TSum (MkRow (as <>< bs) fresh')))
---     (desugarMapCase {m} as fresh (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prfs f).context
-
--- desugarMapChecks (TVar j) len TVar fun arg argSynOnly
---   with (index (dropAll len) (toVar Here) `decEq` j)
---   desugarMapChecks (TVar _) len TVar fun arg argSynOnly | True `Because` Refl =
---     EmbedC App (AppS fun [EmbedC argSynOnly arg $ alphaSym $ alphaRefl b _ $ ?b]) ?c
---   _ | False `Because` neq =
---     EmbedC argSynOnly arg $ alphaSym $ alphaRefl _ _ ?a
--- desugarMapChecks (TArrow a b) len (TArrow prf) fun arg argSynOnly =
---   EmbedC argSynOnly arg $ ?dmc_2
--- desugarMapChecks (TProd (MkRow as fresh)) len (TProd prfs) fun arg argSynOnly =
---   TupC (desugarMapTupleChecks as Z fresh fresh len prfs fun arg argSynOnly)
--- desugarMapChecks (TSum (MkRow as fresh)) len (TSum prfs) fun arg argSynOnly =
---   CaseC arg (desugarMapCaseBranches as Z fresh fresh len prfs fun)
--- desugarMapChecks (TFix x a) len (TFix prf) fun arg' argSynOnly =
---   let
---     x =
---   -- FoldC arg' (RollC $
---     desugarMapChecks
---       { m
---       , meta
---       , tyCtx
---       , arg
---       , bound = bound :< x
---       , env1
---       , env2 = env2 :< ?dmc_90
---       , b
---       , c
---       , tyEnv
---       , tmEnv = tmEnv :< (?dmc_92 `Over` Id)
---       , f = thin (Drop Id) f
---       , t = Var meta ((%%) "_eta" {pos = Here})
---       }
---       a (S len) prf ?x ?y ?z
---   -- Need assoc. of subst
---   in FoldC arg' (RollC ?dmc_99)
-
 -- Desugar Terms ---------------------------------------------------------------
 
 desugarSynths :
@@ -225,8 +142,8 @@ desugarSynths (MapS {meta, x, a, b, c} (TFix prf1 wf1) wf2 wf3) =
     (Abs meta
       (["_fun", "_arg"] ** desugarMap a (%% x) prf1 (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
     (TArrow (TArrow (TArrow b c)
-      (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (b `Over` Id)) a))
-      (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (c `Over` Id)) a))
+      (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a))
+      (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a))
 
 desugarChecks (AnnotC prf1 prf2) = desugarSynths prf1
 desugarChecks (VarC prf1 prf2) = desugarSynths prf1
@@ -277,11 +194,11 @@ maybeDesugarList :
 maybeDesugarAll :
   (len : LengthOf tyCtx) =>
   (ts : Context (Term Sugar m tyCtx tmCtx)) ->
-  Maybe (All (const $ Term NoSugar m tyCtx tmCtx) ts.names)
+  Maybe (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ts.names)
 maybeDesugarBranches :
   (len : LengthOf tyCtx) =>
   (ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))) ->
-  Maybe (All (const $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
+  Maybe (All (Assoc0 $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
 
 maybeDesugar (Annot meta t a) = do
   t <- maybeDesugar t
@@ -302,8 +219,8 @@ maybeDesugar (App meta e ts) = do
   ts <- maybeDesugarList ts
   pure (App meta e ts)
 maybeDesugar (Tup meta (MkRow ts fresh)) = do
-  ts' <- maybeDesugarAll ts
-  pure (Tup meta (fromAll (MkRow ts fresh) ts'))
+  ts <- maybeDesugarAll ts
+  pure (Tup meta (fromAll ts fresh))
 maybeDesugar (Prj meta e l) = do
   e <- maybeDesugar e
   pure (Prj meta e l)
@@ -312,8 +229,8 @@ maybeDesugar (Inj meta l t) = do
   pure (Inj meta l t)
 maybeDesugar (Case meta e (MkRow ts fresh)) = do
   e <- maybeDesugar e
-  ts' <- maybeDesugarBranches ts
-  pure (Case meta e (fromAll (MkRow ts fresh) ts'))
+  ts <- maybeDesugarBranches ts
+  pure (Case meta e (fromAll ts fresh))
 maybeDesugar (Roll meta t) = do
   t <- maybeDesugar t
   pure (Roll meta t)
@@ -333,17 +250,20 @@ maybeDesugar (Map meta (x ** a) b c) =
         (Abs meta
           (["_fun", "_arg"] ** desugarMap a (%% x) prf (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
         (TArrow (TArrow (TArrow b c)
-          (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (b `Over` Id)) a))
-          (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (c `Over` Id)) a))
+          (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a))
+          (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a))
 
 maybeDesugarList [] = pure []
 maybeDesugarList (t :: ts) = [| maybeDesugar t :: maybeDesugarList ts |]
 
 maybeDesugarAll [<] = pure [<]
-maybeDesugarAll (ts :< (l :- t)) = [| maybeDesugarAll ts :< maybeDesugar t |]
+maybeDesugarAll (ts :< (l :- t)) = do
+  ts <- maybeDesugarAll ts
+  t <- maybeDesugar t
+  pure (ts :< (l :- t))
 
 maybeDesugarBranches [<] = pure [<]
 maybeDesugarBranches (ts :< (l :- (x ** t))) = do
   ts <- maybeDesugarBranches ts
   t <- maybeDesugar t
-  pure (ts :< (x ** t))
+  pure (ts :< (l :- (x ** t)))
diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr
index 791014b..690e38c 100644
--- a/src/Inky/Term/Substitution.idr
+++ b/src/Inky/Term/Substitution.idr
@@ -110,24 +110,24 @@ thinTyBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinTyBranchesName
 
 public export
 Env : Mode -> Type -> SnocList String -> SnocList String -> SnocList String -> Type
-Env mode m tyCtx ctx1 ctx2 = All (const $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
+Env mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
 
 public export
 Env' : Mode -> Type -> SnocList String -> List String -> SnocList String -> Type
-Env' mode m tyCtx ctx1 ctx2 = All (const $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
+Env' mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
 
 public export
 thinEnv :
   ctx2 `Thins` ctx3 ->
   Env mode m tyCtx ctx1 ctx2 ->
   Env mode m tyCtx ctx1 ctx3
-thinEnv f = mapProperty (bimap (index f) (thin $ f))
+thinEnv f = mapProperty (map $ bimap (index f) (thin $ f))
 
 public export
 lift :
   Env mode m tyCtx ctx1 ctx2 ->
   Env mode m tyCtx (ctx1 :< x) (ctx2 :< x)
-lift f = thinEnv (Drop Id) f :< Left (%% x)
+lift f = thinEnv (Drop Id) f :< (x :- Left (%% x))
 
 public export
 sub :
@@ -160,12 +160,12 @@ keepBound :
   forall ctx. {0 bound : List String} ->
   LengthOf bound -> Env' mode m tyCtx bound (ctx <>< bound)
 keepBound Z = []
-keepBound (S len) = Left (index (dropFish Id len) (toVar Here)) :: keepBound len
+keepBound (S len) = (_ :- Left (index (dropFish Id len) (toVar Here))) :: keepBound len
 
 sub f (Annot meta t a) = Annot meta (sub f t) a
-sub f (Var meta i) = either (Var meta) id $ indexAll i.pos f
+sub f (Var meta i) = either (Var meta) id (indexAll i.pos f).value
 sub f (Let meta e (x ** t)) = Let meta (sub f e) (x ** sub (lift f) t)
-sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ thinTy (Drop Id)) f) t)
+sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ map $ thinTy (Drop Id)) f) t)
 sub f (Abs meta (bound ** t)) =
   let len = lengthOf bound in
   Abs meta (bound ** sub (thinEnv (dropFish Id len) f <>< keepBound len) t)