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