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 HaskWeakToCore.
  18 Require Import HaskStrongTypes.
  19 Require Import HaskStrong.
  20 Require Import HaskCoreTypes.
  21 Require Import HaskCoreVars.
  22
  23 Open Scope string_scope.
  24 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
  25 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
  26
  27 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
  28   unfold TyVarResolver.
  29   refine (fun tv' =>
  30     if eqd_dec tv tv'
  31     then let fresh := @FreshHaskTyVar Γ tv in OK _
  32     else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
  33   rewrite <- _H; apply fresh.
  34   Defined.
  35
  36 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
  37   : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
  38   induction tvs.
  39   apply φ.
  40   simpl.
  41   apply upφ.
  42   apply IHtvs.
  43   Defined.
  44
  45 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
  46   intro ht.
  47   refine (substT _ θ).
  48   clear θ.
  49   unfold HaskType in ht.
  50   intros.
  51   apply ht.
  52   apply ICons; [ idtac | apply env ].
  53   apply X.
  54   Defined.
  55
  56 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
  57   induction lk.
  58   intro q; apply q.
  59   simpl.
  60   intro q.
  61   apply IHlk.
  62   inversion θ; subst; auto.
  63   inversion θ; subst.
  64   eapply substPhi.
  65   eapply weakT'.
  66   apply X.
  67   apply q.
  68   Defined.
  69
  70 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
  71 Record StrongAltConPlusJunk {tc:TyCon} :=
  72 { sacpj_sac : @StrongAltCon tc
  73 ; sacpj_φ   : forall Γ          (φ:TyVarResolver Γ  ),  (TyVarResolver (sac_Γ sacpj_sac Γ))
  74 ; sacpj_ψ   : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
  75 }.
  76 Implicit Arguments StrongAltConPlusJunk [ ].
  77 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
  78
  79 (* yes, I know, this is really clumsy *)
  80 Variable emptyφ : TyVarResolver nil.
  81   Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
  82
  83 Definition mkPhi (lv:list WeakTypeVar)
  84   : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
  85   set (upφ'(Γ:=nil) lv emptyφ) as φ'.
  86   rewrite <- app_nil_end in φ'.
  87   apply φ'.
  88   Defined.
  89
  90 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
  91 Definition tyConKinds     tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
  92
  93 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
  94 Notation " ` x " := (@fixkind _ x) (at level 100).
  95
  96 Ltac matchThings T1 T2 S :=
  97   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
  98    [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
  99
 100 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
 101   intros.
 102   unfold InstantiatedTypeEnv in ite.
 103   apply X.
 104   apply (X0::::ite).
 105   Defined.
 106
 107 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
 108   intro.
 109   unfold HaskType.
 110   intros.
 111   apply (TAll κ).
 112   eapply mkTAll'.
 113   apply X.
 114   apply X0.
 115   Defined.
 116
 117 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
 118   refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
 119   addErrorMessage ("weakTypeToType " +++ t)
 120   match t with
 121     | WFunTyCon         => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
 122     | WTyCon      tc    => let case_WTyCon := tt    in _
 123     | WClassP   c lt    => let case_WClassP := tt   in Error "weakTypeToType: WClassP not implemented"
 124     | WIParam _ ty      => let case_WIParam := tt   in Error "weakTypeToType: WIParam not implemented"
 125     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
 126     | WTyVarTy  v       => let case_WTyVarTy := tt  in φ v >>= fun v' => _
 127     | WForAllTy wtv t   => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
 128     | WCodeTy ec tbody  => let case_WCodeTy := tt   in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _
 129     | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt  in
 130       weakTypeToType _ φ t1 >>= fun t1' =>
 131       weakTypeToType _ φ t2 >>= fun t2' =>
 132       weakTypeToType _ φ t3 >>= fun t3' => _
 133     | WTyFunApp   tc lt =>
 134       ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
 135         { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
 136         match lt with
 137           | nil    => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
 138                         | nil => OK (fun TV _ => TyFunApp_nil)
 139                         | _   => Error "WTyFunApp not applied to enough types"
 140                       end
 141           | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
 142                         match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
 143                           | nil    => Error "WTyFunApp applied to too many types"
 144                           | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
 145                                         let case_weakTypeListToTypeList := tt in _
 146                         end
 147         end
 148       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
 149   end ); clear weakTypeToType.
 150
 151   destruct case_WTyVarTy.
 152     apply (addErrorMessage "case_WTyVarTy").
 153     apply OK.
 154     exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
 155
 156   destruct case_WAppTy.
 157     apply (addErrorMessage "case_WAppTy").
 158     destruct t1' as  [k1' t1'].
 159     destruct t2' as [k2' t2'].
 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:: ").
 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      := DataAlt 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:AltCon) : ???(@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 := LitAlt 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 := DEFAULT |} |}.
 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 weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(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 weakTypeToType'': ".
 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 weakTypeToType'' φ wev ★  with
 436                                   | Error _ =>  []
 437                                   | OK    t' => [((wev:CoreVar),t')]
 438                                 end
 439     | T_Branch b1 b2         => (varsTypes b1 φ),,(varsTypes b2 φ)
 440   end.
 441
 442
 443 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
 444 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
 445   | nil => match wtl with
 446              | nil => OK INil
 447              | _   => Error "length mismatch in mkAvars"
 448            end
 449   | k::lk' => match wtl with
 450                 | nil => Error "length mismatch in mkAvars"
 451                 | wt::wtl' =>
 452                   weakTypeToType'' φ wt k >>= fun t =>
 453                     mkAvars wtl' lk' φ >>= fun rest =>
 454                     OK (ICons _ _ t rest)
 455               end
 456 end.
 457
 458 Definition weakExprToStrongExpr : forall
 459     (Γ:TypeEnv)
 460     (Δ:CoercionEnv Γ)
 461     (φ:TyVarResolver Γ)
 462     (ψ:CoVarResolver Γ Δ)
 463     (ξ:CoreVar -> LeveledHaskType Γ ★)
 464     (τ:HaskType Γ ★)
 465     (lev:HaskLevel Γ),
 466     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
 467   refine ((
 468     fix weakExprToStrongExpr
 469     (Γ:TypeEnv)
 470     (Δ:CoercionEnv Γ)
 471     (φ:TyVarResolver Γ)
 472     (ψ:CoVarResolver Γ Δ)
 473     (ξ:CoreVar -> LeveledHaskType Γ ★)
 474     (τ:HaskType Γ ★)
 475     (lev:HaskLevel Γ)
 476     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
 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                  => weakTypeToType'' φ ev ★ >>= fun tv =>
 484                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
 485                                                weakTypeToType'' φ 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                                              weakTypeToType'' φ 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                                            weakTypeToType'' φ 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     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 504
 505     | WELet   v ve  ebody               => weakTypeToType'' φ v ★  >>= fun tv =>
 506                                              weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
 507                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
 508                                                >>= fun ebody' =>
 509                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 510
 511     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
 512                                              weakTypeToType'' φ t2 ★ >>= fun t2' =>
 513                                                weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
 514                                                  weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
 515                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 516
 517     | WETyLam tv e                      => let φ' := upφ tv φ in
 518                                              weakTypeOfWeakExpr e >>= fun te =>
 519                                                weakTypeToType'' φ' te ★ >>= fun τ' =>
 520                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
 521                                                     (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
 522                                                  >>= fun e' =>
 523                                                    castExpr we "WETyLam1" _ e' >>= fun e'' =>
 524                                                      castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
 525
 526     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
 527                                            match te with
 528                                              | WForAllTy wtv te' =>
 529                                                let φ' := upφ wtv φ in
 530                                                  weakTypeToType'' φ' te' ★ >>= fun te'' =>
 531                                                    weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
 532                                                      weakTypeToType'' φ t (wtv:Kind) >>= fun t' =>
 533                                                        castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
 534                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
 535                                            end
 536
 537     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
 538                                            match te with
 539                                              | WCoFunTy t1 t2 t3 =>
 540                                                weakTypeToType φ t1 >>= fun t1' =>
 541                                                  match t1' with
 542                                                    haskTypeOfSomeKind κ t1'' =>
 543                                                    weakTypeToType'' φ t2 κ >>= fun t2'' =>
 544                                                      weakTypeToType'' φ t3 ★ >>= fun t3'' =>
 545                                                        weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
 546                                                          castExpr we "WECoApp" _ e' >>= fun e'' =>
 547                                                            OK (ECoApp Γ Δ κ t1'' t2''
 548                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
 549                                                  end
 550                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++te)
 551                                            end
 552
 553     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
 554                                            weakTypeOfWeakExpr e >>= fun te =>
 555                                              weakTypeToType'' φ te ★ >>= fun te' =>
 556                                                weakTypeToType'' φ t1 cv >>= fun t1' =>
 557                                                  weakTypeToType'' φ t2 cv >>= fun t2' =>
 558                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
 559                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 560
 561     | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
 562                                              weakTypeToType'' φ t1 ★ >>= fun t1' =>
 563                                                weakTypeToType'' φ t2 ★ >>= fun t2' =>
 564                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
 565                                                      castExpr we "WECast" _
 566                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 567
 568     | WELetRec rb   e                   =>
 569       let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
 570       in let binds :=
 571         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
 572           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
 573         match t with
 574           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
 575           | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
 576           | T_Branch b1 b2        =>
 577             binds b1 >>= fun b1' =>
 578               binds b2 >>= fun b2' =>
 579                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
 580         end) rb
 581       in binds >>= fun binds' =>
 582            weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
 583              OK (ELetRec Γ Δ ξ lev τ _ binds' e')
 584
 585     | WECase vscrut ve tbranches tc avars alts =>
 586         weakTypeToType'' φ (vscrut:WeakType) ★  >>= fun tv =>
 587           weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
 588             let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
 589               mkAvars avars (tyConKind tc) φ >>= fun avars' =>
 590                 weakTypeToType'' φ tbranches ★  >>= fun tbranches' =>
 591                   (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
 592                       ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
 593                         Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) :=
 594                     match t with
 595                       | T_Leaf None           => OK []
 596                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
 597                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
 598                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
 599                           >>= fun exprvars' =>
 600                             let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
 601                               weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
 602                               (sacpj_ψ sac _ _ avars' ψ)
 603                               (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
 604                                 let case_case := tt in OK [ _ ]
 605                       | T_Branch b1 b2        =>
 606                         mkTree b1 >>= fun b1' =>
 607                           mkTree b2 >>= fun b2' =>
 608                             OK (b1',,b2')
 609                     end) alts >>= fun tree =>
 610                   castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
 611                       castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
 612                         >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
 613
 614
 615
 616     end)).
 617
 618     destruct case_some.
 619     apply (addErrorMessage "case_some").
 620       simpl.
 621       destruct (weakTypeToType'' φ wev ★); try apply (Error error_message).
 622       matchThings h (unlev (ξ' wev)) "LetRec".
 623       destruct wev.
 624       rewrite matchTypeVars_pf.
 625       clear matchTypeVars_pf.
 626       set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
 627       destruct e''; try apply (Error error_message).
 628       apply OK.
 629       apply ELR_leaf.
 630       apply e1.
 631
 632     destruct case_case.
 633       exists scb.
 634       apply ebranch'.
 635
 636     Defined.
 637