For reference this test is in prod/FLWORExpr.xml

The essence of the test is

let $baseElement as empty-sequence() := $extended/baseElement 
        return $baseElement

where $extended/baseElement actually selects something.

By XPTY0005 I think you mean XPST0005. I agree that XPST0005 is a reasonably result.

I'm not happy with the idea that the query can validly return an empty sequence. I know that almost anything can be justified under "errors and optimizations", but this seems a bit extreme. I would argue that it violates at least the spirit of the 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." - the intended effect of this rule is that you can short-cut evaluation of a sequence, but not in such a way that you fail to detect cardinality errors.

I hear the sound of a can of worms being opened.

Following your explanation, I therefore conclude that

declare function local:return($arg)
{
  if (xs:date('2000-01-01') eq current-date())
  then ()
  else $arg
};

let $x as empty-sequence() := local:return(1)
return ()

should fail with an error, even though the value o4 $x is never used.  Here's my reasoning.

1.  local:return has static type item()*.  Because it depends on the dynamic context, a process can do no better (unless it makes assumptions about the date).

2.  let .. return .. is a single expression with two operands, and its static type is empty-sequence().

3.  let $x as empty-sequence() clause is effectively a cardinality check, so any errors resulting from a cardinality-mismatch cannot be optimized away.


However, modifying the body to

(), let $x as empty-sequence() := local:return(1) return ()

would be permitted to be optimized away to the empty sequence, because here the concatenation operator is permitted not to evaluate either operand on the basis of their static types.

Similarly

let $y :=
  let $x as empty-sequence() := local:return(1) return ()
return $y

can also optimize to empty sequence.


Another example which shows up this problem is:

declare function local:return($arg)
{
  if (xs:date('2000-01-01') eq current-date())
  then ()
  else $arg
};

declare function local:let($unused as empty-sequence()) as empty-sequence()
{
  ()
};

local:let(local:return(1))

1.  local:return has static type item()*.  Because it depends on the dynamic context, a process can do no better (unless it makes assumptions about the date).

2.  local:let is a single expression with one operand, and its static type is empty-sequence().

3.  The function call local:let requires a dynamic check on its argument to check that is has cardinality zero.  This can't be optimized away.

It's very difficult to shut the lid on the "Errors and Optimization" can of worms...

My interpretation is

(a) you don't need to evaluate an expression if you don't need its value

(b) but if you do evaluate it then you must check that the cardinality of the result is correct.

In your example $x is not used, so you don't need to evaluate local-return(1), so you don't need to detect the cardinality error.

FWIW, I'm struggling with very similar issues at the moment where we get incorrect error handling for the lookup operator X?Y, because we generate some pretty complex code that's supposed to be equivalent to the semantics of the operator, and the optimizer then mangles it into code with different error behaviour.

Following that through, from the original

let $baseElement as empty-sequence() := $extended/baseElement 
return $baseElement

We begin by optimizing $baseElement.  This expression has static type empty sequence, therefore it optimizes itself to ().  Now the expression is

let $baseElement as empty-sequence() := $extended/baseElement 
return ()

We continue by optimizing the FLWOR expression, and spot that $baseElement is no longer used.  Therefore it happily optimizes to the empty sequence.

I rather wish "as empty-sequence()" was forbidden by the language.

>We begin by optimizing $baseElement.  This expression has static type empty
sequence, therefore it optimizes itself to (). 

I think that's too dangerous. The user is asserting that it will be an empty sequence, but they are also asking for that assertion to be checked, in my view. This is the rule that says cardinality checks should not be bypassed.

Dangerous perhaps, but legitimate.

If the unfortunate user assumes that 

let $x as empty-sequence() := local:return(1)
return $x

will always test the assertion, they'll probably assume that

empty (let $x as empty-sequence() := local:return(1)
       return $x)

will fail rather that returning an error.

or

1 + (let $x as empty-sequence() := local:return(1) return $x)

will fail rather that returning the empty sequence.

The specification should come with a warning saying that "as empty-sequence()" is probably a bad thing to use.

The WG has decided that the best way to resolve this bug issue is to allow alternative assertions. Specifically:

XPTY0004
XPTY0005
assert-empty

Test case has been changed accordingly.