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 Require Import HaskCoreToWeak.
  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 _
  32     else 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 (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
  75                 (WeakCoerVar -> HaskCoVar _ (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 _
 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' => _
 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 (φ (@fixkind ★ 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 => weakV' (φ htv))
 316       ; sacpj_ψ       := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
 317       |}.
 318     intro.
 319     unfold sac_Γ.
 320     unfold HaskCoVar in *.
 321     intros.
 322     apply (x TV CV env).
 323     simpl in cenv.
 324     unfold sac_Δ in *.
 325     unfold InstantiatedCoercionEnv in *.
 326     apply vec_chop' in cenv.
 327     apply cenv.
 328     Defined.
 329
 330   Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
 331     intros.
 332     induction Δ.
 333     reflexivity.
 334     simpl.
 335     rewrite IHΔ.
 336     reflexivity.
 337     Qed.
 338
 339 End StrongAltCon.
 340
 341 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
 342   destruct alt.
 343   set (c:DataCon _) as dc.
 344   set ((dataConTyCon c):TyCon) as tc' in *.
 345   set (eqd_dec tc tc') as eqpf; destruct eqpf;
 346     [ idtac
 347       | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
 348   apply OK.
 349   eapply mkStrongAltConPlusJunk.
 350   simpl in *.
 351   apply dc.
 352
 353   apply OK; refine {| sacpj_sac := {|
 354                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 355                     ; sac_altcon := LitAlt h
 356                     |} |}.
 357             intro; intro φ; apply φ.
 358             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 359             rewrite weakCK'_nil_inert. apply ψ.
 360   apply OK; refine {| sacpj_sac := {|
 361                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 362                       ; sac_altcon := DEFAULT |} |}.
 363             intro; intro φ; apply φ.
 364             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 365             rewrite weakCK'_nil_inert. apply ψ.
 366 Defined.
 367
 368 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
 369   fun wev => match wev with weakExprVar _ t => t end.
 370   Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
 371
 372 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
 373
 374 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
 375   WeakCoerVar -> HaskCoVar Γ (κ::Δ).
 376   intros.
 377   unfold HaskCoVar.
 378   intros.
 379   apply (ψ X TV CV env).
 380   inversion cenv; auto.
 381   Defined.
 382
 383 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
 384 Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
 385   : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
 386   intros.
 387   destruct τ  as [τ  l].
 388   destruct τ' as [τ' l'].
 389   destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ].
 390   destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ].
 391   subst.
 392   apply OK.
 393   apply e.
 394   Defined.
 395
 396 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
 397   match wcv with weakCoerVar _ κ _ _ => κ end.
 398   Coercion coVarKind : WeakCoerVar >-> Kind.
 399
 400 Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
 401   intros.
 402   set (weakTypeToType φ t) as wt.
 403   destruct wt; try apply (Error error_message).
 404   destruct h.
 405   matchThings κ κ0 "Kind mismatch in weakTypeToType'': ".
 406   subst.
 407   apply OK.
 408   apply h.
 409   Defined.
 410
 411 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
 412   match t with
 413     | T_Leaf None            => []
 414     | T_Leaf (Some (wev,e))  => match weakTypeToType'' φ wev ★  with
 415                                   | Error _ =>  []
 416                                   | OK    t' => [((wev:CoreVar),t')]
 417                                 end
 418     | T_Branch b1 b2         => (varsTypes b1 φ),,(varsTypes b2 φ)
 419   end.
 420
 421
 422 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
 423 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
 424   | nil => match wtl with
 425              | nil => OK INil
 426              | _   => Error "length mismatch in mkAvars"
 427            end
 428   | k::lk' => match wtl with
 429                 | nil => Error "length mismatch in mkAvars"
 430                 | wt::wtl' =>
 431                   weakTypeToType'' φ wt k >>= fun t =>
 432                     mkAvars wtl' lk' φ >>= fun rest =>
 433                     OK (ICons _ _ t rest)
 434               end
 435 end.
 436
 437 Definition weakExprToStrongExpr : forall
 438     (Γ:TypeEnv)
 439     (Δ:CoercionEnv Γ)
 440     (φ:TyVarResolver Γ)
 441     (ψ:CoVarResolver Γ Δ)
 442     (ξ:CoreVar -> LeveledHaskType Γ ★)
 443     (τ:HaskType Γ ★)
 444     (lev:HaskLevel Γ),
 445     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
 446   refine ((
 447     fix weakExprToStrongExpr
 448     (Γ:TypeEnv)
 449     (Δ:CoercionEnv Γ)
 450     (φ:TyVarResolver Γ)
 451     (ψ:CoVarResolver Γ Δ)
 452     (ξ:CoreVar -> LeveledHaskType Γ ★)
 453     (τ:HaskType Γ ★)
 454     (lev:HaskLevel Γ)
 455     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
 456     match we with
 457
 458     | WEVar   v                         => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v)
 459
 460     | WELit   lit                       => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev)
 461
 462     | WELam   ev e                      => weakTypeToType'' φ ev ★ >>= fun tv =>
 463                                              weakTypeOfWeakExpr e >>= fun t =>
 464                                                weakTypeToType'' φ t ★ >>= fun τ' =>
 465                                                  weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((ev:CoreVar),tv@@lev)::nil))
 466                                                     τ' _ e >>= fun e' =>
 467                                                    castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
 468
 469     | WEBrak  _ ec e tbody              => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
 470                                              castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
 471
 472     | WEEsc   _ ec e tbody              => weakTypeToType'' φ tbody ★ >>= fun tbody' =>
 473                                            match lev with
 474                                              | nil       => Error "ill-leveled escapification"
 475                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e
 476                                                >>= fun e' =>
 477                                                               castExpr "WEEsc" (τ@@lev) (EEsc _ _ _ (φ (`ec)) _ lev e')
 478                                            end
 479     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 480
 481     | WELet   v ve  ebody               => weakTypeToType'' φ v ★  >>= fun tv =>
 482                                              weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
 483                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
 484                                                >>= fun ebody' =>
 485                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 486
 487     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
 488                                              weakTypeToType'' φ t2 ★ >>= fun t2' =>
 489                                                weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
 490                                                  weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
 491                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 492
 493     | WETyLam tv e                      => let φ' := upφ tv φ in
 494                                              weakTypeOfWeakExpr e >>= fun te =>
 495                                                weakTypeToType'' φ' te ★ >>= fun τ' =>
 496                                                  weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e
 497                                                  >>= fun e' =>
 498                                                    castExpr "WETyLam1" _ e' >>= fun e'' =>
 499                                                      castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
 500
 501     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
 502                                            match te with
 503                                              | WForAllTy wtv te' =>
 504                                                let φ' := upφ wtv φ in
 505                                                  weakTypeToType'' φ' te' ★ >>= fun te'' =>
 506                                                    weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
 507                                                      weakTypeToType'' φ t wtv >>= fun t' =>
 508                                                        castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
 509                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
 510                                            end
 511
 512     (* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two
 513      * to get them back working again *)
 514     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
 515                                            match te with
 516                                              | WCoFunTy t1 t2 t3 =>
 517                                                weakTypeToType φ t1 >>= fun t1' =>
 518                                                  match t1' with
 519                                                    haskTypeOfSomeKind κ t1'' =>
 520                                                    weakTypeToType'' φ t2 κ >>= fun t2'' =>
 521                                                      weakTypeToType'' φ t3 ★ >>= fun t3'' =>
 522                                                        weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
 523                                                          castExpr "WECoApp" _ e' >>= fun e'' =>
 524                                                            OK (ECoApp Γ Δ κ t1'' t2''
 525                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
 526                                                  end
 527                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++te)
 528                                            end
 529
 530     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
 531                                            weakTypeOfWeakExpr e >>= fun te =>
 532                                              weakTypeToType'' φ te ★ >>= fun te' =>
 533                                                weakTypeToType'' φ t1 cv >>= fun t1' =>
 534                                                  weakTypeToType'' φ t2 cv >>= fun t2' =>
 535                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
 536                                                      castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 537
 538     | WECast  e co                      => let (κ,t1,t2,_) := co in
 539                                              weakTypeToType'' φ t1 ★ >>= fun t1' =>
 540                                                weakTypeToType'' φ t2 ★ >>= fun t2' =>
 541                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
 542                                                      castExpr "WECast" _
 543                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 544
 545     | WELetRec rb   e                   =>
 546       let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
 547       in let binds :=
 548         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
 549           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
 550         match t with
 551           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
 552           | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
 553           | T_Branch b1 b2        =>
 554             binds b1 >>= fun b1' =>
 555               binds b2 >>= fun b2' =>
 556                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
 557         end) rb
 558       in binds >>= fun binds' =>
 559            weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
 560              OK (ELetRec Γ Δ ξ lev τ _ binds' e')
 561
 562     | WECase vscrut e tbranches tc avars alts =>
 563       mkAvars avars (tyConKind tc) φ >>= fun avars' =>
 564       weakTypeToType'' φ tbranches ★  >>= fun tbranches' =>
 565           let ξ' := update_ξ ξ (((vscrut:CoreVar), _ @@lev)::nil) in
 566 (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
 567      ??{scb
 568        : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars'
 569        &
 570        Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))
 571          (scbwv_ξ scb ξ' lev) (weakLT' (tbranches' @@  lev))}) :=
 572         match t with
 573           | T_Leaf None           => OK []
 574           | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
 575             mkStrongAltConPlusJunk' tc ac >>= fun sac =>
 576               list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") >>= fun exprvars' =>
 577                 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
 578                   weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ)
 579             (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
 580             let case_case := tt in OK [ _ ]
 581           | T_Branch b1 b2        =>
 582             mkTree b1 >>= fun b1' =>
 583               mkTree b2 >>= fun b2' =>
 584                 OK (b1',,b2')
 585         end
 586 ) alts >>= fun tree =>
 587         weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' =>
 588           castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun evar =>
 589             castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' evar tree) >>= fun ecase' =>
 590               OK (ELet _ _ _ _ _ lev (vscrut:CoreVar) e' ecase')
 591     end)).
 592
 593     destruct case_some.
 594       simpl.
 595       destruct (weakTypeToType'' φ wev ★); try apply (Error error_message).
 596       matchThings h (unlev (ξ' wev)) "LetRec".
 597       destruct wev.
 598       rewrite matchTypeVars_pf.
 599       clear matchTypeVars_pf.
 600       set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
 601       destruct e''; try apply (Error error_message).
 602       apply OK.
 603       apply ELR_leaf.
 604       apply e1.
 605
 606     destruct case_case.
 607       clear mkTree t o p e p0 p1 p2 alts weakExprToStrongExpr ebranch.
 608       exists scb.
 609       apply ebranch'.
 610     Defined.
 611