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