+Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
+ match lht with t@@l => t end.
+
+Structure Global Γ :=
+{ glob_wv : WeakExprVar
+; glob_kinds : list Kind
+; glob_tf : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
+}.
+Coercion glob_tf : Global >-> Funclass.
+Coercion glob_wv : Global >-> WeakExprVar.
+
+(* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
+(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
+Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
+ match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
+ | TApp κ₁ κ₂ x y =>
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
+ | KindStar => fun x' =>
+ match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
+ list (RawHaskType _ KindStar) with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun a b => a::b
+ | _ => fun _ _ => nil
+ end
+ | _ => fun _ _ => nil
+ end x''
+ | _ => fun _ => nil
+ end
+ | _ => fun _ _ => nil
+ end
+ | _ => fun _ _ => nil
+ end) x (take_arg_types y)
+ | _ => nil
+ end.
+
+Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
+ match exp as E in RawHaskType _ K return nat with
+ | TApp κ₁ κ₂ x y =>
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
+ | KindStar => fun x' =>
+ match x' return nat -> nat with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun a b => S b
+ | _ => fun _ _ => 0
+ end
+ | _ => fun _ _ => 0
+ end x''
+ | _ => fun _ => 0
+ end
+ | _ => fun _ _ => 0
+ end
+ | _ => fun _ _ => 0
+ end) x (count_arg_types y)
+ | _ => 0
+ end.
+
+ Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
+ intros.
+ induction Γ.
+ apply INil.
+ apply ICons; auto.
+ apply tt.
+ Defined.