abstract out the kind of environment classifiers (ECKind)

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

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 4715308..122db2a 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).

@@ -96,7 +94,7 @@ Notation " ` x " := (@fixkind _ x) (at level 100).
 
 Ltac matchThings T1 T2 S :=
   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
 
 Ltac matchThings T1 T2 S :=
   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];

-   [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
+   [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].

 
 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
   intros.
 
 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
   intros.

@@ -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 " +++ toString 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 _

@@ -125,7 +124,8 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
     | WTyVarTy  v       => let case_WTyVarTy := tt  in φ v >>= fun v' => _
     | WForAllTy wtv t   => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
     | WTyVarTy  v       => let case_WTyVarTy := tt  in φ v >>= fun v' => _
     | WForAllTy wtv t   => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _

-    | WCodeTy ec tbody  => let case_WCodeTy := tt   in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _
+    | WCodeTy ec tbody  => let case_WCodeTy := tt   in weakTypeToType _ φ tbody
+                                 >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _

     | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt  in
       weakTypeToType _ φ t1 >>= fun t1' =>
       weakTypeToType _ φ t2 >>= fun t2' =>
     | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt  in
       weakTypeToType _ φ t1 >>= fun t1' =>
       weakTypeToType _ φ t2 >>= fun t2' =>

@@ -147,40 +147,49 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
         end
       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
   end ); clear weakTypeToType.
         end
       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
   end ); clear weakTypeToType.

+  apply ConcatenableString.

 
   destruct case_WTyVarTy.
 
   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 "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
+      toString t2'+++" of kind "+++toString 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.

-    apply TyFunApp.
+    apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).

     apply lt'.
     apply X.
 
   destruct case_WTyCon.
     apply lt'.
     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 +202,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 +214,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.

@@ -213,9 +224,6 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply h.
     Defined.
     
     apply h.
     Defined.
     

-
-Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
-

 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 Section StrongAltCon.
   Context (tc : TyCon)(dc:DataCon tc).
 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 Section StrongAltCon.
   Context (tc : TyCon)(dc:DataCon tc).

@@ -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,13 +348,13 @@ 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 *.
   set (eqd_dec tc tc') as eqpf; destruct eqpf;
     [ idtac
   destruct alt.
   set (c:DataCon _) as dc.
   set ((dataConTyCon c):TyCon) as tc' in *.
   set (eqd_dec tc tc') as eqpf; destruct eqpf;
     [ idtac

-      | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
+      | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.

   apply OK.
   eapply mkStrongAltConPlusJunk.
   simpl in *.
   apply OK.
   eapply mkStrongAltConPlusJunk.
   simpl 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 (toString ○ haskTyVarToType) l) "")+++eol+++
+                    "  wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
+    )) ].
+  destruct (eqd_dec τ τ'); [ idtac
+    | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
+                    "  got: " +++toString τ+++eol+++
+                    "  wanted: "+++toString τ'
+    )) ].

   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,18 +448,93 @@ 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
 end.
 
                     mkAvars wtl' lk' φ >>= fun rest =>
                     OK (ICons _ _ t rest)
               end
 end.
 

+Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
+  match vars with
+    | nil => ig
+    | v::vars' =>
+      fun v' =>
+        if eqd_dec v v'
+          then false
+            else update_ig ig vars' v'
+  end.
+
+(* does the specified variable occur free in the expression? *)
+Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
+  match me with
+    | WELit    _        => false
+    | WEVar    cv       => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
+    | WECast   e co     =>                            doesWeakVarOccur wev e
+    | WENote   n e      =>                            doesWeakVarOccur wev e
+    | WETyApp  e t      =>                            doesWeakVarOccur wev e
+    | WECoApp  e co     =>                            doesWeakVarOccur wev e
+    | WEBrak _ ec e _   =>                            doesWeakVarOccur wev e
+    | WEEsc  _ ec e _   =>                            doesWeakVarOccur wev e
+    | WECSP  _ ec e _   =>                            doesWeakVarOccur wev e
+    | WELet    cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
+    | WEApp    e1 e2    => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
+    | WELam    cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+    | WETyLam  cv e     => doesWeakVarOccur wev e
+    | WECoLam  cv e     => doesWeakVarOccur wev e
+    | WECase vscrut escrut tbranches tc avars alts =>
+      doesWeakVarOccur wev escrut ||
+      if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
+        ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
+          match alts with
+            | T_Leaf  None                                         => false
+            | T_Leaf (Some (WeakDEFAULT,_,_,_,e))                      => doesWeakVarOccur wev e
+            | T_Leaf (Some (WeakLitAlt lit,_,_,_,e))                   => doesWeakVarOccur wev e
+            | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e))  => doesWeakVarOccur wev e  (* FIXME!!! *)
+            | T_Branch b1 b2                                       => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
+          end) alts)
+    | WELetRec mlr e =>
+      doesWeakVarOccur wev e ||
+      (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
+      match mlr with
+        | T_Leaf None          => false
+        | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+        | T_Branch b1 b2       => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
+      end) mlr
+  end.
+Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
+  (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool := 
+  match alts with
+    | T_Leaf  None                                             => false
+    | T_Leaf (Some (WeakDEFAULT,_,_,_,e))                      => doesWeakVarOccur wev e
+    | T_Leaf (Some (WeakLitAlt lit,_,_,_,e))                   => doesWeakVarOccur wev e
+    | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e))  => doesWeakVarOccur wev e  (* FIXME!!! *)
+    | T_Branch b1 b2                                           => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
+  end.
+
+Definition checkDistinct :
+  forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
+  intros.
+  set (distinct_decidable lv) as q.
+  destruct q.
+  exact (OK d).
+  exact (Error "checkDistinct failed").
+  Defined.
+
+(* FIXME: check the kind of the type of the weakexprvar to support >0 *)
+Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
+  refine {| glob_kinds := nil |}.
+  apply wev.
+  intros.
+  apply τ.
+  Defined.
+

 Definition weakExprToStrongExpr : forall
     (Γ:TypeEnv)
     (Δ:CoercionEnv Γ)
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
     (ξ:CoreVar -> LeveledHaskType Γ ★)
 Definition weakExprToStrongExpr : forall
     (Γ:TypeEnv)
     (Δ:CoercionEnv Γ)
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
     (ξ:CoreVar -> LeveledHaskType Γ ★)

+    (ig:CoreVar -> bool)

     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ),
     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ),
     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).

@@ -453,67 +545,73 @@ Definition weakExprToStrongExpr : forall
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
     (ξ:CoreVar -> LeveledHaskType Γ ★)
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
     (ξ:CoreVar -> LeveledHaskType Γ ★)

+    (ig:CoreVar -> bool)

     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ)
     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ)
     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=

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

     match we with
 
     match we with
 

-    | WEVar   v                         => castExpr ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
+    | WEVar   v                         => if ig v
+                                              then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
+                                              else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)

 
 

-    | WELit   lit                       => castExpr ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
+    | WELit   lit                       => castExpr we ("WELit "+++toString 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' =>
-                                                 let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
-                                                   weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
-                                                     castExpr "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
+                                               weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
+                                                 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
+                                                 let ig' := update_ig ig ((ev:CoreVar)::nil) in
+                                                   weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun 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' =>
-                                               weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
-                                                 castExpr "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
+                                             weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
+                                               weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun 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"
                                            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')
+                                             | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
+                                               >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')

                                            end
 
                                            end
 

-    | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
+    | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"

 
 

-    | WELet   v ve  ebody               => weakTypeToType'' φ v ★  >>= fun tv =>
-                                             weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
-                                               weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
+    | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
+
+    | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>
+                                             weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
+                                               weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
+                                                    (update_ig ig ((v:CoreVar)::nil)) τ lev ebody

                                                >>= fun ebody' =>
                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 
     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
                                                >>= fun ebody' =>
                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 
     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>

-                                             weakTypeToType'' φ t2 ★ >>= fun t2' =>
-                                               weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
-                                                 weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
+                                             weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
+                                               weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
+                                                 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>

                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 
     | WETyLam tv e                      => let φ' := upφ tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>
                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 
     | WETyLam tv e                      => let φ' := upφ tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>

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

                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
                                                  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'')
+                                                   (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) 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'' =>
-                                                   weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
-                                                     weakTypeToType'' φ t (wtv:Kind) >>= fun t' =>
-                                                       castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
-                                             | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
+                                                 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
+                                                   weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
+                                                     weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
+                                                       castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
+                                             | _                 => Error ("weakTypeToType: WETyApp body with type "+++toString te)

                                            end
 
     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
                                            end
 
     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>

@@ -522,84 +620,88 @@ 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'' =>
-                                                       weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
-                                                         castExpr "WECoApp" _ e' >>= fun e'' =>
+                                                   weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
+                                                     weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
+                                                       weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev 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

-                                             | _                 => Error ("weakTypeToType: WECoApp body with type "+++te)
+                                             | _                 => Error ("weakTypeToType: WECoApp body with type "+++toString te)

                                            end
 
     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
                                            weakTypeOfWeakExpr e >>= fun te =>
                                            end
 
     | 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' =>
-                                                   weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
-                                                     castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
-
-    | WECast  e co                      => let (κ,t1,t2,_) := co in
-                                             weakTypeToType'' φ t1 ★ >>= fun t1' =>
-                                               weakTypeToType'' φ t2 ★ >>= fun t2' =>
-                                                   weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
-                                                     castExpr "WECast" _ 
+                                             weakTypeToTypeOfKind φ te ★ >>= fun te' =>
+                                               weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
+                                                 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
+                                                   weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
+                                                     castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
+
+    | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
+                                             weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
+                                               weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
+                                                   weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
+                                                     castExpr we "WECast" _ 

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

-      let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
-      in let binds := 
+      let ξ' := update_ξ ξ lev _ in
+      let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
+      let binds := 

         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
         match t with
           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
         match t with
           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)

-          | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
+          | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)

           | T_Branch b1 b2        =>
             binds b1 >>= fun b1' =>
               binds b2 >>= fun b2' =>
                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
         end) rb
       in binds >>= fun binds' =>
           | T_Branch b1 b2        =>
             binds b1 >>= fun b1' =>
               binds b2 >>= fun b2' =>
                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
         end) rb
       in binds >>= fun binds' =>

-           weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>       
-             OK (ELetRec Γ Δ ξ lev τ _ binds' e')
-
-    | WECase vscrut ve tbranches tc avars alts =>
-        weakTypeToType'' φ (vscrut:WeakType) ★  >>= fun tv =>
-          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
-                      ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
-                        Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) := 
+         checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
+           weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>       
+             OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
+
+    | WECase vscrut escrut tbranches tc avars alts =>
+        weakTypeOfWeakExpr escrut >>= fun tscrut =>
+          weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
+            if doesWeakVarOccurAlts vscrut alts
+            then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
+            else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+                weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
+                  (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+                      ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
+                        Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@  lev))}}) := 

                     match t with
                       | T_Leaf None           => OK []
                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => 
                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
                           >>= fun exprvars' =>
                     match t with
                       | T_Leaf None           => OK []
                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => 
                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
                           >>= fun exprvars' =>

-                            let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
-                              weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
+                            (let case_pf := tt in _) >>= fun pf =>
+                            let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
+                              weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)

                               (sacpj_ψ sac _ _ avars' ψ)
                               (sacpj_ψ sac _ _ avars' ψ)

-                              (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
+                              (scbwv_ξ scb ξ lev)
+                              (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
+                              (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>

                                 let case_case := tt in OK [ _ ]
                       | T_Branch b1 b2        =>
                         mkTree b1 >>= fun b1' =>
                           mkTree b2 >>= fun b2' =>
                             OK (b1',,b2')
                     end) alts >>= fun tree =>
                                 let case_case := tt in OK [ _ ]
                       | T_Branch b1 b2        =>
                         mkTree b1 >>= fun b1' =>
                           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)
-                        >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
-
-
-
-    end)).

 
 

+                    weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
+                      castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
+    end)); try clear binds; try apply ConcatenableString.
+  

     destruct case_some.
     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.

@@ -608,9 +710,23 @@ Definition weakExprToStrongExpr : forall
       destruct e''; try apply (Error error_message).
       apply OK.
       apply ELR_leaf.
       destruct e''; try apply (Error error_message).
       apply OK.
       apply ELR_leaf.

+      unfold ξ'.
+      simpl.
+      induction (leaves (varsTypes rb φ)).
+        simpl; auto.
+        destruct (ξ c).
+        simpl.

       apply e1.
       apply e1.

+      rewrite mapleaves.
+      apply rb_distinct.
+
+    destruct case_pf.
+      set (distinct_decidable (vec2list exprvars')) as dec.
+      destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].
+      apply OK; auto.

 
     destruct case_case.
 
     destruct case_case.

+      exists sac.

       exists scb.
       apply ebranch'.
 
       exists scb.
       apply ebranch'.