module Inky.Term

import public Inky.Data.Thinned
import public Inky.Type

import Control.Function
import Data.List.Quantifiers
import Data.Singleton
import Data.These
import Inky.Data.SnocList.Quantifiers
import Inky.Decidable
import Inky.Decidable.Maybe

%hide Prelude.Ops.infixl.(>=>)

--------------------------------------------------------------------------------
-- Definition ------------------------------------------------------------------
--------------------------------------------------------------------------------

public export
data Term : (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
  Annot : (meta : m) -> Term m tyCtx tmCtx -> Ty tyCtx -> Term m tyCtx tmCtx
  Var : (meta : m) -> Var tmCtx -> Term m tyCtx tmCtx
  Let : (meta : m) -> Term m tyCtx tmCtx -> (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
  LetTy : (meta : m) -> Ty tyCtx -> (x ** Term m (tyCtx :< x) tmCtx) -> Term m tyCtx tmCtx
  Abs : (meta : m) -> (bound ** Term m tyCtx (tmCtx <>< bound)) -> Term m tyCtx tmCtx
  App : (meta : m) -> Term m tyCtx tmCtx -> List (Term m tyCtx tmCtx) -> Term m tyCtx tmCtx
  Tup : (meta : m) -> Row (Term m tyCtx tmCtx) -> Term m tyCtx tmCtx
  Prj : (meta : m) -> Term m tyCtx tmCtx -> (l : String) -> Term m tyCtx tmCtx
  Inj : (meta : m) -> (l : String) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
  Case : (meta : m) -> Term m tyCtx tmCtx -> Row (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
  Roll : (meta : m) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
  Unroll : (meta : m) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
  Fold : (meta : m) -> Term m tyCtx tmCtx -> (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
  Map : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term m tyCtx tmCtx
  GetChildren : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Term m tyCtx tmCtx

%name Term e, f, t, u

export
(.meta) : Term m tyCtx tmCtx -> m
(Annot meta _ _).meta = meta
(Var meta _).meta = meta
(Let meta _ _).meta = meta
(LetTy meta _ _).meta = meta
(Abs meta _).meta = meta
(App meta _ _).meta = meta
(Tup meta _).meta = meta
(Prj meta _ _).meta = meta
(Inj meta _ _).meta = meta
(Case meta _ _).meta = meta
(Roll meta _).meta = meta
(Unroll meta _).meta = meta
(Fold meta _ _).meta = meta
(Map meta _ _ _).meta = meta
(GetChildren meta _ _).meta = meta

--------------------------------------------------------------------------------
-- Well Formed -----------------------------------------------------------------
--------------------------------------------------------------------------------

-- Test if we have a function, collecting the bound types ----------------------

public export
data IsFunction :
  (bound : List String) -> (a : Ty tyCtx) ->
  (dom : All (const $ Ty tyCtx) bound) -> (cod : Ty tyCtx) ->
  Type
  where
  Done : IsFunction [] a [] a
  Step :
    IsFunction bound b dom cod ->
    IsFunction (x :: bound) (TArrow a b) (a :: dom) cod

public export
data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type
  where
  Step1 :
    ((b, c : Ty tyCtx) -> Not (a = TArrow b c)) ->
    NotFunction (x :: bound) a
  Step2 :
    NotFunction bound b ->
    NotFunction (x :: bound) (TArrow a b)

%name IsFunction prf
%name NotFunction contra

export
isFunctionRecompute :
  {a : Ty tyCtx} -> IsFunction bound a dom cod -> (Singleton dom, Singleton cod)
isFunctionRecompute Done = (Val _, Val _)
isFunctionRecompute (Step {a} prf) =
  mapFst (\case Val _ => Val _) $ isFunctionRecompute prf

export
isFunctionUnique :
  IsFunction bound a dom cod -> IsFunction bound a dom' cod' -> (dom = dom', cod = cod')
isFunctionUnique Done Done = (Refl, Refl)
isFunctionUnique (Step {a} prf) (Step prf') =
  mapFst (\prf => cong (a ::) prf) $ isFunctionUnique prf prf'

export
isFunctionSplit : IsFunction bound a dom cod -> NotFunction bound a -> Void
isFunctionSplit (Step {a, b} prf) (Step1 contra) = void $ contra a b Refl
isFunctionSplit (Step prf) (Step2 contra) = isFunctionSplit prf contra

export
isFunction :
  (bound : List String) -> (a : Ty tyCtx) ->
  Proof (All (const $ Ty tyCtx) bound, Ty tyCtx)
    (uncurry $ IsFunction bound a)
    (NotFunction bound a)
isFunction [] a = Just ([], a) `Because` Done
isFunction (x :: bound) a =
  map
    (\x => (fst (fst x) :: fst (snd x), snd (snd x)))
    (\((a, b), (dom, cod)), (eq, prf) => rewrite eq in Step prf)
    (either Step1 false) $
  (ab := isArrow a) >=> isFunction bound (snd ab)
  where
  false :
    forall a.
    (y : (Ty tyCtx, Ty tyCtx) ** (a = TArrow (fst y) (snd y), NotFunction bound (snd y))) ->
    NotFunction (x :: bound) a
  false ((a, b) ** (Refl, contra)) = Step2 contra

-- Define well-formedness and ill-formedness

namespace Modes
  public export
  data SynthsOnly : Term m tyCtx tmCtx -> Type where
    Annot : SynthsOnly (Annot _ t a)
    Var : SynthsOnly (Var _ i)
    App : SynthsOnly (App _ f ts)
    Prj : SynthsOnly (Prj _ e l)
    Unroll : SynthsOnly (Unroll _ e)
    Map : SynthsOnly (Map _ (x ** a) b c)
    GetChildren : SynthsOnly (GetChildren _ (x ** a) b)

  public export
  data ChecksOnly : Term m tyCtx tmCtx -> Type where
    Abs : ChecksOnly (Abs _ (bounds ** t))
    Inj : ChecksOnly (Inj _ l t)
    Case : ChecksOnly (Case _ e ts)
    Roll : ChecksOnly (Roll _ t)
    Fold : ChecksOnly (Fold _ e (x ** t))

public export
data Synths :
  All (const $ Thinned Ty [<]) tyCtx ->
  All (const $ Thinned Ty [<]) tmCtx ->
  Term m tyCtx tmCtx -> Ty [<] -> Type
public export
data Checks :
  All (const $ Thinned Ty [<]) tyCtx ->
  All (const $ Thinned Ty [<]) tmCtx ->
  Ty [<] -> Term m tyCtx tmCtx -> Type

namespace Spine
  public export
  data CheckSpine :
    All (const $ Thinned Ty [<]) tyCtx ->
    All (const $ Thinned Ty [<]) tmCtx ->
    Ty [<] -> List (Term m tyCtx tmCtx) -> Ty [<] -> Type
    where
    Nil : CheckSpine tyEnv tmEnv a [] a
    (::) :
      Checks tyEnv tmEnv a t ->
      CheckSpine tyEnv tmEnv b ts c ->
      CheckSpine tyEnv tmEnv (TArrow a b) (t :: ts) c

  %name CheckSpine prfs

namespace Synths
  public export
  data AllSynths :
    All (const $ Thinned Ty [<]) tyCtx ->
    All (const $ Thinned Ty [<]) tmCtx ->
    (ts : Context (Term m tyCtx tmCtx)) -> All (const $ Ty [<]) ts.names -> Type
    where
    Lin : AllSynths tyEnv tmEnv [<] [<]
    (:<) :
      AllSynths tyEnv tmEnv ts as ->
      Synths tyEnv tmEnv t a ->
      AllSynths tyEnv tmEnv (ts :< (l :- t)) (as :< a)

  %name AllSynths prfs

namespace Checks
  public export
  data AllChecks :
    All (const $ Thinned Ty [<]) tyCtx ->
    All (const $ Thinned Ty [<]) tmCtx ->
    Context (Ty [<]) -> Context (Term m tyCtx tmCtx) -> Type
    where
    Base : AllChecks tyEnv tmEnv [<] [<]
    Step :
      (i : Elem (l :- a) as) ->
      Checks tyEnv tmEnv a t ->
      AllChecks tyEnv tmEnv (dropElem as i) ts ->
      AllChecks tyEnv tmEnv as (ts :< (l :- t))

  %name AllChecks prfs

namespace Branches
  public export
  data AllBranches :
    All (const $ Thinned Ty [<]) tyCtx ->
    All (const $ Thinned Ty [<]) tmCtx ->
    Context (Ty [<]) -> Ty [<] -> Context (x ** Term m tyCtx (tmCtx :< x)) -> Type
    where
    Base : AllBranches tyEnv tmEnv [<] a [<]
    Step :
      (i : Elem (l :- a) as) ->
      Checks tyEnv (tmEnv :< (a `Over` Id)) b t ->
      AllBranches tyEnv tmEnv (dropElem as i) b ts ->
      AllBranches tyEnv tmEnv as b (ts :< (l :- (x ** t)))

  %name AllBranches prfs

data Synths where
  AnnotS :
    Not (IllFormed a) ->
    Checks tyEnv tmEnv (sub tyEnv a) t ->
    Synths tyEnv tmEnv (Annot meta t a) (sub tyEnv a)
  VarS :
    Synths tyEnv tmEnv (Var meta i) (indexAll i.pos tmEnv).extract
  LetS :
    Synths tyEnv tmEnv e a ->
    Synths tyEnv (tmEnv :< (a `Over` Id)) f b ->
    Synths tyEnv tmEnv (Let meta e (x ** f)) b
  LetTyS :
    Not (IllFormed a) ->
    Synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e b ->
    Synths tyEnv tmEnv (LetTy meta a (x ** e)) b
  AppS :
    Synths tyEnv tmEnv f a ->
    CheckSpine tyEnv tmEnv a ts b ->
    Synths tyEnv tmEnv (App meta f ts) b
  TupS :
    AllSynths tyEnv tmEnv es.context as ->
    Synths tyEnv tmEnv (Tup meta es) (TProd (fromAll es as))
  PrjS :
    Synths tyEnv tmEnv e (TProd as) ->
    Elem (l :- a) as.context ->
    Synths tyEnv tmEnv (Prj meta e l) a
  UnrollS :
    Synths tyEnv tmEnv e (TFix x a) ->
    Synths tyEnv tmEnv (Unroll meta e) (sub [<TFix x a `Over` Id] a)
  MapS :
    Not (IllFormed (TFix x a)) ->
    Not (IllFormed b) ->
    Not (IllFormed c) ->
    Synths tyEnv tmEnv (Map meta (x ** a) b c)
      (TArrow (TArrow (sub tyEnv b) (sub tyEnv c))
      (TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a)
              (sub (tyEnv :< (sub tyEnv c `Over` Id)) a)))
  GetChildrenS :
    Not (IllFormed (TFix x a)) ->
    Not (IllFormed b) ->
    Synths tyEnv tmEnv (GetChildren meta (x ** a) b)
      (TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a)
        (TProd
          [<"Children" :- sub tyEnv b
          , "Shape" :- sub (tyEnv :< (TNat `Over` Id)) a]))

data Checks where
  EmbedC :
    SynthsOnly e ->
    Synths tyEnv tmEnv e a ->
    Alpha a b ->
    Checks tyEnv tmEnv b e
  LetC :
    Synths tyEnv tmEnv e a ->
    Checks tyEnv (tmEnv :< (a `Over` Id)) b t ->
    Checks tyEnv tmEnv b (Let meta e (x ** t))
  LetTyC :
    Not (IllFormed a) ->
    Checks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t ->
    Checks tyEnv tmEnv b (LetTy meta a (x ** t))
  AbsC :
    IsFunction bound a dom cod ->
    Checks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t ->
    Checks tyEnv tmEnv a (Abs meta (bound ** t))
  TupC :
    AllChecks tyEnv tmEnv as.context ts.context ->
    Checks tyEnv tmEnv (TProd as) (Tup meta ts)
  InjC :
    Elem (l :- a) as.context ->
    Checks tyEnv tmEnv a t ->
    Checks tyEnv tmEnv (TSum as) (Inj meta l t)
  CaseC :
    Synths tyEnv tmEnv e (TSum as) ->
    AllBranches tyEnv tmEnv as.context a ts.context ->
    Checks tyEnv tmEnv a (Case meta e ts)
  RollC :
    Checks tyEnv tmEnv (sub [<TFix x a `Over` Id] a) t ->
    Checks tyEnv tmEnv (TFix x a) (Roll meta t)
  FoldC :
    Synths tyEnv tmEnv e (TFix x a) ->
    Checks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t ->
    Checks tyEnv tmEnv b (Fold meta e (y ** t))

%name Synths prf
%name Checks prf

public export
data NotSynths :
  All (const $ Thinned Ty [<]) tyCtx ->
  All (const $ Thinned Ty [<]) tmCtx ->
  Term m tyCtx tmCtx -> Type
public export
data NotChecks :
  All (const $ Thinned Ty [<]) tyCtx ->
  All (const $ Thinned Ty [<]) tmCtx ->
  Ty [<] -> Term m tyCtx tmCtx -> Type

namespace Spine
  public export
  data NotCheckSpine :
    All (const $ Thinned Ty [<]) tyCtx ->
    All (const $ Thinned Ty [<]) tmCtx ->
    Ty [<] -> List (Term m tyCtx tmCtx) -> Type
    where
    Step1 :
      ((b, c : Ty [<]) -> Not (a = TArrow b c)) ->
      NotCheckSpine tyEnv tmEnv a (t :: ts)
    Step2 :
      These (NotChecks tyEnv tmEnv a t) (NotCheckSpine tyEnv tmEnv b ts) ->
      NotCheckSpine tyEnv tmEnv (TArrow a b) (t :: ts)

  %name NotCheckSpine contras

namespace Synths
  public export
  data AnyNotSynths :
    All (const $ Thinned Ty [<]) tyCtx ->
    All (const $ Thinned Ty [<]) tmCtx ->
    (ts : Context (Term m tyCtx tmCtx)) -> Type
    where
    Step :
      These (NotSynths tyEnv tmEnv t) (AnyNotSynths tyEnv tmEnv ts) ->
      AnyNotSynths tyEnv tmEnv (ts :< (l :- t))

  %name AnyNotSynths contras

namespace Checks
  public export
  data AnyNotChecks :
    All (const $ Thinned Ty [<]) tyCtx ->
    All (const $ Thinned Ty [<]) tmCtx ->
    Context (Ty [<]) -> Context (Term m tyCtx tmCtx) -> Type
    where
    Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<]
    Step1 :
      ((a : Ty [<]) -> Not (Elem (l :- a) as)) ->
      AnyNotChecks tyEnv tmEnv as (ts :< (l :- t))
    Step2 :
      (i : Elem (l :- a) as) ->
      These (NotChecks tyEnv tmEnv a t) (AnyNotChecks tyEnv tmEnv (dropElem as i) ts) ->
      AnyNotChecks tyEnv tmEnv as (ts :< (l :- t))

  %name AnyNotChecks contras

namespace Branches
  public export
  data AnyNotBranches :
    All (const $ Thinned Ty [<]) tyCtx ->
    All (const $ Thinned Ty [<]) tmCtx ->
    Context (Ty [<]) -> Ty [<] -> Context (x ** Term m tyCtx (tmCtx :< x)) -> Type
    where
    Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<]
    Step1 :
      ((a : Ty [<]) -> Not (Elem (l :- a) as)) ->
      AnyNotBranches tyEnv tmEnv as b (ts :< (l :- (x ** t)))
    Step2 :
      (i : Elem (l :- a) as) ->
      These
        (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t)
        (AnyNotBranches tyEnv tmEnv (dropElem as i) b ts) ->
      AnyNotBranches tyEnv tmEnv as b (ts :< (l :- (x ** t)))

  %name AnyNotBranches contras

data NotSynths where
  ChecksNS :
    ChecksOnly t ->
    NotSynths tyEnv tmEnv t
  AnnotNS :
    These (IllFormed a) (NotChecks tyEnv tmEnv (sub tyEnv a) t) ->
    NotSynths tyEnv tmEnv (Annot meta t a)
  LetNS1 :
    NotSynths tyEnv tmEnv e ->
    NotSynths tyEnv tmEnv (Let meta e (x ** f))
  LetNS2 :
    Synths tyEnv tmEnv e a ->
    NotSynths tyEnv (tmEnv :< (a `Over` Id)) f ->
    NotSynths tyEnv tmEnv (Let meta e (x ** f))
  LetTyNS :
    These (IllFormed a) (NotSynths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e) ->
    NotSynths tyEnv tmEnv (LetTy meta a (x ** e))
  AppNS1 :
    NotSynths tyEnv tmEnv f ->
    NotSynths tyEnv tmEnv (App meta f ts)
  AppNS2 :
    Synths tyEnv tmEnv f a ->
    NotCheckSpine tyEnv tmEnv a ts ->
    NotSynths tyEnv tmEnv (App meta f ts)
  TupNS :
    AnyNotSynths tyEnv tmEnv es.context ->
    NotSynths tyEnv tmEnv (Tup meta es)
  PrjNS1 :
    NotSynths tyEnv tmEnv e ->
    NotSynths tyEnv tmEnv (Prj meta e l)
  PrjNS2 :
    Synths tyEnv tmEnv e a ->
    ((as : Row (Ty [<])) -> Not (a = TProd as)) ->
    NotSynths tyEnv tmEnv (Prj meta e l)
  PrjNS3 :
    Synths tyEnv tmEnv e (TProd as) ->
    ((a : Ty [<]) -> Not (Elem (l :- a) as.context)) ->
    NotSynths tyEnv tmEnv (Prj meta e l)
  UnrollNS1 :
    NotSynths tyEnv tmEnv e ->
    NotSynths tyEnv tmEnv (Unroll meta e)
  UnrollNS2 :
    Synths tyEnv tmEnv e a ->
    ((x : String) -> (b : Ty [<x]) -> Not (a = TFix x b)) ->
    NotSynths tyEnv tmEnv (Unroll meta e)
  MapNS :
    These (IllFormed (TFix x a)) (These (IllFormed b) (IllFormed c)) ->
    NotSynths tyEnv tmEnv (Map meta (x ** a) b c)
  GetChildrenNS :
    These (IllFormed (TFix x a)) (IllFormed b) ->
    NotSynths tyEnv tmEnv (GetChildren meta (x ** a) b)

data NotChecks where
  EmbedNC1 :
    SynthsOnly e ->
    NotSynths tyEnv tmEnv e ->
    NotChecks tyEnv tmEnv b e
  EmbedNC2 :
    SynthsOnly e ->
    Synths tyEnv tmEnv e a ->
    NotAlpha a b ->
    NotChecks tyEnv tmEnv b e
  LetNC1 :
    NotSynths tyEnv tmEnv e ->
    NotChecks tyEnv tmEnv b (Let meta e (x ** t))
  LetNC2 :
    Synths tyEnv tmEnv e a ->
    NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t ->
    NotChecks tyEnv tmEnv b (Let meta e (x ** t))
  LetTyNC :
    These (IllFormed a) (NotChecks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t) ->
    NotChecks tyEnv tmEnv b (LetTy meta a (x ** t))
  AbsNC1 :
    NotFunction bound a ->
    NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
  AbsNC2 :
    IsFunction bound a dom cod ->
    NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t ->
    NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
  TupNC1 :
    ((as : Row (Ty [<])) -> Not (a = TProd as)) ->
    NotChecks tyEnv tmEnv a (Tup meta ts)
  TupNC2 :
    AnyNotChecks tyEnv tmEnv as.context ts.context ->
    NotChecks tyEnv tmEnv (TProd as) (Tup meta ts)
  InjNC1 :
    ((as : Row (Ty [<])) -> Not (a = TSum as)) ->
    NotChecks tyEnv tmEnv a (Inj meta l t)
  InjNC2 :
    ((a : Ty [<]) -> Not (Elem (l :- a) as.context)) ->
    NotChecks tyEnv tmEnv (TSum as) (Inj meta l t)
  InjNC3 :
    Elem (l :- a) as.context ->
    NotChecks tyEnv tmEnv a t ->
    NotChecks tyEnv tmEnv (TSum as) (Inj meta l t)
  CaseNC1 :
    NotSynths tyEnv tmEnv e ->
    NotChecks tyEnv tmEnv a (Case meta e ts)
  CaseNC2 :
    Synths tyEnv tmEnv e b ->
    ((as : Row (Ty [<])) -> Not (b = TSum as)) ->
    NotChecks tyEnv tmEnv a (Case meta e ts)
  CaseNC3 :
    Synths tyEnv tmEnv e (TSum as) ->
    AnyNotBranches tyEnv tmEnv as.context a ts.context ->
    NotChecks tyEnv tmEnv a (Case meta e ts)
  RollNC1 :
    ((x : String) -> (b : Ty [<x]) -> Not (a = TFix x b)) ->
    NotChecks tyEnv tmEnv a (Roll meta t)
  RollNC2 :
    NotChecks tyEnv tmEnv (sub [<TFix x a `Over` Id] a) t ->
    NotChecks tyEnv tmEnv (TFix x a) (Roll meta t)
  FoldNC1 :
    NotSynths tyEnv tmEnv e ->
    NotChecks tyEnv tmEnv b (Fold meta e (y ** t))
  FoldNC2 :
    Synths tyEnv tmEnv e a ->
    ((x : String) -> (c : Ty [<x]) -> Not (a = TFix x c)) ->
    NotChecks tyEnv tmEnv b (Fold meta e (y ** t))
  FoldNC3 :
    Synths tyEnv tmEnv e (TFix x a) ->
    NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t ->
    NotChecks tyEnv tmEnv b (Fold meta e (y ** t))

%name NotSynths contra
%name NotChecks contra

Uninhabited (NotSynths tyEnv tmEnv (Var meta i)) where
  uninhabited (ChecksNS Abs) impossible
  uninhabited (ChecksNS Inj) impossible
  uninhabited (ChecksNS Case) impossible
  uninhabited (ChecksNS Roll) impossible
  uninhabited (ChecksNS Fold) impossible

-- Can recompute type from synthesis proof

export
synthsRecompute :
  {tyEnv : _} -> {tmEnv : _} -> {e : _} ->
  Synths tyEnv tmEnv e a -> Singleton a
checkSpineRecompute :
  {tyEnv : _} -> {tmEnv : _} -> {a : _} ->
  CheckSpine tyEnv tmEnv a ts b -> Singleton b
allSynthsRecompute :
  {tyEnv : _} -> {tmEnv : _} -> {es : Context _} ->
  {0 as : All (const $ Ty [<]) es.names} ->
  AllSynths tyEnv tmEnv es as -> Singleton as

synthsRecompute (AnnotS wf prf) = Val _
synthsRecompute VarS = Val _
synthsRecompute (LetS prf1 prf2) with (synthsRecompute prf1)
  _ | Val _ = synthsRecompute prf2
synthsRecompute (LetTyS wf prf) = synthsRecompute prf
synthsRecompute (AppS prf prfs) with (synthsRecompute prf)
  _ | Val _ = checkSpineRecompute prfs
synthsRecompute (TupS prfs) with (allSynthsRecompute prfs)
  _ | Val _ = Val _
synthsRecompute (PrjS prf i) with (synthsRecompute prf)
  _ | Val _ = [| (nameOf i).value |]
synthsRecompute (UnrollS prf) with (synthsRecompute prf)
  _ | Val _ = Val _
synthsRecompute (MapS f g h) = Val _
synthsRecompute (GetChildrenS f g) = Val _

checkSpineRecompute [] = Val _
checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs

allSynthsRecompute [<] = Val _
allSynthsRecompute (prfs :< prf) = [| allSynthsRecompute prfs :< synthsRecompute prf |]

-- Synthesis gives unique types

synthsUnique : Synths tyEnv tmEnv e a -> Synths tyEnv tmEnv e b -> a = b
checkSpineUnique : CheckSpine tyEnv tmEnv a ts b -> CheckSpine tyEnv tmEnv a ts c -> b = c
allSynthsUnique : AllSynths tyEnv tmEnv es as -> AllSynths tyEnv tmEnv es bs -> as = bs

synthsUnique (AnnotS _ _) (AnnotS _ _) = Refl
synthsUnique VarS VarS = Refl
synthsUnique (LetS prf1 prf2) (LetS prf1' prf2') =
  let prf2' = rewrite synthsUnique prf1 prf1' in prf2' in
  synthsUnique prf2 prf2'
synthsUnique (LetTyS _ prf) (LetTyS _ prf') = synthsUnique prf prf'
synthsUnique (AppS prf prfs) (AppS prf' prfs') =
  let prfs' = rewrite synthsUnique prf prf' in prfs' in
  checkSpineUnique prfs prfs'
synthsUnique (TupS {es} prfs) (TupS prfs') =
  cong (TProd . fromAll es) $ allSynthsUnique prfs prfs'
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) $
  fixInjective $
  synthsUnique prf prf'
synthsUnique (MapS _ _ _) (MapS _ _ _) = Refl
synthsUnique (GetChildrenS _ _) (GetChildrenS _ _) = Refl

checkSpineUnique [] [] = Refl
checkSpineUnique (prf :: prfs) (prf' :: prfs') = checkSpineUnique prfs prfs'

allSynthsUnique [<] [<] = Refl
allSynthsUnique (prfs :< prf) (prfs' :< prf') =
  cong2 (:<) (allSynthsUnique prfs prfs') (synthsUnique prf prf')

-- We cannot both succeed and fail

synthsSplit : Synths tyEnv tmEnv e a -> NotSynths tyEnv tmEnv e -> Void
checksSplit : Checks tyEnv tmEnv a t -> NotChecks tyEnv tmEnv a t -> Void
checkSpineSplit : CheckSpine tyEnv tmEnv a ts b -> NotCheckSpine tyEnv tmEnv a ts -> Void
allSynthsSplit : AllSynths tyEnv tmEnv es as -> AnyNotSynths tyEnv tmEnv es -> Void
allChecksSplit :
  (0 fresh : AllFresh as.names) ->
  AllChecks tyEnv tmEnv as ts -> AnyNotChecks tyEnv tmEnv as ts -> Void
allBranchesSplit :
  (0 fresh : AllFresh as.names) ->
  AllBranches tyEnv tmEnv as a ts -> AnyNotBranches tyEnv tmEnv as a ts -> Void

synthsSplit (AnnotS wf prf) (AnnotNS contras) =
  these wf (checksSplit prf) (const $ checksSplit prf) contras
synthsSplit VarS contra = absurd contra
synthsSplit (LetS prf1 prf2) (LetNS1 contra) = synthsSplit prf1 contra
synthsSplit (LetS prf1 prf2) (LetNS2 prf1' contra) =
  let contra = rewrite synthsUnique prf1 prf1' in contra in
  synthsSplit prf2 contra
synthsSplit (LetTyS wf prf) (LetTyNS contras) =
  these wf (synthsSplit prf) (const $ synthsSplit prf) contras
synthsSplit (AppS prf prfs) (AppNS1 contra) = synthsSplit prf contra
synthsSplit (AppS prf prfs) (AppNS2 prf' contras) =
  let contras = rewrite synthsUnique prf prf' in contras in
  checkSpineSplit prfs contras
synthsSplit (TupS prfs) (TupNS contras) = allSynthsSplit prfs contras
synthsSplit (PrjS prf i) (PrjNS1 contra) = synthsSplit prf contra
synthsSplit (PrjS {as} prf i) (PrjNS2 prf' contra) =
  void $ contra as $ synthsUnique prf' prf
synthsSplit (PrjS {as, a} prf i) (PrjNS3 {as = bs} prf' contra) =
  let i = rewrite inj TProd $ synthsUnique prf' prf in i in
  void $ contra a i
synthsSplit (UnrollS prf) (UnrollNS1 contra) = synthsSplit prf contra
synthsSplit (UnrollS {x, a} prf) (UnrollNS2 prf' contra) =
  void $ contra x a $ synthsUnique prf' prf
synthsSplit (MapS wf1 wf2 wf3) (MapNS contras) =
  these wf1 (these wf2 wf3 (const wf3)) (const $ these wf2 wf3 (const wf3)) contras
synthsSplit (GetChildrenS wf1 wf2) (GetChildrenNS contras) =
  these wf1 wf2 (const wf2) contras

checksSplit (EmbedC _ prf1 prf2) (EmbedNC1 _ contra) = synthsSplit prf1 contra
checksSplit (EmbedC _ prf1 prf2) (EmbedNC2 _ prf1' contra) =
  let contra = rewrite synthsUnique prf1 prf1' in contra in
  alphaSplit prf2 contra
checksSplit (LetC prf1 prf2) (LetNC1 contra) = synthsSplit prf1 contra
checksSplit (LetC prf1 prf2) (LetNC2 prf1' contra) =
  let contra = rewrite synthsUnique prf1 prf1' in contra in
  checksSplit prf2 contra
checksSplit (LetTyC wf prf) (LetTyNC contras) =
  these wf (checksSplit prf) (const $ checksSplit prf) contras
checksSplit (AbsC prf1 prf2) (AbsNC1 contra) = isFunctionSplit prf1 contra
checksSplit (AbsC prf1 prf2) (AbsNC2 prf1' contra) =
  let (eq1, eq2) = isFunctionUnique prf1 prf1' in
  let contra = rewrite eq1 in rewrite eq2 in contra in
  checksSplit prf2 contra
checksSplit (TupC {as} prfs) (TupNC1 contra) = void $ contra as Refl
checksSplit (TupC {as} prfs) (TupNC2 contras) = allChecksSplit as.fresh prfs contras
checksSplit (InjC {as} i prf) (InjNC1 contra) = void $ contra as Refl
checksSplit (InjC {a} i prf) (InjNC2 contra) = void $ contra a i
checksSplit (InjC {as} i prf) (InjNC3 j contra) =
  let contra = rewrite cong fst $ lookupUnique as i j in contra in
  checksSplit prf contra
checksSplit (CaseC prf prfs) (CaseNC1 contra) = synthsSplit prf contra
checksSplit (CaseC {as} prf prfs) (CaseNC2 prf' contra) =
  void $ contra as $ synthsUnique prf' prf
checksSplit (CaseC {as} prf prfs) (CaseNC3 prf' contras) =
  let contras = rewrite inj TSum $ synthsUnique prf prf' in contras in
  allBranchesSplit as.fresh prfs contras
checksSplit (RollC {x, a} prf) (RollNC1 contra) = void $ contra x a Refl
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) =
  let
    contra =
      replace
        {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t}
        (fixInjective $ synthsUnique prf1' prf1)
        contra
  in
  checksSplit prf2 contra

checkSpineSplit (prf :: prfs) (Step1 contra) = void $ contra _ _ Refl
checkSpineSplit (prf :: prfs) (Step2 contras) =
  these (checksSplit prf) (checkSpineSplit prfs) (const $ checkSpineSplit prfs) contras

allSynthsSplit (prfs :< prf) (Step contras) =
  these (synthsSplit prf) (allSynthsSplit prfs) (const $ allSynthsSplit prfs) contras

allChecksSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i
allChecksSplit fresh (Step {as, t, ts} i prf prfs) (Step2 j contras) =
  let
    contras =
      replace
        {p = \(a ** i) => These (NotChecks tyEnv tmEnv a t) (AnyNotChecks tyEnv tmEnv (dropElem as i) ts)}
        (lookupUnique (MkRow as fresh) j i)
        contras
    0 fresh = dropElemFresh as fresh i
  in
  these (checksSplit prf) (allChecksSplit fresh prfs) (const $ allChecksSplit fresh prfs) contras

allBranchesSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i
allBranchesSplit fresh (Step {as, b, x, t, ts} i prf prfs) (Step2 j contras) =
  let
    contras =
      replace
        {p = \(a ** i) =>
          These
            (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t)
            (AnyNotBranches tyEnv tmEnv (dropElem as i) b ts)}
        (lookupUnique (MkRow as fresh) j i)
        contras
    0 fresh = dropElemFresh as fresh i
  in
  these (checksSplit prf) (allBranchesSplit fresh prfs) (const $ allBranchesSplit fresh prfs) contras

-- Synthesis and Checking are decidable

fallbackCheck :
  SynthsOnly e ->
  Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e) ->
  (a : Ty [<]) ->
  LazyEither (Checks tyEnv tmEnv a e) (NotChecks tyEnv tmEnv a e)
fallbackCheck prf p a =
  map
    (\xPrf => uncurry (EmbedC prf) $ snd xPrf)
    (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $
  (b := p) >=> alpha b a

synths :
  (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
  (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
  (e : Term 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) ->
  (a : Ty [<]) -> (t : Term 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) ->
  (a : Ty [<]) -> (ts : List (Term 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) ->
  (es : Context (Term m tyCtx tmCtx)) ->
  Proof (All (const $ Ty [<]) es.names) (AllSynths tyEnv tmEnv es) (AnyNotSynths tyEnv tmEnv es)
allChecks :
  (tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
  (tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
  (as : Context (Ty [<])) -> (ts : Context (Term 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) ->
  (as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term m tyCtx (tmCtx :< x))) ->
  LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts)

synths tyEnv tmEnv (Annot _ t a) =
  pure (sub tyEnv a) $
  map (uncurry AnnotS) AnnotNS $
  all (not $ illFormed a) (checks tyEnv tmEnv (sub tyEnv a) t)
synths tyEnv tmEnv (Var _ i) = Just (indexAll i.pos tmEnv).extract `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
synths tyEnv tmEnv (LetTy _ a (x ** e)) =
  map id (\_, (wf, prf) => LetTyS wf prf) LetTyNS $
  all (not $ illFormed a) (synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e)
synths tyEnv tmEnv (Abs _ (bound ** t)) = Nothing `Because` ChecksNS Abs
synths tyEnv tmEnv (App _ e ts) =
  map snd
    (\(_, _), (prf1, prf2) => AppS prf1 prf2)
    (either AppNS1 (\xPrfs => uncurry AppNS2 (snd xPrfs))) $
  (a := synths tyEnv tmEnv e) >=> checkSpine tyEnv tmEnv a ts
synths tyEnv tmEnv (Tup _ (MkRow es fresh)) =
  map (TProd . fromAll (MkRow es fresh)) (\_ => TupS) TupNS $
  allSynths tyEnv tmEnv es
synths tyEnv tmEnv (Prj meta e l) =
  map (snd . snd) true false $
  (a := synths tyEnv tmEnv e) >=>
  (as := isProd a) >=>
  decLookup l as.context
  where
  true :
    (x : (Ty [<], Row (Ty [<]), Ty [<])) ->
    (Synths tyEnv tmEnv e (fst x), uncurry (\x, yz => (x = TProd (fst yz), uncurry (\y,z => Elem (l :- z) y.context) yz)) x) ->
    Synths tyEnv tmEnv (Prj meta e l) (snd $ snd x)
  true (.(TProd as), as, a) (prf, Refl, i) = PrjS prf i

  false :
    Either
      (NotSynths tyEnv tmEnv e)
      (a : Ty [<] ** (Synths tyEnv tmEnv e a,
        Either
          ((as : Row (Ty [<])) -> Not (a = TProd as))
          (as : Row (Ty [<]) ** (a = TProd as, (b : Ty [<]) -> Not (Elem (l :- b) as.context))))) ->
    NotSynths tyEnv tmEnv (Prj meta e l)
  false (Left contra) = PrjNS1 contra
  false (Right (a ** (prf1, Left contra))) = PrjNS2 prf1 contra
  false (Right (.(TProd as) ** (prf1, Right (as ** (Refl, contra))))) = PrjNS3 prf1 contra
synths tyEnv tmEnv (Inj _ l t) = Nothing `Because` ChecksNS Inj
synths tyEnv tmEnv (Case _ e (MkRow ts _)) = Nothing `Because` ChecksNS Case
synths tyEnv tmEnv (Roll _ t) = Nothing `Because` ChecksNS Roll
synths tyEnv tmEnv (Unroll _ e) =
  map f true false $
  synths tyEnv tmEnv e `andThen` isFix
  where
  f : (Ty [<], (x ** Ty [<x])) -> Ty [<]
  f (a, (x ** b)) = sub [<TFix x b `Over` Id] b

  true :
    (axb : _) ->
    (Synths tyEnv tmEnv e (fst axb), uncurry (\a,xb => a = TFix xb.fst xb.snd) axb) ->
    Synths tyEnv tmEnv (Unroll meta e) (f axb)
  true (.(TFix x a), (x ** a)) (prf, Refl) = UnrollS prf

  false :
    Either
      (NotSynths tyEnv tmEnv e)
      (a ** (Synths tyEnv tmEnv e a, (x : _) -> (b : _) -> Not (a = TFix x b))) ->
    NotSynths tyEnv tmEnv (Unroll meta e)
  false (Left contra) = UnrollNS1 contra
  false (Right (a ** (prf, contra))) = UnrollNS2 prf contra
synths tyEnv tmEnv (Fold _ e (x ** t)) = Nothing `Because` ChecksNS Fold
synths tyEnv tmEnv (Map _ (x ** a) b c) =
  pure _ $
  map (\(wf1, wf2, wf3) => MapS wf1 wf2 wf3) MapNS $
  all (not $ illFormed (TFix x a)) (all (not $ illFormed b) (not $ illFormed c))
synths tyEnv tmEnv (GetChildren _ (x ** a) b) =
  pure _ $
  map (uncurry GetChildrenS) GetChildrenNS $
  all (not $ illFormed (TFix x a)) (not $ illFormed b)

checks tyEnv tmEnv a (Annot meta t b) = fallbackCheck Annot (synths tyEnv tmEnv $ Annot meta t b) a
checks tyEnv tmEnv a (Var meta i) = fallbackCheck Var (synths tyEnv tmEnv $ Var meta i) a
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
checks tyEnv tmEnv a (LetTy _ b (x ** t)) =
  map (uncurry LetTyC) LetTyNC $
  all (not $ illFormed b) (checks (tyEnv :< (sub tyEnv b `Over` Id)) 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
  where
  false :
    (x ** (uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) (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
checks tyEnv tmEnv a (Tup _ (MkRow ts fresh')) =
  map true false $
  (as := isProd a) >=> allChecks tyEnv tmEnv as.context ts
  where
  true :
    forall a.
    (as : Row (Ty [<]) ** (a = TProd as, AllChecks tyEnv tmEnv as.context ts)) ->
    Checks tyEnv tmEnv a (Tup meta (MkRow ts fresh'))
  true (as ** (Refl, prf)) = TupC prf

  false :
    forall a.
    Either
      ((as : Row (Ty [<])) -> Not (a = TProd as))
      (as : Row (Ty [<]) ** (a = TProd as, AnyNotChecks tyEnv tmEnv as.context ts)) ->
    NotChecks tyEnv tmEnv a (Tup meta (MkRow ts fresh'))
  false (Left contra) = TupNC1 contra
  false (Right (as ** (Refl, contra))) = TupNC2 contra
checks tyEnv tmEnv a (Prj meta e l) = fallbackCheck Prj (synths tyEnv tmEnv $ Prj meta e l) a
checks tyEnv tmEnv a (Inj _ l t) =
  map true false $
  (as := isSum a) >=>
  (b := decLookup l as.context) >=>
  checks tyEnv tmEnv b t
  where
  true :
    forall a.
    (as ** (a = TSum as, (b ** (Elem (l :- b) as.context, Checks tyEnv tmEnv b t)))) ->
    Checks tyEnv tmEnv a (Inj meta l t)
  true (as ** (Refl, (b ** (i, prf)))) = InjC i prf

  false :
    forall a.
    Either
      ((as : _) -> Not (a = TSum as))
      (as ** (a = TSum as,
        Either
          ((b : _) -> Not (Elem (l :- b) as.context))
          (b ** (Elem (l :- b) as.context, NotChecks tyEnv tmEnv b t)))) ->
    NotChecks tyEnv tmEnv a (Inj meta l t)
  false (Left contra) = InjNC1 contra
  false (Right (as ** (Refl, Left contra))) = InjNC2 contra
  false (Right (as ** (Refl, Right (b ** (i, contra))))) = InjNC3 i contra
checks tyEnv tmEnv a (Case _ e (MkRow ts fresh)) =
  map true false $
  (b := synths tyEnv tmEnv e) >=>
  (as := isSum b) >=>
  allBranches tyEnv tmEnv as.context a ts
  where
  true :
    forall fresh.
    (b ** (Synths tyEnv tmEnv e b, (as ** (b = TSum as, AllBranches tyEnv tmEnv as.context a ts)))) ->
    Checks tyEnv tmEnv a (Case meta e (MkRow ts fresh))
  true (.(TSum as) ** (prf, (as ** (Refl, prfs)))) = CaseC prf prfs

  false :
    forall fresh.
    Either
      (NotSynths tyEnv tmEnv e)
      (b ** (Synths tyEnv tmEnv e b,
        Either
          ((as : _) -> Not (b = TSum as))
          (as ** (b = TSum as, AnyNotBranches tyEnv tmEnv as.context a ts)))) ->
    NotChecks tyEnv tmEnv a (Case meta e (MkRow ts fresh))
  false (Left contra) = CaseNC1 contra
  false (Right (b ** (prf, Left contra))) = CaseNC2 prf contra
  false (Right (.(TSum as) ** (prf, Right (as ** (Refl, contras))))) = CaseNC3 prf contras
checks tyEnv tmEnv a (Roll _ t) =
  map true false $
  (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

  true :
    forall a.
    (xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), Checks tyEnv tmEnv (ty xb) t)) ->
    Checks tyEnv tmEnv a (Roll meta t)
  true ((x ** b) ** (Refl, prf)) = RollC prf

  false :
    forall a.
    Either
      ((x : _) -> (b : Ty [<x]) -> Not (a = TFix x b))
      (xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), NotChecks tyEnv tmEnv (ty xb) t)) ->
    NotChecks tyEnv tmEnv a (Roll meta t)
  false (Left contra) = RollNC1 contra
  false (Right ((x ** b) ** (Refl, contra))) = RollNC2 contra
checks tyEnv tmEnv a (Unroll meta e) = fallbackCheck Unroll (synths tyEnv tmEnv $ Unroll meta e) a
checks tyEnv tmEnv a (Fold _ e (x ** t)) =
  map true false $
  (b := synths tyEnv tmEnv e) >=>
  (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)

  true :
    (b ** (Synths tyEnv tmEnv e b,
      (yc ** (b = TFix (fst yc) (snd yc), Checks tyEnv (tmEnv' yc) a t)))) ->
    Checks tyEnv tmEnv a (Fold meta e (x ** t))
  true (.(TFix y b) ** (prf1, ((y ** b) ** (Refl, prf2)))) = FoldC prf1 prf2

  false :
    Either
      (NotSynths tyEnv tmEnv e)
      (b ** (Synths tyEnv tmEnv e b,
        Either
          ((y : _) -> (c : Ty [<y]) -> Not (b = TFix y c))
          (yc ** (b = TFix (fst yc) (snd yc), NotChecks tyEnv (tmEnv' yc) a t)))) ->
    NotChecks tyEnv tmEnv a (Fold meta e (x ** t))
  false (Left contra) = FoldNC1 contra
  false (Right (b ** (prf1, Left contra))) = FoldNC2 prf1 contra
  false (Right (.(TFix y b) ** (prf1, Right ((y ** b) ** (Refl, contra))))) = FoldNC3 prf1 contra
checks tyEnv tmEnv a (Map meta (x ** b) c d) =
  fallbackCheck Map (synths tyEnv tmEnv $ Map meta (x ** b) c d) a
checks tyEnv tmEnv a (GetChildren meta (x ** b) c) =
  fallbackCheck GetChildren (synths tyEnv tmEnv $ GetChildren meta (x ** b) c) a

checkSpine tyEnv tmEnv a [] = Just a `Because` []
checkSpine tyEnv tmEnv a (t :: ts) =
  map snd true false $
  (bc := isArrow a) >=>
  all (checks tyEnv tmEnv (fst bc) t) (checkSpine tyEnv tmEnv (snd bc) ts)
  where
  true :
    forall a.
    (bcd : ((Ty [<], Ty [<]), Ty [<])) ->
    ( a = TArrow (fst $ fst bcd) (snd $ fst bcd)
    , uncurry (\bc,d => (Checks tyEnv tmEnv (fst bc) t, CheckSpine tyEnv tmEnv (snd bc) ts d)) bcd) ->
    CheckSpine tyEnv tmEnv a (t :: ts) (snd bcd)
  true ((b, c), d) (Refl, (prf1, prf2)) = prf1 :: prf2

  false :
    forall a.
    Either
      ((b, c : Ty [<]) -> Not (a = TArrow b c))
      (bc : (Ty [<], Ty [<]) ** (a = TArrow (fst bc) (snd bc),
        These
          (NotChecks tyEnv tmEnv (fst bc) t)
          (NotCheckSpine tyEnv tmEnv (snd bc) ts))) ->
    NotCheckSpine tyEnv tmEnv a (t :: ts)
  false (Left contra) = Step1 contra
  false (Right ((b, c) ** (Refl, contras))) = Step2 contras

allSynths tyEnv tmEnv [<] = Just [<] `Because` [<]
allSynths tyEnv tmEnv (es :< (l :- e)) =
  map (uncurry (flip (:<))) (\(a, as), (prf, prfs) => prfs :< prf) Step $
  all (synths tyEnv tmEnv e) (allSynths tyEnv tmEnv es)

allChecks tyEnv tmEnv [<] [<] = True `Because` Base
allChecks tyEnv tmEnv (as :< la) [<] = False `Because` Base1
allChecks tyEnv tmEnv as (ts :< (l :- t)) =
  map
    (\((a ** i) ** (prf, prfs)) => Step i prf prfs)
    (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $
  (ai := (decLookup l as).forget) >=>
  all (checks tyEnv tmEnv (fst ai) t) (allChecks tyEnv tmEnv (dropElem as $ snd ai) ts)

allBranches tyEnv tmEnv [<] b [<] = True `Because` Base
allBranches tyEnv tmEnv (as :< la) b [<] = False `Because` Base1
allBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) =
  map
    (\((a ** i) ** (prf, prfs)) => Step i prf prfs)
    (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $
  (ai := (decLookup l as).forget) >=>
  all
    (checks tyEnv (tmEnv :< (fst ai `Over` Id)) b t)
    (allBranches tyEnv tmEnv (dropElem as $ snd ai) b ts)

-- Sugar -----------------------------------------------------------------------

public export
CheckLit : m -> Nat -> Term m tyCtx tmCtx
CheckLit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<])
CheckLit meta (S n) = Roll meta (Inj meta "S" $ CheckLit meta n)

public export
Lit : m -> Nat -> Term m tyCtx tmCtx
Lit meta n = Annot meta (CheckLit meta n) TNat

public export
Suc : m -> Term m tyCtx tmCtx
Suc meta =
  Annot meta (Abs meta (["_x"] ** Roll meta (Inj meta "S" $ Var meta (%% "_x"))))
    (TArrow TNat TNat)

export
isCheckLit : Term m tyCtx tmCtx -> Maybe Nat
isCheckLit (Roll _ (Inj _ "Z" (Tup _ (MkRow [<] _)))) = Just 0
isCheckLit (Roll _ (Inj _ "S" t)) = S <$> isCheckLit t
isCheckLit _ = Nothing

export
isLit : Term m tyCtx tmCtx -> Maybe Nat
isLit (Annot _ t a) =
  if (alpha {ctx2 = [<]} a TNat).does
  then isCheckLit t
  else Nothing
isLit _ = Nothing

export
isSuc : Term m tyCtx tmCtx -> Bool
isSuc (Annot _ (Abs _ ([x] ** Roll _ (Inj _ "S" $ Var _ ((%%) x {pos = Here})))) a) =
  does (alpha {ctx2 = [<]} a (TArrow TNat TNat))
isSuc _ = False