src/HaskWeakToStrong.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeakToStrong: convert HaskWeak to HaskStrong                                                                              *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import NaturalDeduction.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11 Require Import Coq.Init.Specif.
  12 Require Import HaskKinds.
  13 Require Import HaskCoreLiterals.
  14 Require Import HaskWeakTypes.
  15 Require Import HaskWeakVars.
  16 Require Import HaskWeak.
  17 Require Import HaskStrongTypes.
  18 Require Import HaskStrong.
  19 Require Import HaskCoreTypes.
  20
  21 Definition upφ {Γ}(tv:WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) : (WeakTypeVar -> HaskTyVar ((tv:Kind)::Γ)) :=
  22   fun tv' =>
  23     if eqd_dec tv tv'
  24     then FreshHaskTyVar (tv:Kind)
  25     else fun TV ite => φ tv' TV (weakITE ite).
  26
  27
  28
  29 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ)
  30   : (WeakTypeVar -> HaskTyVar (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
  31   induction tvs.
  32   apply φ.
  33   simpl.
  34   apply upφ.
  35   apply IHtvs.
  36   Defined.
  37
  38 Open Scope string_scope.
  39
  40 Fixpoint weakTypeToType {Γ:TypeEnv}(φ:WeakTypeVar -> HaskTyVar Γ)(t:WeakType) : HaskType Γ :=
  41     match t with
  42       | WTyVarTy  v       => fun TV env => @TVar TV (φ v TV env)
  43       | WCoFunTy t1 t2 t3 => (weakTypeToType φ t1) ∼∼ (weakTypeToType φ t2) ⇒ (weakTypeToType φ t3)
  44       | WFunTyCon         => fun TV env => TArrow
  45       | WTyCon      tc    => fun TV env => TCon tc
  46       | WTyFunApp   tc lt => fun TV env => fold_left TApp (map (fun t => weakTypeToType φ t TV env) lt) (TCon tc) (* FIXME *)
  47       | WClassP   c lt    => fun TV env => fold_left TApp (map (fun t=> weakTypeToType φ t TV env) lt) (TCon (classTyCon c))
  48       | WIParam _ ty      => weakTypeToType φ ty
  49       | WForAllTy wtv t   => (fun TV env => TAll (wtv:Kind) (fun tv => weakTypeToType (@upφ Γ wtv φ) t TV (tv:::env)))
  50       | WAppTy  t1 t2     => fun TV env => TApp (weakTypeToType φ t1 TV env) (weakTypeToType φ t2 TV env)
  51       | WCodeTy ec tbody  => fun TV env => TCode (TVar (φ ec TV env)) (weakTypeToType φ tbody TV env)
  52     end.
  53
  54
  55 Definition substPhi0 {Γ:TypeEnv}(κ:Kind)(θ:HaskType Γ) : HaskType (κ::Γ) -> HaskType Γ.
  56   intro ht.
  57   refine (substT _ θ).
  58   clear θ.
  59   unfold HaskType in ht.
  60   intros.
  61   apply ht.
  62   apply vec_cons; [ idtac | apply env ].
  63   apply X.
  64   Defined.
  65
  66 Definition substPhi {Γ:TypeEnv}(κ:list Kind)(θ:vec (HaskType Γ) (length κ)) : HaskType (app κ Γ) -> HaskType Γ.
  67   induction κ.
  68   intro q; apply q.
  69   simpl.
  70   intro q.
  71   apply IHκ.
  72   inversion θ; subst; auto.
  73   inversion θ; subst.
  74   apply (substPhi0 _ (weakT' X) q).
  75   Defined.
  76
  77 Definition substφ {Γ}{n}(ltypes:vec (HaskType Γ) n)(Γ':vec _ n)(ht:HaskType (app (vec2list Γ') Γ)) : HaskType Γ.
  78   apply (@substPhi Γ (vec2list Γ')).
  79   rewrite vec2list_len.
  80   apply ltypes.
  81   apply ht.
  82   Defined.
  83
  84 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
  85 Record StrongAltConPlusJunk {tc:TyCon} :=
  86 { sacpj_sac : @StrongAltCon tc
  87 ; sacpj_φ   : forall Γ          (φ:WeakTypeVar -> HaskTyVar Γ  ),  (WeakTypeVar -> HaskTyVar (sac_Γ sacpj_sac Γ))
  88 ; sacpj_ψ   : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
  89                 (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ)))
  90 }.
  91 Implicit Arguments StrongAltConPlusJunk [ ].
  92 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
  93
  94 (* yes, I know, this is really clumsy *)
  95 Variable emptyφ : WeakTypeVar -> HaskTyVar nil.
  96   Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
  97
  98 Definition mkPhi (lv:list WeakTypeVar)
  99   : (WeakTypeVar -> HaskTyVar (map (fun x:WeakTypeVar => x:Kind) lv)).
 100   set (upφ'(Γ:=nil) lv emptyφ) as φ'.
 101   rewrite <- app_nil_end in φ'.
 102   apply φ'.
 103   Defined.
 104
 105 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
 106 Definition tyConKinds     tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
 107
 108 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 109 Section StrongAltCon.
 110   Context (tc : TyCon)(dc:DataCon tc).
 111
 112 Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ).
 113   intro avars.
 114   intro ct.
 115   set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
 116   set (@substφ _ _ avars') as q.
 117   set (upφ' (tyConTyVars tc)  (mkPhi (dataConExTyVars dc))) as φ'.
 118   set (@weakTypeToType _ φ' ct) as t.
 119   set (@weakT'' _ Γ t) as t'.
 120   set (@lamer _ _ _ t') as t''.
 121   fold (tyConKinds tc) in t''.
 122   fold (dataConExKinds dc) in t''.
 123   apply (q (tyConKinds tc)).
 124   unfold tyConKinds.
 125   unfold dataConExKinds.
 126   rewrite <- vec2list_map_list2vec.
 127   rewrite <- vec2list_map_list2vec.
 128   rewrite vec2list_list2vec.
 129   rewrite vec2list_list2vec.
 130   apply t''.
 131   Defined.
 132
 133 Definition mkStrongAltCon : @StrongAltCon tc.
 134   refine
 135    {| sac_altcon      := DataAlt dc
 136     ; sac_numCoerVars := length (dataConCoerKinds dc)
 137     ; sac_numExprVars := length (dataConFieldTypes dc)
 138     ; sac_akinds      := tyConKinds tc
 139     ; sac_ekinds      := dataConExKinds dc
 140     ; sac_coercions   := fun Γ avars => let case_sac_coercions := tt in _
 141     ; sac_types       := fun Γ avars => let case_sac_types := tt in _
 142     |}.
 143
 144   destruct case_sac_coercions.
 145     refine (vec_map _ (list2vec (dataConCoerKinds dc))).
 146     intro.
 147     destruct X.
 148     apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)).
 149
 150   destruct case_sac_types.
 151     refine (vec_map _ (list2vec (dataConFieldTypes dc))).
 152     intro X.
 153     apply (weakTypeToType' avars).
 154     apply X.
 155     Defined.
 156
 157 Lemma weakCV' : forall {Γ}{Δ} Γ',
 158    HaskCoVar Γ Δ
 159    -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
 160   intros.
 161   unfold HaskCoVar in *.
 162   intros; apply (X TV CV).
 163   apply vec_chop' in env; auto.
 164   unfold InstantiatedCoercionEnv in *.
 165   unfold weakCK'' in cenv.
 166   destruct Γ'.
 167   apply cenv.
 168   rewrite <- map_preserves_length in cenv.
 169   apply cenv.
 170   Defined.
 171
 172 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
 173     refine
 174      {| sacpj_sac     := mkStrongAltCon
 175       ; sacpj_φ       := fun Γ φ => (fun htv => weakV' (φ htv))
 176       ; sacpj_ψ       := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
 177       |}.
 178     intro.
 179     unfold sac_Γ.
 180     unfold HaskCoVar in *.
 181     intros.
 182     apply (x TV CV env).
 183     simpl in cenv.
 184     unfold sac_Δ in *.
 185     unfold InstantiatedCoercionEnv in *.
 186     apply vec_chop' in cenv.
 187     apply cenv.
 188     Defined.
 189 End StrongAltCon.
 190
 191 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
 192   destruct alt.
 193   set (c:DataCon _) as dc.
 194   set ((dataConTyCon c):TyCon) as tc' in *.
 195   set (eqd_dec tc tc') as eqpf; destruct eqpf;
 196     [ idtac
 197       | apply (Error ("in a case of tycon "+++tyConToString tc+++", found a branch with datacon "+++dataConToString dc)) ]; subst.
 198   apply OK.
 199   eapply mkStrongAltConPlusJunk.
 200   simpl in *.
 201   apply dc.
 202
 203   apply OK; refine {| sacpj_sac := {| sac_akinds  := tyConKinds tc
 204                     ; sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 205                     ; sac_altcon := LitAlt h
 206                     |} |}.
 207             intro; intro φ; apply φ.
 208             intro; intro; intro; intro ψ; apply ψ.
 209   apply OK; refine {| sacpj_sac := {| sac_akinds  := tyConKinds tc
 210                     ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 211                       ; sac_altcon := DEFAULT |} |}.
 212             intro; intro φ; apply φ.
 213             intro; intro; intro; intro ψ; apply ψ.
 214 Defined.
 215
 216 Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ) :=
 217   match mlr with
 218   | T_Leaf None         => []
 219   | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)]
 220   | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ))
 221   end.
 222
 223 Open Scope string_scope.
 224 Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ   := match lht with t @@ l => t end.
 225
 226 Definition Indexed_Bind T f t (e:@Indexed T f t) : forall Q, (forall t, f t -> ???Q) -> ???Q.
 227 intros.
 228 destruct e; subst.
 229 apply (Error error_message).
 230 apply (X t f0).
 231 Defined.
 232 Notation "a >>>= b" := (@Indexed_Bind _ _ _ a _ b) (at level 20).
 233
 234 Definition DoublyIndexed_Bind T f t (e:@Indexed T (fun z => ???(f z)) t) : forall Q, (forall t, f t -> ???Q) -> ???Q.
 235   intros.
 236   eapply Indexed_Bind.
 237   apply e.
 238   intros.
 239   destruct X0.
 240   apply (Error error_message).
 241   apply (X t0 f0).
 242   Defined.
 243
 244 Notation "a >>>>= b" := (@DoublyIndexed_Bind _ _ _ a _ b) (at level 20).
 245
 246 Ltac matchTypes T1 T2 S :=
 247   destruct (eqd_dec T1 T2) as [matchTypes_pf|];
 248    [ idtac | apply (Error ("type mismatch in "+++S+++": " +++ (weakTypeToString T1) +++ " and " +++ (weakTypeToString T2))) ].
 249 Ltac matchTypeVars T1 T2 S :=
 250   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
 251    [ idtac | apply (Error ("type variable mismatch in"+++S)) ].
 252 Ltac matchLevs L1 L2 S :=
 253   destruct (eqd_dec L1 L2) as [matchLevs_pf|];
 254    [ idtac | apply (Error ("level mismatch in "+++S)) ].
 255
 256
 257 Definition cure {Γ}(ξ:WeakExprVar -> WeakType * list WeakTypeVar)(φ:WeakTypeVar->HaskTyVar Γ)
 258   : WeakExprVar->LeveledHaskType Γ :=
 259   fun wtv => weakTypeToType φ (fst (ξ wtv)) @@ map φ (snd (ξ wtv)).
 260
 261 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
 262   fun wev => match wev with weakExprVar _ t => t end.
 263   Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
 264
 265 Fixpoint upξ (ξ:WeakExprVar -> WeakType * list WeakTypeVar)
 266  (evs:list WeakExprVar)
 267  (lev:list WeakTypeVar) :
 268   (WeakExprVar -> WeakType * list WeakTypeVar) :=
 269   fun wev =>
 270   match evs with
 271     | nil  => ξ wev
 272     | a::b => if eqd_dec wev a then ((wev:WeakType),lev) else upξ ξ b lev wev
 273   end.
 274
 275 Variable weakCoercionToHaskCoercion : forall Γ Δ, WeakCoercion -> HaskCoercion Γ Δ.
 276
 277 Notation "'checkit' ( Y ) X" := (match weakTypeOfWeakExpr Y as CTE return
 278                                    CTE=weakTypeOfWeakExpr Y -> forall Γ Δ φ ψ ξ lev, Indexed _ CTE with
 279                                 | Error s   =>   fun  _ _ _ _ _ _  _   => Indexed_Error _ s
 280                                 | OK    cte =>  fun cte_pf => (fun x Γ Δ φ ψ ξ lev => Indexed_OK _ _ (x Γ Δ φ ψ ξ lev)) X
 281                               end (refl_equal _)) (at level 10).
 282
 283
 284 (* equality lemmas I have yet to prove *)
 285
 286 Lemma upξ_lemma Γ ξ v lev φ
 287   : cure(Γ:=Γ) (upξ ξ (v :: nil) lev) φ = update_ξ (cure ξ φ) ((v,weakTypeToType φ v @@  map φ lev)::nil).
 288   admit.
 289   Qed.
 290
 291 (* this is tricky because of the test for ModalBoxTyCon is a type index for tc and because the fold is a left-fold *)
 292
 293 Lemma letrec_lemma : forall Γ ξ φ rb lev,
 294 let ξ' := upξ ξ (map (@fst _ _) (leaves (mLetRecTypesVars rb φ))) lev in
 295 (cure ξ' φ) = (
 296         update_ξ (cure ξ φ)
 297           (map
 298              (fun x : WeakExprVar * HaskType Γ =>
 299               ⟨fst x, snd x @@  map φ lev ⟩) (leaves (mLetRecTypesVars rb φ)))).
 300 admit.
 301 Qed.
 302
 303 Lemma case_lemma1 tc Γ avars' (sac:StrongAltConPlusJunk tc) vars ξ φ lev :
 304 (@scbwv_ξ WeakExprVar WeakExprVarEqDecidable tc Γ avars'
 305         {| scbwv_sac := sac; scbwv_exprvars := vars |}
 306         (@cure Γ ξ φ) (@map WeakTypeVar (HaskTyVar Γ) φ lev))
 307       = (cure ξ (sacpj_φ sac Γ φ)).
 308   admit.
 309   Qed.
 310 Lemma case_lemma2 tc Γ  (sac:@StrongAltConPlusJunk tc)  φ lev :
 311   (map (sacpj_φ sac Γ φ) lev) = weakL' (map φ lev).
 312   admit.
 313   Qed.
 314 Lemma case_lemma3 Γ φ t tc   (sac:@StrongAltConPlusJunk tc) :
 315  (weakT' (weakTypeToType φ t) = weakTypeToType (sacpj_φ sac Γ φ) t).
 316         admit.
 317   Qed.
 318 Lemma case_lemma4 Γ φ (tc:TyCon) avars0 : forall Q1 Q2, (@weakTypeToType Γ φ Q2)=Q1 ->
 319    fold_left HaskAppT (map (weakTypeToType φ) avars0) Q1 =
 320    weakTypeToType φ (fold_left WAppTy avars0 Q2).
 321    induction avars0; intros.
 322    simpl.
 323    symmetry; auto.
 324    simpl.
 325    set (IHavars0 (HaskAppT Q1 (weakTypeToType φ a)) (WAppTy Q2 a)) as z.
 326    rewrite z.
 327    reflexivity.
 328    rewrite <- H.
 329    simpl.
 330    auto.
 331    Qed.
 332
 333 (* for now... *)
 334 Axiom assume_all_coercions_well_formed : forall Γ (Δ:CoercionEnv Γ) t1 t2 co, Δ ⊢ᴄᴏ  co : t1 ∼ t2.
 335 Axiom assume_all_types_well_formed     : forall Γ t x,    Γ ⊢ᴛy t : x.
 336
 337 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
 338   WeakCoerVar -> HaskCoVar Γ (κ::Δ).
 339   intros.
 340   unfold HaskCoVar.
 341   intros.
 342   apply (ψ X TV CV env).
 343   inversion cenv; auto.
 344   Defined.
 345
 346 Lemma substRaw {Γ}{κ} : HaskType (κ::Γ) -> (∀ TV, @InstantiatedTypeEnv TV Γ -> TV -> @RawHaskType TV).
 347   intro ht.
 348   intro TV.
 349   intro env.
 350   intro tv.
 351   apply ht.
 352   apply (tv:::env).
 353   Defined.
 354
 355 Lemma substRaw_lemma : forall (Γ:TypeEnv) (φ:WeakTypeVar->HaskTyVar Γ) wt tsubst wtv,
 356   substT (substRaw (weakTypeToType (upφ wtv φ) wt)) (weakTypeToType φ tsubst) =
 357   weakTypeToType φ (replaceWeakTypeVar wt wtv tsubst).
 358   admit.
 359   Qed.
 360
 361 Definition weakExprToStrongExpr : forall
 362     (ce:WeakExpr)
 363     (Γ:TypeEnv)
 364     (Δ:CoercionEnv Γ)
 365     (φ:WeakTypeVar->HaskTyVar Γ)
 366     (ψ:WeakCoerVar->HaskCoVar Γ Δ)
 367     (ξ:WeakExprVar->WeakType * list WeakTypeVar)
 368     (lev:list WeakTypeVar)
 369     ,
 370     Indexed (fun t' => ???(@Expr _ WeakExprVarEqDecidable Γ Δ (cure ξ φ) (weakTypeToType φ t' @@ (map φ lev))))
 371        (weakTypeOfWeakExpr ce).
 372   refine ((
 373     fix weakExprToStrongExpr (ce:WeakExpr) {struct ce} : forall Γ Δ φ ψ ξ lev,
 374       Indexed (fun t' => ???(Expr Γ Δ (cure ξ φ) (weakTypeToType φ t' @@ (map φ lev)))) (weakTypeOfWeakExpr ce) :=
 375     (match ce as CE return (forall Γ Δ φ ψ ξ lev, Indexed _ (weakTypeOfWeakExpr CE))
 376       with
 377     | WEVar   v                   => let case_WEVar := tt in checkit (WEVar   v) (fun Γ Δ φ ψ ξ lev => _)
 378     | WELit   lit                 => let case_WELit := tt in checkit (WELit   lit) (fun Γ Δ φ ψ ξ lev => _)
 379     | WEApp   e1 e2               => let case_WEApp := tt in checkit (WEApp   e1 e2)       (fun Γ Δ φ ψ ξ lev =>
 380         weakExprToStrongExpr e1 Γ Δ φ ψ ξ lev >>>>= fun te1 e1' =>
 381           ((weakExprToStrongExpr e2 Γ Δ φ ψ ξ lev) >>>>= fun te2 e2' => _))
 382     | WETyApp e t                 => let case_WETyApp := tt in
 383       checkit (WETyApp e t) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _)
 384     | WECoApp e t                 => let case_WECoApp := tt in
 385       checkit (WECoApp e t) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _)
 386     | WELam   ev e                => let case_WELam   := tt in
 387       checkit (WELam   ev e) (fun Γ Δ φ ψ ξ lev =>
 388         let ξ' := @upξ ξ (ev::nil) lev in
 389         weakExprToStrongExpr e Γ Δ φ ψ ξ' lev >>>>= fun te' e' => _)
 390     | WECoLam cv e                => let case_WECoLam := tt in
 391       checkit (WECoLam cv e) (fun Γ Δ φ ψ ξ lev => (fun e' => _) (weakExprToStrongExpr e))
 392     | WEBrak  ec e tbody              => let case_WEBrak  := tt in
 393       checkit (WEBrak  ec e tbody) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ (ec::lev) >>>>= fun te' e' => _)
 394     | WEEsc   ec e tbody              =>
 395       checkit (WEEsc   ec e tbody) (fun Γ Δ φ ψ ξ lev =>
 396         match lev as LEV return lev=LEV -> _ with
 397           | nil       => let case_WEEsc_bogus   := tt in _
 398           | ec'::lev' => fun ecpf =>  weakExprToStrongExpr e Γ Δ φ ψ ξ lev' >>>>= fun te' e' => let case_WEEsc   := tt in _
 399         end (refl_equal _))
 400     | WETyLam tv e                => let case_WETyLam := tt in
 401       checkit (WETyLam tv e) (fun Γ Δ φ ψ ξ lev => (fun e' => _) (weakExprToStrongExpr e))
 402     | WENote  n e                 => let case_WENote := tt in
 403       checkit (WENote  n e) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _)
 404     | WECast  e co                => let case_WECast := tt in
 405       checkit (WECast  e co) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _)
 406     | WELet   v ve  e             => let case_WELet   := tt in
 407       checkit (WELet   v ve e) (fun Γ Δ φ ψ ξ lev =>
 408         let ξ' := upξ ξ (v::nil) lev in
 409           ((weakExprToStrongExpr e Γ Δ φ ψ ξ lev)
 410             >>>>= (fun te' e' => ((weakExprToStrongExpr ve Γ Δ φ ψ ξ' lev) >>>>= (fun vet' ve' => _)))))
 411
 412     | WELetRec rb   e             =>
 413       checkit (WELetRec rb e) (fun Γ Δ φ ψ ξ lev =>
 414 let ξ' := upξ ξ (map (@fst _ _) (leaves (mLetRecTypesVars rb φ))) lev in
 415           ((fix mLetRecBindingsToELetRecBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) : forall Γ Δ φ ψ ξ lev,
 416             ???(ELetRecBindings Γ Δ (cure ξ φ) (map φ lev) (mLetRecTypesVars mlr φ)) :=
 417             match mlr as MLR return forall Γ Δ φ ψ ξ lev,
 418               ???(ELetRecBindings Γ Δ (cure ξ φ) (map φ lev) (mLetRecTypesVars MLR φ)) with
 419               | T_Leaf None       => fun Γ Δ φ ψ ξ lev => OK (ELR_nil _ _ _ _)
 420               | T_Leaf (Some  (cv,e)) => fun Γ Δ φ ψ ξ lev =>
 421                 let case_mlr_leaf := tt in weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun me => _
 422               | T_Branch b1 b2   =>
 423                 fun Γ Δ φ ψ ξ lev  =>
 424                   mLetRecBindingsToELetRecBindings b1 Γ Δ φ ψ ξ lev >>= fun x1' =>
 425                     mLetRecBindingsToELetRecBindings b2 Γ Δ φ ψ ξ lev >>= fun x2' =>
 426                       OK (ELR_branch _ _ _ _ _ _ x1' x2')
 427             end) rb Γ Δ φ ψ ξ' lev) >>= fun rb' => (weakExprToStrongExpr e Γ Δ φ ψ ξ' lev)
 428           >>>>= fun et' e' =>
 429       let case_MLLetRec := tt in _)
 430
 431     | WECase  e tbranches tc avars alts =>
 432       checkit (WECase  e tbranches  tc avars alts) (fun Γ Δ φ ψ ξ lev =>
 433         list2vecOrFail avars _ (fun _ _ => "number of types provided did not match the tycon's number of universal tyvars in Case")
 434         >>= fun avars0 =>
 435           let avars' := vec_map (@weakTypeToType Γ φ) avars0 in
 436           let tbranches' := @weakTypeToType Γ φ tbranches in
 437             ((fix caseBranches (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
 438               :
 439                ???(Tree ??{ scb : StrongCaseBranchWithVVs WeakExprVar _ tc avars'
 440                             & Expr (sac_Γ scb Γ)
 441                                    (sac_Δ scb Γ avars' (weakCK'' Δ))
 442                                    (scbwv_ξ scb (cure ξ φ) (map φ lev))
 443                                    (weakLT' (tbranches'@@(map φ lev))) }) :=
 444               match alts with
 445               | T_Leaf None             => OK []
 446               | T_Branch b1 b2          => caseBranches b1 >>= fun b1' => caseBranches b2 >>= fun b2' => OK (b1',,b2')
 447               | T_Leaf (Some (alt,tvars,cvars,vvars,e')) =>
 448                 mkStrongAltConPlusJunk' tc alt >>= fun sac =>
 449                 list2vecOrFail vvars (sac_numExprVars (sac:@StrongAltCon tc))
 450                 (fun _ _ => "number of expression variables provided did not match the datacon's number of fields") >>= fun vars =>
 451                   let scb := @Build_StrongCaseBranchWithVVs WeakExprVar _ tc Γ avars' sac vars in
 452                   let rec
 453                     := @weakExprToStrongExpr e'
 454                     (sac_Γ scb Γ)
 455                     (sac_Δ scb Γ avars' (weakCK'' Δ))
 456                     (sacpj_φ sac Γ φ)
 457                     (let case_psi := tt in _)
 458                     ξ
 459                     lev in (let case_ECase_leaf := tt in _)
 460               end
 461               ) alts) >>= fun alts' =>
 462             weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' =>
 463               let case_ECase := tt in _)
 464      end))); clear weakExprToStrongExpr.
 465
 466     destruct case_WEVar; intros.
 467       matchTypes cte (fst (ξ v)) "HaskWeak EVar".
 468       rewrite matchTypes_pf.
 469       matchLevs (snd (ξ v)) lev "HaskWeak EVar".
 470       rewrite <- matchLevs_pf.
 471       apply OK.
 472       apply (EVar _ _ (cure ξ φ)).
 473
 474     destruct case_WELit; intros.
 475       matchTypes (WTyCon (haskLiteralToTyCon lit)) cte "HaskWeak ELit".
 476       rewrite <- matchTypes_pf.
 477       apply OK.
 478       replace (weakTypeToType φ (WTyCon (haskLiteralToTyCon lit))) with (@literalType lit Γ); [ idtac | reflexivity].
 479       apply ELit.
 480
 481     destruct case_WELet; intros.
 482       unfold ξ' in ve'.
 483       matchTypes te' v "HaskWeak ELet".
 484       rename matchTypes_pf into matchTypes_pf'.
 485       matchTypes cte vet' "HaskWeak ELet".
 486       apply OK.
 487       eapply ELet.
 488       apply e'.
 489       rewrite matchTypes_pf'.
 490       rewrite matchTypes_pf.
 491       rewrite upξ_lemma in ve'.
 492       apply ve'.
 493
 494     destruct case_mlr_leaf; intros.
 495       simpl.
 496       destruct cv.
 497       matchTypes me w "HaskWeak LetRec".
 498       apply OK.
 499       apply ELR_leaf.
 500       rewrite <- matchTypes_pf.
 501       apply X.
 502
 503     destruct case_MLLetRec; intros.
 504       matchTypes et' cte "HaskWeak LetRec".
 505       apply OK.
 506       unfold ξ' in rb'.
 507       rewrite (letrec_lemma Γ ξ φ rb lev) in rb'.
 508       apply (@ELetRec WeakExprVar _ Γ Δ (cure ξ φ) (map φ lev) (weakTypeToType φ cte) _ rb').
 509       rewrite <- (letrec_lemma Γ ξ φ rb lev).
 510       rewrite <- matchTypes_pf.
 511       apply e'.
 512
 513     destruct case_WECast; intros.
 514       apply OK.
 515       apply (fun pf => @ECast WeakExprVar _ Γ Δ (cure ξ φ) (weakCoercionToHaskCoercion Γ Δ co) _ _ (map φ lev) pf e').
 516       apply assume_all_coercions_well_formed.
 517
 518     destruct case_WENote; intros.
 519       matchTypes te' cte "HaskWeak ENote".
 520       apply OK.
 521       apply ENote.
 522       apply n.
 523       rewrite <- matchTypes_pf.
 524       apply e'.
 525
 526     destruct case_WEApp; intros.
 527       matchTypes te1 (WAppTy (WAppTy WFunTyCon te2) cte) "HaskWeak EApp".
 528       inversion cte_pf.
 529       destruct (weakTypeOfWeakExpr e1); try apply (Error error_message).
 530       simpl in H0.
 531       destruct w; try apply (Error error_message); inversion H0.
 532       destruct w1; try apply (Error error_message); inversion H0.
 533       destruct w1_1; try apply (Error error_message); inversion H0.
 534       clear H0 H1 H2.
 535       rewrite matchTypes_pf in e1'.
 536       simpl in e1'.
 537       rewrite <- H3.
 538       apply (OK (EApp _ _ _ _ _ _ e1' e2')).
 539
 540     destruct case_WETyApp; intros.
 541       inversion cte_pf.
 542       destruct (weakTypeOfWeakExpr e); simpl in *; inversion H0.
 543       clear H1.
 544       destruct w; inversion H0.
 545       simpl in cte_pf.
 546       clear cte_pf.
 547       rename w0 into wt.
 548       rename t into tsubst.
 549       rename w into wtv.
 550       set (@ETyApp WeakExprVar _ Γ Δ wtv
 551         (substRaw (weakTypeToType (upφ wtv φ) wt))
 552         (weakTypeToType φ tsubst)
 553         (cure ξ φ)
 554         (map φ lev)
 555         (assume_all_types_well_formed _ _ _)
 556       ) as q.
 557
 558       (* really messy –– but it works! *)
 559       matchTypes te' (WForAllTy wtv wt) "HaskWeak ETyApp".
 560       apply OK.
 561       rewrite substRaw_lemma in q.
 562       apply q.
 563       clear q H1 H0.
 564       rewrite matchTypes_pf in e'.
 565       simpl in e'.
 566       unfold HaskTAll.
 567       unfold substRaw.
 568       apply e'.
 569
 570     destruct case_WECoApp; intros.
 571       inversion cte_pf.
 572       destruct (weakTypeOfWeakExpr e); simpl in *; inversion H0.
 573       clear H1.
 574       destruct w; inversion H0.
 575       subst.
 576       destruct t as [ct1 ct2 cc].
 577       set (@ECoApp WeakExprVar _ Γ Δ (weakCoercionToHaskCoercion Γ Δ (weakCoercion ct1 ct2 cc))
 578               (weakTypeToType φ ct1) (weakTypeToType φ ct2) (weakTypeToType φ te') (cure ξ φ) (map φ lev)) as q.
 579       matchTypes w3 te' "HaskWeak ECoApp".
 580       rewrite matchTypes_pf.
 581       clear matchTypes_pf.
 582       matchTypes (WCoFunTy ct1 ct2 te') te' "HaskWeak ECoApp".
 583       apply OK.
 584       apply q.
 585       apply assume_all_coercions_well_formed.
 586       clear q H0 cte_pf.
 587       rewrite <- matchTypes_pf in e'.
 588       simpl in e'.
 589       apply e'.
 590
 591     destruct case_WELam; intros.
 592       simpl in cte_pf.
 593       destruct ev as [evv evt].
 594       destruct (weakTypeOfWeakExpr e); simpl in cte_pf; inversion cte_pf; try apply (Error error_message).
 595       matchTypes te' w "HaskWeak ELam".
 596       rewrite <- matchTypes_pf.
 597       apply OK.
 598       simpl.
 599       eapply ELam.
 600       apply assume_all_types_well_formed.
 601       unfold ξ' in e'.
 602       rewrite upξ_lemma in e'.
 603       apply e'.
 604
 605     destruct case_WETyLam; intros.
 606       inversion cte_pf.
 607       destruct tv.
 608       destruct (weakTypeOfWeakExpr e).
 609       inversion H0.
 610       inversion H0.
 611       set (e' (k::Γ) (weakCE Δ) (upφ (weakTypeVar c k) φ) (fun x => weakCV (ψ x)) ξ lev) as e''.
 612       inversion e''; try apply (Error error_message).
 613       inversion X; try apply (Error error_message).
 614       apply (Error "FIXME: HaskWeakToStrong: type lambda not yet implemented").
 615
 616     destruct case_WECoLam; intros.
 617       inversion cte_pf.
 618       destruct cv.
 619       destruct (weakTypeOfWeakExpr e).
 620       inversion H0.
 621       inversion H0.
 622       set (e' Γ (weakTypeToType φ w ∼∼∼ weakTypeToType φ w0 :: Δ) φ (weakψ ψ) ξ lev) as q.
 623       inversion q.
 624       destruct X; try apply (Error error_message).
 625       set (kindOfType (weakTypeToType φ w)) as qq.
 626       destruct qq; try apply (Error error_message).
 627       apply OK.
 628       apply ECoLam with (κ:=k).
 629       apply assume_all_types_well_formed.
 630       apply assume_all_types_well_formed.
 631       fold (@weakTypeToType Γ).
 632       apply e0.
 633
 634     destruct case_WEBrak; intros.
 635       simpl in cte_pf.
 636       destruct ec as [ecv eck].
 637       destruct (weakTypeOfWeakExpr e); inversion cte_pf; try apply (Error error_message).
 638       simpl.
 639       matchTypes te' w "HaskWeak EBrak".
 640       apply OK.
 641       apply EBrak.
 642       rewrite matchTypes_pf in e'.
 643       apply e'.
 644
 645     destruct case_WEEsc_bogus; intros.
 646       apply (Error "attempt to use escape symbol at level zero").
 647
 648     destruct case_WEEsc; intros.
 649       rewrite ecpf.
 650       clear ecpf lev.
 651       matchTypes te' (WCodeTy ec' cte) "HaskWeak EEsc".
 652       apply OK.
 653       apply EEsc.
 654       rewrite matchTypes_pf in e'.
 655       simpl in e'.
 656       apply e'.
 657
 658     destruct case_psi.
 659       apply (sacpj_ψ sac Γ Δ avars' ψ).
 660
 661     destruct case_ECase_leaf.
 662       inversion rec; try apply (Error error_message).
 663       destruct X; try apply (Error error_message).
 664       matchTypes tbranches t "HaskWeak ECase".
 665       apply OK.
 666       apply T_Leaf.
 667       apply Some.
 668       apply (existT _ {| scbwv_sac := scb ; scbwv_exprvars := vars |}).
 669       simpl.
 670       unfold tbranches'.
 671       rewrite matchTypes_pf.
 672       rewrite case_lemma1.
 673       rewrite <- case_lemma2.
 674       rewrite case_lemma3.
 675       apply e0.
 676
 677     destruct case_ECase; intros.
 678       matchTypes cte tbranches "HaskWeak ECase".
 679       rewrite matchTypes_pf.
 680       clear matchTypes_pf.
 681       matchTypes te' (fold_left WAppTy (vec2list avars0) (WTyCon tc)) "HaskWeak ECase".
 682       apply OK.
 683       apply (fun e => @ECase WeakExprVar _ Γ Δ (cure ξ φ) (map φ lev) tc _ _ e alts').
 684       unfold caseType.
 685       unfold avars'.
 686       replace (fold_left HaskAppT (vec2list (vec_map (weakTypeToType φ) avars0)) (HaskTCon tc))
 687         with (weakTypeToType φ (fold_left WAppTy (vec2list avars0) (WTyCon tc))).
 688       rewrite <- matchTypes_pf.
 689       apply e'.
 690       symmetry.
 691       rewrite <- vec2list_map_list2vec.
 692       apply case_lemma4.
 693       apply tc.
 694       reflexivity.
 695       Defined.