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 HaskLiteralsAndTyCons.
  14 Require Import HaskWeakTypes.
  15 Require Import HaskWeakVars.
  16 Require Import HaskWeak.
  17 Require Import HaskWeakToCore.
  18 Require Import HaskStrongTypes.
  19 Require Import HaskStrong.
  20 Require Import HaskCoreVars.
  21
  22 Open Scope string_scope.
  23 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
  24 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
  25
  26 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
  27   unfold TyVarResolver.
  28   refine (fun tv' =>
  29     if eqd_dec tv tv'
  30     then let fresh := @FreshHaskTyVar Γ tv in OK _
  31     else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
  32   rewrite <- _H; apply fresh.
  33   Defined.
  34
  35 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
  36   : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
  37   induction tvs.
  38   apply φ.
  39   simpl.
  40   apply upφ.
  41   apply IHtvs.
  42   Defined.
  43
  44 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
  45   intro ht.
  46   refine (substT _ θ).
  47   clear θ.
  48   unfold HaskType in ht.
  49   intros.
  50   apply ht.
  51   apply ICons; [ idtac | apply env ].
  52   apply X.
  53   Defined.
  54
  55 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
  56   induction lk.
  57   intro q; apply q.
  58   simpl.
  59   intro q.
  60   apply IHlk.
  61   inversion θ; subst; auto.
  62   inversion θ; subst.
  63   eapply substPhi.
  64   eapply weakT'.
  65   apply X.
  66   apply q.
  67   Defined.
  68
  69 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
  70 Record StrongAltConPlusJunk {tc:TyCon} :=
  71 { sacpj_sac : @StrongAltCon tc
  72 ; sacpj_φ   : forall Γ          (φ:TyVarResolver Γ  ),  (TyVarResolver (sac_Γ sacpj_sac Γ))
  73 ; sacpj_ψ   : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
  74 }.
  75 Implicit Arguments StrongAltConPlusJunk [ ].
  76 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
  77
  78 (* yes, I know, this is really clumsy *)
  79 Variable emptyφ : TyVarResolver nil.
  80   Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
  81
  82 Definition mkPhi (lv:list WeakTypeVar)
  83   : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
  84   set (upφ'(Γ:=nil) lv emptyφ) as φ'.
  85   rewrite <- app_nil_end in φ'.
  86   apply φ'.
  87   Defined.
  88
  89 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
  90 Definition tyConKinds     tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
  91
  92 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
  93 Notation " ` x " := (@fixkind _ x) (at level 100).
  94
  95 Ltac matchThings T1 T2 S :=
  96   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
  97    [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
  98
  99 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
 100   intros.
 101   unfold InstantiatedTypeEnv in ite.
 102   apply X.
 103   apply (X0::::ite).
 104   Defined.
 105
 106 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
 107   intro.
 108   unfold HaskType.
 109   intros.
 110   apply (TAll κ).
 111   eapply mkTAll'.
 112   apply X.
 113   apply X0.
 114   Defined.
 115
 116 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
 117   refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
 118   addErrorMessage ("weakTypeToType " +++ t)
 119   match t with
 120     | WFunTyCon         => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
 121     | WTyCon      tc    => let case_WTyCon := tt    in _
 122     | WClassP   c lt    => let case_WClassP := tt   in Error "weakTypeToType: WClassP not implemented"
 123     | WIParam _ ty      => let case_WIParam := tt   in Error "weakTypeToType: WIParam not implemented"
 124     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
 125     | WTyVarTy  v       => let case_WTyVarTy := tt  in φ v >>= fun v' => _
 126     | WForAllTy wtv t   => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
 127     | WCodeTy ec tbody  => let case_WCodeTy := tt   in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _
 128     | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt  in
 129       weakTypeToType _ φ t1 >>= fun t1' =>
 130       weakTypeToType _ φ t2 >>= fun t2' =>
 131       weakTypeToType _ φ t3 >>= fun t3' => _
 132     | WTyFunApp   tc lt =>
 133       ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
 134         { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
 135         match lt with
 136           | nil    => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
 137                         | nil => OK (fun TV _ => TyFunApp_nil)
 138                         | _   => Error "WTyFunApp not applied to enough types"
 139                       end
 140           | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
 141                         match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
 142                           | nil    => Error "WTyFunApp applied to too many types"
 143                           | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
 144                                         let case_weakTypeListToTypeList := tt in _
 145                         end
 146         end
 147       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
 148   end ); clear weakTypeToType.
 149
 150   destruct case_WTyVarTy.
 151     apply (addErrorMessage "case_WTyVarTy").
 152     apply OK.
 153     exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
 154
 155   destruct case_WAppTy.
 156     apply (addErrorMessage "case_WAppTy").
 157     destruct t1' as  [k1' t1'].
 158     destruct t2' as [k2' t2'].
 159     set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.
 160     destruct k1';
 161       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
 162         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
 163       apply (Error ("Kind mismatch in WAppTy: "+++err)).
 164
 165   destruct case_weakTypeListToTypeList.
 166     apply (addErrorMessage "case_weakTypeListToTypeList").
 167     destruct t' as [ k' t' ].
 168     matchThings k k' "Kind mismatch in weakTypeListToTypeList".
 169     subst.
 170     apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
 171
 172   destruct case_WTyFunApp.
 173     apply (addErrorMessage "case_WTyFunApp").
 174     apply OK.
 175     eapply haskTypeOfSomeKind.
 176     unfold HaskType; intros.
 177     apply TyFunApp.
 178     apply lt'.
 179     apply X.
 180
 181   destruct case_WTyCon.
 182     apply (addErrorMessage "case_WTyCon").
 183     apply OK.
 184     eapply haskTypeOfSomeKind.
 185     unfold HaskType; intros.
 186     apply (TCon tc).
 187
 188   destruct case_WCodeTy.
 189     apply (addErrorMessage "case_WCodeTy").
 190     destruct tbody'.
 191     matchThings κ ★ "Kind mismatch in WCodeTy: ".
 192     apply OK.
 193     eapply haskTypeOfSomeKind.
 194     unfold HaskType; intros.
 195     apply TCode.
 196     apply (TVar (ec' TV X)).
 197     subst.
 198     apply h.
 199     apply X.
 200
 201   destruct case_WCoFunTy.
 202     apply (addErrorMessage "case_WCoFunTy").
 203     destruct t1' as [ k1' t1' ].
 204     destruct t2' as [ k2' t2' ].
 205     destruct t3' as [ k3' t3' ].
 206     matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
 207     subst.
 208     matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
 209     subst.
 210     apply OK.
 211     apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
 212
 213   destruct case_WForAllTy.
 214     apply (addErrorMessage "case_WForAllTy").
 215     destruct t1.
 216     matchThings ★  κ "Kind mismatch in WForAllTy: ".
 217     subst.
 218     apply OK.
 219     apply (@haskTypeOfSomeKind _ ★).
 220     apply (@mkTAll wtv).
 221     apply h.
 222     Defined.
 223
 224
 225 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
 226
 227 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 228 Section StrongAltCon.
 229   Context (tc : TyCon)(dc:DataCon tc).
 230
 231 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
 232  -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
 233   intro avars.
 234   intro ct.
 235   apply (addErrorMessage "weakTypeToType'").
 236   set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
 237   set (@substφ _ _ avars') as q.
 238   set (upφ' (tyConTyVars tc)  (mkPhi (dataConExTyVars dc))) as φ'.
 239   set (@weakTypeToType _ φ' ct) as t.
 240   destruct t as [|t]; try apply (Error error_message).
 241   destruct t as [tk t].
 242   matchThings tk ★ "weakTypeToType'".
 243   subst.
 244   apply OK.
 245   set (@weakT'' _ Γ _ t) as t'.
 246   set (@lamer _ _ _ _ t') as t''.
 247   fold (tyConKinds tc) in t''.
 248   fold (dataConExKinds dc) in t''.
 249   apply q.
 250   clear q.
 251   unfold tyConKinds.
 252   unfold dataConExKinds.
 253   rewrite <- vec2list_map_list2vec.
 254   rewrite <- vec2list_map_list2vec.
 255   rewrite vec2list_list2vec.
 256   rewrite vec2list_list2vec.
 257   apply t''.
 258   Defined.
 259
 260 Definition mkStrongAltCon : @StrongAltCon tc.
 261   refine
 262    {| sac_altcon      := WeakDataAlt dc
 263     ; sac_numCoerVars := length (dataConCoerKinds dc)
 264     ; sac_numExprVars := length (dataConFieldTypes dc)
 265     ; sac_ekinds      := dataConExKinds dc
 266     ; sac_coercions   := fun Γ avars => let case_sac_coercions := tt in _
 267     ; sac_types       := fun Γ avars => let case_sac_types := tt in _
 268     |}.
 269
 270   destruct case_sac_coercions.
 271     refine (vec_map _ (list2vec (dataConCoerKinds dc))).
 272     intro.
 273     destruct X.
 274     unfold tyConKind in avars.
 275     set (@weakTypeToType' Γ) as q.
 276     unfold tyConKinds in q.
 277     rewrite <- vec2list_map_list2vec in q.
 278     rewrite vec2list_list2vec in q.
 279     apply (
 280       match
 281         q avars w >>= fun t1 =>
 282         q avars w0 >>= fun t2 =>
 283           OK (mkHaskCoercionKind t1 t2)
 284       with
 285         | Error s => Prelude_error s
 286         | OK y => y
 287       end).
 288
 289   destruct case_sac_types.
 290     refine (vec_map _ (list2vec (dataConFieldTypes dc))).
 291     intro X.
 292     unfold tyConKind in avars.
 293     set (@weakTypeToType' Γ) as q.
 294     unfold tyConKinds in q.
 295     rewrite <- vec2list_map_list2vec in q.
 296     rewrite vec2list_list2vec in q.
 297     set (q avars X) as y.
 298     apply (match y with
 299              | Error s =>Prelude_error s
 300              | OK y' => y'
 301            end).
 302     Defined.
 303
 304
 305 Lemma weakCV' : forall {Γ}{Δ} Γ',
 306    HaskCoVar Γ Δ
 307    -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
 308   intros.
 309   unfold HaskCoVar in *.
 310   intros; apply (X TV CV).
 311   apply ilist_chop' in env; auto.
 312   unfold InstantiatedCoercionEnv in *.
 313   unfold weakCK'' in cenv.
 314   destruct Γ'.
 315   rewrite <- map_preserves_length in cenv.
 316   apply cenv.
 317   rewrite <- map_preserves_length in cenv.
 318   apply cenv.
 319   Defined.
 320
 321 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
 322     refine
 323      {| sacpj_sac     := mkStrongAltCon
 324       ; sacpj_φ       := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
 325       ; sacpj_ψ       :=
 326       fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
 327       |}.
 328     intro.
 329     unfold sac_Γ.
 330     unfold HaskCoVar in *.
 331     intros.
 332     apply (x TV CV env).
 333     simpl in cenv.
 334     unfold sac_Δ in *.
 335     unfold InstantiatedCoercionEnv in *.
 336     apply vec_chop' in cenv.
 337     apply cenv.
 338     Defined.
 339
 340   Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
 341     intros.
 342     induction Δ.
 343     reflexivity.
 344     simpl.
 345     rewrite IHΔ.
 346     reflexivity.
 347     Qed.
 348
 349 End StrongAltCon.
 350
 351 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
 352   destruct alt.
 353   set (c:DataCon _) as dc.
 354   set ((dataConTyCon c):TyCon) as tc' in *.
 355   set (eqd_dec tc tc') as eqpf; destruct eqpf;
 356     [ idtac
 357       | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
 358   apply OK.
 359   eapply mkStrongAltConPlusJunk.
 360   simpl in *.
 361   apply dc.
 362
 363   apply OK; refine {| sacpj_sac := {|
 364                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 365                     ; sac_altcon := WeakLitAlt h
 366                     |} |}.
 367             intro; intro φ; apply φ.
 368             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 369             rewrite weakCK'_nil_inert. apply ψ.
 370   apply OK; refine {| sacpj_sac := {|
 371                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 372                       ; sac_altcon := WeakDEFAULT |} |}.
 373             intro; intro φ; apply φ.
 374             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 375             rewrite weakCK'_nil_inert. apply ψ.
 376 Defined.
 377
 378 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
 379   fun wev => match wev with weakExprVar _ t => t end.
 380   Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
 381
 382 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
 383
 384 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
 385   WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
 386   intros.
 387   refine (ψ X >>= _).
 388   unfold HaskCoVar.
 389   intros.
 390   apply OK.
 391   intros.
 392   inversion cenv; auto.
 393   Defined.
 394
 395 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
 396 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
 397   : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
 398   apply (addErrorMessage ("castExpr " +++ err_msg)).
 399   intros.
 400   destruct τ  as [τ  l].
 401   destruct τ' as [τ' l'].
 402   destruct (eqd_dec l l'); [ idtac
 403     | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
 404                     "  got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
 405                     "  wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
 406     )) ].
 407   destruct (eqd_dec τ τ'); [ idtac
 408     | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
 409                     "  got: " +++τ+++eol+++
 410                     "  wanted: "+++τ'
 411     )) ].
 412   subst.
 413   apply OK.
 414   apply e.
 415   Defined.
 416
 417 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
 418   match wcv with weakCoerVar _ κ _ _ => κ end.
 419   Coercion coVarKind : WeakCoerVar >-> Kind.
 420
 421 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
 422   intros.
 423   set (weakTypeToType φ t) as wt.
 424   destruct wt; try apply (Error error_message).
 425   destruct h.
 426   matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
 427   subst.
 428   apply OK.
 429   apply h.
 430   Defined.
 431
 432 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
 433   match t with
 434     | T_Leaf None            => []
 435     | T_Leaf (Some (wev,e))  => match weakTypeToTypeOfKind φ wev ★ with
 436                                   | OK    t' => [((wev:CoreVar),t')]
 437                                   | _        => []
 438                                 end
 439     | T_Branch b1 b2         => (varsTypes b1 φ),,(varsTypes b2 φ)
 440   end.
 441
 442 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
 443 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
 444   | nil => match wtl with
 445              | nil => OK INil
 446              | _   => Error "length mismatch in mkAvars"
 447            end
 448   | k::lk' => match wtl with
 449                 | nil => Error "length mismatch in mkAvars"
 450                 | wt::wtl' =>
 451                   weakTypeToTypeOfKind φ wt k >>= fun t =>
 452                     mkAvars wtl' lk' φ >>= fun rest =>
 453                     OK (ICons _ _ t rest)
 454               end
 455 end.
 456
 457 Definition weakExprToStrongExpr : forall
 458     (Γ:TypeEnv)
 459     (Δ:CoercionEnv Γ)
 460     (φ:TyVarResolver Γ)
 461     (ψ:CoVarResolver Γ Δ)
 462     (ξ:CoreVar -> LeveledHaskType Γ ★)
 463     (τ:HaskType Γ ★)
 464     (lev:HaskLevel Γ),
 465     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
 466   refine ((
 467     fix weakExprToStrongExpr
 468     (Γ:TypeEnv)
 469     (Δ:CoercionEnv Γ)
 470     (φ:TyVarResolver Γ)
 471     (ψ:CoVarResolver Γ Δ)
 472     (ξ:CoreVar -> LeveledHaskType Γ ★)
 473     (τ:HaskType Γ ★)
 474     (lev:HaskLevel Γ)
 475     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
 476     addErrorMessage ("in weakExprToStrongExpr " +++ we)
 477     match we with
 478
 479     | WEVar   v                         => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
 480
 481     | WELit   lit                       => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
 482
 483     | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
 484                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
 485                                                weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 486                                                  let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
 487                                                    weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
 488                                                      castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
 489
 490     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
 491                                              weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 492                                                weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
 493                                                  castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
 494
 495     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
 496                                            weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 497                                            match lev with
 498                                              | nil       => Error "ill-leveled escapification"
 499                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e
 500                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
 501                                            end
 502
 503     | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
 504
 505     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 506
 507     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>
 508                                              weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
 509                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
 510                                                >>= fun ebody' =>
 511                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 512
 513     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
 514                                              weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 515                                                weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
 516                                                  weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
 517                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 518
 519     | WETyLam tv e                      => let φ' := upφ tv φ in
 520                                              weakTypeOfWeakExpr e >>= fun te =>
 521                                                weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
 522                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
 523                                                     (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
 524                                                  >>= fun e' =>
 525                                                    castExpr we "WETyLam1" _ e' >>= fun e'' =>
 526                                                      castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
 527
 528     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
 529                                            match te with
 530                                              | WForAllTy wtv te' =>
 531                                                let φ' := upφ wtv φ in
 532                                                  weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
 533                                                    weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
 534                                                      weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
 535                                                        castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
 536                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
 537                                            end
 538
 539     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
 540                                            match te with
 541                                              | WCoFunTy t1 t2 t3 =>
 542                                                weakTypeToType φ t1 >>= fun t1' =>
 543                                                  match t1' with
 544                                                    haskTypeOfSomeKind κ t1'' =>
 545                                                    weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
 546                                                      weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
 547                                                        weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
 548                                                          castExpr we "WECoApp" _ e' >>= fun e'' =>
 549                                                            OK (ECoApp Γ Δ κ t1'' t2''
 550                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
 551                                                  end
 552                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++te)
 553                                            end
 554
 555     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
 556                                            weakTypeOfWeakExpr e >>= fun te =>
 557                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
 558                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
 559                                                  weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
 560                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
 561                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 562
 563     | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
 564                                              weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
 565                                                weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 566                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
 567                                                      castExpr we "WECast" _
 568                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 569
 570     | WELetRec rb   e                   =>
 571       let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
 572       in let binds :=
 573         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
 574           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
 575         match t with
 576           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
 577           | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
 578           | T_Branch b1 b2        =>
 579             binds b1 >>= fun b1' =>
 580               binds b2 >>= fun b2' =>
 581                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
 582         end) rb
 583       in binds >>= fun binds' =>
 584            weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
 585              OK (ELetRec Γ Δ ξ lev τ _ binds' e')
 586
 587     | WECase vscrut ve tbranches tc avars alts =>
 588         weakTypeToTypeOfKind φ (vscrut:WeakType) ★  >>= fun tv =>
 589           weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
 590             let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
 591               mkAvars avars (tyConKind tc) φ >>= fun avars' =>
 592                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
 593                   (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
 594                       ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
 595                         Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) :=
 596                     match t with
 597                       | T_Leaf None           => OK []
 598                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
 599                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
 600                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
 601                           >>= fun exprvars' =>
 602                             let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
 603                               weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
 604                               (sacpj_ψ sac _ _ avars' ψ)
 605                               (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
 606                                 let case_case := tt in OK [ _ ]
 607                       | T_Branch b1 b2        =>
 608                         mkTree b1 >>= fun b1' =>
 609                           mkTree b2 >>= fun b2' =>
 610                             OK (b1',,b2')
 611                     end) alts >>= fun tree =>
 612                   castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
 613                       castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
 614                         >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
 615
 616
 617
 618     end)).
 619
 620     destruct case_some.
 621     apply (addErrorMessage "case_some").
 622       simpl.
 623       destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
 624       matchThings h (unlev (ξ' wev)) "LetRec".
 625       destruct wev.
 626       rewrite matchTypeVars_pf.
 627       clear matchTypeVars_pf.
 628       set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
 629       destruct e''; try apply (Error error_message).
 630       apply OK.
 631       apply ELR_leaf.
 632       apply e1.
 633
 634     destruct case_case.
 635       exists scb.
 636       apply ebranch'.
 637
 638     Defined.
 639