Hi Jerome,

correct me if I am wrong, but I think there is a problem with the static type inference rules in Section 8.2.3.1.1 (Name Tests).

Consider the expression

  $v/self::foo

and $v has the static type `element *' (we know it's exactly one element, but we don't know its name).

The Formal Semantics essentially depends on two judgments to derive the result type of this expression:

  axis self:: of element * : element *      (Sect. 8.2.2.1.2)

then

  test foo with element of element * : element foo .

The latter is a rule in Section 8.2.3.1.1 where we perform a (non-wildcard) name test on an element type with a wildcard name:


--------------------------------------------------------------------------------
 test QName2 with element of element * OptTypeSpec : element QName2 OptTypeSpec

I think a `?' occurrence indicator is missing here.  If $v in the above example is a `foo' element, the result type is indeed `element foo'.  But if $v carries a different name (say, `bar') the path step will return the empty sequence (which would not be permitted by the above static typing rule).

The same problem arises also in some of the remaining judgments in Section 8.2.3.1.1.