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 (Σ₁₂'' @@@ (h::l)));
 433           [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
 434         destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
 435         rewrite <- e.
 436         clear e.
 437         destruct s.
 438         eapply nd_comp.
 439           eapply nd_prod.
 440           eapply nd_rule.
 441           eapply SFlat.
 442           eapply RArrange.
 443           eapply AComp.
 444           eapply ALeft.
 445           eapply arrangeCancelEmptyTree with (q:=x).
 446           apply e.
 447           apply ACanR.
 448           apply nd_id.
 449         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 450         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
 451         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
 452         apply nd_prod.
 453         apply nd_id.
 454         eapply nd_rule.
 455           eapply SFlat.
 456           eapply RArrange.
 457           eapply AComp.
 458           eapply AuAssoc.
 459           eapply ALeft.
 460           eapply AComp.
 461           eapply AuAssoc.
 462           eapply ALeft.
 463           eapply AId.
 464
 465       destruct case_RLeft.
 466         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
 467         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
 468         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
 469         set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
 470         set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
 471         destruct (decide_tree_empty (Σ' @@@ (h::l)));
 472           [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
 473         destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
 474         rewrite <- e.
 475         clear Σ'' e.
 476         destruct s.
 477         set (arrangeUnCancelEmptyTree _ _ e) as q.
 478         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
 479         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
 480         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 481         apply nd_rule.
 482         eapply SFlat.
 483         eapply RLeft.
 484
 485       destruct case_RRight.
 486         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
 487         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
 488         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
 489         set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
 490         set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
 491         destruct (decide_tree_empty (Σ' @@@ (h::l)));
 492           [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
 493         destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
 494         rewrite <- e.
 495         clear Σ'' e.
 496         destruct s.
 497         set (arrangeUnCancelEmptyTree _ _ e) as q.
 498         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
 499         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
 500         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 501         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ].  (* yuck *)
 502         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
 503         eapply nd_rule.
 504         eapply SFlat.
 505         apply RRight.
 506
 507       destruct case_RVoid.
 508         simpl.
 509         destruct l.
 510         apply nd_rule.
 511         apply SFlat.
 512         apply RVoid.
 513         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].
 514         apply nd_rule.
 515         apply SFlat.
 516         apply RVoid.
 517
 518       destruct case_RAppT.
 519         simpl.
 520         destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
 521         apply (Prelude_error "RAppT at depth>0").
 522
 523       destruct case_RAbsT.
 524         simpl.
 525         destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
 526         apply (Prelude_error "RAbsT at depth>0").
 527
 528       destruct case_RAppCo.
 529         simpl.
 530         destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
 531         apply γ.
 532         apply (Prelude_error "RAppCo at depth>0").
 533
 534       destruct case_RAbsCo.
 535         simpl.
 536         destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
 537         apply (Prelude_error "RAbsCo at depth>0").
 538
 539       destruct case_RLetRec.
 540         simpl.
 541         destruct t.
 542         apply nd_rule.
 543         apply SFlat.
 544         apply (@RLetRec Γ Δ lri x y nil).
 545         apply (Prelude_error "RLetRec at depth>0").
 546
 547       destruct case_RCase.
 548         simpl.
 549         apply (Prelude_error "CASE: BIG FIXME").
 550         Defined.
 551
 552   Transparent take_arg_types_as_tree.
 553
 554 End HaskSkolemizer.