The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hello,

While reading Section 4.2 of the Reference Manual, paragraph "Typing rules", 
I have noticed some contradictions and some ambiguities.


(1)

The first version of the W-S rule

     E[Γ] ⊢ T : s    s ∈ S    x ∉ Γ
     ──────────────────────────────
            WF(E)[Γ ∷ (x:T)]

is too strict considering the Lam-rule

     E[Γ] ⊢ ∀x:T,U : s   E[Γ ∷ (x:T)] ⊢ t : U
     ────────────────────────────────────────
              E[Γ] ⊢ λx:T.t : ∀x:T,U

because Lam-rule (plausibly) allows shadowing of variables already existing 
in the current context.
Such contexts are rejected by the current version of the W-S rule.

This seem to be a known issue: see "RefMan-cic.tex", inline comment "% Ce 
n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma".


(2)

Also, the second version of the W-S rule

     E[Γ] ⊢ t : T       x ∉ Γ
     ────────────────────────
       WF(E)[Γ ∷ (x := t:T)]

is too strict, considering the Let-rule

     E[Γ] ⊢ t : T    E[Γ ∷ (x := t:T)] ⊢ u : U
     ─────────────────────────────────────────
        E[Γ] ⊢ let x := t in u : U{x/t}

becase Let-rule (plausibly) allows shadowing of variables already existing in 
the current context.
Such contexts are rejected by the current version of the W-S rule.


(3)

In this light, Var and Const rules are ambiguous in several ways.
If some "x" appears in E as well as in Γ, both rules are applicable and 
enable us, in general, to infer different types for the same x.


(4)

If some "x" appears in Γ several times, the Var-rule enables us, in general, 
to infer different types for the same x.


Whoever can, please let me know whether you see what I see.

Many thanks in advance.
--
Matej