Type checking order problem [BUG]

[PieterLamers]

Describe the bug
Type checking on the incorrectly typed variable is not done, or done after the variable is supplied to a function.

Expected behavior
I want the type error to be shown on the variable declaration (as does Saxon 12.3)

To Reproduce
When the following is run, it returns exerr:ERROR XPTY0004: The actual cardinality for parameter 1 does not match the cardinality declared in the function's signature: local:myfunction($input as xs:string) item()*. Expected cardinality: exactly one, got 0. [at line 11, column 48, source: String/-4954723990344000104] In function: local:myfunction(xs:string)

it should return An empty sequence is not allowed as the value of variable $input.

Code to reproduce

xquery version "3.1";

declare function local:myfunction( $input as xs:string ) 
{
  ()
};

(: invalid variable declaration, should be caught:)
let $input as xs:string := ()

let $output as xs:string :=  local:myfunction($input)

return 
  ()

Context (please always complete the following information)

• Build: eXist-6.2.0
• Java: 11.0.17 Temurin
• OS: Windows, Linux

[PieterLamers]

I noticed it is not related to having a function call. There is simply no top-down ordering of the type checks, as is demonstrated by the following:

(: invalid variable declaration, should be caught:)
let $input as xs:string := ()

let $output as xs:string :=  $input

return 
  $output

which barfs about the incorrect type of the $output variable, rather than the $input variable. I will therefore update the title of the bug.
I know processing order is not always top-down. However I expect type checking to use a top-down order. @line-o labeling this as enhancement suggests this may not be defined as a requirement in the xquery language spec.

[adamretter]

@PieterLamers This is definitely a bug and not an enhancement; I have modified the labels.

I can also confirm that this happens in 7.0.0-SNAPSHOT also.

I also note that BaseX 10.6 correctly returns the error:

Error:
Stopped at /Users/aretter/code/XQS/test/file2, 9/5:
[XPTY0004] Cannot treat empty-sequence() as xs:string: $input := ().

[line-o]

@PieterLamers Ah, thanks for clarifying what you meant by top-down! So, as I now understand you it is the location rather than the message that is wrong. The message should definitely be improved, that is why I put the enhancement label on it.
That exist-db is not checking the type in variable declaration is known. So, this issue is possibly a duplicate.

[PieterLamers]

@line-o I don't understand what you mean by 'exist-db is not checking the type in variable declaration' as this still throws an error:

let $input as xs:string := ()

return  ()

[nverwer]

I remote-debugged eXist, and ran the script

let $input as xs:string := ()
let $output as xs:string := $input
return $output

In org.exist.xquery.LetExpr::eval, with a breakpoint on line 110,

                resultSequence = returnExpr.eval(contextSequence, null);

on the first break,

• var = $input as xs:string := ()
• returnExpr = let $output := $input return $output
  The returnExpr is a LetExpr, and in line 110 it is evaluated before the declaration of $input is typechecked.

In the recursive call to eval,

• var = $output as xs:string := ()
• returnExpr = $output is a DebuggableExpression, and returnExpr.eval(contextSequence, null) evaluates to ().
  Then the type of $output is checked before the calling eval checks the type for $input, so the type error occurs on $output.

Then I moved line 110 to line 167, after the if (sequenceType != null) { ... ... }, which seems safe because resultSequence is not used in the if. I assume that eval has no side effects
This gives the expected error message about $input.

I did not make a pull request (yet) because

• I have no idea which things I have broken;
• A similar change may be needed in ForExpr.

I thought it might be useful to share these preliminary results. When I know more, I will come back to add another comment.

[adamretter]

@nverwer If I remember correctly there are some issues with Lazy Evaluation of variables in eXist-db. Additionally, this should really be caught in the static analysis phase; that would be the analyze method of the expression rather than the eval method.

[nverwer]

@adamretter As far as I understand, the analyze method in LetExpr does not check the type of a variable against the type of the expression that is bound to the variable. Type checking (and producing XPTY0004 errors) is done in eval.
While I agree that in this case the error might be caught in analyze, since the type of () can be statically determined, in general that might be difficult (but not impossible).
Anyway, to my untrained eye, analyze does not seem to do any type checking. For the time being I will see what happens when postpone eval of the returnExpr.

[nverwer]

In addition to the above, after running eXist with the proposed change, Pieter and I have noticed several type errors in our software that were not detected without this change. Although not detecting these in analyze would be better, detecting them at runtime in eval has helped us to fix some potential problems.