X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;h=60e84b67eaa9b2e53c7bfc76e9e86c3695bc3089;hp=916afe14ac601e8fd68f551e432ef95ef61e9590;hb=4c5c94487aa2bf5489371f112607f0a4c4f01a94;hpb=bcb16a7fa1ff772f12807c4587609fd756b7762e

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 916afe1..60e84b6 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -8,29 +8,22 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
-Require Import HaskCoreTypes.  (* FIXME *)
-Require Import HaskCoreVars.   (* FIXME *)
+Require Import HaskLiterals.
+Require Import HaskTyCons.
+Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
-Require Import HaskWeakVars.   (* FIXME *)
-Require Import HaskCoreToWeak. (* FIXME *)
+Require Import HaskWeakVars.
+Require Import HaskWeak.
+Require Import HaskCoreToWeak.
 
-Variable CoFunConst        : nat -> Type.  (* FIXME *)
-Variable TyFunConst        : nat -> Type.  (* FIXME *)
+Variable dataConTyCon      : CoreDataCon -> TyCon.         Extract Inlined Constant dataConTyCon      => "DataCon.dataConTyCon".
+Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Constant dataConExVars_    => "DataCon.dataConExTyVars".
+Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
+Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
 
-Variable dataConTyCon      : CoreDataCon -> TyCon.     Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
-
-Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
-Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta".
-Variable dataConOrigArgTys_:CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_ =>"DataCon.dataConOrigArgTys".
-Variable getTyConTyVars_   : TyCon   -> list CoreVar.  Extract Inlined Constant getTyConTyVars_ => "TyCon.tyConTyVars".
-
-(* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
-Definition tyConTyVars (tc:TyCon) :=
-  filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)).
-  Opaque tyConTyVars.
 Definition dataConExTyVars cdc :=
-  filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
+  filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (dataConExVars_ cdc)).
   Opaque dataConExTyVars.
 Definition dataConCoerKinds cdc :=
   filter (map (fun x => match x with EqPred t1 t2 =>
@@ -60,80 +53,66 @@ Inductive DataCon : TyCon -> Type :=
   Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
   (*Opaque DataCon.*)
 
-Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool.
-  intros.
-  destruct dc1.
-  destruct dc2.
-  exact (if eqd_dec cdc cdc0 then true else false).
-  Defined.
-
-Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2).
-
-Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
-  intros.
-  apply Build_EqDecidable.
-  intros.
-  set (trust_compare_datacons _ v1 v2) as x.
-  set (compare_datacons tc v1 v2) as y.
-  assert (y=compare_datacons tc v1 v2). reflexivity.
-  destruct y; rewrite <- H in x.
-  left; auto.
-  right; auto.
-  Defined.
+Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
 
 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
 Section Raw.
 
   (* TV is the PHOAS type which stands for type variables of System FC *)
-  Context {TV:Type}.
+  Context {TV:Kind -> Type}.
 
   (* Figure 7: ρ, σ, τ, ν *)
-  Inductive RawHaskType  : Type :=
-  | TVar           : TV                                                     -> RawHaskType   (* a        *)
-  | TCon           : TyCon                                                  -> RawHaskType   (* T        *)
-  | TArrow         :                                                           RawHaskType   (* (->)     *)
-  | TCoerc         : RawHaskType -> RawHaskType -> RawHaskType              -> RawHaskType   (* (+>)     *)
-  | TApp           : RawHaskType                  ->     RawHaskType        -> RawHaskType   (* φ φ      *)
-  | TFCApp         : forall tc:TyCon,                vec RawHaskType tc     -> RawHaskType   (* S_n      *)
-  | TAll           : Kind  -> (TV -> RawHaskType)                           -> RawHaskType   (* ∀a:κ.φ   *)
-  | TCode          : RawHaskType -> RawHaskType                             -> RawHaskType   (* from λ^α *).
+  Inductive RawHaskType : Kind -> Type :=
+  | TVar           : ∀ κ, TV κ                                              -> RawHaskType κ                     (* a        *)
+  | TCon           : ∀ tc,                                                     RawHaskType (tyConKind' tc)       (* T        *)
+  | TArrow         :                                                           RawHaskType (★ ⇛★ ⇛★ )            (* (->)     *)
+  | TCoerc         : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★   -> RawHaskType ★                     (* (+>)     *)
+  | TApp           : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁)        -> RawHaskType κ₂  -> RawHaskType κ₁                    (* φ φ      *)
+  | TAll           : ∀ κ,                          (TV κ -> RawHaskType ★)  -> RawHaskType ★                     (* ∀a:κ.φ   *)
+  | TCode          : RawHaskType ECKind                  -> RawHaskType ★   -> RawHaskType ★                     (* from λ^α *)
+  | TyFunApp       : forall (tf:TyFun) kl k, RawHaskTypeList kl             -> RawHaskType k                     (* S_n      *)
+  with RawHaskTypeList : list Kind -> Type :=
+  | TyFunApp_nil   : RawHaskTypeList nil
+  | TyFunApp_cons  : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
     
   (* the "kind" of a coercion is a pair of types *)
-  Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind.
-
-  Section CV.
-
-    (* the PHOAS type which stands for coercion variables of System FC *)
-    Context {CV:Type}.
-
-    (* Figure 7: γ, δ *)
-    Inductive RawHaskCoer : Prop :=
-    | CoVar          : CV                                           -> RawHaskCoer (* g      *)
-    | CoType         : RawHaskType                                  -> RawHaskCoer (* τ      *)
-    | CoApp          : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* γ γ    *)
-    | CoAppT         : RawHaskCoer -> RawHaskType                   -> RawHaskCoer (* γ@v    *)
-    | CoCFApp        : ∀ n, CoFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* C   γⁿ *)
-    | CoTFApp        : ∀ n, TyFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* S_n γⁿ *)
-    | CoAll          : Kind  -> (TV -> RawHaskCoer)                 -> RawHaskCoer (* ∀a:κ.γ *)
-    | CoSym          : RawHaskCoer                                  -> RawHaskCoer (* sym    *)
-    | CoComp         : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* ◯      *)
-    | CoLeft         : RawHaskCoer                                  -> RawHaskCoer (* left   *)
-    | CoRight        : RawHaskCoer                                  -> RawHaskCoer (* right  *).
-
-  End CV.
+  Inductive RawCoercionKind : Type :=
+    mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
+
+  (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
+  Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
+  (*  
+   *  This has been disabled until we manage to reconcile SystemFC's
+   *  coercions with what GHC actually implements (they are not the
+   *  same!)
+   *  
+  | CoVar          : CV                                           -> RawHaskCoer (* g      *)
+  | CoType         : RawHaskType                                  -> RawHaskCoer (* τ      *)
+  | CoApp          : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* γ γ    *)
+  | CoAppT         : RawHaskCoer -> RawHaskType                   -> RawHaskCoer (* γ@v    *)
+  | CoCFApp        : ∀ n, CoFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* C   γⁿ *)
+  | CoTFApp        : ∀ n, TyFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* S_n γⁿ *)
+  | CoAll          : Kind  -> (TV -> RawHaskCoer)                 -> RawHaskCoer (* ∀a:κ.γ *)
+  | CoSym          : RawHaskCoer                                  -> RawHaskCoer (* sym    *)
+  | CoComp         : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* ◯      *)
+  | CoLeft         : RawHaskCoer                                  -> RawHaskCoer (* left   *)
+  | CoRight        : RawHaskCoer                                  -> RawHaskCoer (* right  *).
+  *)
 End Raw.
 
 Implicit Arguments TCon   [ [TV] ].
-Implicit Arguments TFCApp [ [TV] ].
+Implicit Arguments TyFunApp [ [TV] ].
 Implicit Arguments RawHaskType  [ ].
 Implicit Arguments RawHaskCoer  [ ].
 Implicit Arguments RawCoercionKind [ ].
+Implicit Arguments TVar [ [TV] [κ] ].
+Implicit Arguments TCoerc [ [TV] [κ] ].
+Implicit Arguments TApp   [ [TV] [κ₁] [κ₂] ].
+Implicit Arguments TAll   [ [TV] ].
 
 Notation "t1 ---> t2"        := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"     := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
 
-
-
 (* Kind and Coercion Environments *)
 (*
  *  In System FC, the environment consists of three components, each of
@@ -145,68 +124,197 @@ Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"     := (fun TV env => TCoerc (φ₁ TV e
  *)
 
 Definition TypeEnv                                                         := list Kind.
-Definition InstantiatedTypeEnv     (TV:Type)   (Γ:TypeEnv)                 := vec TV (length Γ).
+Definition InstantiatedTypeEnv     (TV:Kind->Type)         (Γ:TypeEnv)     := IList _ TV Γ.
 Definition HaskCoercionKind                    (Γ:TypeEnv)                 := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
-Definition CoercionEnv                         (Γ:TypeEnv)                 := list (HaskCoercionKind Γ).
-Definition InstantiatedCoercionEnv (TV CV:Type)(Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
-
+Definition CoercionEnv             (Γ:TypeEnv)                             := list (HaskCoercionKind Γ).
+Definition InstantiatedCoercionEnv (TV:Kind->Type) CV       (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
 
 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
-Definition HaskTyVar (Γ:TypeEnv) :=  forall TV    (env:@InstantiatedTypeEnv TV Γ), TV.
-Definition HaskCoVar Γ Δ         :=  forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
-Definition HaskLevel (Γ:TypeEnv) :=  list (HaskTyVar Γ).
-Definition HaskType         (Γ:TypeEnv)                  := ∀ TV, @InstantiatedTypeEnv TV    Γ -> RawHaskType           TV.
-Definition HaskCoercion Γ Δ := ∀ TV CV,
-  @InstantiatedTypeEnv TV Γ -> @InstantiatedCoercionEnv TV CV Γ Δ -> RawHaskCoer TV CV.
-Inductive  LeveledHaskType (Γ:TypeEnv) := mkLeveledHaskType : HaskType Γ -> HaskLevel Γ -> LeveledHaskType Γ.
-Definition FreshHaskTyVar {Γ}(κ:Kind)  : HaskTyVar (κ::Γ) := fun TV env => vec_head env.
-Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) : HaskType Γ
+Definition HaskTyVar (Γ:TypeEnv) κ :=  forall TV    (env:@InstantiatedTypeEnv TV Γ), TV κ.
+Definition HaskCoVar Γ Δ           :=  forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
+Definition HaskLevel (Γ:TypeEnv)   :=  list (HaskTyVar Γ ECKind).
+Definition HaskType  (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
+Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
+
+Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
+  haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
+  Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
+  Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
+    match htosk with
+      haskTypeOfSomeKind κ _ => κ
+    end.
+  Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
+  Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
+    match htosk as H return HaskType Γ H with
+      haskTypeOfSomeKind _ ht => ht
+      end.
+  Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
+
+Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
+    @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
+Inductive  LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
+
+Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
+Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
   := fun TV env => TAll κ (σ TV env).
-Definition HaskTApp {Γ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(cv:HaskTyVar Γ) : HaskType Γ
+Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
+  (cv:HaskTyVar Γ κ) : HaskType Γ ★
   := fun TV env => σ TV env (cv TV env).
-Definition HaskBrak {Γ}(v:HaskTyVar Γ)(t:HaskType Γ) : HaskType Γ := fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
-Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ := fun TV ite => TCon tc.
-Definition HaskAppT {Γ}(t1 t2:HaskType Γ) : HaskType Γ := fun TV ite => TApp (t1 TV ite) (t2 TV ite).
-Definition mkHaskCoercionKind {Γ}(t1 t2:HaskType Γ) : HaskCoercionKind Γ :=
- fun TV ite => mkRawCoercionKind (t1 TV ite) (t2 TV ite).
-Definition unMkHaskCoercionKind {Γ}(hck:HaskCoercionKind Γ) : (HaskType Γ * HaskType Γ) :=
-  ((fun TV ite => match (hck TV ite) with mkRawCoercionKind t1 _ => t1 end),
-   (fun TV ite => match (hck TV ite) with mkRawCoercionKind _ t2 => t2 end)).
-
-
-(* PHOAS substitution on types *)
-Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(v:@HaskType Γ) : @HaskType Γ
-  := fun TV env =>
-    (fix flattenT (exp: RawHaskType (RawHaskType TV)) : RawHaskType TV :=
+Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
+  fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
+Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
+  := fun TV ite => TCon tc.
+Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
+  fun TV ite => TApp (t1 TV ite) (t2 TV ite).
+Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
+ fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
+
+Section Flatten.
+  Context {TV:Kind -> Type }.
+Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
      match exp with
-    | TVar       x        => x
-    | TAll       k y      => TAll      k (fun v => flattenT (y (TVar v)))
-    | TApp       x y      => TApp      (flattenT x) (flattenT y)
+    | TVar    _  x        => x
+    | TAll     _ y        => TAll   _  (fun v => flattenT  (y (TVar v)))
+    | TApp   _ _ x y      => TApp      (flattenT  x) (flattenT  y)
     | TCon       tc       => TCon      tc
-    | TCoerc t1 t2   t    => TCoerc    (flattenT t1) (flattenT t2)   (flattenT t)
+    | TCoerc _ t1 t2 t    => TCoerc    (flattenT  t1) (flattenT  t2)   (flattenT  t)
     | TArrow              => TArrow
-    | TCode      v e      => TCode     (flattenT v) (flattenT e)
-    | TFCApp       tfc lt => TFCApp    tfc
-      ((fix flatten_vec n (expv:vec (RawHaskType (RawHaskType TV)) n) : vec (RawHaskType TV) n :=
-        match expv in vec _ N return vec (RawHaskType TV) N with
-          | vec_nil => vec_nil
-          | x:::y   => (flattenT x):::(flatten_vec _ y)
-        end) _ lt)
-    end)
-    (exp (RawHaskType TV) (vec_map (fun tv => TVar tv) env) (v TV env)).
-Notation "t @@  l" := (@mkLeveledHaskType _ t l) (at level 20).
-Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
-Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
-
-
+    | TCode      v e      => TCode     (flattenT  v) (flattenT  e)
+    | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt)
+    end
+    with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
+    match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
+    | TyFunApp_nil               => TyFunApp_nil
+    | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flattenT  t) (flattenTyFunApp _ rest)
+    end.
+End Flatten.
 
+(* PHOAS substitution on types *)
+Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
+  : @HaskType Γ κ₂ :=
+  fun TV env =>
+    flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
 
+Notation "t @@  l" := (@mkLeveledHaskType _ _ t l) (at level 20).
+Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
+Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
 
+Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end.
 
+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.
 
+Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
+  fun pf =>
+  fun TV ite =>
+    match take_arg_types (ht TV ite) with
+    | nil => Prelude_error "impossible"
+    | x::y => x
+    end.
+
+(* From (t1->(t2->(t3-> ... t))), return t *)
+(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
+Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
+  match exp as E in RawHaskType _ K return RawHaskType _ K with
+    | TApp   κ₁ κ₂ x y      =>
+      let q :=
+      (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
+         | KindStar =>
+           match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
+             | KindStar => fun x' =>
+               match x' return  (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
+                 | TApp κ₁'' κ₂'' w'' x'' =>
+                   match κ₂'' as K2'' return RawHaskType TV K2'' ->  (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
+                     | KindStar     =>
+                       match w'' with
+                         | TArrow => fun _ b => Some b
+                         | _      => fun _ b => None
+                       end
+                     | _ => fun _ b => None
+                   end x''
+                 | _       => fun _ => None
+               end
+             | _        => fun _ _ => None
+           end
+         | _ => fun _ _ => None
+       end) x (drop_arg_types y)
+      in match q with
+           | None   => TApp x y
+           | Some y => y
+         end
+    | b                     => b
+  end.
 
 
 
@@ -214,12 +322,14 @@ Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
 (* yeah, things are kind of messy below this point *)
 
 
-Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) := vec_tail ite.
+Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
+  := ilist_tail ite.
 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
   map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
-Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind)
-  : InstantiatedTypeEnv TV (κ::Γ) := tv:::env.
-Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV CV:Type}(env:InstantiatedCoercionEnv TV CV Γ Δ)(tv:TV)(κ:Kind)
+Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
+  : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
+Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
+  (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
   : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
     simpl.
     unfold InstantiatedCoercionEnv.
@@ -228,9 +338,7 @@ Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV CV:Type}(env:Ins
     rewrite <- map_preserves_length.
     apply env.
     Defined.
-Definition typeEnvContainsType {Γ}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind) : Prop
-  := @vec_In _ _ (tv,κ) (vec_zip env (list2vec Γ)).
-Definition coercionEnvContainsCoercion {Γ}{Δ}{TV CV:Type}(ite:InstantiatedTypeEnv TV Γ)
+Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
   (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
   := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
@@ -242,46 +350,40 @@ Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:Instanti
   unfold InstantiatedCoercionEnv; simpl. 
   apply vec_cons; auto.
   Defined.
-Notation "env  ∋  tv : κ"        := (@typeEnvContainsType  _ _ env tv κ).
-Notation "env '+' tv : κ"        := (@addKindToInstantiatedTypeEnv  _ _ env tv κ).
-
 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
-Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := vec_tail ite.
+Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
+  := ilist_tail ite.
 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
   induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
-Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
-Definition weakV  {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (κ::Γ) := fun TV ite => (cv' TV (weakITE ite)).
-Definition weakV' {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (app κ Γ).
+Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
+  := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
+Definition weakV  {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
+  := fun TV ite => (cv' TV (weakITE ite)).
+Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
   induction κ; auto. apply weakV; auto. Defined.
-Definition weakT {Γ:TypeEnv}{κ:Kind}(lt:HaskType Γ) : HaskType (κ::Γ) := fun TV ite => lt TV (weakITE ite).
-Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
-Definition weakT' {Γ}{κ}(lt:HaskType Γ) : HaskType (app κ Γ).
+Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
+  := fun TV ite => lt TV (weakITE ite).
+Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
+  := map weakV lt.
+Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
   induction κ; auto. apply weakT; auto. Defined.
-Definition weakT'' {Γ}{κ}(lt:HaskType Γ) : HaskType (app Γ κ).
-unfold HaskType in *.
-unfold InstantiatedTypeEnv in *.
-intros.
-apply vec_chop in X.
-apply lt.
-apply X.
-Defined.
-Definition lamer {a}{b}{c}(lt:HaskType (app (app a  b) c)) : HaskType  (app a (app b c)).
-rewrite <- ass_app in lt.
-exact lt.
-Defined.
-Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ) :=
-  let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT t1) (weakT t2).
-Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ) :=
-  let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT' t1) (weakT' t2).
-Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
-match κ as K return list (HaskCoercionKind (app K Γ)) with
-  | nil => hck
-  | _   => map weakCK' hck
-end.
+Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
+  unfold HaskType in *.
+  unfold InstantiatedTypeEnv in *.
+  intros.
+  apply ilist_chop in X.
+  apply lt.
+  apply X.
+  Defined.
+Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
+  rewrite <- ass_app in lt.
+  exact lt.
+  Defined.
 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
   induction κ; auto. apply weakL; auto. Defined.
-Definition weakLT {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (κ::Γ) := match lt with t @@ l => weakT t @@ weakL l end.
-Definition weakLT' {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (app κ Γ)
+Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
+  := match lt with t @@ l => weakT t @@ weakL l end.
+Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
   := match lt with t @@ l => weakT' t @@ weakL' l end.
 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
   induction κ; auto. apply weakCE; auto. Defined.
@@ -295,108 +397,116 @@ Definition weakICE  {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:Instantiated
   rewrite <- map_preserves_length in ice.
   apply ice.
   Defined.
-Definition weakICE' {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (app κ Γ) (weakCE' Δ))
-  : InstantiatedCoercionEnv TV CV Γ Δ.
-  induction κ; auto. apply IHκ. eapply weakICE. apply ice. Defined.
+Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
+  unfold HaskCoercionKind in *.
+  intros.
+  apply hck; clear hck.
+  inversion X; subst; auto.
+  Defined.
+Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
+  induction κ; auto.
+  apply weakCK.
+  apply IHκ.
+  Defined.
+Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
+  map weakCK' hck.
 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
   fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
-Definition weakC  {Γ}{κ}{Δ}(c:HaskCoercion Γ Δ) : HaskCoercion (κ::Γ) (weakCE Δ) :=
-  fun TV CV ite ice => c TV CV (weakITE ite) (weakICE ice).
-Definition weakF {Γ:TypeEnv}{κ:Kind}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) : 
-  forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV -> RawHaskType TV
+Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : 
+  forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
   := fun TV ite tv => (f TV (weakITE ite) tv).
 
+Fixpoint caseType0 {Γ}(lk:list Kind) :
+  IList _ (HaskType Γ) lk ->
+  HaskType Γ (fold_right KindArrow ★ lk) ->
+  HaskType Γ ★ :=
+  match lk as LK return
+    IList _ (HaskType Γ) LK ->
+    HaskType Γ (fold_right KindArrow ★ LK) ->
+    HaskType Γ ★ 
+  with
+  | nil    => fun _     ht => ht
+  | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
+  end.
+
+Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
+  caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
+
 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 Record StrongAltCon {tc:TyCon} :=
-{ sac_altcon      :  AltCon
+{ sac_tc          := tc
+; sac_altcon      :  WeakAltCon
 ; sac_numExTyVars :  nat
 ; sac_numCoerVars :  nat
 ; sac_numExprVars :  nat
-; sac_akinds      :  vec Kind tc
 ; sac_ekinds      :  vec Kind sac_numExTyVars
-; sac_kinds       := app (vec2list sac_akinds) (vec2list sac_ekinds)
-; sac_Γ           := fun Γ => app (vec2list sac_ekinds) Γ
-; sac_coercions   :  forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
-; sac_types       :  forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskType (sac_Γ Γ)) sac_numExprVars
-; sac_Δ           := fun    Γ (atypes:vec (HaskType Γ) tc) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
+; sac_kinds       := app (tyConKind tc) (vec2list sac_ekinds)
+; sac_gamma          := fun Γ => app (vec2list sac_ekinds) Γ
+; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars
+; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars
+; sac_delta          := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 }.
-Coercion sac_altcon : StrongAltCon >-> AltCon.
+Coercion sac_tc     : StrongAltCon >-> TyCon.
+Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
+  
 
-Definition caseType {Γ:TypeEnv}(tc:TyCon)(atypes:vec (HaskType Γ) tc) :=
-  fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc).
+Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
 
+Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
 
-(***************************************************************************************************)
-(* Well-Formedness of Types and Coercions                                                          *)
-(* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
-Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
-  mkTFD : Kind -> TypeFunctionDecl tfc vk.
+Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
+  set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
+  unfold tyConKind' in z.
+  rewrite literal_tycons_are_of_ordinary_kind in z.
+  unfold HaskType.
+  apply z.
+  Defined.
 
+Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 
-(* Figure 8, upper half *)
-Inductive WellKinded_RawHaskType (TV:Type)
-  : forall Γ:TypeEnv, InstantiatedTypeEnv TV Γ -> RawHaskType TV -> Kind -> Prop :=
-  | WFTyVar  : forall Γ env κ d,
-                env∋d:κ ->
-                WellKinded_RawHaskType TV Γ env (TVar d) κ
-  | WFTyApp  : forall Γ env κ₁ κ₂ σ₁ σ₂,
-                WellKinded_RawHaskType TV Γ env σ₁  (κ₁ ⇛ κ₂)  ->
-                WellKinded_RawHaskType TV Γ env σ₂        κ₂   ->
-                WellKinded_RawHaskType TV Γ env (TApp σ₁ σ₂) κ₂
-  | WFTyAll  : forall Γ (env:InstantiatedTypeEnv TV Γ) κ     σ    ,
-                (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ )        -> 
-                WellKinded_RawHaskType TV _  env      (TAll κ σ) ★ 
-  | TySCon   : forall Γ env tfc lt vk ι ,
-                @TypeFunctionDecl tfc vk  ->
-                ListWellKinded_RawHaskType TV Γ _ env lt vk ->
-                WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι
-with ListWellKinded_RawHaskType (TV:Type)
-  : forall (Γ:TypeEnv) n, InstantiatedTypeEnv TV Γ -> vec (RawHaskType TV) n -> vec Kind n -> Prop :=
-  | ListWFRawHaskTypenil  : forall Γ env,
-                ListWellKinded_RawHaskType TV Γ 0 env  vec_nil vec_nil
-  | ListWFRawHaskTypecons : forall Γ env n t k lt lk,
-                WellKinded_RawHaskType     TV Γ env      t       k  ->
-                ListWellKinded_RawHaskType TV Γ n env     lt      lk  ->
-                ListWellKinded_RawHaskType TV Γ (S n) env  (t:::lt) (k:::lk).
-
-Variable kindOfTyCon : forall (tc:TyCon), Kind.
-  Extract Inlined Constant kindOfTyCon => "(\x -> Prelude.error ""not implemented yet"")".
-
-Fixpoint kindOfRawHaskType (rht:RawHaskType Kind) : ???Kind :=
-match rht with
-  | TVar   k         => OK k
-  | TCon     tc      => OK (kindOfTyCon tc)
-  | TCoerc t1 t2   t => OK (★ ⇛ ★ )
-  | TArrow           => OK (★ ⇛ ★ ⇛ ★ )
-  | TApp   ht1 ht2   => kindOfRawHaskType ht1 >>= fun k1 =>
-                        kindOfRawHaskType ht2 >>= fun k2 =>
-                          match k1 with
-                            | k1' ⇛ k2' => if eqd_dec k1' k1 then OK k2' else Error "kind mismatch"
-                            | _         =>                                    Error "attempt to apply a non-functional kind"
-                          end
-  | TFCApp   tc rht' => Error "calculating kind of TFCApp is not yet implemented"
-  | TAll   k t'      => kindOfRawHaskType (t' k) >>= fun k' => OK (k ⇛ k')
-  | TCode  t1 t2     => OK ★
-end.
-
-Definition kindITE (Γ:TypeEnv) : InstantiatedTypeEnv Kind Γ :=
-  list2vec Γ.
+Fixpoint update_xi
+  `{EQD_VV:EqDecidable VV}{Γ}
+   (ξ:VV -> LeveledHaskType Γ ★)
+   (lev:HaskLevel Γ)
+   (vt:list (VV * HaskType Γ ★))
+   : VV -> LeveledHaskType Γ ★ :=
+  match vt with
+    | nil => ξ
+    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
+  end.
 
-Definition kindOfType {Γ}(ht:HaskType Γ) : ???Kind :=
-  kindOfRawHaskType (ht Kind (kindITE Γ)).
+Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+  not (In v (map (@fst _ _) varstypes)) ->
+  (update_xi ξ lev varstypes) v = ξ v.
+  intros.
+  induction varstypes.
+  reflexivity.
+  simpl.
+  destruct a.
+  destruct (eqd_dec v0 v).
+  subst.
+  simpl in  H.
+  assert False. 
+  apply H.
+  auto.
+  inversion H0.
+  apply IHvarstypes.
+  unfold not; intros.
+  apply H.
+  simpl.
+  auto.
+  Defined.
 
-Definition WellKindedHaskType Γ (ht:HaskType Γ) κ :=
-  forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ.
-  Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ).
 
-(* "decl", production for "axiom" *)
-Structure AxiomDecl (n:nat)(ccon:CoFunConst n)(vk:vec Kind n){TV:Type} : Type :=
-{ axd_τ : vec TV n -> RawHaskType TV
-; axd_σ : vec TV n -> RawHaskType TV
-}.
+(***************************************************************************************************)
+(* Well-Formedness of Types and Coercions                                                          *)
+(* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
+Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
+  mkTFD : Kind -> TypeFunctionDecl tfc vk.
 
+(*
 Section WFCo.
-  Context {TV:Type}.
+  Context {TV:Kind->Type}.
   Context {CV:Type}.
 
   (* local notations *)
@@ -420,7 +530,7 @@ Section WFCo.
   | Right  :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t   )   -> e⊢ᴄᴏ CoRight γ   :        σ₂ ∼ τ₂ : Δ :Γ: t
   (*
   | SComp  :∀ Γ Δ t e γ n S σ τ κ,
-            ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TFCApp(n:=n) S σ : κ  -> e⊢ᴄᴏ CoTFApp S γ : TFCApp S σ∼TFCApp S τ : Δ : Γ : t
+            ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ  -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
   | CoAx   :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
     ListWFCo                              Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
     ListWellKinded_RawHaskType TV Γ t   (map TVar (vec2list σ₁))            (vec2list κ)  ->
@@ -453,14 +563,127 @@ Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:Hask
   forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
     @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
     Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
+*)
+
+
+
+
+(* Decidable equality on PHOAS types *)
+Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
+match t1 with
+| TVar    _  x     => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
+| TAll     _ y     => match t2 with TAll _ y' => compareT (S n) (y n) (y' n)          | _ => false end
+| TApp   _ _ x y   => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
+| TCon       tc    => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
+| TArrow           => match t2 with TArrow => true | _ => false end
+| TCode      ec t  => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
+| TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end
+| TyFunApp tfc kl k lt  => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
+end
+with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
+match t1 with
+| TyFunApp_nil              => match t2 with TyFunApp_nil => true | _ => false end
+| TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
+end.
 
-Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)).
+Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
+match lk as LK return IList _ _ LK with
+  | nil    => INil
+  | h::t   => n::::(count' t (S n))
+end.
 
-Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18).
+Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
+  compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
+
+(* The PHOAS axioms
+ * 
+ * This is not provable in Coq's logic because the Coq function space
+ * is "too big" - although its only definable inhabitants are Coq
+ * functions, it is not provable in Coq that all function space
+ * inhabitants are definable (i.e. there are no "exotic" inhabitants).
+ * This is actually an important feature of Coq: it lets us reason
+ * about properties of non-computable (non-recursive) functions since
+ * any property proven to hold for the entire function space will hold
+ * even for those functions.  However when representing binding
+ * structure using functions we would actually prefer the smaller
+ * function-space of *definable* functions only.  These two axioms
+ * assert that. *)
+Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
+  if compareHT Γ κ ht1 ht2
+  then ht1=ht2
+  else ht1≠ht2.
+Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
+  if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
+  then htv1=htv2
+  else htv1≠htv2.
+
+(* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
+Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
+  apply Build_EqDecidable.
+  intros.
+  set (compareHT_decides _ _ v1 v2) as z.
+  set (compareHT Γ κ v1 v2) as q.
+  destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
+    left; auto.
+    right; auto.
+    Defined.
 
-Fixpoint update_ξ
-  `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ :=
-  match vt with
-    | nil => ξ
-    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
+Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
+  apply Build_EqDecidable.
+  intros.
+  set (compareVars _ _ v1 v2) as z.
+  set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
+  destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
+    left; auto.
+    right; auto.
+    Defined.
+
+Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
+  apply Build_EqDecidable.
+  intros.
+  unfold HaskLevel in *.
+  apply (eqd_dec v1 v2).
+  Defined.
+
+
+
+
+
+(* ToString instance for PHOAS types *)
+Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
+    match t with
+    | TVar    _ v          => "tv" +++ toString v
+    | TCon    tc           => toString tc
+    | TCoerc _ t1 t2   t   => "("+++typeToString' false n t1+++"~"
+                                  +++typeToString' false n t2+++")=>"
+                                  +++typeToString' needparens n t
+    | TApp  _ _  t1 t2     =>
+      match t1 with
+        | TApp _ _ TArrow t1 =>
+                     if needparens
+                     then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
+                     else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
+        | _ =>
+                     if needparens
+                     then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
+                     else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
+      end
+    | TArrow => "(->)"
+    | TAll   k f           => let alpha := "tv"+++ toString n
+                              in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
+                                   typeToString' false (S n) (f n)
+    | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
+    | TyFunApp   tfc kl k lt    => toString tfc+++ "_" +++ toString n+++" ["+++
+      (fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
+  end
+  with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
+  match t with
+  | TyFunApp_nil                 => nil
+  | TyFunApp_cons  κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
   end.
+
+Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
+  typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
+
+Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
+  { toString := typeToString }.