reshuffle definitions in an attempt to iron out inter-file dependenceies

[coq-hetmet.git] / src / HaskWeakToStrong.v

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 4715308..2593a5c 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -10,16 +10,14 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.

-Require Import HaskCoreTypes.

 Require Import HaskCoreVars.
 Require Import HaskCoreVars.

-Require Import HaskCoreToWeak.

 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).

@@ -117,6 +115,7 @@ Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
 
 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
   refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
 
 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
   refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=

+  addErrorMessage ("weakTypeToType " +++ t)

   match t with
     | WFunTyCon         => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
     | WTyCon      tc    => let case_WTyCon := tt    in _
   match t with
     | WFunTyCon         => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
     | WTyCon      tc    => let case_WTyCon := tt    in _

@@ -149,24 +148,29 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
   end ); clear weakTypeToType.
 
   destruct case_WTyVarTy.
   end ); clear weakTypeToType.
 
   destruct case_WTyVarTy.

+    apply (addErrorMessage "case_WTyVarTy").

     apply OK.
     exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
 
   destruct case_WAppTy.
     apply OK.
     exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
 
   destruct case_WAppTy.

+    apply (addErrorMessage "case_WAppTy").

     destruct t1' as  [k1' t1'].
     destruct t2' as [k2' t2'].
     destruct t1' as  [k1' t1'].
     destruct t2' as [k2' t2'].

+    set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.

     destruct k1';
       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
     destruct k1';
       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));

-      apply (Error "Kind mismatch in WAppTy:: ").
+      apply (Error ("Kind mismatch in WAppTy: "+++err)).

    
   destruct case_weakTypeListToTypeList.
    
   destruct case_weakTypeListToTypeList.

+    apply (addErrorMessage "case_weakTypeListToTypeList").

     destruct t' as [ k' t' ].
     matchThings k k' "Kind mismatch in weakTypeListToTypeList".
     subst.
     apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
 
   destruct case_WTyFunApp.
     destruct t' as [ k' t' ].
     matchThings k k' "Kind mismatch in weakTypeListToTypeList".
     subst.
     apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
 
   destruct case_WTyFunApp.

+    apply (addErrorMessage "case_WTyFunApp").

     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.
     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.

@@ -175,12 +179,14 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply X.
 
   destruct case_WTyCon.
     apply X.
 
   destruct case_WTyCon.

+    apply (addErrorMessage "case_WTyCon").

     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.
     apply (TCon tc).
 
   destruct case_WCodeTy.    
     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.
     apply (TCon tc).
 
   destruct case_WCodeTy.    

+    apply (addErrorMessage "case_WCodeTy").

     destruct tbody'.
     matchThings κ ★ "Kind mismatch in WCodeTy: ".
     apply OK.
     destruct tbody'.
     matchThings κ ★ "Kind mismatch in WCodeTy: ".
     apply OK.

@@ -193,6 +199,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply X.
 
   destruct case_WCoFunTy.
     apply X.
 
   destruct case_WCoFunTy.

+    apply (addErrorMessage "case_WCoFunTy").

     destruct t1' as [ k1' t1' ].
     destruct t2' as [ k2' t2' ].
     destruct t3' as [ k3' t3' ].
     destruct t1' as [ k1' t1' ].
     destruct t2' as [ k2' t2' ].
     destruct t3' as [ k3' t3' ].

@@ -204,6 +211,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
 
   destruct case_WForAllTy.
     apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
 
   destruct case_WForAllTy.

+    apply (addErrorMessage "case_WForAllTy").

     destruct t1.
     matchThings ★  κ "Kind mismatch in WForAllTy: ".
     subst.
     destruct t1.
     matchThings ★  κ "Kind mismatch in WForAllTy: ".
     subst.

@@ -224,6 +232,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds
  -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
   intro avars.
   intro ct.
  -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
   intro avars.
   intro ct.

+  apply (addErrorMessage "weakTypeToType'").

   set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
   set (@substφ _ _ avars') as q.
   set (upφ' (tyConTyVars tc)  (mkPhi (dataConExTyVars dc))) as φ'.
   set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
   set (@substφ _ _ avars') as q.
   set (upφ' (tyConTyVars tc)  (mkPhi (dataConExTyVars dc))) as φ'.

@@ -250,7 +259,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds
 
 Definition mkStrongAltCon : @StrongAltCon tc.
   refine
 
 Definition mkStrongAltCon : @StrongAltCon tc.
   refine

-   {| sac_altcon      := DataAlt dc
+   {| sac_altcon      := WeakDataAlt dc

     ; sac_numCoerVars := length (dataConCoerKinds dc)
     ; sac_numExprVars := length (dataConFieldTypes dc)
     ; sac_ekinds      := dataConExKinds dc
     ; sac_numCoerVars := length (dataConCoerKinds dc)
     ; sac_numExprVars := length (dataConFieldTypes dc)
     ; sac_ekinds      := dataConExKinds dc

@@ -339,7 +348,7 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
   
 End StrongAltCon.
 
   
 End StrongAltCon.
 

-Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
+Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).

   destruct alt.
   set (c:DataCon _) as dc.
   set ((dataConTyCon c):TyCon) as tc' in *.
   destruct alt.
   set (c:DataCon _) as dc.
   set ((dataConTyCon c):TyCon) as tc' in *.

@@ -353,14 +362,14 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConP
 
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil

-                    ; sac_altcon := LitAlt h
+                    ; sac_altcon := WeakLitAlt h

                     |} |}.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
                     |} |}.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil

-                      ; sac_altcon := DEFAULT |} |}.
+                      ; sac_altcon := WeakDEFAULT |} |}.

             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.

@@ -384,13 +393,22 @@ Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar 
   Defined.
 
 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
   Defined.
 
 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)

-Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
+Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)

   : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
   : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').

+  apply (addErrorMessage ("castExpr " +++ err_msg)).

   intros.
   destruct τ  as [τ  l].
   destruct τ' as [τ' l'].
   intros.
   destruct τ  as [τ  l].
   destruct τ' as [τ' l'].

-  destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ].
-  destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ].
+  destruct (eqd_dec l l'); [ idtac
+    | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
+                    "  got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
+                    "  wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
+    )) ].
+  destruct (eqd_dec τ τ'); [ idtac
+    | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
+                    "  got: " +++τ+++eol+++
+                    "  wanted: "+++τ'
+    )) ].

   subst.
   apply OK.
   apply e.
   subst.
   apply OK.
   apply e.

@@ -400,12 +418,12 @@ Definition coVarKind (wcv:WeakCoerVar) : Kind :=
   match wcv with weakCoerVar _ κ _ _ => κ end.
   Coercion coVarKind : WeakCoerVar >-> Kind.
 
   match wcv with weakCoerVar _ κ _ _ => κ end.
   Coercion coVarKind : WeakCoerVar >-> Kind.
 

-Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
+Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).

   intros.
   set (weakTypeToType φ t) as wt.
   destruct wt; try apply (Error error_message).
   destruct h.
   intros.
   set (weakTypeToType φ t) as wt.
   destruct wt; try apply (Error error_message).
   destruct h.

-  matchThings κ κ0 "Kind mismatch in weakTypeToType'': ".
+  matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").

   subst.
   apply OK.
   apply h.
   subst.
   apply OK.
   apply h.

@@ -414,14 +432,13 @@ Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakTyp
 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) := 
   match t with
     | T_Leaf None            => []
 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) := 
   match t with
     | T_Leaf None            => []

-    | T_Leaf (Some (wev,e))  => match weakTypeToType'' φ wev ★  with
-                                  | Error _ =>  []
+    | T_Leaf (Some (wev,e))  => match weakTypeToTypeOfKind φ wev ★ with

                                   | OK    t' => [((wev:CoreVar),t')]
                                   | OK    t' => [((wev:CoreVar),t')]

+                                  | _        => []

                                 end
     | T_Branch b1 b2         => (varsTypes b1 φ),,(varsTypes b2 φ)
   end.
 
                                 end
     | T_Branch b1 b2         => (varsTypes b1 φ),,(varsTypes b2 φ)
   end.
 

-

 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
   | nil => match wtl with
 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
   | nil => match wtl with

@@ -431,7 +448,7 @@ match lk as LK return ???(IList Kind (HaskType Γ) LK) with
   | k::lk' => match wtl with
                 | nil => Error "length mismatch in mkAvars"
                 | wt::wtl' =>
   | k::lk' => match wtl with
                 | nil => Error "length mismatch in mkAvars"
                 | wt::wtl' =>

-                  weakTypeToType'' φ wt k >>= fun t =>
+                  weakTypeToTypeOfKind φ wt k >>= fun t =>

                     mkAvars wtl' lk' φ >>= fun rest =>
                     OK (ICons _ _ t rest)
               end
                     mkAvars wtl' lk' φ >>= fun rest =>
                     OK (ICons _ _ t rest)
               end

@@ -456,63 +473,66 @@ Definition weakExprToStrongExpr : forall
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ)
     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ)
     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=

+    addErrorMessage ("in weakExprToStrongExpr " +++ we)

     match we with
 
     match we with
 

-    | WEVar   v                         => castExpr ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
+    | WEVar   v                         => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)

 
 

-    | WELit   lit                       => castExpr ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
+    | WELit   lit                       => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)

 
 

-    | WELam   ev ebody                  => weakTypeToType'' φ ev ★ >>= fun tv =>
+    | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>

                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
                                              weakTypeOfWeakExpr ebody >>= fun tbody =>

-                                               weakTypeToType'' φ tbody ★ >>= fun tbody' =>
+                                               weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>

                                                  let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
                                                    weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
                                                  let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
                                                    weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>

-                                                     castExpr "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
+                                                     castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')

 
     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
 
     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>

-                                             weakTypeToType'' φ tbody ★ >>= fun tbody' =>
+                                             weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>

                                                weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
                                                weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>

-                                                 castExpr "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
+                                                 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')

 
     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
 
     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>

-                                           weakTypeToType'' φ tbody ★ >>= fun tbody' =>
+                                           weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>

                                            match lev with
                                              | nil       => Error "ill-leveled escapification"
                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e
                                            match lev with
                                              | nil       => Error "ill-leveled escapification"
                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e

-                                               >>= fun e' => castExpr "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
+                                               >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')

                                            end
 
                                            end
 

+    | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
+

     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 
     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 

-    | WELet   v ve  ebody               => weakTypeToType'' φ v ★  >>= fun tv =>
+    | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>

                                              weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
                                                >>= fun ebody' =>
                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 
     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
                                              weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
                                                >>= fun ebody' =>
                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 
     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>

-                                             weakTypeToType'' φ t2 ★ >>= fun t2' =>
+                                             weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>

                                                weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
                                                  weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 
     | WETyLam tv e                      => let φ' := upφ tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>
                                                weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
                                                  weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 
     | WETyLam tv e                      => let φ' := upφ tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>

-                                               weakTypeToType'' φ' te ★ >>= fun τ' =>
+                                               weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>

                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
                                                     (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
                                                  >>= fun e' =>
                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
                                                     (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
                                                  >>= fun e' =>

-                                                   castExpr "WETyLam1" _ e' >>= fun e'' =>
-                                                     castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
+                                                   castExpr we "WETyLam1" _ e' >>= fun e'' =>
+                                                     castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')

 
     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
                                            match te with
                                              | WForAllTy wtv te' =>
                                                let φ' := upφ wtv φ in
 
     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
                                            match te with
                                              | WForAllTy wtv te' =>
                                                let φ' := upφ wtv φ in

-                                                 weakTypeToType'' φ' te' ★ >>= fun te'' =>
+                                                 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>

                                                    weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
                                                    weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>

-                                                     weakTypeToType'' φ t (wtv:Kind) >>= fun t' =>
-                                                       castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
+                                                     weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
+                                                       castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')

                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
                                            end
 
                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
                                            end
 

@@ -522,10 +542,10 @@ Definition weakExprToStrongExpr : forall
                                                weakTypeToType φ t1 >>= fun t1' =>
                                                  match t1' with
                                                    haskTypeOfSomeKind κ t1'' =>
                                                weakTypeToType φ t1 >>= fun t1' =>
                                                  match t1' with
                                                    haskTypeOfSomeKind κ t1'' =>

-                                                   weakTypeToType'' φ t2 κ >>= fun t2'' =>
-                                                     weakTypeToType'' φ t3 ★ >>= fun t3'' =>
+                                                   weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
+                                                     weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>

                                                        weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
                                                        weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>

-                                                         castExpr "WECoApp" _ e' >>= fun e'' =>
+                                                         castExpr we "WECoApp" _ e' >>= fun e'' =>

                                                            OK (ECoApp Γ Δ κ t1'' t2''
                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
                                                  end
                                                            OK (ECoApp Γ Δ κ t1'' t2''
                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
                                                  end

@@ -534,17 +554,17 @@ Definition weakExprToStrongExpr : forall
 
     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
                                            weakTypeOfWeakExpr e >>= fun te =>
 
     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
                                            weakTypeOfWeakExpr e >>= fun te =>

-                                             weakTypeToType'' φ te ★ >>= fun te' =>
-                                               weakTypeToType'' φ t1 cv >>= fun t1' =>
-                                                 weakTypeToType'' φ t2 cv >>= fun t2' =>
+                                             weakTypeToTypeOfKind φ te ★ >>= fun te' =>
+                                               weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
+                                                 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>

                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>

-                                                     castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
+                                                     castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')

 
 

-    | WECast  e co                      => let (κ,t1,t2,_) := co in
-                                             weakTypeToType'' φ t1 ★ >>= fun t1' =>
-                                               weakTypeToType'' φ t2 ★ >>= fun t2' =>
+    | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
+                                             weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
+                                               weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>

                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>

-                                                     castExpr "WECast" _ 
+                                                     castExpr we "WECast" _ 

                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 
     | WELetRec rb   e                   =>
                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 
     | WELetRec rb   e                   =>

@@ -565,12 +585,12 @@ Definition weakExprToStrongExpr : forall
              OK (ELetRec Γ Δ ξ lev τ _ binds' e')
 
     | WECase vscrut ve tbranches tc avars alts =>
              OK (ELetRec Γ Δ ξ lev τ _ binds' e')
 
     | WECase vscrut ve tbranches tc avars alts =>

-        weakTypeToType'' φ (vscrut:WeakType) ★  >>= fun tv =>
+        weakTypeToTypeOfKind φ (vscrut:WeakType) ★  >>= fun tv =>

           weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
             let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
               mkAvars avars (tyConKind tc) φ >>= fun avars' =>
           weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
             let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
               mkAvars avars (tyConKind tc) φ >>= fun avars' =>

-                weakTypeToType'' φ tbranches ★  >>= fun tbranches' =>
-                  (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+                weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
+                  (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree

                       ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
                         Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) := 
                     match t with
                       ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
                         Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) := 
                     match t with

@@ -589,8 +609,8 @@ Definition weakExprToStrongExpr : forall
                           mkTree b2 >>= fun b2' =>
                             OK (b1',,b2')
                     end) alts >>= fun tree =>
                           mkTree b2 >>= fun b2' =>
                             OK (b1',,b2')
                     end) alts >>= fun tree =>

-                  castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
-                      castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
+                  castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
+                      castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)

                         >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
 
 
                         >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
 
 

@@ -598,8 +618,9 @@ Definition weakExprToStrongExpr : forall
     end)).
 
     destruct case_some.
     end)).
 
     destruct case_some.

+    apply (addErrorMessage "case_some").

       simpl.
       simpl.

-      destruct (weakTypeToType'' φ wev ★); try apply (Error error_message).
+      destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).

       matchThings h (unlev (ξ' wev)) "LetRec".
       destruct wev.
       rewrite matchTypeVars_pf.
       matchThings h (unlev (ξ' wev)) "LetRec".
       destruct wev.
       rewrite matchTypeVars_pf.