I believe that another paragraph from section 2.3.4, Errors and Optimization, must be considered:

"There is an exception to this rule: If a processor evaluates an operand E (wholly or in part), then it is required to establish that the actual value of the operand E does not violate any constraints on its cardinality. For example, the expression $e eq 0 results in a type error if the value of $e contains two or more items. A processor is not allowed to decide, after evaluating the first item in the value of $e and finding it equal to zero, that the only possible outcomes are the value true or a type error caused by the cardinality violation. It must establish that the value of $e contains no more than one item."


The first parameter of normalize-unicode is of type string?. The operands of the sequence constructor that makes up the first argument must be evaluated to ensure that the sequence does not contain more than one item.

For this reason, I believe that the query cannot return a value other than an error. Frans, do you agree with this?

I'm puzzled by your reasoning, Andrew. The paragraph you quote says that "it is required to establish that the actual value of the operand E does not violate any constraints on its cardinality". But Tim asserts (and no doubt he is right) that this has already been done during static analysis, which determined the cardinality of ("a string", error()) to be (1,1). 

This seems like an absurd and undesirable result, but it's hard to argue with the logic that the spec allows it.

Or perhaps it's not so absurd after all: the only reason we have the rule that you can't do early-exit until you've established the cardinality is to outlaw the XPath 1.0 "use first item, ignore rest of sequence" semantics, because we think that's error-prone. Here, if you carried on evaluating the sequence, you would not get a cardinality error but whatever error is thrown by error(), so it doesn't fall into this category and shouldn't be caught by this rule.

I'm now less convinced that

("a string", error())

is of type xs:string.  In FS 8.4

quantifier(none) = 1

The type none matches no values, therefore from the FS rules in 8.3.1 Matches and 8.3.2 Subtyping (<:) there is no rule:

--------------------------------
statEnv |-  error() matches none

therefore we can't apply:

statEnv |-  Value1 matches Type1
statEnv |-  Value2 matches Type2
---------------------------------------------
statEnv |-  Value1,Value2 matches Type1,Type2

so we have to deduce that whatever type (xs:string, none) is, it certainly isn't a subtype of xs:string.  All we can say is that it is of type (xs:string, none), which is roughly xs:string+.

Therefore this test should allow for a type checking error as well as the error thrown by error().  Quite a few of the tests use a similar construct, so will also need to permit a type check error.

As an aside, I do find it a little strange that (Type|none) = Type _and_ quantifier(none) = 1.  It almost seems as if a type which matches no values should have the unusual quantifier of zero.

>It almost seems as if a type which matches no values should have the unusual quantifier of zero.

I handled it that way at one time but it caused too many problems. I now type error() as item(), which works for optimistic typing - it means that error() will never cause a static type error, except in the pathological case where the required type is empty-sequence(), because item() overlaps every other type. (Perhaps I should have chosen item()? which would work for empty-sequence() as well...)

Being more or less incapable to comment on FS, I gladly trusted Tim and added XPTY0004 to the baseline. XQTS_current.zip is updated in CVS.

Thanks.

I think this should be reopened to update the following tests as well:

K-NumericAdd-34 
   (4, error()) + 3

K-NumericAdd-35 
   3 + (4, error())

K-ValCompTypeChecking-39
   3 eq (3, error())

K-ValCompTypeChecking-41
   (3, error()) eq 3

Thanks,
Josh

I think these are simply bad tests. They are testing an area where the spec is fuzzy and where we have in effect chosen to leave it fuzzy; so the outcome of the test tells us very little.

It would be much more useful to replace the call on error() with something like

if (doc-available('unavailable.xml')) then () else error()

to remove the effect of static type inferencing.

if (doc-available('unavailable.xml')) then () else error()

has static type 'empty | none' which is equivalent to 'empty' according to the Formal Semantics.

Fixed in CVS by adding XPST0005 to tests mentioned in comment #7.

Thanks.

I think this fix is incomplete.  

I can see that XPST0005 was added for K-NumericAdd-34 and K-NumericAdd-35 but the tests themselves seem unchanged.  I don't think adding XPST0005 makes sense unless you also change the tests as described in comment #8.  

I don't see any changes for K-ValCompTypeChecking-39 or K-ValCompTypeChecking-41 even though comment #10 indicates they have changed.

If K-NormalizeUnicodeFunc-13 accepts XPTY0004 as a valid result, it seems odd to me if the tests in comment #7 do not accept XPTY0004 as well. i.e. isn't Tim's analysis in comment #3 valid for the comment #7 tests as well - "(integer, none) isn't a subtype of integer"? I expected the fix to be adding XPTY0004 as a valid result for each of the comment #7 tests (not XPST0005).

I believe this bug has been addressed in QT3.

I have updated K-NumericAdd-34 and K-NumericAdd-35 so they are consistent with K-ValCompTypeChecking-39 and K-ValCompTypeChecking-41.  The tests now accept XPTY0004 as well as FOER0000 (and not XPST0005) which is justified by the analysis in comment 3.  See also bug 26860.