The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Matej,

  well spoted. There is a set precedence in the variable rules in the refinement algorithm: Var >> Const, and the rightmost binding (most recent) is found first. After refinement there is no ambiguity left for the kernel typechecke as local variables are turned into de Bruijn indices, and "global"/section variables are unique (automatic renaming to enfore no-shadowing is done at printing time though). I agree it's imprecise.

Best,

-- Matthieu

On Mon, May 4, 2015 at 1:38 PM Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

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