X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=122db2afc13408cffed68494a968c0a7c7bd4abc;hp=e70e17dd0d33d855f5202a5d3510298a73cdd9a7;hb=b4857a6f575dffd5c9c9d5decbc21ff63a338270;hpb=8c26722a1ee110077968a8a166eb7130266b2035

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index e70e17d..122db2a 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -10,25 +10,25 @@ Require Import Coq.Strings.String.
 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 HaskCoreTypes.
 Require Import HaskCoreVars.
 
 Open Scope string_scope.
-Definition TyVarResolver Γ   := forall wt:WeakTypeVar, HaskTyVar Γ wt.
-Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, HaskCoVar Γ Δ.
+Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
+Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
 
 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
   unfold TyVarResolver.
   refine (fun tv' =>
     if eqd_dec tv tv' 
-    then let fresh := @FreshHaskTyVar Γ tv in _
-    else fun TV ite => φ tv' TV (weakITE ite)).
+    then let fresh := @FreshHaskTyVar Γ tv in OK _
+    else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
   rewrite <- _H; apply fresh.
   Defined.
 
@@ -70,8 +70,7 @@ Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ
 Record StrongAltConPlusJunk {tc:TyCon} :=
 { sacpj_sac : @StrongAltCon tc
 ; sacpj_φ   : forall Γ          (φ:TyVarResolver Γ  ),  (TyVarResolver (sac_Γ sacpj_sac Γ))
-; sacpj_ψ   : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
-                (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ)))
+; sacpj_ψ   : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
 }.
 Implicit Arguments StrongAltConPlusJunk [ ].
 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon. 
@@ -95,7 +94,7 @@ Notation " ` x " := (@fixkind _ x) (at level 100).
 
 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.
@@ -116,15 +115,17 @@ Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
 
 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 _
     | WClassP   c lt    => let case_WClassP := tt   in Error "weakTypeToType: WClassP not implemented"
     | WIParam _ ty      => let case_WIParam := tt   in Error "weakTypeToType: WIParam not implemented"
     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
-    | WTyVarTy  v       => let case_WTyVarTy := tt  in _
+    | 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' => _
+    | 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' =>
@@ -146,52 +147,62 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
         end
       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
   end ); clear weakTypeToType.
+  apply ConcatenableString.
 
   destruct case_WTyVarTy.
+    apply (addErrorMessage "case_WTyVarTy").
     apply OK.
-    exact (haskTypeOfSomeKind (fun TV env => TVar (φ v TV env))).
+    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'].
+    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))));
-      apply (Error "Kind mismatch in WAppTy:: ").
+      apply (Error ("Kind mismatch in WAppTy: "+++err)).
    
   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.
+    apply (addErrorMessage "case_WTyFunApp").
     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 (addErrorMessage "case_WTyCon").
     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.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.
     apply TCode.
-    apply (TVar (φ (@fixkind ★ ec) TV X)).
+    apply (TVar (ec' TV X)).
     subst.
     apply h.
     apply X.
 
   destruct case_WCoFunTy.
+    apply (addErrorMessage "case_WCoFunTy").
     destruct t1' as [ k1' t1' ].
     destruct t2' as [ k2' t2' ].
     destruct t3' as [ k3' t3' ].
@@ -203,6 +214,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
 
   destruct case_WForAllTy.
+    apply (addErrorMessage "case_WForAllTy").
     destruct t1.
     matchThings ★  κ "Kind mismatch in WForAllTy: ".
     subst.
@@ -212,24 +224,30 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply h.
     Defined.
     
-
-
 (* 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).
-(*
-Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ).
+
+Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
+ -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
   intro avars.
   intro ct.
-  set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
+  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 (@weakTypeToType _ φ' ct) as t.
-  set (@weakT'' _ Γ t) as t'.
-  set (@lamer _ _ _ t') as t''.
+  destruct t as [|t]; try apply (Error error_message).
+  destruct t as [tk t].
+  matchThings tk ★ "weakTypeToType'".
+  subst.
+  apply OK.
+  set (@weakT'' _ Γ _ t) as t'.
+  set (@lamer _ _ _ _ t') as t''.
   fold (tyConKinds tc) in t''.
   fold (dataConExKinds dc) in t''.
-  apply (q (tyConKinds tc)).
+  apply q.
+  clear q.
   unfold tyConKinds.
   unfold dataConExKinds.
   rewrite <- vec2list_map_list2vec.
@@ -241,10 +259,9 @@ Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType
 
 Definition mkStrongAltCon : @StrongAltCon tc.
   refine
-   {| sac_altcon      := DataAlt dc
+   {| sac_altcon      := WeakDataAlt dc
     ; sac_numCoerVars := length (dataConCoerKinds dc)
     ; sac_numExprVars := length (dataConFieldTypes dc)
-    ; sac_akinds      := tyConKinds tc
     ; sac_ekinds      := dataConExKinds dc
     ; sac_coercions   := fun Γ avars => let case_sac_coercions := tt in _
     ; sac_types       := fun Γ avars => let case_sac_types := tt in _
@@ -254,25 +271,48 @@ Definition mkStrongAltCon : @StrongAltCon tc.
     refine (vec_map _ (list2vec (dataConCoerKinds dc))).
     intro.
     destruct X.
-    apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)).
+    unfold tyConKind in avars.
+    set (@weakTypeToType' Γ) as q.
+    unfold tyConKinds in q.
+    rewrite <- vec2list_map_list2vec in q.
+    rewrite vec2list_list2vec in q.
+    apply (
+      match
+        q avars w >>= fun t1 =>
+        q avars w0 >>= fun t2 =>
+          OK (mkHaskCoercionKind t1 t2)
+      with
+        | Error s => Prelude_error s
+        | OK y => y
+      end).
 
   destruct case_sac_types.
     refine (vec_map _ (list2vec (dataConFieldTypes dc))).
     intro X.
-    apply (weakTypeToType' avars).
-    apply X.
+    unfold tyConKind in avars.
+    set (@weakTypeToType' Γ) as q.
+    unfold tyConKinds in q.
+    rewrite <- vec2list_map_list2vec in q.
+    rewrite vec2list_list2vec in q.
+    set (q avars X) as y.
+    apply (match y with 
+             | Error s =>Prelude_error s
+             | OK y' => y'
+           end).
     Defined.
- 
+
+
 Lemma weakCV' : forall {Γ}{Δ} Γ',
    HaskCoVar Γ Δ
    -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
   intros.
   unfold HaskCoVar in *.
   intros; apply (X TV CV).
-  apply vec_chop' in env; auto.
+  apply ilist_chop' in env; auto.
   unfold InstantiatedCoercionEnv in *.
   unfold weakCK'' in cenv.
   destruct Γ'.
+  rewrite <- map_preserves_length in cenv.
   apply cenv.
   rewrite <- map_preserves_length in cenv.
   apply cenv.
@@ -281,8 +321,9 @@ Lemma weakCV' : forall {Γ}{Δ} Γ',
 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
     refine 
      {| sacpj_sac     := mkStrongAltCon
-      ; sacpj_φ       := fun Γ φ => (fun htv => weakV' (φ htv))
-      ; sacpj_ψ       := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
+      ; sacpj_φ       := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
+      ; sacpj_ψ       :=
+      fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
       |}.
     intro.
     unfold sac_Γ.
@@ -295,162 +336,399 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
     apply vec_chop' in cenv.
     apply cenv.
     Defined.
-*)
+
+  Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
+    intros.
+    induction Δ.
+    reflexivity.
+    simpl.
+    rewrite IHΔ.
+    reflexivity.
+    Qed.
+  
 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
-      | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++dc)) ]; 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 dc.
 
-  apply OK; refine {| sacpj_sac := {| sac_akinds  := tyConKinds tc
-                    ; sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
-                    ; sac_altcon := LitAlt h
+  apply OK; refine {| sacpj_sac := {| 
+                     sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
+                    ; sac_altcon := WeakLitAlt h
                     |} |}.
             intro; intro φ; apply φ.
-            intro; intro; intro; intro ψ; apply ψ.
-  apply OK; refine {| sacpj_sac := {| sac_akinds  := tyConKinds tc
-                    ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
-                      ; sac_altcon := DEFAULT |} |}.
+            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 := WeakDEFAULT |} |}.
             intro; intro φ; apply φ.
-            intro; intro; intro; intro ψ; apply ψ.
+            intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
+            rewrite weakCK'_nil_inert. apply ψ.
 Defined.
-Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ ★) :=
-  match mlr with
-  | T_Leaf None                         => []
-  | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)]
-  | T_Branch b1 b2                      => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ))
-  end.
-*)
-
 
 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
   fun wev => match wev with weakExprVar _ t => t end.
   Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
 
-(*Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.*)
+Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
 
-Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
-  WeakCoerVar -> HaskCoVar Γ (κ::Δ).
+Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
+  WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
   intros.
+  refine (ψ X >>= _).
   unfold HaskCoVar.
   intros.
-  apply (ψ X TV CV env).
+  apply OK.
+  intros.
   inversion cenv; auto.
   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 _ WeakExprVarEqDecidable Γ Δ ξ τ)
-  : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ').
+Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
+  : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
+  apply (addErrorMessage ("castExpr " +++ err_msg)).
   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.
   Defined.
 
-Definition weakTypeToType' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
+Definition coVarKind (wcv:WeakCoerVar) : Kind :=
+  match wcv with weakCoerVar _ κ _ _ => κ end.
+  Coercion coVarKind : WeakCoerVar >-> Kind.
+
+Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
   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.
   Defined.
 
+Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) := 
+  match t with
+    | T_Leaf None            => []
+    | T_Leaf (Some (wev,e))  => match weakTypeToTypeOfKind φ wev ★ with
+                                  | OK    t' => [((wev:CoreVar),t')]
+                                  | _        => []
+                                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
+             | nil => OK INil
+             | _   => Error "length mismatch in mkAvars"
+           end
+  | k::lk' => match wtl with
+                | nil => Error "length mismatch in mkAvars"
+                | wt::wtl' =>
+                  weakTypeToTypeOfKind φ wt k >>= fun t =>
+                    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 Γ Δ)
-    (ξ:WeakExprVar -> LeveledHaskType Γ ★)
+    (ξ:CoreVar -> LeveledHaskType Γ ★)
+    (ig:CoreVar -> bool)
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ),
-    WeakExpr -> ???(Expr Γ Δ ξ (τ @@ lev) ).
+    WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
   refine ((
     fix weakExprToStrongExpr 
     (Γ:TypeEnv)
     (Δ:CoercionEnv Γ)
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
-    (ξ:WeakExprVar -> LeveledHaskType Γ ★)
+    (ξ:CoreVar -> LeveledHaskType Γ ★)
+    (ig:CoreVar -> bool)
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ)
-    (we:WeakExpr) : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
+    (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
+    addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
     match we with
 
-    | WEVar   v                         => castExpr "WEVar" (τ @@ 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" (τ @@ lev) (ELit Γ Δ ξ lit lev)
+    | WELit   lit                       => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
 
-    | WELam   ev e                      => weakTypeToType' φ ev ★ >>= fun tv =>
-                                             weakTypeOfWeakExpr e >>= fun t =>
-                                               weakTypeToType' φ t ★ >>= fun τ' =>
-                                                 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((ev,tv@@lev)::nil)) τ' _ e >>= fun e' =>
-                                                   castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
+    | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
+                                             weakTypeOfWeakExpr ebody >>= fun tbody =>
+                                               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                => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
-                                             castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
+    | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
+                                             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                => weakTypeToType' φ tbody ★ >>= fun tbody' =>
+    | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
+                                           weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
                                            match lev with
                                              | nil       => Error "ill-leveled escapification"
-                                             | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e
-                                               >>= fun e' =>
-                                                              castExpr "WEEsc" (τ@@lev) (EEsc _ _ _ (φ (`ec)) _ lev e')
+                                             | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
+                                               >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
                                            end
-    | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 
-    | WELet   v ve  ebody               => weakTypeToType' φ v ★  >>= fun tv =>
-                                             weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
-                                               weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((v,tv@@lev)::nil)) τ lev ebody
+    | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
+
+    | 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 ve' 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 =>
-                                               weakTypeToType' φ' te ★ >>= fun τ' =>
-                                                 weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e
-                                                 >>= fun e' =>
-                                                   castExpr "WETyLam1" _ e' >>= fun e'' =>
-                                                     castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
+                                               weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
+                                                 weakExprToStrongExpr _ (weakCE Δ) φ'
+                                                   (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
-                                                 weakTypeToType' φ' te' ★ >>= fun te'' =>
-                                                   weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
-                                                     weakTypeToType' φ t wtv >>= 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
 
-    (* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two
-     * to get them back working again *)
-    | WECoApp e t                       => Error "weakExprToStrongExpr: WECoApp  not yet implemented"
-    | WECoLam cv e                      => Error "weakExprToStrongExpr: WECoLam  not yet implemented"
-    | WECast  e co                      => Error "weakExprToStrongExpr: WECast   not yet implemented"
-    | WELetRec rb   e                   => Error "weakExprToStrongExpr: WELetRec not yet implemented"
-    | WECase  e tbranches tc avars alts => Error "weakExprToStrongExpr: WECase   not yet implemented"
-    end)).
+    | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
+                                           match te with
+                                             | WCoFunTy t1 t2 t3 =>
+                                               weakTypeToType φ t1 >>= fun t1' =>
+                                                 match t1' with
+                                                   haskTypeOfSomeKind κ t1'' =>
+                                                   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
+                                             | _                 => Error ("weakTypeToType: WECoApp body with type "+++toString te)
+                                           end
+
+    | WECoLam cv e                      => let (_,_,t1,t2) := cv in
+                                           weakTypeOfWeakExpr e >>= fun te =>
+                                             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                   =>
+      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 _ _ _ _)
+          | 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' =>
+         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' =>
+                            (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' ψ)
+                              (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 =>
+
+                    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.
+    apply (addErrorMessage "case_some").
+      simpl.
+      destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
+      matchThings h (unlev (ξ' wev)) "LetRec".
+      destruct wev.
+      rewrite matchTypeVars_pf.
+      clear matchTypeVars_pf.
+      set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
+      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.
+      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.
+      exists sac.
+      exists scb.
+      apply ebranch'.
+
     Defined.