Note that this could either be considered a bug against XPath, or a bug against Formal Semantics, depending on the resolution.

XPath 2.0 SE and FS 1.0 SE seem to give conflicting definitions for matching schema elements.


To summarize the differences between the definitions:

Formal Semantics says that an element X matches schema-element(E) if its name, type and nillability of X match those of an element S which substitutes for E.

XQuery says that an element X matches schema-element(E) if its name matches the name of an element S which substitutes for E, and if its type and nillability match those of E.



In particular I am concerned with the following case

define element foo of type xs:anyAtomicType
define element bar substitutes for foo of type xs:integer

and consider the following query:

validate lax { <bar xsi:type="xs:decimal">123</bar> } instance of schema-element(foo)



Quoting the rules for matching schema types from XPath 2.0 (2.5.4.4):


A SchemaElementTest matches a candidate element node if all three of the following conditions are satisfied:

1. The name of the candidate node matches the specified ElementName or matches the name of an element in a substitution group headed by an element named ElementName.

2. derives-from(AT, ET) is true, where AT is the type annotation of the candidate node and ET is the schema type declared for element ElementName in the in-scope element declarations.

3. If the element declaration for ElementName in the in-scope element declarations is not nillable, then the nilled property of the candidate node is false.


In this case all 3 conditions are satisfied - bar substitutes for foo, the type of bar (xs:decimal) is a subtype of the type of foo (xs:anyAtomicType) and neither element is nilled.  Thus the test should match.


However, I do not believe that formal semantics correctly reflects condition 2.




Consider the dynamic semantics specified by FS.

Firstly, look at the name-lookup judgement  (FS 8.1.3):

statEnv |- ElementName1 substitutes for ElementName2
statEnv |-  ElementName1 of elem/type expands to expanded-QName1
statEnv.elemDecl(expanded-QName1) = define element ElementName1 OptSubstitution OptNillable TypeReference
-------------------------------------------------------------
statEnv |- ElementName1 name lookup element ElementName2 yields OptNillable TypeReference

Substituting in our types, I believe

statEnv |- bar name lookup element foo yields xs:integer

And thus taking the rule for matches (FS 8.3.1):

statEnv |- ElementName name lookup ElementType yields OptNillable of type BaseTypeName
statEnv |- TypeName derives from BaseTypeName
Value1 filter @xsi:nil => SimpleValue
SimpleValue in { (), false }
--------------------------------------------------
statEnv |- element ElementName of type TypeName { Value } matches ElementType

Substitute in our element (replace ElementName with bar, TypeName with xs:decimal) and ElementType with element foo.

The first line restricts BaseTypeName to xs:integer (as bar name lookup element foo yields xs:integer)
The second line then does not hold (as xs:decimal derives from xs:integer is false).

And so formal semantics yields false for the judgement.



The static semantics are also different according to FS, as they use this same matches judgment.

I believe the type inferred for 

let $node := validate lax { <bar xsi:type="xs:decimal" /> } as node()
return $node/self::schema-element(foo)

is computed as:

(element(foo, xs:anyAtomicType) | element(bar, xs:integer))?

which does not match the type of the value returned when using the rules in XQuery (element(bar, xs:decimal)).  When using the rules specified in formal semantics, this produces the empty sequence though, and I believe the rules to be sound in this respect.




In order to fix these problems we can either move XPath in line with Formal semantics, or move formal semantics in line with XPath.  Whilst the obvious answer is "FS is no longer normative", both these specifications were written to be normative and since both these definitions are consistent with themselves I see no reason why one should hold more merit that the other.  I know that at least one implementation implements the rules as stated in FS (XQSharp) and at least one implementation implements the rules as stated in XPath (Saxon).



To make XPath behave as the Formal Semantics describes, we need to change 2.5.4.4 from


A SchemaElementTest matches a candidate element node if all three of the following conditions are satisfied:

1. The name of the candidate node matches the specified ElementName or matches the name of an element in a substitution group headed by an element named ElementName.

2. derives-from(AT, ET) is true, where AT is the type annotation of the candidate node and ET is the schema type declared for element ElementName in the in-scope element declarations.

3. If the element declaration for ElementName in the in-scope element declarations is not nillable, then the nilled property of the candidate node is false.


to


A SchemaElementTest matches a candidate element node if all three of the following conditions are satisfied:

1. The name of the candidate node matches the specified ElementName or matches the name of an element in a substitution group headed by an element named ElementName.  Call this element the substituted element.

2. derives-from(AT, ET) is true, where AT is the type annotation of the candidate node and ET is the schema type declared for the substituted element in the in-scope element declarations.

3. If the substituted element is not nillable, then the nilled property of the candidate node is false.




To bring FS in line with XPath I believe the following changes need to be made:

In FS 8.1.3, change the judgement

statEnv |- ElementName1 substitutes for ElementName2
statEnv |-  ElementName1 of elem/type expands to expanded-QName1
statEnv.elemDecl(expanded-QName1) = define element ElementName1 OptSubstitution OptNillable TypeReference
-------------------------------------------------------------
statEnv |- ElementName1 name lookup element ElementName2 yields OptNillable TypeReference

to

statEnv |- ElementName1 substitutes for ElementName2
statEnv |-  ElementName2 of elem/type expands to expanded-QName2
statEnv.elemDecl(expanded-QName2) = define element ElementName2 OptSubstitution OptNillable TypeReference
-------------------------------------------------------------
statEnv |- ElementName1 name lookup element ElementName2 yields OptNillable TypeReference

Significant changes would also have to be made to the text describing these judgements.



Personally, I find the FS rules far more intuitive.