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