Make everything relevant.

Too few proofs were relevant. Now they are.

1 files changed, 643 insertions, 330 deletions

diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 26f3c0f..45645bc 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -1,421 +1,734 @@
 module Inky.Type
 
-import Data.Bool.Decidable
+import public Inky.Data.Context.Var
+import public Inky.Data.Row
+import public Inky.Data.SnocList.Var
+
+import Control.Function
 import Data.DPair
-import Data.Maybe.Decidable
 import Data.These
-import Data.These.Decidable
-import Inky.Context
-import Inky.Thinning
+
+import Inky.Data.SnocList.Thinning
+import Inky.Data.Thinned
+import Inky.Decidable
+import Inky.Decidable.Maybe
+
+%hide Prelude.Ops.infixl.(>=>)
 
 -- Definition ------------------------------------------------------------------
 
 public export
-data Ty : Context () -> () -> Type where
-  TVar : Var ctx v -> Ty ctx v
-  TNat : Ty ctx ()
-  TArrow : Ty ctx () -> Ty ctx () -> Ty ctx ()
-  TProd : Row (Ty ctx ()) -> Ty ctx ()
-  TSum : Row (Ty ctx ()) -> Ty ctx ()
-  TFix : (x : String) -> Ty (ctx :< (x :- ())) () -> Ty ctx ()
+data Ty : SnocList String -> Type where
+  TVar : Var ctx -> Ty ctx
+  TArrow : Ty ctx -> Ty ctx -> Ty ctx
+  TProd : (as : Row (Ty ctx)) -> Ty ctx
+  TSum : (as : Row (Ty ctx)) -> Ty ctx
+  TFix : (x : String) -> Ty (ctx :< x) -> Ty ctx
 
 %name Ty a, b, c
 
---------------------------------------------------------------------------------
+export
+Injective TProd where
+ injective Refl = Refl
+
+export
+Injective TSum where
+ injective Refl = Refl
+
+export
+fixInjective : TFix x t = TFix y u -> the (x ** Ty (ctx :< x)) (x ** t) = (y ** u)
+fixInjective Refl = Refl
+
+-- Decisions -------------------------------------------------------------------
+
+export
+Uninhabited (TVar i = TArrow a b) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TVar i = TProd as) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TVar i = TSum as) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TVar i = TFix x a) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TArrow a b = TProd as) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TArrow a b = TSum as) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TArrow a b = TFix x c) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TProd as = TArrow a b) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TProd as = TSum bs) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TProd as = TFix x a) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TSum as = TArrow a b) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TSum as = TProd bs) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TSum as = TFix x a) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TFix x a = TArrow b c) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TFix x a = TProd as) where
+  uninhabited Refl impossible
+
+export
+Uninhabited (TFix x a = TSum as) where
+  uninhabited Refl impossible
+
+public export
+isArrow :
+  (a : Ty ctx) ->
+  Proof (Ty ctx, Ty ctx) (\bc => a = TArrow (fst bc) (snd bc))
+    ((b, c : Ty ctx) -> Not (a = TArrow b c))
+isArrow (TVar i) = Nothing `Because` (\_, _ => absurd)
+isArrow (TArrow a b) = Just (a, b) `Because` Refl
+isArrow (TProd as) = Nothing `Because` (\_, _ => absurd)
+isArrow (TSum as) = Nothing `Because` (\_, _ => absurd)
+isArrow (TFix x a) = Nothing `Because` (\_, _ => absurd)
+
+public export
+isProd : (a : Ty ctx) -> DecWhen (Row (Ty ctx)) (\as => a = TProd as)
+isProd (TVar i) = Nothing `Because` (\_ => absurd)
+isProd (TArrow a b) = Nothing `Because` (\_ => absurd)
+isProd (TProd as) = Just as `Because` Refl
+isProd (TSum as) = Nothing `Because` (\_ => absurd)
+isProd (TFix x a) = Nothing `Because` (\_ => absurd)
+
+public export
+isSum : (a : Ty ctx) -> DecWhen (Row (Ty ctx)) (\as => a = TSum as)
+isSum (TVar i) = Nothing `Because` (\_ => absurd)
+isSum (TArrow a b) = Nothing `Because` (\_ => absurd)
+isSum (TProd as) = Nothing `Because` (\_ => absurd)
+isSum (TSum as) = Just as `Because` Refl
+isSum (TFix x a) = Nothing `Because` (\_ => absurd)
+
+public export
+isFix :
+  (a : Ty ctx) ->
+  Proof (x ** Ty (ctx :< x)) (\xb => a = TFix (fst xb) (snd xb))
+    ((x : _) -> (b : _) -> Not (a = TFix x b))
+isFix (TVar i) = Nothing `Because` (\_, _ => absurd)
+isFix (TArrow a b) = Nothing `Because` (\_, _ => absurd)
+isFix (TProd as) = Nothing `Because` (\_, _ => absurd)
+isFix (TSum as) = Nothing `Because` (\_, _ => absurd)
+isFix (TFix x a) = Just (x ** a) `Because` Refl
+
 -- Thinning --------------------------------------------------------------------
---------------------------------------------------------------------------------
 
-thin : ctx1 `Thins` ctx2 -> forall v. Ty ctx1 v -> Ty ctx2 v
-thinAll : ctx1 `Thins` ctx2 -> forall v. Row (Ty ctx1 v) -> Row (Ty ctx2 v)
-thinAllFresh :
-  (f : ctx1 `Thins` ctx2) -> (x : String) ->
-  forall v. (row : Row (Ty ctx1 v)) ->
-  So (x `freshIn` row) -> So (x `freshIn` thinAll f row)
+thin : ctx1 `Thins` ctx2 -> Ty ctx1 -> Ty ctx2
+thinAll : ctx1 `Thins` ctx2 -> Context (Ty ctx1) -> Context (Ty ctx2)
+thinAllNames :
+  (f : ctx1 `Thins` ctx2) ->
+  (ctx : Context (Ty ctx1)) ->
+  (thinAll f ctx).names = ctx.names
 
 thin f (TVar i) = TVar (index f i)
-thin f TNat = TNat
 thin f (TArrow a b) = TArrow (thin f a) (thin f b)
-thin f (TProd as) = TProd (thinAll f as)
-thin f (TSum as) = TSum (thinAll f as)
+thin f (TProd (MkRow as fresh)) = TProd (MkRow (thinAll f as) (rewrite thinAllNames f as in fresh))
+thin f (TSum (MkRow as fresh)) = TSum (MkRow (thinAll f as) (rewrite thinAllNames f as in fresh))
 thin f (TFix x a) = TFix x (thin (Keep f) a)
 
 thinAll f [<] = [<]
-thinAll f ((:<) as (x :- a) {fresh}) =
-  (:<) (thinAll f as) (x :- thin f a) {fresh = thinAllFresh f x as fresh}
+thinAll f (as :< (n :- a)) = thinAll f as :< (n :- thin f a)
 
-thinAllFresh f x [<] = id
-thinAllFresh f x (as :< (y :- a)) = andSo . mapSnd (thinAllFresh f x as) . soAnd
+thinAllNames f [<] = Refl
+thinAllNames f (as :< (n :- a)) = cong (:< n) $ thinAllNames f as
 
 -- Renaming Coalgebra
 
-thinCong : f ~~~ g -> forall v. (a : Ty ctx1 v) -> thin f a = thin g a
-thinCongAll : f ~~~ g -> forall v. (as : Row (Ty ctx1 v)) -> thinAll f as = thinAll g as
+thinCong : f ~~~ g -> (a : Ty ctx1) -> thin f a = thin g a
+thinCongAll : f ~~~ g -> (as : Context (Ty ctx1)) -> thinAll f as = thinAll g as
 
 thinCong prf (TVar i) = cong TVar (prf.index i)
-thinCong prf TNat = Refl
 thinCong prf (TArrow a b) = cong2 TArrow (thinCong prf a) (thinCong prf b)
-thinCong prf (TProd as) = cong TProd (thinCongAll prf as)
-thinCong prf (TSum as) = cong TSum (thinCongAll prf as)
+thinCong prf (TProd (MkRow as fresh)) = cong TProd (rowCong $ thinCongAll prf as)
+thinCong prf (TSum (MkRow as fresh)) = cong TSum (rowCong $ thinCongAll prf as)
 thinCong prf (TFix x a) = cong (TFix x) (thinCong (KeepKeep prf) a)
 
 thinCongAll prf [<] = Refl
-thinCongAll prf (as :< (x :- a)) =
-  snocCong2 (thinCongAll prf as) (cong (x :-) $ thinCong prf a)
+thinCongAll prf (as :< (n :- a)) =
+  cong2 (:<) (thinCongAll prf as) (cong (n :-) $ thinCong prf a)
 
-thinId : (a : Ty ctx v) -> thin Id a = a
-thinIdAll : (as : Row (Ty ctx v)) -> thinAll Id as = as
+thinId : (a : Ty ctx) -> thin Id a = a
+thinIdAll : (as : Context (Ty ctx)) -> thinAll Id as = as
 
 thinId (TVar (%% x)) = Refl
-thinId TNat = Refl
 thinId (TArrow a b) = cong2 TArrow (thinId a) (thinId b)
-thinId (TProd as) = cong TProd (thinIdAll as)
-thinId (TSum as) = cong TSum (thinIdAll as)
+thinId (TProd (MkRow as fresh)) = cong TProd (rowCong $ thinIdAll as)
+thinId (TSum (MkRow as fresh)) = cong TSum (rowCong $ thinIdAll as)
 thinId (TFix x a) = cong (TFix x) (trans (thinCong (KeepId IdId) a) (thinId a))
 
 thinIdAll [<] = Refl
-thinIdAll (as :< (x :- a)) =
-  snocCong2 (thinIdAll as) (cong (x :-) $ thinId a)
+thinIdAll (as :< (n :- a)) = cong2 (:<) (thinIdAll as) (cong (n :-) $ thinId a)
 
 export
-Rename () Ty where
-  var = TVar
+Rename String Ty where
   rename = thin
   renameCong = thinCong
   renameId = thinId
 
--- Equality --------------------------------------------------------------------
-
-Preeq :
-  {ctx2 : Context ()} -> {v : ()} ->
-  Ty ctx1 v -> Ty ctx2 v -> ctx1 `Thins` ctx2 -> Type
-PreeqAll :
-  {ctx2 : Context ()} -> {v : ()} ->
-  Row (Ty ctx1 v) -> Row (Ty ctx2 v) -> ctx1 `Thins` ctx2 -> Type
-
-Preeq (TVar i) (TVar j) f = index f i = j
-Preeq (TNat) (TNat) f = ()
-Preeq (TArrow a b) (TArrow c d) f = (Preeq a c f, Preeq b d f)
-Preeq (TProd as) (TProd bs) f = PreeqAll as bs f
-Preeq (TSum as) (TSum bs) f = PreeqAll as bs f
-Preeq (TFix x a) (TFix y b) f = Preeq a b (Keep f)
-Preeq _ _ f = Void
-
-PreeqAll [<] bs f = (bs = [<])
-PreeqAll (as :< (x :- a)) bs f =
-  ( b ** cs **
-  ( Remove x bs b cs
-  , Preeq a b f
-  , PreeqAll as cs f
-  ))
-
-preeqAllReorder :
-  (as : Row (Ty ctx1 v)) -> bs <~> cs -> (f : ctx1 `Thins` ctx2) ->
-  PreeqAll as bs f -> PreeqAll as cs f
-preeqAllReorder [<] [] f Refl = Refl
-preeqAllReorder [<] (step :: prf) f Refl impossible
-preeqAllReorder (as :< (x :- a)) prf f (b ** bs ** (prf', eq1, eq2)) =
-  (b ** bs ** (bimap id (trans (sym prf)) prf', eq1, eq2))
-
-preeq : Ty ctx1 v -> Ty ctx2 v -> ctx1 `Thins` ctx2 -> Bool
-preeqAll : Row (Ty ctx1 v) -> Row (Ty ctx2 v) -> ctx1 `Thins` ctx2 -> Bool
-
-preeq (TVar i) (TVar j) f = index f i == j
-preeq TNat TNat f = True
-preeq (TArrow a b) (TArrow c d) f = preeq a c f && preeq b d f
-preeq (TProd as) (TProd bs) f = preeqAll as bs f
-preeq (TSum as) (TSum bs) f = preeqAll as bs f
-preeq (TFix x a) (TFix y b) f = preeq a b (Keep f)
-preeq _ _ f = False
-
-preeqAll [<] bs f = null bs
-preeqAll (as :< (x :- a)) bs f =
-  case remove' x bs of
-    Just (b, bs) => preeq a b f && preeqAll as bs f
-    Nothing => False
-
-export
-reflectAnd : a `Reflects` b1 -> b `Reflects` b2 -> (a, b) `Reflects` (b1 && b2)
-reflectAnd (RTrue x) (RTrue y) = RTrue (x, y)
-reflectAnd (RTrue x) (RFalse f) = RFalse (f . snd)
-reflectAnd (RFalse f) _ = RFalse (f . fst)
-
-0 reflectPreeq :
-  (a : Ty ctx1 v) -> (b : Ty ctx2 v) -> (f : ctx1 `Thins` ctx2) ->
-  Preeq a b f `Reflects` preeq a b f
-0 reflectPreeqAll :
-  (as : Row (Ty ctx1 v)) -> (bs : Row (Ty ctx2 v)) -> (f : ctx1 `Thins` ctx2) ->
-  PreeqAll as bs f `Reflects` preeqAll as bs f
-
-reflectPreeq (TVar i) (TVar j) f = reflectEq (index f i) j
-reflectPreeq (TVar i) TNat f = RFalse id
-reflectPreeq (TVar i) (TArrow a b) f = RFalse id
-reflectPreeq (TVar i) (TProd as) f = RFalse id
-reflectPreeq (TVar i) (TSum as) f = RFalse id
-reflectPreeq (TVar i) (TFix x a) f = RFalse id
-reflectPreeq TNat (TVar i) f = RFalse id
-reflectPreeq TNat TNat f = RTrue ()
-reflectPreeq TNat (TArrow a b) f = RFalse id
-reflectPreeq TNat (TProd as) f = RFalse id
-reflectPreeq TNat (TSum as) f = RFalse id
-reflectPreeq TNat (TFix x a) f = RFalse id
-reflectPreeq (TArrow a c) (TVar i) f = RFalse id
-reflectPreeq (TArrow a c) TNat f = RFalse id
-reflectPreeq (TArrow a c) (TArrow b d) f = reflectAnd (reflectPreeq a b f) (reflectPreeq c d f)
-reflectPreeq (TArrow a c) (TProd as) f = RFalse id
-reflectPreeq (TArrow a c) (TSum as) f = RFalse id
-reflectPreeq (TArrow a c) (TFix x b) f = RFalse id
-reflectPreeq (TProd as) (TVar i) f = RFalse id
-reflectPreeq (TProd as) TNat f = RFalse id
-reflectPreeq (TProd as) (TArrow a b) f = RFalse id
-reflectPreeq (TProd as) (TProd bs) f = reflectPreeqAll as bs f
-reflectPreeq (TProd as) (TSum bs) f = RFalse id
-reflectPreeq (TProd as) (TFix x a) f = RFalse id
-reflectPreeq (TSum as) (TVar i) f = RFalse id
-reflectPreeq (TSum as) TNat f = RFalse id
-reflectPreeq (TSum as) (TArrow a b) f = RFalse id
-reflectPreeq (TSum as) (TProd bs) f = RFalse id
-reflectPreeq (TSum as) (TSum bs) f = reflectPreeqAll as bs f
-reflectPreeq (TSum as) (TFix x a) f = RFalse id
-reflectPreeq (TFix x a) (TVar i) f = RFalse id
-reflectPreeq (TFix x a) TNat f = RFalse id
-reflectPreeq (TFix x a) (TArrow b c) f = RFalse id
-reflectPreeq (TFix x a) (TProd as) f = RFalse id
-reflectPreeq (TFix x a) (TSum as) f = RFalse id
-reflectPreeq (TFix x a) (TFix y b) f = reflectPreeq a b (Keep f)
-
-reflectPreeqAll [<] [<] f = RTrue Refl
-reflectPreeqAll [<] (_ :< _) f = RFalse (\case Refl impossible)
-reflectPreeqAll (as :< (x :- a)) bs f with (reflectRemove x bs) | (remove' x bs)
-  _ | RJust (Evidence fresh prf) | Just (b, cs) with (reflectAnd (reflectPreeq a b f) (reflectPreeqAll as cs f)) | (preeq a b f && preeqAll as cs f)
-    _ | RTrue prf' | _ = RTrue (b ** cs ** (Evidence fresh prf, prf'))
-    _ | RFalse nprf | _ =
-      RFalse (\(b' ** cs' ** (prf1, prf2)) =>
-        let (eq, reorder) = removeUnique x bs (Evidence fresh prf) prf1 in
-        nprf $
-        bimap
-          (\x => rewrite eq in x)
-          (preeqAllReorder as (sym reorder) f)
-          prf2)
-  _ | RNothing nprf | _ = RFalse (\(b ** cs ** (prf, _)) => nprf (b, cs) prf)
+-- Alpha Equivalence ------------------------------------------------------------
 
-public export
-Eq (Ty ctx v) where
-  a == b = preeq a b Id
+namespace Shape
+  public export
+  data SameShape : Ty ctx1 -> Ty ctx2 -> Type where
+    TVar : SameShape (TVar i) (TVar j)
+    TArrow : SameShape (TArrow a c) (TArrow b d)
+    TProd : SameShape (TProd as) (TProd bs)
+    TSum : SameShape (TSum as) (TSum bs)
+    TFix : SameShape (TFix x a) (TFix y b)
 
 export
-Eq : {ctx : Context ()} -> {v : ()} -> Ty ctx v -> Ty ctx v -> Type
-Eq a b = Preeq a b Id
+Uninhabited (SameShape (TVar i) (TArrow b d))
+  where uninhabited TVar impossible
 
 export
-0 reflectEq : (a, b : Ty ctx v) -> (a `Eq` b) `Reflects` (a == b)
-reflectEq a b = reflectPreeq a b Id
+Uninhabited (SameShape (TVar i) (TProd bs))
+  where uninhabited TVar impossible
 
--- Occurs ----------------------------------------------------------------------
+export
+Uninhabited (SameShape (TVar i) (TSum bs))
+  where uninhabited TVar impossible
 
-OccursIn : Var ctx v -> Ty ctx w -> Type
-OccursInAny : Var ctx v -> Row (Ty ctx w) -> Type
+export
+Uninhabited (SameShape (TVar i) (TFix y b))
+  where uninhabited TVar impossible
 
-i `OccursIn` TVar j = i = j
-i `OccursIn` TNat = Void
-i `OccursIn` TArrow a b = These (i `OccursIn` a) (i `OccursIn` b)
-i `OccursIn` TProd as = i `OccursInAny` as
-i `OccursIn` TSum as = i `OccursInAny` as
-i `OccursIn` TFix x a = ThereVar i `OccursIn` a
+export
+Uninhabited (SameShape (TArrow a b) (TVar j))
+  where uninhabited TVar impossible
 
-i `OccursInAny` [<] = Void
-i `OccursInAny` (as :< (x :- a)) = These (i `OccursIn` a) (i `OccursInAny` as)
+export
+Uninhabited (SameShape (TArrow a c) (TProd bs))
+  where uninhabited TVar impossible
 
--- Decidable
+export
+Uninhabited (SameShape (TArrow a c) (TSum bs))
+  where uninhabited TVar impossible
 
-occursIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool
-occursInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool
+export
+Uninhabited (SameShape (TArrow a c) (TFix y b))
+  where uninhabited TVar impossible
 
-i `occursIn` (TVar j) = i `eq` j
-i `occursIn` TNat = False
-i `occursIn` (TArrow a b) = (i `occursIn` a) || (i `occursIn` b)
-i `occursIn` (TProd as) = i `occursInAny` as
-i `occursIn` (TSum as) = i `occursInAny` as
-i `occursIn` (TFix x a) = ThereVar i `occursIn` a
+export
+Uninhabited (SameShape (TProd as) (TVar j))
+  where uninhabited TVar impossible
 
-i `occursInAny` [<] = False
-i `occursInAny` (as :< (x :- a)) = (i `occursIn` a) || (i `occursInAny` as)
+export
+Uninhabited (SameShape (TProd as) (TArrow b d))
+  where uninhabited TVar impossible
 
-reflectOccursIn :
-  (i : Var ctx v) -> (a : Ty ctx w) ->
-  (i `OccursIn` a) `Reflects` (i `occursIn` a)
-reflectOccursInAny :
-  (i : Var ctx v) -> (as : Row (Ty ctx w)) ->
-  (i `OccursInAny` as) `Reflects` (i `occursInAny` as)
+export
+Uninhabited (SameShape (TProd as) (TSum bs))
+  where uninhabited TVar impossible
 
-reflectOccursIn i (TVar j) = reflectEq i j
-reflectOccursIn i TNat = RFalse id
-reflectOccursIn i (TArrow a b) = reflectThese (reflectOccursIn i a) (reflectOccursIn i b)
-reflectOccursIn i (TProd as) = reflectOccursInAny i as
-reflectOccursIn i (TSum as) = reflectOccursInAny i as
-reflectOccursIn i (TFix x a) = reflectOccursIn (ThereVar i) a
+export
+Uninhabited (SameShape (TProd as) (TFix y b))
+  where uninhabited TVar impossible
+
+export
+Uninhabited (SameShape (TSum as) (TVar j))
+  where uninhabited TVar impossible
+
+export
+Uninhabited (SameShape (TSum as) (TArrow b d))
+  where uninhabited TVar impossible
+
+export
+Uninhabited (SameShape (TSum as) (TProd bs))
+  where uninhabited TVar impossible
+
+export
+Uninhabited (SameShape (TSum as) (TFix y b))
+  where uninhabited TVar impossible
+
+export
+Uninhabited (SameShape (TFix x a) (TVar j))
+  where uninhabited TVar impossible
+
+export
+Uninhabited (SameShape (TFix x a) (TArrow b d))
+  where uninhabited TVar impossible
+
+export
+Uninhabited (SameShape (TFix x a) (TProd bs))
+  where uninhabited TVar impossible
+
+export
+Uninhabited (SameShape (TFix x a) (TSum bs))
+  where uninhabited TVar impossible
+
+namespace Equivalence
+  public export
+  data Alpha : Ty ctx1 -> Ty ctx2 -> Type
+  public export
+  data AllAlpha : Context (Ty ctx1) -> Context (Ty ctx2) -> Type
+
+  data Alpha where
+    TVar : elemToNat i.pos = elemToNat j.pos -> Alpha (TVar i) (TVar j)
+    TArrow : Alpha a b -> Alpha c d -> Alpha (TArrow a c) (TArrow b d)
+    TProd : AllAlpha as.context bs.context -> Alpha (TProd as) (TProd bs)
+    TSum : AllAlpha as.context bs.context -> Alpha (TSum as) (TSum bs)
+    TFix : Alpha a b -> Alpha (TFix x a) (TFix y b)
+
+  data AllAlpha where
+    Base : AllAlpha [<] [<]
+    Step :
+      (i : Elem (n :- b) bs) ->
+      Alpha a b ->
+      AllAlpha as (dropElem bs i) ->
+      AllAlpha (as :< (n :- a)) bs
+
+namespace Inequivalence
+  public export
+  data NotAlpha : Ty ctx1 -> Ty ctx2 -> Type
+  public export
+  data AnyNotAlpha : Context (Ty ctx1) -> Context (Ty ctx2) -> Type
+
+  data NotAlpha where
+    Shape :
+      Not (SameShape a b) ->
+      NotAlpha a b
+    TVar :
+      Not (elemToNat i.pos = elemToNat j.pos) ->
+      NotAlpha (TVar i) (TVar j)
+    TArrow :
+      These (NotAlpha a b) (NotAlpha c d) ->
+      NotAlpha (TArrow a c) (TArrow b d)
+    TProd :
+      AnyNotAlpha as.context bs.context ->
+      NotAlpha (TProd as) (TProd bs)
+    TSum :
+      AnyNotAlpha as.context bs.context ->
+      NotAlpha (TSum as) (TSum bs)
+    TFix :
+      NotAlpha a b ->
+      NotAlpha (TFix x a) (TFix y b)
+
+  data AnyNotAlpha where
+    Base : AnyNotAlpha [<] (bs :< b)
+    Step1 :
+      ((b : Ty ctx2) -> Not (Elem (n :- b) bs)) ->
+      AnyNotAlpha (as :< (n :- a)) bs
+    Step2 :
+      (i : Elem (n :- b) bs) ->
+      These (NotAlpha a b) (AnyNotAlpha as (dropElem bs i)) ->
+      AnyNotAlpha (as :< (n :- a)) bs
+
+%name Alpha prf
+%name AllAlpha prfs
+%name NotAlpha contra
+%name AnyNotAlpha contras
+
+export
+alphaShape : Alpha a b -> SameShape a b
+alphaShape (TVar prf) = TVar
+alphaShape (TArrow prf1 prf2) = TArrow
+alphaShape (TProd prfs) = TProd
+alphaShape (TSum prfs) = TSum
+alphaShape (TFix prf) = TFix
+
+export
+alphaRefl : (a : Ty ctx1) -> (0 b : Ty ctx2) -> a ~=~ b -> Alpha a b
+allAlphaRefl : (as : Context (Ty ctx1)) -> (bs : Context (Ty ctx2)) -> as ~=~ bs -> AllAlpha as bs
+
+alphaRefl (TVar i) .(TVar i) Refl = TVar Refl
+alphaRefl (TArrow a b) .(TArrow a b) Refl = TArrow (alphaRefl a a Refl) (alphaRefl b b Refl)
+alphaRefl (TProd (MkRow as fresh)) .(TProd (MkRow as fresh)) Refl = TProd (allAlphaRefl as as Refl)
+alphaRefl (TSum (MkRow as fresh)) .(TSum (MkRow as fresh)) Refl = TSum (allAlphaRefl as as Refl)
+alphaRefl (TFix x a) .(TFix x a) Refl = TFix (alphaRefl a a Refl)
+
+allAlphaRefl [<] .([<]) Refl = Base
+allAlphaRefl (as :< (l :- a)) .(as :< (l :- a)) Refl =
+  Step Here (alphaRefl a a Refl) (allAlphaRefl as as Refl)
+
+export
+alphaSplit :
+  {0 a : Ty ctx1} -> {0 b : Ty ctx2} ->
+  Alpha a b -> NotAlpha a b -> Void
+export
+allAlphaSplit :
+  {0 as : Context (Ty ctx1)} -> {0 bs : Context (Ty ctx2)} ->
+  (0 fresh : AllFresh bs.names) ->
+  AllAlpha as bs -> AnyNotAlpha as bs -> Void
+
+alphaSplit prf (Shape contra) = contra (alphaShape prf)
+alphaSplit (TVar prf) (TVar contra) = contra prf
+alphaSplit (TArrow prf1 prf2) (TArrow contras) =
+  these (alphaSplit prf1) (alphaSplit prf2) (const $ alphaSplit prf2) contras
+alphaSplit (TProd {bs} prfs) (TProd contras) = allAlphaSplit bs.fresh prfs contras
+alphaSplit (TSum {bs} prfs) (TSum contras) = allAlphaSplit bs.fresh prfs contras
+alphaSplit (TFix prf) (TFix contra) = alphaSplit prf contra
+
+allAlphaSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i
+allAlphaSplit fresh (Step {as, n} i prf prfs) (Step2 j contras) =
+  let 0 eq = lookupUnique (MkRow bs fresh) i j in
+  these
+    (\contra => alphaSplit prf $ rewrite cong fst eq in contra)
+    (\contras =>
+      allAlphaSplit (dropElemFresh bs fresh i) prfs $
+      replace {p = \bi => AnyNotAlpha as (dropElem bs {x = n :- fst bi} $ snd bi)}
+        (sym eq)
+        contras)
+    (\contra, _ => alphaSplit prf $ rewrite cong fst eq in contra)
+    contras
+
+export
+alpha : (a : Ty ctx1) -> (b : Ty ctx2) -> LazyEither (Alpha a b) (NotAlpha a b)
+export
+allAlpha :
+  (as : Context (Ty ctx1)) -> (bs : Context (Ty ctx2)) ->
+  LazyEither (AllAlpha as bs) (AnyNotAlpha as bs)
+
+alpha (TVar i) (TVar j) = map TVar TVar $ decEq (elemToNat i.pos) (elemToNat j.pos)
+alpha (TVar i) (TArrow a b) = False `Because` Shape absurd
+alpha (TVar i) (TProd as) = False `Because` Shape absurd
+alpha (TVar i) (TSum as) = False `Because` Shape absurd
+alpha (TVar i) (TFix x a) = False `Because` Shape absurd
+alpha (TArrow a c) (TVar i) = False `Because` Shape absurd
+alpha (TArrow a c) (TArrow b d) = map (uncurry TArrow) TArrow $ all (alpha a b) (alpha c d)
+alpha (TArrow a c) (TProd as) = False `Because` Shape absurd
+alpha (TArrow a c) (TSum as) = False `Because` Shape absurd
+alpha (TArrow a c) (TFix x b) = False `Because` Shape absurd
+alpha (TProd as) (TVar i) = False `Because` Shape absurd
+alpha (TProd as) (TArrow a b) = False `Because` Shape absurd
+alpha (TProd (MkRow as _)) (TProd bs) = map TProd TProd $ allAlpha as bs.context
+alpha (TProd as) (TSum bs) = False `Because` Shape absurd
+alpha (TProd as) (TFix x a) = False `Because` Shape absurd
+alpha (TSum as) (TVar i) = False `Because` Shape absurd
+alpha (TSum as) (TArrow a b) = False `Because` Shape absurd
+alpha (TSum as) (TProd bs) = False `Because` Shape absurd
+alpha (TSum (MkRow as _)) (TSum bs) = map TSum TSum $ allAlpha as bs.context
+alpha (TSum as) (TFix x a) = False `Because` Shape absurd
+alpha (TFix x a) (TVar i) = False `Because` Shape absurd
+alpha (TFix x a) (TArrow b c) = False `Because` Shape absurd
+alpha (TFix x a) (TProd as) = False `Because` Shape absurd
+alpha (TFix x a) (TSum as) = False `Because` Shape absurd
+alpha (TFix x a) (TFix y b) = map TFix TFix $ alpha a b
+
+allAlpha [<] [<] = True `Because` Base
+allAlpha [<] (bs :< nb) = False `Because` Base
+allAlpha (as :< (n :- a)) bs =
+  map
+    (\((b ** i) ** (prf1, prf2)) => Step i prf1 prf2)
+    (either Step1 false) $
+  (bi := (decLookup n bs).forget) >=>
+  all (alpha a $ fst bi) (allAlpha as (dropElem bs $ snd bi))
+  where
+  p : (b ** Elem (n :- b) bs) -> Type
+  p bi = (Alpha a (fst bi), AllAlpha as (dropElem bs $ snd bi))
+
+  q : (b ** Elem (n :- b) bs) -> Type
+  q bi = These (NotAlpha a (fst bi)) (AnyNotAlpha as (dropElem bs $ snd bi))
+
+  false : (bi ** q bi) -> AnyNotAlpha (as :< (n :- a)) bs
+  false ((b ** i) ** contras) = Step2 i contras
+
+-- Occurs ----------------------------------------------------------------------
 
-reflectOccursInAny i [<] = RFalse id
-reflectOccursInAny i (as :< (x :- a)) =
-  reflectThese (reflectOccursIn i a) (reflectOccursInAny i as)
+namespace Strengthen
+  public export
+  data Strengthen : (i : Var ctx) -> Ty ctx -> Ty (dropElem ctx i.pos) -> Type
+  public export
+  data StrengthenAll :
+    (i : Var ctx) -> (as : Context (Ty ctx)) ->
+    All (const $ Ty $ dropElem ctx i.pos) as.names -> Type
+
+  data Strengthen where
+    TVar : (j = index (dropPos i.pos) k) -> Strengthen i (TVar j) (TVar k)
+    TArrow : Strengthen i a c -> Strengthen i b d -> Strengthen i (TArrow a b) (TArrow c d)
+    TProd : StrengthenAll i as.context bs -> Strengthen i (TProd as) (TProd $ fromAll as bs)
+    TSum : StrengthenAll i as.context bs -> Strengthen i (TSum as) (TSum $ fromAll as bs)
+    TFix : Strengthen (ThereVar i) a b -> Strengthen i (TFix x a) (TFix x b)
+
+  data StrengthenAll where
+    Lin : StrengthenAll i [<] [<]
+    (:<) : StrengthenAll i as bs -> Strengthen i a b -> StrengthenAll i (as :< (l :- a)) (bs :< b)
+
+  %name Strengthen prf
+  %name StrengthenAll prfs
+
+strengthenEq : Strengthen i a b -> a = thin (dropPos i.pos) b
+strengthenAllEq : StrengthenAll i as bs -> as = thinAll (dropPos i.pos) (fromAll as bs)
+
+strengthenEq (TVar prf) = cong TVar prf
+strengthenEq (TArrow prf1 prf2) = cong2 TArrow (strengthenEq prf1) (strengthenEq prf2)
+strengthenEq (TProd {as = MkRow _ _} prfs) = cong TProd $ rowCong $ strengthenAllEq prfs
+strengthenEq (TSum {as = MkRow _ _} prfs) = cong TSum $ rowCong $ strengthenAllEq prfs
+strengthenEq (TFix prf) = cong (TFix _) $ strengthenEq prf
+
+strengthenAllEq [<] = Refl
+strengthenAllEq ((:<) {l} prfs prf) =
+  cong2 (:<) (strengthenAllEq prfs) (cong (l :-) $ strengthenEq prf)
+
+namespace Occurs
+  public export
+  data OccursIn : Var ctx -> Ty ctx -> Type
+  public export
+  data OccursInAny : Var ctx -> Context (Ty ctx) -> Type
+
+  data OccursIn where
+    TVar : i = j -> i `OccursIn` TVar j
+    TArrow : These (i `OccursIn` a) (i `OccursIn` b) -> i `OccursIn` TArrow a b
+    TProd : i `OccursInAny` as.context -> i `OccursIn` TProd as
+    TSum : i `OccursInAny` as.context -> i `OccursIn` TSum as
+    TFix : ThereVar i `OccursIn` a -> i `OccursIn` TFix x a
+
+  data OccursInAny where
+    And : These (i `OccursInAny` as) (i `OccursIn` a) -> i `OccursInAny` (as :< (n :- a))
+
+  %name OccursIn contra
+  %name OccursInAny contras
+
+export
+Uninhabited (i `OccursInAny` [<]) where
+  uninhabited (And prf) impossible
+
+export
+strengthenSplit : Strengthen i a b -> i `OccursIn` a -> Void
+strengthenAllSplit : StrengthenAll i as bs -> i `OccursInAny` as -> Void
+
+strengthenSplit (TVar Refl) (TVar {i = %% n} contra) = void $ lemma _ _ contra
+  where
+  lemma :
+    (i : Elem x sx) -> (j : Elem y (dropElem sx i)) ->
+    Not (toVar i = toVar (indexPos (dropPos i) j))
+  lemma Here j prf = absurd (toVarInjective prf)
+  lemma (There i) Here prf = absurd (toVarInjective prf)
+  lemma (There i) (There j) prf = lemma i j $ toVarCong $ thereInjective $ toVarInjective prf
+strengthenSplit (TArrow prf1 prf2) (TArrow contras) =
+  these (strengthenSplit prf1) (strengthenSplit prf2) (const $ strengthenSplit prf2) contras
+strengthenSplit (TProd prfs) (TProd contras) = strengthenAllSplit prfs contras
+strengthenSplit (TSum prfs) (TSum contras) = strengthenAllSplit prfs contras
+strengthenSplit (TFix prf) (TFix contra) = strengthenSplit prf contra
+
+strengthenAllSplit (prfs :< prf) (And contras) =
+  these (strengthenAllSplit prfs) (strengthenSplit prf) (const $ strengthenSplit prf) contras
+
+export
+strengthen :
+  (i : Var ctx) -> (a : Ty ctx) ->
+  Proof (Ty (dropElem ctx i.pos)) (Strengthen i a) (i `OccursIn` a)
+export
+strengthenAll :
+  (i : Var ctx) -> (as : Context (Ty ctx)) ->
+  Proof (All (const $ Ty $ dropElem ctx i.pos) as.names) (StrengthenAll i as) (i `OccursInAny` as)
+
+strengthen ((%%) x {pos = i}) (TVar ((%%) y {pos = j})) =
+  map (TVar . toVar)
+    (\_, prf => TVar $ toVarCong prf)
+    (TVar . toVarCong . skipsDropPos i) $
+  strengthen (dropPos i) j
+strengthen i (TArrow a b) =
+  map (uncurry TArrow) (\(c, d) => uncurry TArrow) TArrow $
+  all (strengthen i a) (strengthen i b)
+strengthen i (TProd (MkRow as fresh)) =
+  map (TProd . fromAll (MkRow as fresh)) (\_ => TProd) TProd $
+  strengthenAll i as
+strengthen i (TSum (MkRow as fresh)) =
+  map (TSum . fromAll (MkRow as fresh)) (\_ => TSum) TSum $
+  strengthenAll i as
+strengthen i (TFix x a) =
+  map (TFix x) (\_ => TFix) TFix $
+  strengthen (ThereVar i) a
+
+strengthenAll i [<] = Just [<] `Because` [<]
+strengthenAll i (as :< (l :- a)) =
+  map (uncurry (:<) . swap) (\(_, _) => uncurry (:<) . swap) (And . swap) $
+  all (strengthen i a) (strengthenAll i as)
 
 -- Not Strictly Positive -----------------------------------------------------------
 
 -- We use negation so we get a cause on failure.
 
-NotPositiveIn : Var ctx v -> Ty ctx w -> Type
-NotPositiveInAny : Var ctx v -> Row (Ty ctx w) -> Type
-
-i `NotPositiveIn` TVar j = Void
-i `NotPositiveIn` TNat = Void
-i `NotPositiveIn` TArrow a b =
-  -- NOTE: forbid on right side of arrow to prevent infinite breadth.
-  i `OccursIn` TArrow a b
-i `NotPositiveIn` TProd as = i `NotPositiveInAny` as
-i `NotPositiveIn` TSum as = i `NotPositiveInAny` as
-i `NotPositiveIn` TFix x a =
-  -- BUG: forbid under fixpoint to prevent unbounded width
-  -- this is safe to add back with the complex encoding of fixpoints
-  ThereVar i `OccursIn` a
-
-i `NotPositiveInAny` [<] = Void
-i `NotPositiveInAny` as :< (x :- a) = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as)
-
--- Not Positive implies Occurs
-
-notPositiveToOccurs : (a : Ty ctx v) -> i `NotPositiveIn` a -> i `OccursIn` a
-notPositiveAnyToOccursAny : (as : Row (Ty ctx v)) -> i `NotPositiveInAny` as -> i `OccursInAny` as
-
-notPositiveToOccurs (TVar j) = absurd
-notPositiveToOccurs TNat = id
-notPositiveToOccurs (TArrow a b) = id
-notPositiveToOccurs (TProd as) = notPositiveAnyToOccursAny as
-notPositiveToOccurs (TSum as) = notPositiveAnyToOccursAny as
-notPositiveToOccurs (TFix x a) = id
-
-notPositiveAnyToOccursAny [<] = id
-notPositiveAnyToOccursAny (as :< (x :- a)) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as)
-
--- -- Decidable
-
-notPositiveIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool
-notPositiveInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool
-
-i `notPositiveIn` (TVar j) = False
-i `notPositiveIn` TNat = False
-i `notPositiveIn` (TArrow a b) = i `occursIn` TArrow a b
-i `notPositiveIn` (TProd as) = i `notPositiveInAny` as
-i `notPositiveIn` (TSum as) = i `notPositiveInAny` as
-i `notPositiveIn` (TFix x a) = ThereVar i `occursIn` a
-
-i `notPositiveInAny` [<] = False
-i `notPositiveInAny` (as :< (x :- a)) = (i `notPositiveIn` a) || (i `notPositiveInAny` as)
-
-reflectNotPositiveIn :
-  (i : Var ctx v) -> (a : Ty ctx w) ->
-  (i `NotPositiveIn` a) `Reflects` (i `notPositiveIn` a)
-reflectNotPositiveInAny :
-  (i : Var ctx v) -> (as : Row (Ty ctx w)) ->
-  (i `NotPositiveInAny` as) `Reflects` (i `notPositiveInAny` as)
-
-reflectNotPositiveIn i (TVar j) = RFalse id
-reflectNotPositiveIn i TNat = RFalse id
-reflectNotPositiveIn i (TArrow a b) = reflectOccursIn i (TArrow a b)
-reflectNotPositiveIn i (TProd as) = reflectNotPositiveInAny i as
-reflectNotPositiveIn i (TSum as) = reflectNotPositiveInAny i as
-reflectNotPositiveIn i (TFix x a) = reflectOccursIn (ThereVar i) a
-
-reflectNotPositiveInAny i [<] = RFalse id
-reflectNotPositiveInAny i (as :< (x :- a)) =
-  reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as)
+namespace NotPositive
+  public export
+  data NotPositiveIn : Var ctx -> Ty ctx -> Type
+  public export
+  data NotPositiveInAny : Var ctx -> Context (Ty ctx) -> Type
 
--- Well Formed -----------------------------------------------------------------
+  data NotPositiveIn where
+    TArrow : i `OccursIn` TArrow a b -> i `NotPositiveIn` TArrow a b
+    TProd : i `NotPositiveInAny` as.context -> i `NotPositiveIn` TProd as
+    TSum : i `NotPositiveInAny` as.context -> i `NotPositiveIn` TSum as
+    TFix : ThereVar i `NotPositiveIn` a -> i `NotPositiveIn` TFix x a
 
--- Negating decidable properties is fun.
+  data NotPositiveInAny where
+    And :
+      These (i `NotPositiveInAny` as) (i `NotPositiveIn` a) ->
+      i `NotPositiveInAny` (as :< (n :- a))
+
+  %name NotPositiveIn prf
+  %name NotPositiveInAny prf
+
+export
+Uninhabited (i `NotPositiveIn` TVar j) where
+  uninhabited (TArrow prf) impossible
 
 export
-IllFormed : Ty ctx v -> Type
-AnyIllFormed : Row (Ty ctx v) -> Type
+Uninhabited (i `NotPositiveInAny` [<]) where
+  uninhabited (And prf) impossible
 
-IllFormed (TVar v) = Void
-IllFormed TNat = Void
-IllFormed (TArrow a b) = These (IllFormed a) (IllFormed b)
-IllFormed (TProd as) = AnyIllFormed as
-IllFormed (TSum as) = AnyIllFormed as
-IllFormed (TFix x a) = These (%% x `NotPositiveIn` a) (IllFormed a)
+export
+getOccurs : i `NotPositiveIn` a -> i `OccursIn` a
+export
+getOccursAny : i `NotPositiveInAny` as -> i `OccursInAny` as
 
-AnyIllFormed [<] = Void
-AnyIllFormed (as :< (x :- a)) = These (IllFormed a) (AnyIllFormed as)
+getOccurs (TArrow prf) = prf
+getOccurs (TProd prf) = TProd (getOccursAny prf)
+getOccurs (TSum prf) = TSum (getOccursAny prf)
+getOccurs (TFix prf) = TFix (getOccurs prf)
 
--- Decidable
+getOccursAny (And (This prf)) = And (This (getOccursAny prf))
+getOccursAny (And (That prf)) = And (That (getOccurs prf))
+getOccursAny (And (Both prf1 prf2)) = And (Both (getOccursAny prf1) (getOccurs prf2))
 
 export
-illFormed : (a : Ty ctx v) -> Bool
-anyIllFormed : (as : Row (Ty ctx v)) -> Bool
+notPositiveIn : (i : Var ctx) -> (a : Ty ctx) -> Dec' (i `NotPositiveIn` a)
+notPositiveInAny : (i : Var ctx) -> (as : Context (Ty ctx)) -> Dec' (i `NotPositiveInAny` as)
+
+i `notPositiveIn` TVar j = False `Because` absurd
+i `notPositiveIn` TArrow a b =
+  map TArrow (\(_ ** prf) => \case (TArrow contra) => strengthenSplit prf contra) $
+  not $
+  (strengthen i $ TArrow a b).forget
+i `notPositiveIn` TProd (MkRow as _) = mapDec TProd (\case TProd prf => prf) (i `notPositiveInAny` as)
+i `notPositiveIn` TSum (MkRow as _) = mapDec TSum (\case TSum prf => prf) (i `notPositiveInAny` as)
+i `notPositiveIn` TFix x a = mapDec TFix (\case TFix prf => prf) $ ThereVar i `notPositiveIn` a
+
+i `notPositiveInAny` [<] = False `Because` absurd
+i `notPositiveInAny` (as :< (n :- a)) =
+  mapDec (And . swap) (\case And prf => swap prf) $
+  orDec (i `notPositiveIn` a) (i `notPositiveInAny` as)
 
-illFormed (TVar j) = False
-illFormed TNat = False
-illFormed (TArrow a b) = illFormed a || illFormed b
-illFormed (TProd as) = anyIllFormed as
-illFormed (TSum as) = anyIllFormed as
-illFormed (TFix x a) = (%% x `notPositiveIn` a) || illFormed a
+-- Well Formed -----------------------------------------------------------------
 
-anyIllFormed [<] = False
-anyIllFormed (as :< (x :- a)) = illFormed a || anyIllFormed as
+-- Negating decidable properties is fun.
 
+namespace WellFormed
+  public export
+  data IllFormed : Ty ctx -> Type
+  public export
+  data AnyIllFormed : Context (Ty ctx) -> Type
+
+  data IllFormed where
+    TArrow : These (IllFormed a) (IllFormed b) -> IllFormed (TArrow a b)
+    TProd : AnyIllFormed as.context -> IllFormed (TProd as)
+    TSum : AnyIllFormed as.context -> IllFormed (TSum as)
+    TFix : These (toVar Here `NotPositiveIn` a) (IllFormed a) -> IllFormed (TFix x a)
+
+  data AnyIllFormed where
+    And : These (AnyIllFormed as) (IllFormed a) -> AnyIllFormed (as :< (n :- a))
+
+export
+Uninhabited (IllFormed (TVar i)) where
+  uninhabited (TArrow prf) impossible
+
+export
+Uninhabited (AnyIllFormed [<]) where
+  uninhabited (And prf) impossible
+
+export
+illFormed : (a : Ty ctx) -> Dec' (IllFormed a)
 export
-reflectIllFormed : (a : Ty ctx v) -> IllFormed a `Reflects` illFormed a
-reflectAnyIllFormed : (as : Row (Ty ctx v)) -> AnyIllFormed as `Reflects` anyIllFormed as
+anyIllFormed : (as : Context (Ty ctx)) -> Dec' (AnyIllFormed as)
 
-reflectIllFormed (TVar j) = RFalse id
-reflectIllFormed TNat = RFalse id
-reflectIllFormed (TArrow a b) = reflectThese (reflectIllFormed a) (reflectIllFormed b)
-reflectIllFormed (TProd as) = reflectAnyIllFormed as
-reflectIllFormed (TSum as) = reflectAnyIllFormed as
-reflectIllFormed (TFix x a) = reflectThese (reflectNotPositiveIn (%% x) a) (reflectIllFormed a)
+illFormed (TVar j) = False `Because` absurd
+illFormed (TArrow a b) = mapDec TArrow (\case TArrow prf => prf) $ orDec (illFormed a) (illFormed b)
+illFormed (TProd (MkRow as _)) = mapDec TProd (\case TProd prf => prf) (anyIllFormed as)
+illFormed (TSum (MkRow as _)) = mapDec TSum (\case TSum prf => prf) (anyIllFormed as)
+illFormed (TFix x a) = mapDec TFix (\case TFix prf => prf) $ orDec (%% x `notPositiveIn` a) (illFormed a)
 
-reflectAnyIllFormed [<] = RFalse id
-reflectAnyIllFormed (as :< (x :- a)) =
-  reflectThese (reflectIllFormed a) (reflectAnyIllFormed as)
+anyIllFormed [<] = False `Because` absurd
+anyIllFormed (as :< (n :- a)) =
+  mapDec (And . swap) (\case And prf => swap prf) $
+  orDec (illFormed a) (anyIllFormed as)
 
 --------------------------------------------------------------------------------
 -- Substitution ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
-public export
-fromVar : Either (Var ctx v) (Ty ctx v) -> Ty ctx v
-fromVar = either TVar id
-
 export
-sub : Env ctx1 ctx2 (Ty ctx2) -> Ty ctx1 v -> Ty ctx2 v
-subAll : Env ctx1 ctx2 (Ty ctx2) -> Row (Ty ctx1 v) -> Row (Ty ctx2 v)
-subAllFresh :
-  (env : Env ctx1 ctx2 (Ty ctx2)) -> (x : String) ->
-  (row : Row (Ty ctx1 v)) ->
-  So (x `freshIn` row) -> So (x `freshIn` subAll env row)
-
-sub env (TVar i) = fromVar $ lookup env i
-sub env TNat = TNat
+sub : All (const $ Thinned Ty ctx2) ctx1 -> Ty ctx1 -> Ty ctx2
+subAll : All (const $ Thinned Ty ctx2) ctx1 -> Context (Ty ctx1) -> Context (Ty ctx2)
+subAllNames :
+  (f : All (const $ Thinned Ty ctx2) ctx1) ->
+  (ctx : Context (Ty ctx1)) ->
+  (subAll f ctx).names = ctx.names
+
+sub env (TVar i) = (indexAll i.pos env).extract
 sub env (TArrow a b) = TArrow (sub env a) (sub env b)
-sub env (TProd as) = TProd (subAll env as)
-sub env (TSum as) = TSum (subAll env as)
-sub env (TFix x a) = TFix x (sub (lift (Drop Id) env :< (x :- TVar (%% x))) a)
+sub env (TProd (MkRow as fresh)) = TProd (MkRow (subAll env as) (rewrite subAllNames env as in fresh))
+sub env (TSum (MkRow as fresh)) = TSum (MkRow (subAll env as) (rewrite subAllNames env as in fresh))
+sub env (TFix x a) = TFix x (sub (mapProperty (rename (Drop Id)) env :< (TVar (%% x) `Over` Id)) a)
 
 subAll env [<] = [<]
-subAll env ((:<) as (x :- a) {fresh}) =
-  (:<) (subAll env as) (x :- sub env a) {fresh = subAllFresh env x as fresh}
+subAll env (as :< (n :- a)) = subAll env as :< (n :- sub env a)
 
-subAllFresh env x [<] = id
-subAllFresh env x (as :< (y :- a)) = andSo . mapSnd (subAllFresh env x as) . soAnd
+subAllNames env [<] = Refl
+subAllNames env (as :< (n :- a)) = cong (:< n) (subAllNames env as)
 
--- Expansion -------------------------------------------------------------------
+-- Special Types ---------------------------------------------------------------
 
-export
-expandEnv : DEnv Ty ctx -> Env ctx [<] (Ty [<])
-expandEnv [<] = Base Id
-expandEnv {ctx = ctx :< (x :- v)} (env :< (y :- a)) =
-  let env' = expandEnv env in
-  expandEnv env :< (x :- sub env' a)
+public export
+TNat : Ty ctx
+TNat = TFix "Nat" (TSum [<"Z" :- TProd [<], "S" :- TVar (%% "Nat")])
 
-export
-expand : DEnv Ty ctx -> Ty ctx v -> Ty [<] v
-expand = sub . expandEnv
+public export
+TList : Ty ctx -> Ty ctx
+TList a =
+  TFix "List" (TSum
+    [<"N" :- TProd [<]
+    , "C" :- TProd [<"H" :- thin (Drop Id) a, "T" :- TVar (%% "List")]])
+
+-- Testing if we have a list
+
+-- TODO: prove correct
+isList : (a : Ty ctx) -> Maybe (Ty ctx)
+isList (TFix x (TSum (MkRow
+  [<"N" :- TProd (MkRow [<] _)
+  , "C" :- TProd (MkRow [<"H" :- a, "T" :- TVar ((%%) x {pos = Here})] _)] _))) =
+  does (strengthen (%% x) a)
+isList (TFix x (TSum (MkRow
+  [<"N" :- TProd (MkRow [<] _)
+  , "C" :- TProd (MkRow [<"T" :- TVar ((%%) x {pos = Here}), "H" :- a] _)] _))) =
+  does (strengthen (%% x) a)
+isList (TFix x (TSum (MkRow
+  [<"C" :- TProd (MkRow [<"H" :- a, "T" :- TVar ((%%) x {pos = Here})] _)
+  , "N" :- TProd (MkRow [<] _)] _))) =
+  does (strengthen (%% x) a)
+isList (TFix x (TSum (MkRow
+  [<"C" :- TProd (MkRow [<"T" :- TVar ((%%) x {pos = Here}), "H" :- a] _)
+  , "N" :- TProd (MkRow [<] _)] _))) =
+  does (strengthen (%% x) a)
+isList _ = Nothing