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

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index e79927a..60e84b6 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -8,7 +8,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
@@ -21,9 +22,8 @@ Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Const
 Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
 
-(* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
 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 =>
@@ -53,28 +53,7 @@ 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 KindTypeFunction ★ (tyConKind tc).
+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.
@@ -90,8 +69,8 @@ Section Raw.
   | TCoerc         : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★   -> RawHaskType ★                     (* (+>)     *)
   | TApp           : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁)        -> RawHaskType κ₂  -> RawHaskType κ₁                    (* φ φ      *)
   | TAll           : ∀ κ,                          (TV κ -> RawHaskType ★)  -> RawHaskType ★                     (* ∀a:κ.φ   *)
-  | TCode          : RawHaskType ★                       -> RawHaskType ★   -> RawHaskType ★                     (* from λ^α *)
-  | TyFunApp       : ∀ tf, RawHaskTypeList (fst (tyFunKind tf))             -> RawHaskType (snd (tyFunKind tf))  (* S_n      *)
+  | 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).
@@ -100,27 +79,25 @@ Section Raw.
   Inductive RawCoercionKind : Type :=
     mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
 
-  Section CV.
-
-    (* the PHOAS type which stands for coercion variables of System FC *)
-    
-
-    (* Figure 7: γ, δ *)
-    Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *).
-(*
-    | 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.
+  (* 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] ].
@@ -155,7 +132,7 @@ Definition InstantiatedCoercionEnv (TV:Kind->Type) CV       (Γ:TypeEnv)(Δ:Coer
 (* 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 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).
 
@@ -183,45 +160,161 @@ Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ),
 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 Γ ★:=
+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 KindTypeFunction ★ (tyConKind tc))
+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).
 
-(* 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 (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
+Section Flatten.
+  Context {TV:Kind -> Type }.
+Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
      match exp with
     | TVar    _  x        => x
-    | TAll     _ y        => TAll   _  (fun v => flattenT _ (y (TVar v)))
-    | TApp   _ _ x y      => TApp      (flattenT _ x) (flattenT _ y)
+    | 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)
-    | TyFunApp       tfc lt => TyFunApp tfc (flattenTyFunApp _ lt)
+    | 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
-    for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
+    | 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.
 
 
 
@@ -315,13 +408,6 @@ Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ
   apply weakCK.
   apply IHκ.
   Defined.
-(*
-Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
-  match κ as K return list (HaskCoercionKind (app K Γ)) with
-  | nil => hck
-  | _   => map weakCK' hck
-  end.
-*)
 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
   map weakCK' hck.
 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
@@ -330,17 +416,13 @@ Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv T
   forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
   := fun TV ite tv => (f TV (weakITE ite) tv).
 
-(* I keep mixing up left/right folds *)
-(* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *)
-(*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*)
-
 Fixpoint caseType0 {Γ}(lk:list Kind) :
   IList _ (HaskType Γ) lk ->
-  HaskType Γ (fold_right KindTypeFunction ★ lk) ->
+  HaskType Γ (fold_right KindArrow ★ lk) ->
   HaskType Γ ★ :=
   match lk as LK return
     IList _ (HaskType Γ) LK ->
-    HaskType Γ (fold_right KindTypeFunction ★ LK) ->
+    HaskType Γ (fold_right KindArrow ★ LK) ->
     HaskType Γ ★ 
   with
   | nil    => fun _     ht => ht
@@ -353,19 +435,19 @@ Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc))
 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 Record StrongAltCon {tc:TyCon} :=
 { sac_tc          := tc
-; sac_altcon      :  AltCon
+; sac_altcon      :  WeakAltCon
 ; sac_numExTyVars :  nat
 ; sac_numCoerVars :  nat
 ; sac_numExprVars :  nat
 ; sac_ekinds      :  vec Kind sac_numExTyVars
 ; sac_kinds       := app (tyConKind tc) (vec2list sac_ekinds)
-; sac_Γ           := fun Γ => app (vec2list sac_ekinds) Γ
-; sac_coercions   :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
-; sac_types       :  forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
-; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
+; 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_tc     : StrongAltCon >-> TyCon.
-Coercion sac_altcon : StrongAltCon >-> AltCon.
+Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
   
 
 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
@@ -382,16 +464,38 @@ Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
 
 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 
-Fixpoint update_ξ
+Fixpoint update_xi
   `{EQD_VV:EqDecidable VV}{Γ}
    (ξ:VV -> LeveledHaskType Γ ★)
-   (vt:list (VV * LeveledHaskType Γ ★))
+   (lev:HaskLevel Γ)
+   (vt:list (VV * HaskType Γ ★))
    : VV -> LeveledHaskType Γ ★ :=
   match vt with
     | nil => ξ
-    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
+    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
   end.
 
+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.
 
 
 (***************************************************************************************************)
@@ -474,7 +578,7 @@ match t1 with
 | 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 lt  => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => 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
@@ -491,7 +595,9 @@ end.
 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
   compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
 
-(* This is not provable in Coq's logic because the Coq function space
+(* 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).
@@ -546,7 +652,7 @@ Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
 (* ToString instance for PHOAS types *)
 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
     match t with
-    | TVar    _ v          => "tv" +++ v
+    | TVar    _ v          => "tv" +++ toString v
     | TCon    tc           => toString tc
     | TCoerc _ t1 t2   t   => "("+++typeToString' false n t1+++"~"
                                   +++typeToString' false n t2+++")=>"
@@ -563,11 +669,12 @@ Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat)
                      else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
       end
     | TArrow => "(->)"
-    | TAll   k f           => let alpha := "tv"+++n
-                              in "(forall "+++ alpha +++ ":"+++ k +++")"+++
+    | 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 lt    => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
+    | 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