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     set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.
 161     destruct k1';
 162       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
 163         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
 164       apply (Error ("Kind mismatch in WAppTy: "+++err)).
 165
 166   destruct case_weakTypeListToTypeList.
 167     apply (addErrorMessage "case_weakTypeListToTypeList").
 168     destruct t' as [ k' t' ].
 169     matchThings k k' "Kind mismatch in weakTypeListToTypeList".
 170     subst.
 171     apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
 172
 173   destruct case_WTyFunApp.
 174     apply (addErrorMessage "case_WTyFunApp").
 175     apply OK.
 176     eapply haskTypeOfSomeKind.
 177     unfold HaskType; intros.
 178     apply TyFunApp.
 179     apply lt'.
 180     apply X.
 181
 182   destruct case_WTyCon.
 183     apply (addErrorMessage "case_WTyCon").
 184     apply OK.
 185     eapply haskTypeOfSomeKind.
 186     unfold HaskType; intros.
 187     apply (TCon tc).
 188
 189   destruct case_WCodeTy.
 190     apply (addErrorMessage "case_WCodeTy").
 191     destruct tbody'.
 192     matchThings κ ★ "Kind mismatch in WCodeTy: ".
 193     apply OK.
 194     eapply haskTypeOfSomeKind.
 195     unfold HaskType; intros.
 196     apply TCode.
 197     apply (TVar (ec' TV X)).
 198     subst.
 199     apply h.
 200     apply X.
 201
 202   destruct case_WCoFunTy.
 203     apply (addErrorMessage "case_WCoFunTy").
 204     destruct t1' as [ k1' t1' ].
 205     destruct t2' as [ k2' t2' ].
 206     destruct t3' as [ k3' t3' ].
 207     matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
 208     subst.
 209     matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
 210     subst.
 211     apply OK.
 212     apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
 213
 214   destruct case_WForAllTy.
 215     apply (addErrorMessage "case_WForAllTy").
 216     destruct t1.
 217     matchThings ★  κ "Kind mismatch in WForAllTy: ".
 218     subst.
 219     apply OK.
 220     apply (@haskTypeOfSomeKind _ ★).
 221     apply (@mkTAll wtv).
 222     apply h.
 223     Defined.
 224
 225
 226 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
 227
 228 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 229 Section StrongAltCon.
 230   Context (tc : TyCon)(dc:DataCon tc).
 231
 232 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
 233  -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
 234   intro avars.
 235   intro ct.
 236   apply (addErrorMessage "weakTypeToType'").
 237   set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
 238   set (@substφ _ _ avars') as q.
 239   set (upφ' (tyConTyVars tc)  (mkPhi (dataConExTyVars dc))) as φ'.
 240   set (@weakTypeToType _ φ' ct) as t.
 241   destruct t as [|t]; try apply (Error error_message).
 242   destruct t as [tk t].
 243   matchThings tk ★ "weakTypeToType'".
 244   subst.
 245   apply OK.
 246   set (@weakT'' _ Γ _ t) as t'.
 247   set (@lamer _ _ _ _ t') as t''.
 248   fold (tyConKinds tc) in t''.
 249   fold (dataConExKinds dc) in t''.
 250   apply q.
 251   clear q.
 252   unfold tyConKinds.
 253   unfold dataConExKinds.
 254   rewrite <- vec2list_map_list2vec.
 255   rewrite <- vec2list_map_list2vec.
 256   rewrite vec2list_list2vec.
 257   rewrite vec2list_list2vec.
 258   apply t''.
 259   Defined.
 260
 261 Definition mkStrongAltCon : @StrongAltCon tc.
 262   refine
 263    {| sac_altcon      := DataAlt dc
 264     ; sac_numCoerVars := length (dataConCoerKinds dc)
 265     ; sac_numExprVars := length (dataConFieldTypes dc)
 266     ; sac_ekinds      := dataConExKinds dc
 267     ; sac_coercions   := fun Γ avars => let case_sac_coercions := tt in _
 268     ; sac_types       := fun Γ avars => let case_sac_types := tt in _
 269     |}.
 270
 271   destruct case_sac_coercions.
 272     refine (vec_map _ (list2vec (dataConCoerKinds dc))).
 273     intro.
 274     destruct X.
 275     unfold tyConKind in avars.
 276     set (@weakTypeToType' Γ) as q.
 277     unfold tyConKinds in q.
 278     rewrite <- vec2list_map_list2vec in q.
 279     rewrite vec2list_list2vec in q.
 280     apply (
 281       match
 282         q avars w >>= fun t1 =>
 283         q avars w0 >>= fun t2 =>
 284           OK (mkHaskCoercionKind t1 t2)
 285       with
 286         | Error s => Prelude_error s
 287         | OK y => y
 288       end).
 289
 290   destruct case_sac_types.
 291     refine (vec_map _ (list2vec (dataConFieldTypes dc))).
 292     intro X.
 293     unfold tyConKind in avars.
 294     set (@weakTypeToType' Γ) as q.
 295     unfold tyConKinds in q.
 296     rewrite <- vec2list_map_list2vec in q.
 297     rewrite vec2list_list2vec in q.
 298     set (q avars X) as y.
 299     apply (match y with
 300              | Error s =>Prelude_error s
 301              | OK y' => y'
 302            end).
 303     Defined.
 304
 305
 306 Lemma weakCV' : forall {Γ}{Δ} Γ',
 307    HaskCoVar Γ Δ
 308    -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
 309   intros.
 310   unfold HaskCoVar in *.
 311   intros; apply (X TV CV).
 312   apply ilist_chop' in env; auto.
 313   unfold InstantiatedCoercionEnv in *.
 314   unfold weakCK'' in cenv.
 315   destruct Γ'.
 316   rewrite <- map_preserves_length in cenv.
 317   apply cenv.
 318   rewrite <- map_preserves_length in cenv.
 319   apply cenv.
 320   Defined.
 321
 322 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
 323     refine
 324      {| sacpj_sac     := mkStrongAltCon
 325       ; sacpj_φ       := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
 326       ; sacpj_ψ       :=
 327       fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
 328       |}.
 329     intro.
 330     unfold sac_Γ.
 331     unfold HaskCoVar in *.
 332     intros.
 333     apply (x TV CV env).
 334     simpl in cenv.
 335     unfold sac_Δ in *.
 336     unfold InstantiatedCoercionEnv in *.
 337     apply vec_chop' in cenv.
 338     apply cenv.
 339     Defined.
 340
 341   Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
 342     intros.
 343     induction Δ.
 344     reflexivity.
 345     simpl.
 346     rewrite IHΔ.
 347     reflexivity.
 348     Qed.
 349
 350 End StrongAltCon.
 351
 352 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
 353   destruct alt.
 354   set (c:DataCon _) as dc.
 355   set ((dataConTyCon c):TyCon) as tc' in *.
 356   set (eqd_dec tc tc') as eqpf; destruct eqpf;
 357     [ idtac
 358       | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
 359   apply OK.
 360   eapply mkStrongAltConPlusJunk.
 361   simpl in *.
 362   apply dc.
 363
 364   apply OK; refine {| sacpj_sac := {|
 365                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 366                     ; sac_altcon := LitAlt h
 367                     |} |}.
 368             intro; intro φ; apply φ.
 369             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 370             rewrite weakCK'_nil_inert. apply ψ.
 371   apply OK; refine {| sacpj_sac := {|
 372                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 373                       ; sac_altcon := DEFAULT |} |}.
 374             intro; intro φ; apply φ.
 375             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 376             rewrite weakCK'_nil_inert. apply ψ.
 377 Defined.
 378
 379 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
 380   fun wev => match wev with weakExprVar _ t => t end.
 381   Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
 382
 383 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
 384
 385 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
 386   WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
 387   intros.
 388   refine (ψ X >>= _).
 389   unfold HaskCoVar.
 390   intros.
 391   apply OK.
 392   intros.
 393   inversion cenv; auto.
 394   Defined.
 395
 396 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
 397 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
 398   : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
 399   apply (addErrorMessage ("castExpr " +++ err_msg)).
 400   intros.
 401   destruct τ  as [τ  l].
 402   destruct τ' as [τ' l'].
 403   destruct (eqd_dec l l'); [ idtac
 404     | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
 405                     "  got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
 406                     "  wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
 407     )) ].
 408   destruct (eqd_dec τ τ'); [ idtac
 409     | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
 410                     "  got: " +++τ+++eol+++
 411                     "  wanted: "+++τ'
 412     )) ].
 413   subst.
 414   apply OK.
 415   apply e.
 416   Defined.
 417
 418 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
 419   match wcv with weakCoerVar _ κ _ _ => κ end.
 420   Coercion coVarKind : WeakCoerVar >-> Kind.
 421
 422 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
 423   intros.
 424   set (weakTypeToType φ t) as wt.
 425   destruct wt; try apply (Error error_message).
 426   destruct h.
 427   matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
 428   subst.
 429   apply OK.
 430   apply h.
 431   Defined.
 432
 433 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
 434   match t with
 435     | T_Leaf None            => []
 436     | T_Leaf (Some (wev,e))  => match weakTypeToTypeOfKind φ wev ★ with
 437                                   | OK    t' => [((wev:CoreVar),t')]
 438                                   | _        => []
 439                                 end
 440     | T_Branch b1 b2         => (varsTypes b1 φ),,(varsTypes b2 φ)
 441   end.
 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                   weakTypeToTypeOfKind φ 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     addErrorMessage ("in weakExprToStrongExpr " +++ we)
 478     match we with
 479
 480     | WEVar   v                         => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
 481
 482     | WELit   lit                       => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
 483
 484     | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
 485                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
 486                                                weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 487                                                  let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
 488                                                    weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
 489                                                      castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
 490
 491     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
 492                                              weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 493                                                weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
 494                                                  castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
 495
 496     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
 497                                            weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 498                                            match lev with
 499                                              | nil       => Error "ill-leveled escapification"
 500                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e
 501                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
 502                                            end
 503
 504     | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
 505
 506     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 507
 508     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>
 509                                              weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
 510                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
 511                                                >>= fun ebody' =>
 512                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 513
 514     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
 515                                              weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 516                                                weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
 517                                                  weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
 518                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 519
 520     | WETyLam tv e                      => let φ' := upφ tv φ in
 521                                              weakTypeOfWeakExpr e >>= fun te =>
 522                                                weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
 523                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
 524                                                     (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
 525                                                  >>= fun e' =>
 526                                                    castExpr we "WETyLam1" _ e' >>= fun e'' =>
 527                                                      castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
 528
 529     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
 530                                            match te with
 531                                              | WForAllTy wtv te' =>
 532                                                let φ' := upφ wtv φ in
 533                                                  weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
 534                                                    weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
 535                                                      weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
 536                                                        castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
 537                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
 538                                            end
 539
 540     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
 541                                            match te with
 542                                              | WCoFunTy t1 t2 t3 =>
 543                                                weakTypeToType φ t1 >>= fun t1' =>
 544                                                  match t1' with
 545                                                    haskTypeOfSomeKind κ t1'' =>
 546                                                    weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
 547                                                      weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
 548                                                        weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
 549                                                          castExpr we "WECoApp" _ e' >>= fun e'' =>
 550                                                            OK (ECoApp Γ Δ κ t1'' t2''
 551                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
 552                                                  end
 553                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++te)
 554                                            end
 555
 556     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
 557                                            weakTypeOfWeakExpr e >>= fun te =>
 558                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
 559                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
 560                                                  weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
 561                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
 562                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 563
 564     | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
 565                                              weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
 566                                                weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 567                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
 568                                                      castExpr we "WECast" _
 569                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 570
 571     | WELetRec rb   e                   =>
 572       let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
 573       in let binds :=
 574         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
 575           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
 576         match t with
 577           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
 578           | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
 579           | T_Branch b1 b2        =>
 580             binds b1 >>= fun b1' =>
 581               binds b2 >>= fun b2' =>
 582                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
 583         end) rb
 584       in binds >>= fun binds' =>
 585            weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
 586              OK (ELetRec Γ Δ ξ lev τ _ binds' e')
 587
 588     | WECase vscrut ve tbranches tc avars alts =>
 589         weakTypeToTypeOfKind φ (vscrut:WeakType) ★  >>= fun tv =>
 590           weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
 591             let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
 592               mkAvars avars (tyConKind tc) φ >>= fun avars' =>
 593                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
 594                   (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
 595                       ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
 596                         Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) :=
 597                     match t with
 598                       | T_Leaf None           => OK []
 599                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
 600                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
 601                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
 602                           >>= fun exprvars' =>
 603                             let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
 604                               weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
 605                               (sacpj_ψ sac _ _ avars' ψ)
 606                               (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
 607                                 let case_case := tt in OK [ _ ]
 608                       | T_Branch b1 b2        =>
 609                         mkTree b1 >>= fun b1' =>
 610                           mkTree b2 >>= fun b2' =>
 611                             OK (b1',,b2')
 612                     end) alts >>= fun tree =>
 613                   castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
 614                       castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
 615                         >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
 616
 617
 618
 619     end)).
 620
 621     destruct case_some.
 622     apply (addErrorMessage "case_some").
 623       simpl.
 624       destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
 625       matchThings h (unlev (ξ' wev)) "LetRec".
 626       destruct wev.
 627       rewrite matchTypeVars_pf.
 628       clear matchTypeVars_pf.
 629       set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
 630       destruct e''; try apply (Error error_message).
 631       apply OK.
 632       apply ELR_leaf.
 633       apply e1.
 634
 635     destruct case_case.
 636       exists scb.
 637       apply ebranch'.
 638
 639     Defined.
 640