The XQuery Formal Semantics define a number of specific typing
rules for the built-in function fn:subsequence() in order to
reveal a static type as specific as possible.

Among others, the following rule is included in these specifics:

     statEnv |- Expr : Type       quantifier(Type) in {1, +}
 -------------------------------------------------------------
   statEnv |- fn:subsequence(Expr, $fs:last, 1) : prime(Type)

Note that in this inference rule, $fs:last is completely unrelated
to the expression Expr.  The current context is not necessarily
related to the argument of fn:subsequence().

In particular, the size of the current context set (and thus
$fs:last) may be larger than the size of Expr.  fn:subsequence()
returns the empty sequence if its start argument is greater than
the length of the sequence.  The avove typing rule, however, does
not include the empty sequence in the (static) return type of
fn:subsequence().  If the start argument is smaller than the
length of Expr, fn:subsequence() will return a sequence longer than
one.

Consider the following query (not really a sensible query, but it
demonstrates a wrong type inference when applying the above rule):

  let $a := <a><b/><b/><b/><b/></a> return
    $a/b[fn:subsequence( (1,2), last() )]

In this query, $a/b evaluates to 4 nodes.  last() will thus return
4, which is greater than the length of the sequence (1,2).  So the
result of fn:subsequence( (1,2), last() ) will be the empty
sequence, while we get `xs:integer' as the static return type for
it.

If we replace the sequence (1,2) in the above example by (1,2,3,4,5),
fn:subsequence() will return a list of length 2, though the static
type is (still) `xs:integer'.