| TVar : ∀ κ, TV κ -> RawHaskType κ (* a *)
| TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *)
| TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *)
+ (*
+ | TKappa : RawHaskType (★ ⇛★ ⇛★ ) (* (~~>) *)
+ *)
| TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
| TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
| TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
Implicit Arguments TAll [ [TV] ].
Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
+(*Notation "t1 ~~~> t2" := (fun TV env => (TApp (TApp TKappa (t1 TV env)) (t2 TV env))).*)
Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
(* Kind and Coercion Environments *)
Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
{ toString := typeToString }.
+
+Definition TBool {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp BoolTyCon _ _ TyFunApp_nil.
+Definition TInt {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp IntTyCon _ _ TyFunApp_nil.