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