Define terms.

4 files changed, 737 insertions, 1 deletions

diff --git a/inky.ipkg b/inky.ipkg
index 43e6e51..4de3027 100644
--- a/inky.ipkg
+++ b/inky.ipkg
@@ -7,6 +7,8 @@ options = "--total"
 depends = contrib
 
 modules
-  = Data.These.Decidable
+  = Data.Maybe.Decidable
+  , Data.These.Decidable
+  , Inky.Term
   , Inky.Thinning
   , Inky.Type
diff --git a/src/Data/Maybe/Decidable.idr b/src/Data/Maybe/Decidable.idr
new file mode 100644
index 0000000..e301ab1
--- /dev/null
+++ b/src/Data/Maybe/Decidable.idr
@@ -0,0 +1,6 @@
+module Data.Maybe.Decidable
+
+public export
+data OnlyWhen : (p : a -> Type) -> Maybe a -> Type where
+  RJust : forall x. (px : p x) -> p `OnlyWhen` Just x
+  RNothing : (false : (x : a) -> Not (p x)) -> p `OnlyWhen` Nothing
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
new file mode 100644
index 0000000..f5de797
--- /dev/null
+++ b/src/Inky/Term.idr
@@ -0,0 +1,720 @@
+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 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
+public export
+data CheckTerm : Nat -> Nat -> 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
+
+data CheckTerm where
+  Let :
+    SynthTerm ty tm ->
+    CheckTerm ty (S tm) ->
+    CheckTerm ty tm
+  FoldN :
+    CheckTerm ty tm ->
+    CheckTerm 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
+  Case :
+    SynthTerm ty tm ->
+    List (CheckTerm ty (S tm)) ->
+    CheckTerm ty tm
+  Contract : CheckTerm ty tm -> CheckTerm ty tm
+  Fold :
+    SynthTerm ty tm ->
+    CheckTerm ty (S tm) ->
+    CheckTerm ty tm
+  Embed :
+    SynthTerm ty tm ->
+    CheckTerm ty tm
+
+%name SynthTerm e
+%name CheckTerm t, u, v
+
+--------------------------------------------------------------------------------
+-- Well Formed -----------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+GetAt : Nat -> List a -> a -> Type
+GetAt k xs x = (n : Elem x xs ** elemToNat n = k)
+
+CanProject : Ty ty -> List (Ty ty) -> Type
+CanProject (TUnion as) bs = forget as = bs
+CanProject (TProd as) bs = as = bs
+CanProject _ 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
+
+IsFixpoint : Ty ty -> Ty (S ty) -> Type
+IsFixpoint (TFix a) b = a = b
+IsFixpoint _ b = Void
+
+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
+
+IsProduct : Ty ty -> List (Ty ty) -> Type
+IsProduct (TProd as) bs = as = bs
+IsProduct _ bs = Void
+
+IsSum : Ty ty -> List (Ty ty) -> Type
+IsSum (TSum as) bs = as = bs
+IsSum _ bs = Void
+
+Synths :
+  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
+  SynthTerm ty tm -> Ty ty -> Type
+Checks :
+  {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) ->
+  Ty ty -> CheckTerm ty tm -> 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
+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 =
+  ( fun **
+  ( Synths ctx e fun
+  , CheckSpine1 ctx fun ts a
+  ))
+Synths ctx (Prj e k) a =
+  ( b **
+  ( Synths ctx e b
+  , ( as **
+    ( CanProject b as
+    , GetAt k as a
+    ))
+  ))
+Synths ctx (Expand e) a =
+  ( b **
+  ( Synths ctx e b
+  , ( c **
+    ( IsFixpoint b c
+    , a = sub (Base Id :< b) c))
+  ))
+Synths ctx (Annot t a) b =
+  ( Not (IllFormed a)
+  , Checks ctx a t
+  , a = b
+  )
+
+Checks ctx a (Let e t) =
+  ( b **
+  ( Synths ctx e b
+  , Checks (b :: ctx) a t
+  ))
+Checks ctx a (FoldN t u v) =
+  ( Checks ctx TNat t
+  , Checks ctx a u
+  , Checks (a :: ctx) a v
+  )
+Checks ctx a (Abs k t) =
+  ( as : Vect (S k) _ ** b **
+  ( IsArrow (S k) a as b
+  , Checks (as ++ ctx) b t
+  ))
+Checks ctx a (Inj k t) =
+  ( as **
+  ( CanInject a as
+  , ( b **
+    ( GetAt k as b
+    , Checks ctx b t
+    ))
+  ))
+Checks ctx a (Tup ts) =
+  ( as **
+  ( IsProduct a as
+  , AllCheck ctx as ts
+  ))
+Checks ctx a (Case e ts) =
+  ( b **
+  ( Synths ctx e b
+  , ( as **
+    ( IsSum b as
+    , AllCheckBinding ctx as a ts
+    ))
+  ))
+Checks ctx a (Contract t) =
+  ( b **
+  ( IsFixpoint a b
+  , Checks ctx (sub (Base Id :< a) b) t
+  ))
+Checks ctx a (Fold e t) =
+  ( b **
+  ( Synths ctx e b
+  , ( c **
+    ( IsFixpoint b c
+    , Checks (sub (Base Id :< a) c :: ctx) 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
+  ))
+
+CheckSpine1 ctx fun (t ::: ts) res =
+  ( a ** b **
+  ( IsArrow 1 fun [a] b
+  , Checks ctx a t
+  , CheckSpine ctx 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)
+
+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)
+
+-- Uniqueness
+
+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 (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
+
+isSumUnique : (a : Ty ty) -> IsSum a as -> IsSum a bs -> as = bs
+isSumUnique (TSum as) Refl Refl = Refl
+
+
+synthsUnique :
+  (0 ctx : Vect tm (Ty ty)) -> (e : SynthTerm ty tm) ->
+  Synths ctx e a -> Synths ctx 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 =
+      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
+    with (isFixpointUnique a prf11 prf21)
+    synthsUnique ctx (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 (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
+
+isProduct : Ty ty -> Maybe (List (Ty ty))
+isProduct (TProd as) = Just as
+isProduct _ = Nothing
+
+isSum : Ty ty -> Maybe (List (Ty ty))
+isSum (TSum as) = Just as
+isSum _ = Nothing
+
+synths :
+  (ctx : Vect tm (Ty ty)) ->
+  SynthTerm ty tm -> Maybe (Ty ty)
+checks :
+  (ctx : Vect tm (Ty ty)) ->
+  Ty ty -> CheckTerm ty tm -> 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)
+allCheck :
+  (ctx : Vect tm (Ty ty)) ->
+  List (Ty ty) -> List (CheckTerm ty tm) -> 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)
+  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
+  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
+  guard (not $ illFormed a)
+  guard (checks ctx a t)
+  Just a
+
+checks ctx a (Let e t) =
+  case synths ctx e of
+    Just b => checks (b :: ctx) a t
+    Nothing => False
+checks ctx a (FoldN t u v) =
+  checks ctx TNat t &&
+  checks ctx a u &&
+  checks (a :: ctx) a v
+checks ctx a (Abs k t) =
+  case isArrow (S k) a of
+    Just (as, b) => checks (as ++ ctx) b t
+    Nothing => False
+checks ctx a (Inj k t) =
+  case canInject a of
+    Just as =>
+      case getAt k as of
+        Just b => checks ctx b t
+        Nothing => False
+    Nothing => False
+checks ctx a (Tup ts) =
+  case isProduct a of
+    Just as => allCheck ctx as ts
+    Nothing => False
+checks ctx a (Case e ts) =
+  case synths ctx e of
+    Just b =>
+      case isSum b of
+        Just as => allCheckBinding ctx as a ts
+        Nothing => False
+    Nothing => False
+checks ctx a (Contract t) =
+  case isFixpoint a of
+    Just b => checks ctx (sub (Base Id :< a) b) t
+    Nothing => False
+checks ctx a (Fold e t) =
+  case synths ctx e of
+    Just b =>
+      case isFixpoint b of
+        Just c => checks (sub (Base Id :< a) c :: ctx) a t
+        Nothing => False
+    Nothing => False
+checks ctx a (Embed e) =
+  case synths ctx 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
+
+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
+
+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
+
+-- 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 = RNothing (\x, y => y)
+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
+partial
+reflectCheckSpine :
+  (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty tm)) ->
+  CheckSpine ctx a ts `OnlyWhen` checkSpine ctx a ts
+partial
+reflectCheckSpine1 :
+  (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List1 (CheckTerm ty tm)) ->
+  CheckSpine1 ctx a ts `OnlyWhen` checkSpine1 ctx a 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
+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)
+  _ | 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)
+    _ | 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
+          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)
+      _ | 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
+          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
+        nprf as' prf)
+  _ | RNothing eBad | _ = RNothing (\x, (a' ** (eTy, _)) => eBad a' eTy)
+reflectSynths ctx (Expand e) with (reflectSynths ctx e) | (synths ctx e)
+  _ | RJust eTy | Just a with (reflectIsFixpoint a) | (isFixpoint a)
+    _ | RJust prf | Just b = RJust (a ** (eTy, (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
+        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)
+    _ | 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)
+    _ | 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
+        tBad tTy)
+  _ | RNothing eBad | Nothing = RFalse (\(b ** (eTy, _)) => eBad b eTy)
+reflectChecks ctx a (FoldN t u v) with (reflectChecks ctx TNat t) | (checks ctx TNat t)
+  _ | RTrue tTy | _ with (reflectChecks ctx a u) | (checks ctx a u)
+    _ | RTrue uTy | _ with (reflectChecks (a :: ctx) a v) | (checks (a :: ctx) a v)
+      _ | RTrue vTy | _ = RTrue (tTy, uTy, vTy)
+      _ | RFalse vBad | _ = RFalse (\(_, _, vTy) => vBad vTy)
+    _ | RFalse uBad | _ = RFalse (\(_, uTy, _) => uBad uTy)
+  _ | RFalse tBad | _ = RFalse (\(tTy, _) => tBad tTy)
+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)
+    _ | 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
+        in
+        tBad tTy)
+  _ | RNothing nprf | _ = RFalse (\(as ** b ** (prf, _)) => nprf (as, b) prf)
+reflectChecks ctx a (Inj k t) with (reflectCanInject a) | (canInject 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)
+      _ | 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)
+    _ | RNothing not | _ =
+      RFalse (\(as' ** (prf', (b ** (got, _)))) =>
+        let got = rewrite canInjectUnique 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)
+    _ | 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)
+  _ | RJust eTy | Just b with (reflectIsSum b) | (isSum b)
+    _ | RJust prf | Just as with (reflectAllCheckBinding ctx as a ts) | (allCheckBinding ctx 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 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
+        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))
+    _ | RFalse tBad | _ =
+      RFalse (\(b' ** (prf', tTy)) =>
+        let tTy = rewrite isFixpointUnique a {b, c = b'} prf prf' in 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)
+  _ | 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))))
+      _ | 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
+          tBad tTy)
+    _ | RNothing nprf | _ =
+      RFalse (\(b' ** (eTy', (c ** (prf, _)))) =>
+        let prf = rewrite synthsUnique ctx 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)
+  _ | 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)
+
+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)
+      _ | 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)
+
+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)
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index aadd968..3021f96 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -38,6 +38,14 @@ export
 Injective TVar where
   injective Refl = Refl
 
+export
+Injective TUnion where
+  injective Refl = Refl
+
+export
+Injective TProd where
+  injective Refl = Refl
+
 -- Equality --------------------------------------------------------------------
 
 export