Static Typing in XQ Update Test Suite

Andrew Eisenberg wrote:
> We are still looking for implementations that support the 
> Update Facility Static Typing Feature and implementations that support 
> XQueryX. We'd like to encourage implementors of these features to submit 
> their results to us, so that we can advance XQuery Update Facility to W3C 
> Recommendation.

Dear Andrew,

contemplating the test group "Update Facility Static Typing Feature",
I think there are some reasons why no implementations so far can
pass the related tests:
IMHO, there are no more than 10 tests in 27 that really belong to this 
category and are correct.

As far as I understand the static typing feature, an implementation 
supporting it is supposed to raise an error when the static analysis can 
determine that an expression will *certainly* raise an error at runtime:
 [XQ 5.2.3 Static Typing Feature]
 /If an implementation does not support the Static Typing Feature, but 
can nevertheless determine during the static analysis phase that an 
expression, if evaluated, will *necessarily raise a type error* at run 
time, the implementation MAY raise that error during the static analysis 
phase./
It is also stated [XQ 2.2.3.1 Static Analysis Phase]:
  /[Definition: The static analysis phase depends on the expression 
itself and on the static context. The static analysis phase *does not 
depend on input data* (other than schemas).]     /

* tests of the kind "ST is too vague" are wrong IMO:
    a static type node()* can perfectly correspond to correct node types 
at runtime.
* tests of the kind "ST of Target/Source has cardinality greater than one"
    - either involve the knowledge of input data (through $input-context),
    - or assume that the path-expression will always return several nodes,
     which cannot be asserted during static analysis (and BTW it returns 
exactly one node).
* Test "stf-insert-02: insert: ST of SourceExpr has non-attribute before 
attribute.":
    although this error can indeed be detected by static analysis, that 
seems
   far too complex, and looks more like "formal proof of program" than
   like what a compiler can achieve.

Best regards