src/HaskSkolemizer.v

   1 (*********************************************************************************************************************************)
   2 (* HaskSkolemizer:                                                                                                               *)
   3 (*                                                                                                                               *)
   4 (*   Skolemizes the portion of a proof which uses judgments at level >0                                                          *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import NaturalDeductionContext.
  13 Require Import Coq.Strings.String.
  14 Require Import Coq.Lists.List.
  15
  16 Require Import HaskKinds.
  17 Require Import HaskCoreTypes.
  18 Require Import HaskCoreVars.
  19 Require Import HaskWeakTypes.
  20 Require Import HaskWeakVars.
  21 Require Import HaskLiterals.
  22 Require Import HaskTyCons.
  23 Require Import HaskStrongTypes.
  24 Require Import HaskProof.
  25 Require Import NaturalDeduction.
  26
  27 Require Import HaskStrongTypes.
  28 Require Import HaskStrong.
  29 Require Import HaskProof.
  30 Require Import HaskStrongToProof.
  31 Require Import HaskProofToStrong.
  32 Require Import HaskWeakToStrong.
  33
  34 Open Scope nd_scope.
  35 Set Printing Width 130.
  36
  37 Section HaskSkolemizer.
  38
  39 (*
  40   Fixpoint debruijn2phoas {κ} (exp: RawHaskType (fun _ => nat) κ) : HaskType TV κ :=
  41      match exp with
  42     | TVar    _  x          => x
  43     | TAll     _ y          => TAll   _  (fun v => debruijn2phoas  (y (TVar v)))
  44     | TApp   _ _ x y        => TApp      (debruijn2phoas  x) (debruijn2phoas  y)
  45     | TCon       tc         => TCon      tc
  46     | TCoerc _ t1 t2 t      => TCoerc    (debruijn2phoas  t1) (debruijn2phoas  t2)   (debruijn2phoas  t)
  47     | TArrow                => TArrow
  48     | TCode      v e        => TCode     (debruijn2phoas  v) (debruijn2phoas  e)
  49     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (debruijn2phoasyFunApp _ lt)
  50     end
  51     with debruijn2phoasyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun _ => nat) lk) : @HaskTypeList TV lk :=
  52     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
  53     | TyFunApp_nil               => TyFunApp_nil
  54     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (debruijn2phoas  t) (debruijn2phoasyFunApp _ rest)
  55     end.
  56 *)
  57   Definition isNotBrakOrEsc {h}{c} (r:Rule h c) : Prop :=
  58     match r with
  59       | RBrak _ _ _ _ _ _ => False
  60       | REsc  _ _ _ _ _ _ => False
  61       | _                 => True
  62     end.
  63
  64   Fixpoint mkArrows {Γ}(lt:list (HaskType Γ ★))(t:HaskType Γ ★) : HaskType Γ ★ :=
  65     match lt with
  66       | nil => t
  67       | a::b => mkArrows b (a ---> t)
  68     end.
  69
  70 (*
  71   Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
  72     match l with
  73       | nil  => t
  74       | a::b => unleaves_ (t,,[a @@ lev]) b lev
  75     end.
  76 *)
  77   (* weak inverse of "leaves" *)
  78   Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) :=
  79     match l with
  80       | nil      => []
  81       | (a::nil) => [a]
  82       | (a::b)   => [a],,(unleaves_ b)
  83     end.
  84
  85   (* rules of skolemized proofs *)
  86   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ @ _ => Γ end.
  87
  88   Fixpoint take_trustme {Γ}
  89     (n:nat)
  90     (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
  91     : list (HaskType Γ ★) :=
  92
  93     match n with
  94       | 0    => nil
  95       | S n' => (fun TV ite => match l TV ite with
  96                 | nil  => Prelude_error "impossible"
  97                 | a::b => a
  98                 end)
  99                 ::
 100                 take_trustme n' (fun TV ite => match l TV ite with
 101                 | nil  => Prelude_error "impossible"
 102                 | a::b => b
 103                 end)
 104     end.
 105
 106   Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
 107     (forall tv ite, f tv ite = g tv ite) -> f=g.
 108
 109   Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
 110     unleaves_
 111     (take_trustme
 112       (count_arg_types (ht _ (ite_unit _)))
 113       (fun TV ite => take_arg_types (ht TV ite))).
 114
 115   Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
 116     fun TV ite => drop_arg_types (ht TV ite).
 117
 118   Implicit Arguments take_arg_types_as_tree [[Γ]].
 119   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 120
 121   Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
 122     Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev)
 123       (take_arg_types_as_tree (tx ---> te) @@@ lev).
 124     intros.
 125     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
 126       rewrite <- e.
 127       simpl.
 128       apply AId.
 129     unfold take_arg_types_as_tree.
 130       Opaque take_arg_types_as_tree.
 131       simpl.
 132       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
 133       simpl.
 134       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
 135       apply ACanR.
 136         apply phoas_extensionality.
 137         reflexivity.
 138     apply (Prelude_error "should not be possible").
 139     Defined.
 140     Transparent take_arg_types_as_tree.
 141
 142   Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
 143     Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
 144       ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).
 145     intros.
 146     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
 147       rewrite <- e.
 148       simpl.
 149       apply AId.
 150     unfold take_arg_types_as_tree.
 151       Opaque take_arg_types_as_tree.
 152       simpl.
 153       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
 154       simpl.
 155       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
 156       apply AuCanR.
 157         apply phoas_extensionality.
 158         reflexivity.
 159     apply (Prelude_error "should not be possible").
 160     Defined.
 161     Transparent take_arg_types_as_tree.
 162
 163   Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
 164     drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
 165     intros.
 166     unfold drop_arg_types_as_tree.
 167     simpl.
 168     reflexivity.
 169     Qed.
 170
 171   Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
 172 (*  | SFlat  : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
 173   | SFlat  : forall h c, Rule h c -> SRule h c
 174   | SBrak  : forall Γ Δ t ec Σ l,
 175     SRule
 176     [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        ] @ (ec::l)]
 177     [Γ > Δ > Σ                                  |- [<[ec |- t]>                ] @l]
 178
 179   | SEsc   : forall Γ Δ t ec Σ l,
 180     SRule
 181     [Γ > Δ > Σ                                  |- [<[ec |- t]>                ] @l]
 182     [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t         ] @ (ec::l)]
 183     .
 184
 185   Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
 186     match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
 187
 188   Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
 189     match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
 190
 191   Definition skolemize_judgment (j:Judg) : Judg :=
 192     match j with
 193       | Γ > Δ > Σ₁ |- Σ₂ @ nil       => j
 194         | Γ > Δ > Σ₁ |- Σ₂ @ lev =>
 195           Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂ @@@ lev) |- mapOptionTree drop_arg_types_as_tree Σ₂ @ lev
 196     end.
 197
 198   Definition check_hof : forall {Γ}(t:HaskType Γ ★),
 199     sumbool
 200     True
 201     (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
 202     intros.
 203     destruct (eqd_dec (take_arg_types_as_tree t) []);
 204     destruct (eqd_dec (drop_arg_types_as_tree t) t).
 205     right; auto.
 206     left; auto.
 207     left; auto.
 208     left; auto.
 209     Defined.
 210
 211   Opaque take_arg_types_as_tree.
 212   Definition skolemize_proof :
 213     forall  {h}{c},
 214       ND Rule  h c ->
 215       ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
 216     intros.
 217     eapply nd_map'; [ idtac | apply X ].
 218     clear h c X.
 219     intros.
 220
 221     refine (match X as R in Rule H C with
 222       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 223       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 224       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 225       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 226       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 227       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 228       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 229       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 230       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 231       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 232       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 233       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 234       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 235       | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
 236       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 237       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
 238       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
 239       | RVoid    _ _           l       => let case_RVoid := tt   in _
 240       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
 241       | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
 242       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 243       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 244       end); clear X h c.
 245
 246       destruct case_RArrange.
 247         simpl.
 248         destruct l.
 249         apply nd_rule.
 250         apply SFlat.
 251         apply RArrange.
 252         apply d.
 253         apply nd_rule.
 254         apply SFlat.
 255         apply RArrange.
 256         apply ARight.
 257         apply d.
 258
 259       destruct case_RBrak.
 260         simpl.
 261         destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
 262         apply nd_rule.
 263         apply SBrak.
 264
 265       destruct case_REsc.
 266         simpl.
 267         destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
 268         apply nd_rule.
 269         apply SEsc.
 270
 271       destruct case_RNote.
 272         apply nd_rule.
 273         apply SFlat.
 274         simpl.
 275         destruct l.
 276         apply RNote.
 277         apply n.
 278         apply RNote.
 279         apply n.
 280
 281       destruct case_RLit.
 282         simpl.
 283         destruct l0.
 284         apply nd_rule.
 285         apply SFlat.
 286         apply RLit.
 287         set (check_hof (@literalType l Γ)) as hof.
 288         destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
 289         destruct a.
 290         rewrite H.
 291         rewrite H0.
 292         simpl.
 293         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ].
 294         apply nd_rule.
 295         apply SFlat.
 296         apply RLit.
 297
 298       destruct case_RVar.
 299         simpl.
 300         destruct lev.
 301         apply nd_rule; apply SFlat; apply RVar.
 302         set (check_hof σ) as hof.
 303         destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
 304         destruct a.
 305         rewrite H.
 306         rewrite H0.
 307         simpl.
 308         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
 309         apply nd_rule.
 310         apply SFlat.
 311         apply RVar.
 312
 313       destruct case_RGlobal.
 314         simpl.
 315         destruct σ.
 316         apply nd_rule; apply SFlat; apply RGlobal.
 317         set (check_hof (l wev)) as hof.
 318         destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
 319         destruct a.
 320         rewrite H.
 321         rewrite H0.
 322         simpl.
 323         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
 324         apply nd_rule.
 325         apply SFlat.
 326         apply RGlobal.
 327
 328       destruct case_RLam.
 329         destruct lev.
 330           apply nd_rule.
 331           apply SFlat.
 332           simpl.
 333           apply RLam.
 334         simpl.
 335         rewrite drop_works.
 336         apply nd_rule.
 337           apply SFlat.
 338           apply RArrange.
 339           eapply AComp.
 340           eapply AuAssoc.
 341           eapply ALeft.
 342           apply take_arrange.
 343
 344       destruct case_RCast.
 345         simpl.
 346         destruct lev.
 347         apply nd_rule.
 348         apply SFlat.
 349         apply RCast.
 350         apply γ.
 351         apply (Prelude_error "found RCast at level >0").
 352
 353       destruct case_RApp.
 354         simpl.
 355         destruct lev.
 356         apply nd_rule.
 357         apply SFlat.
 358         apply RApp.
 359         rewrite drop_works.
 360         set (check_hof tx) as hof_tx.
 361         destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
 362         destruct a.
 363         rewrite H.
 364         rewrite H0.
 365         simpl.
 366         eapply nd_comp.
 367         eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
 368         eapply nd_rule.
 369         eapply SFlat.
 370         eapply RArrange.
 371         eapply ALeft.
 372         eapply take_unarrange.
 373
 374         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
 375         eapply nd_rule; eapply SFlat; apply RWhere.
 376
 377       destruct case_RLet.
 378         simpl.
 379         destruct lev.
 380         apply nd_rule.
 381         apply SFlat.
 382         apply RLet.
 383         set (check_hof σ₁) as hof_tx.
 384         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 385         destruct a.
 386         rewrite H.
 387         rewrite H0.
 388
 389         eapply nd_comp.
 390         eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ].
 391
 392         set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
 393         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
 394         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
 395         apply nd_prod.
 396           apply nd_id.
 397           apply nd_rule.
 398           eapply SFlat.
 399           eapply RArrange.
 400           eapply AuAssoc.
 401
 402       destruct case_RWhere.
 403         simpl.
 404         destruct lev.
 405         apply nd_rule.
 406         apply SFlat.
 407         apply RWhere.
 408         set (check_hof σ₁) as hof_tx.
 409         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 410         destruct a.
 411         rewrite H.
 412         rewrite H0.
 413
 414         eapply nd_comp.
 415         eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
 416         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 417         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
 418         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
 419         apply nd_prod; [ idtac | eapply nd_id ].
 420         eapply nd_rule; apply SFlat; eapply RArrange.
 421         eapply AComp.
 422         eapply AuAssoc.
 423         apply ALeft.
 424         eapply AuAssoc.
 425
 426       destruct case_RCut.
 427         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].
 428         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''.
 429         set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
 430         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
 431         set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
 432         destruct (decide_tree_empty Σ₁₂''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
 433         destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
 434         rewrite <- e.
 435         eapply nd_comp.
 436         eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
 437         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 438         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
 439         apply nd_prod.
 440         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
 441         apply nd_rule.
 442         apply SFlat.
 443         apply RArrange.
 444         apply ALeft.
 445         destruct s.
 446         eapply arrangeCancelEmptyTree with (q:=x).
 447         rewrite e0.
 448         admit.   (* FIXME, but not serious *)
 449         apply nd_id.
 450
 451       destruct case_RLeft.
 452         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
 453         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
 454         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
 455         set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
 456         set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
 457         destruct (decide_tree_empty (Σ' @@@ (h::l)));
 458           [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
 459         destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
 460         rewrite <- e.
 461         clear Σ'' e.
 462         destruct s.
 463         set (arrangeUnCancelEmptyTree _ _ e) as q.
 464         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
 465         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
 466         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 467         apply nd_rule.
 468         eapply SFlat.
 469         eapply RLeft.
 470
 471       destruct case_RRight.
 472         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
 473         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
 474         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
 475         set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
 476         set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
 477         destruct (decide_tree_empty (Σ' @@@ (h::l)));
 478           [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
 479         destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
 480         rewrite <- e.
 481         clear Σ'' e.
 482         destruct s.
 483         set (arrangeUnCancelEmptyTree _ _ e) as q.
 484         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
 485         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
 486         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 487         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ].  (* yuck *)
 488         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
 489         eapply nd_rule.
 490         eapply SFlat.
 491         apply RRight.
 492
 493       destruct case_RVoid.
 494         simpl.
 495         destruct l.
 496         apply nd_rule.
 497         apply SFlat.
 498         apply RVoid.
 499         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].
 500         apply nd_rule.
 501         apply SFlat.
 502         apply RVoid.
 503
 504       destruct case_RAppT.
 505         simpl.
 506         destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
 507         apply (Prelude_error "RAppT at depth>0").
 508
 509       destruct case_RAbsT.
 510         simpl.
 511         destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
 512         apply (Prelude_error "RAbsT at depth>0").
 513
 514       destruct case_RAppCo.
 515         simpl.
 516         destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
 517         apply γ.
 518         apply (Prelude_error "RAppCo at depth>0").
 519
 520       destruct case_RAbsCo.
 521         simpl.
 522         destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
 523         apply (Prelude_error "RAbsCo at depth>0").
 524
 525       destruct case_RLetRec.
 526         simpl.
 527         destruct t.
 528         apply nd_rule.
 529         apply SFlat.
 530         apply (@RLetRec Γ Δ lri x y nil).
 531         apply (Prelude_error "RLetRec at depth>0").
 532
 533       destruct case_RCase.
 534         simpl.
 535         apply (Prelude_error "CASE: BIG FIXME").
 536         Defined.
 537
 538   Transparent take_arg_types_as_tree.
 539
 540 End HaskSkolemizer.