Require Import HaskCoreTypes.
Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
+Require Import HaskWeakVars.
(* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
* in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think
| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l) ]]
(* Part of GHC, but not explicitly in System FC *)
-| RNote : ∀ h c, Note -> Rule h [ c ]
+| RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]]
| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@ l]]
(* SystemFC rules *)
| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]]
+| RGlobal : ∀ Γ Δ τ l, WeakExprVar -> Rule [ ] [Γ>Δ> [] |- [τ @@l]]
| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
| RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
[Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
-| RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ]
+| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- [τ₁],,τ₂ ] [Γ > Δ > Σ₁ |- [τ₁] ]
| RCase : forall Γ Δ lev tc Σ avars tbranches
(alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)),
Rule
(* A rule is considered "flat" if it is neither RBrak nor REsc *)
Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
| Flat_RURule : ∀ Γ Δ h c r , Rule_Flat (RURule Γ Δ h c r)
-| Flat_RNote : ∀ x y z , Rule_Flat (RNote x y z)
+| Flat_RNote : ∀ Γ Δ Σ τ l n , Rule_Flat (RNote Γ Δ Σ τ l n)
| Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
| Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q )
| Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q )
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
Qed.
Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.