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 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 228 Section StrongAltCon.
 229   Context (tc : TyCon)(dc:DataCon tc).
 230
 231 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
 232  -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
 233   intro avars.
 234   intro ct.
 235   apply (addErrorMessage "weakTypeToType'").
 236   set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
 237   set (@substφ _ _ avars') as q.
 238   set (upφ' (tyConTyVars tc)  (mkPhi (dataConExTyVars dc))) as φ'.
 239   set (@weakTypeToType _ φ' ct) as t.
 240   destruct t as [|t]; try apply (Error error_message).
 241   destruct t as [tk t].
 242   matchThings tk ★ "weakTypeToType'".
 243   subst.
 244   apply OK.
 245   set (@weakT'' _ Γ _ t) as t'.
 246   set (@lamer _ _ _ _ t') as t''.
 247   fold (tyConKinds tc) in t''.
 248   fold (dataConExKinds dc) in t''.
 249   apply q.
 250   clear q.
 251   unfold tyConKinds.
 252   unfold dataConExKinds.
 253   rewrite <- vec2list_map_list2vec.
 254   rewrite <- vec2list_map_list2vec.
 255   rewrite vec2list_list2vec.
 256   rewrite vec2list_list2vec.
 257   apply t''.
 258   Defined.
 259
 260 Definition mkStrongAltCon : @StrongAltCon tc.
 261   refine
 262    {| sac_altcon      := WeakDataAlt dc
 263     ; sac_numCoerVars := length (dataConCoerKinds dc)
 264     ; sac_numExprVars := length (dataConFieldTypes dc)
 265     ; sac_ekinds      := dataConExKinds dc
 266     ; sac_coercions   := fun Γ avars => let case_sac_coercions := tt in _
 267     ; sac_types       := fun Γ avars => let case_sac_types := tt in _
 268     |}.
 269
 270   destruct case_sac_coercions.
 271     refine (vec_map _ (list2vec (dataConCoerKinds dc))).
 272     intro.
 273     destruct X.
 274     unfold tyConKind in avars.
 275     set (@weakTypeToType' Γ) as q.
 276     unfold tyConKinds in q.
 277     rewrite <- vec2list_map_list2vec in q.
 278     rewrite vec2list_list2vec in q.
 279     apply (
 280       match
 281         q avars w >>= fun t1 =>
 282         q avars w0 >>= fun t2 =>
 283           OK (mkHaskCoercionKind t1 t2)
 284       with
 285         | Error s => Prelude_error s
 286         | OK y => y
 287       end).
 288
 289   destruct case_sac_types.
 290     refine (vec_map _ (list2vec (dataConFieldTypes dc))).
 291     intro X.
 292     unfold tyConKind in avars.
 293     set (@weakTypeToType' Γ) as q.
 294     unfold tyConKinds in q.
 295     rewrite <- vec2list_map_list2vec in q.
 296     rewrite vec2list_list2vec in q.
 297     set (q avars X) as y.
 298     apply (match y with
 299              | Error s =>Prelude_error s
 300              | OK y' => y'
 301            end).
 302     Defined.
 303
 304
 305 Lemma weakCV' : forall {Γ}{Δ} Γ',
 306    HaskCoVar Γ Δ
 307    -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
 308   intros.
 309   unfold HaskCoVar in *.
 310   intros; apply (X TV CV).
 311   apply ilist_chop' in env; auto.
 312   unfold InstantiatedCoercionEnv in *.
 313   unfold weakCK'' in cenv.
 314   destruct Γ'.
 315   rewrite <- map_preserves_length in cenv.
 316   apply cenv.
 317   rewrite <- map_preserves_length in cenv.
 318   apply cenv.
 319   Defined.
 320
 321 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
 322     refine
 323      {| sacpj_sac     := mkStrongAltCon
 324       ; sacpj_φ       := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
 325       ; sacpj_ψ       :=
 326       fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
 327       |}.
 328     intro.
 329     unfold sac_Γ.
 330     unfold HaskCoVar in *.
 331     intros.
 332     apply (x TV CV env).
 333     simpl in cenv.
 334     unfold sac_Δ in *.
 335     unfold InstantiatedCoercionEnv in *.
 336     apply vec_chop' in cenv.
 337     apply cenv.
 338     Defined.
 339
 340   Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
 341     intros.
 342     induction Δ.
 343     reflexivity.
 344     simpl.
 345     rewrite IHΔ.
 346     reflexivity.
 347     Qed.
 348
 349 End StrongAltCon.
 350
 351 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
 352   destruct alt.
 353   set (c:DataCon _) as dc.
 354   set ((dataConTyCon c):TyCon) as tc' in *.
 355   set (eqd_dec tc tc') as eqpf; destruct eqpf;
 356     [ idtac
 357       | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
 358   apply OK.
 359   eapply mkStrongAltConPlusJunk.
 360   simpl in *.
 361   apply dc.
 362
 363   apply OK; refine {| sacpj_sac := {|
 364                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 365                     ; sac_altcon := WeakLitAlt h
 366                     |} |}.
 367             intro; intro φ; apply φ.
 368             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 369             rewrite weakCK'_nil_inert. apply ψ.
 370   apply OK; refine {| sacpj_sac := {|
 371                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 372                       ; sac_altcon := WeakDEFAULT |} |}.
 373             intro; intro φ; apply φ.
 374             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
 375             rewrite weakCK'_nil_inert. apply ψ.
 376 Defined.
 377
 378 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
 379   fun wev => match wev with weakExprVar _ t => t end.
 380   Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
 381
 382 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
 383
 384 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
 385   WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
 386   intros.
 387   refine (ψ X >>= _).
 388   unfold HaskCoVar.
 389   intros.
 390   apply OK.
 391   intros.
 392   inversion cenv; auto.
 393   Defined.
 394
 395 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
 396 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
 397   : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
 398   apply (addErrorMessage ("castExpr " +++ err_msg)).
 399   intros.
 400   destruct τ  as [τ  l].
 401   destruct τ' as [τ' l'].
 402   destruct (eqd_dec l l'); [ idtac
 403     | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
 404                     "  got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
 405                     "  wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
 406     )) ].
 407   destruct (eqd_dec τ τ'); [ idtac
 408     | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
 409                     "  got: " +++τ+++eol+++
 410                     "  wanted: "+++τ'
 411     )) ].
 412   subst.
 413   apply OK.
 414   apply e.
 415   Defined.
 416
 417 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
 418   match wcv with weakCoerVar _ κ _ _ => κ end.
 419   Coercion coVarKind : WeakCoerVar >-> Kind.
 420
 421 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
 422   intros.
 423   set (weakTypeToType φ t) as wt.
 424   destruct wt; try apply (Error error_message).
 425   destruct h.
 426   matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
 427   subst.
 428   apply OK.
 429   apply h.
 430   Defined.
 431
 432 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
 433   match t with
 434     | T_Leaf None            => []
 435     | T_Leaf (Some (wev,e))  => match weakTypeToTypeOfKind φ wev ★ with
 436                                   | OK    t' => [((wev:CoreVar),t')]
 437                                   | _        => []
 438                                 end
 439     | T_Branch b1 b2         => (varsTypes b1 φ),,(varsTypes b2 φ)
 440   end.
 441
 442 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
 443 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
 444   | nil => match wtl with
 445              | nil => OK INil
 446              | _   => Error "length mismatch in mkAvars"
 447            end
 448   | k::lk' => match wtl with
 449                 | nil => Error "length mismatch in mkAvars"
 450                 | wt::wtl' =>
 451                   weakTypeToTypeOfKind φ wt k >>= fun t =>
 452                     mkAvars wtl' lk' φ >>= fun rest =>
 453                     OK (ICons _ _ t rest)
 454               end
 455 end.
 456
 457 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
 458   match vars with
 459     | nil => ig
 460     | v::vars' =>
 461       fun v' =>
 462         if eqd_dec v v'
 463           then false
 464             else update_ig ig vars' v'
 465   end.
 466
 467 (* does the specified variable occur free in the expression? *)
 468 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
 469   match me with
 470     | WELit    _        => false
 471     | WEVar    cv       => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
 472     | WECast   e co     =>                            doesWeakVarOccur wev e
 473     | WENote   n e      =>                            doesWeakVarOccur wev e
 474     | WETyApp  e t      =>                            doesWeakVarOccur wev e
 475     | WECoApp  e co     =>                            doesWeakVarOccur wev e
 476     | WEBrak _ ec e _   =>                            doesWeakVarOccur wev e
 477     | WEEsc  _ ec e _   =>                            doesWeakVarOccur wev e
 478     | WECSP  _ ec e _   =>                            doesWeakVarOccur wev e
 479     | WELet    cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
 480     | WEApp    e1 e2    => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
 481     | WELam    cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
 482     | WETyLam  cv e     => doesWeakVarOccur wev e
 483     | WECoLam  cv e     => doesWeakVarOccur wev e
 484     | WECase vscrut escrut tbranches tc avars alts =>
 485       doesWeakVarOccur wev escrut ||
 486       if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
 487         ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
 488           match alts with
 489             | T_Leaf  None                                         => false
 490             | T_Leaf (Some (WeakDEFAULT,_,_,_,e))                      => doesWeakVarOccur wev e
 491             | T_Leaf (Some (WeakLitAlt lit,_,_,_,e))                   => doesWeakVarOccur wev e
 492             | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e))  => doesWeakVarOccur wev e  (* FIXME!!! *)
 493             | T_Branch b1 b2                                       => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
 494           end) alts)
 495     | WELetRec mlr e =>
 496       doesWeakVarOccur wev e ||
 497       (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
 498       match mlr with
 499         | T_Leaf None          => false
 500         | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
 501         | T_Branch b1 b2       => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
 502       end) mlr
 503   end.
 504 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
 505   (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
 506   match alts with
 507     | T_Leaf  None                                             => false
 508     | T_Leaf (Some (WeakDEFAULT,_,_,_,e))                      => doesWeakVarOccur wev e
 509     | T_Leaf (Some (WeakLitAlt lit,_,_,_,e))                   => doesWeakVarOccur wev e
 510     | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e))  => doesWeakVarOccur wev e  (* FIXME!!! *)
 511     | T_Branch b1 b2                                           => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
 512   end.
 513
 514 (*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
 515
 516 Definition weakExprToStrongExpr : forall
 517     (Γ:TypeEnv)
 518     (Δ:CoercionEnv Γ)
 519     (φ:TyVarResolver Γ)
 520     (ψ:CoVarResolver Γ Δ)
 521     (ξ:CoreVar -> LeveledHaskType Γ ★)
 522     (ig:CoreVar -> bool)
 523     (τ:HaskType Γ ★)
 524     (lev:HaskLevel Γ),
 525     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
 526   refine ((
 527     fix weakExprToStrongExpr
 528     (Γ:TypeEnv)
 529     (Δ:CoercionEnv Γ)
 530     (φ:TyVarResolver Γ)
 531     (ψ:CoVarResolver Γ Δ)
 532     (ξ:CoreVar -> LeveledHaskType Γ ★)
 533     (ig:CoreVar -> bool)
 534     (τ:HaskType Γ ★)
 535     (lev:HaskLevel Γ)
 536     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
 537     addErrorMessage ("in weakExprToStrongExpr " +++ we)
 538     match we with
 539
 540     | WEVar   v                         => if ig v
 541                                               then OK (EGlobal Γ Δ ξ (τ@@lev) v)
 542                                               else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
 543
 544     | WELit   lit                       => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
 545
 546     | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
 547                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
 548                                                weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 549                                                  let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
 550                                                  let ig' := update_ig ig ((ev:CoreVar)::nil) in
 551                                                    weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
 552                                                      castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
 553
 554     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
 555                                              weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 556                                                weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
 557                                                  castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
 558
 559     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
 560                                            weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 561                                            match lev with
 562                                              | nil       => Error "ill-leveled escapification"
 563                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
 564                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
 565                                            end
 566
 567     | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
 568
 569     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 570
 571     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>
 572                                              weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
 573                                                weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
 574                                                     (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
 575                                                >>= fun ebody' =>
 576                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 577
 578     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
 579                                              weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 580                                                weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
 581                                                  weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
 582                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 583
 584     | WETyLam tv e                      => let φ' := upφ tv φ in
 585                                              weakTypeOfWeakExpr e >>= fun te =>
 586                                                weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
 587                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
 588                                                    (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
 589                                                      >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
 590
 591     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
 592                                            match te with
 593                                              | WForAllTy wtv te' =>
 594                                                let φ' := upφ wtv φ in
 595                                                  weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
 596                                                    weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
 597                                                      weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
 598                                                        castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
 599                                              | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
 600                                            end
 601
 602     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
 603                                            match te with
 604                                              | WCoFunTy t1 t2 t3 =>
 605                                                weakTypeToType φ t1 >>= fun t1' =>
 606                                                  match t1' with
 607                                                    haskTypeOfSomeKind κ t1'' =>
 608                                                    weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
 609                                                      weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
 610                                                        weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
 611                                                          castExpr we "WECoApp" _ e' >>= fun e'' =>
 612                                                            OK (ECoApp Γ Δ κ t1'' t2''
 613                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
 614                                                  end
 615                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++te)
 616                                            end
 617
 618     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
 619                                            weakTypeOfWeakExpr e >>= fun te =>
 620                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
 621                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
 622                                                  weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
 623                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
 624                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 625
 626     | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
 627                                              weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
 628                                                weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
 629                                                    weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
 630                                                      castExpr we "WECast" _
 631                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 632
 633     | WELetRec rb   e                   =>
 634       let ξ' := update_ξ ξ lev _ in
 635       let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
 636       let binds :=
 637         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
 638           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
 639         match t with
 640           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
 641           | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
 642           | T_Branch b1 b2        =>
 643             binds b1 >>= fun b1' =>
 644               binds b2 >>= fun b2' =>
 645                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
 646         end) rb
 647       in binds >>= fun binds' =>
 648            weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
 649              OK (ELetRec Γ Δ ξ lev τ _ binds' e')
 650
 651     | WECase vscrut escrut tbranches tc avars alts =>
 652         weakTypeOfWeakExpr escrut >>= fun tscrut =>
 653           weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
 654             if doesWeakVarOccurAlts vscrut alts
 655             then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
 656             else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
 657                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
 658                   (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
 659                       ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
 660                         Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@  lev))}}) :=
 661                     match t with
 662                       | T_Leaf None           => OK []
 663                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
 664                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
 665                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
 666                           >>= fun exprvars' =>
 667                             (let case_pf := tt in _) >>= fun pf =>
 668                             let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
 669                               weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
 670                               (sacpj_ψ sac _ _ avars' ψ)
 671                               (scbwv_ξ scb ξ lev)
 672                               (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
 673                               (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
 674                                 let case_case := tt in OK [ _ ]
 675                       | T_Branch b1 b2        =>
 676                         mkTree b1 >>= fun b1' =>
 677                           mkTree b2 >>= fun b2' =>
 678                             OK (b1',,b2')
 679                     end) alts >>= fun tree =>
 680
 681                     weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
 682                       castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
 683     end)); try clear binds.
 684
 685     destruct case_some.
 686     apply (addErrorMessage "case_some").
 687       simpl.
 688       destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
 689       matchThings h (unlev (ξ' wev)) "LetRec".
 690       destruct wev.
 691       rewrite matchTypeVars_pf.
 692       clear matchTypeVars_pf.
 693       set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
 694       destruct e''; try apply (Error error_message).
 695       apply OK.
 696       apply ELR_leaf.
 697       unfold ξ'.
 698       simpl.
 699       induction (leaves (varsTypes rb φ)).
 700         simpl; auto.
 701         destruct (ξ c).
 702         simpl.
 703       apply e1.
 704
 705     destruct case_pf.
 706       set (distinct_decidable (vec2list exprvars')) as dec.
 707       destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].
 708       apply OK; auto.
 709
 710     destruct case_case.
 711       exists sac.
 712       exists scb.
 713       apply ebranch'.
 714
 715     Defined.
 716