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       | RJoin    Γ p lri m x q l       => let case_RJoin := tt in _
 240       | RVoid    _ _           l       => let case_RVoid := tt   in _
 241       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
 242       | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
 243       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 244       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 245       end); clear X h c.
 246
 247       destruct case_RArrange.
 248         simpl.
 249         destruct l.
 250         apply nd_rule.
 251         apply SFlat.
 252         apply RArrange.
 253         apply d.
 254         apply nd_rule.
 255         apply SFlat.
 256         apply RArrange.
 257         apply ARight.
 258         apply d.
 259
 260       destruct case_RBrak.
 261         simpl.
 262         destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
 263         apply nd_rule.
 264         apply SBrak.
 265
 266       destruct case_REsc.
 267         simpl.
 268         destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
 269         apply nd_rule.
 270         apply SEsc.
 271
 272       destruct case_RNote.
 273         apply nd_rule.
 274         apply SFlat.
 275         simpl.
 276         destruct l.
 277         apply RNote.
 278         apply n.
 279         apply RNote.
 280         apply n.
 281
 282       destruct case_RLit.
 283         simpl.
 284         destruct l0.
 285         apply nd_rule.
 286         apply SFlat.
 287         apply RLit.
 288         set (check_hof (@literalType l Γ)) as hof.
 289         destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
 290         destruct a.
 291         rewrite H.
 292         rewrite H0.
 293         simpl.
 294         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ].
 295         apply nd_rule.
 296         apply SFlat.
 297         apply RLit.
 298
 299       destruct case_RVar.
 300         simpl.
 301         destruct lev.
 302         apply nd_rule; apply SFlat; apply RVar.
 303         set (check_hof σ) as hof.
 304         destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
 305         destruct a.
 306         rewrite H.
 307         rewrite H0.
 308         simpl.
 309         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
 310         apply nd_rule.
 311         apply SFlat.
 312         apply RVar.
 313
 314       destruct case_RGlobal.
 315         simpl.
 316         destruct σ.
 317         apply nd_rule; apply SFlat; apply RGlobal.
 318         set (check_hof (l wev)) as hof.
 319         destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
 320         destruct a.
 321         rewrite H.
 322         rewrite H0.
 323         simpl.
 324         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
 325         apply nd_rule.
 326         apply SFlat.
 327         apply RGlobal.
 328
 329       destruct case_RLam.
 330         destruct lev.
 331           apply nd_rule.
 332           apply SFlat.
 333           simpl.
 334           apply RLam.
 335         simpl.
 336         rewrite drop_works.
 337         apply nd_rule.
 338           apply SFlat.
 339           apply RArrange.
 340           eapply AComp.
 341           eapply AuAssoc.
 342           eapply ALeft.
 343           apply take_arrange.
 344
 345       destruct case_RCast.
 346         simpl.
 347         destruct lev.
 348         apply nd_rule.
 349         apply SFlat.
 350         apply RCast.
 351         apply γ.
 352         apply (Prelude_error "found RCast at level >0").
 353
 354       destruct case_RJoin.
 355         simpl.
 356         destruct l.
 357         apply nd_rule.
 358         apply SFlat.
 359         apply RJoin.
 360         apply (Prelude_error "found RJoin at level >0").
 361
 362       destruct case_RApp.
 363         simpl.
 364         destruct lev.
 365         apply nd_rule.
 366         apply SFlat.
 367         apply RApp.
 368         rewrite drop_works.
 369         set (check_hof tx) as hof_tx.
 370         destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
 371         destruct a.
 372         rewrite H.
 373         rewrite H0.
 374         simpl.
 375         eapply nd_comp.
 376         eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
 377         eapply nd_rule.
 378         eapply SFlat.
 379         eapply RArrange.
 380         eapply ALeft.
 381         eapply take_unarrange.
 382
 383         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
 384         eapply nd_rule; eapply SFlat; apply RWhere.
 385
 386       destruct case_RLet.
 387         simpl.
 388         destruct lev.
 389         apply nd_rule.
 390         apply SFlat.
 391         apply RLet.
 392         set (check_hof σ₁) as hof_tx.
 393         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 394         destruct a.
 395         rewrite H.
 396         rewrite H0.
 397
 398         eapply nd_comp.
 399         eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ].
 400
 401         set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
 402         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
 403         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
 404         apply nd_prod.
 405           apply nd_id.
 406           apply nd_rule.
 407           eapply SFlat.
 408           eapply RArrange.
 409           eapply AuAssoc.
 410
 411       destruct case_RWhere.
 412         simpl.
 413         destruct lev.
 414         apply nd_rule.
 415         apply SFlat.
 416         apply RWhere.
 417         set (check_hof σ₁) as hof_tx.
 418         destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
 419         destruct a.
 420         rewrite H.
 421         rewrite H0.
 422
 423         eapply nd_comp.
 424         eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
 425         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 426         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
 427         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
 428         apply nd_prod; [ idtac | eapply nd_id ].
 429         eapply nd_rule; apply SFlat; eapply RArrange.
 430         eapply AComp.
 431         eapply AuAssoc.
 432         apply ALeft.
 433         eapply AuAssoc.
 434
 435       destruct case_RCut.
 436         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].
 437         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''.
 438         set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
 439         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
 440         set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
 441         destruct (decide_tree_empty Σ₁₂''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
 442         destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
 443         rewrite <- e.
 444         eapply nd_comp.
 445         eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
 446         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 447         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
 448         apply nd_prod.
 449         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
 450         apply nd_rule.
 451         apply SFlat.
 452         apply RArrange.
 453         apply ALeft.
 454         destruct s.
 455         eapply arrangeCancelEmptyTree with (q:=x).
 456         rewrite e0.
 457         admit.   (* FIXME, but not serious *)
 458         apply nd_id.
 459
 460       destruct case_RLeft.
 461         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
 462         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
 463         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
 464         set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
 465         set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
 466         destruct (decide_tree_empty (Σ' @@@ (h::l)));
 467           [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
 468         destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
 469         rewrite <- e.
 470         clear Σ'' e.
 471         destruct s.
 472         set (arrangeUnCancelEmptyTree _ _ e) as q.
 473         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
 474         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
 475         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 476         apply nd_rule.
 477         eapply SFlat.
 478         eapply RLeft.
 479
 480       destruct case_RRight.
 481         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
 482         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
 483         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
 484         set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
 485         set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
 486         destruct (decide_tree_empty (Σ' @@@ (h::l)));
 487           [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
 488         destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
 489         rewrite <- e.
 490         clear Σ'' e.
 491         destruct s.
 492         set (arrangeUnCancelEmptyTree _ _ e) as q.
 493         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
 494         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
 495         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 496         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ].  (* yuck *)
 497         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
 498         eapply nd_rule.
 499         eapply SFlat.
 500         apply RRight.
 501
 502       destruct case_RVoid.
 503         simpl.
 504         destruct l.
 505         apply nd_rule.
 506         apply SFlat.
 507         apply RVoid.
 508         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].
 509         apply nd_rule.
 510         apply SFlat.
 511         apply RVoid.
 512
 513       destruct case_RAppT.
 514         simpl.
 515         destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
 516         apply (Prelude_error "RAppT at depth>0").
 517
 518       destruct case_RAbsT.
 519         simpl.
 520         destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
 521         apply (Prelude_error "RAbsT at depth>0").
 522
 523       destruct case_RAppCo.
 524         simpl.
 525         destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
 526         apply γ.
 527         apply (Prelude_error "RAppCo at depth>0").
 528
 529       destruct case_RAbsCo.
 530         simpl.
 531         destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
 532         apply (Prelude_error "RAbsCo at depth>0").
 533
 534       destruct case_RLetRec.
 535         simpl.
 536         destruct t.
 537         apply nd_rule.
 538         apply SFlat.
 539         apply (@RLetRec Γ Δ lri x y nil).
 540         apply (Prelude_error "RLetRec at depth>0").
 541
 542       destruct case_RCase.
 543         simpl.
 544         apply (Prelude_error "CASE: BIG FIXME").
 545         Defined.
 546
 547   Transparent take_arg_types_as_tree.
 548
 549 End HaskSkolemizer.