Section 2.3.4 Errors and Optimization of the XQuery 3.1 spec says that:

"The effect of these rules is that the processor is free to stop examining further items in a sequence as soon as it can establish that further items would not affect the result except possibly by causing an error. For example, the processor may return true as the result of the expression S1 = S2 as soon as it finds a pair of equal values from the two sequences."

This is currently specified at the level of expressions, but I have not found a clear hint if it can also be applied to type checks.

See the following example:

  function() as xs:integer+ { 1 to 100000, <x/> }() = 1

This query could be rewritten to (something similar like) the following expression, and it would yield true (provided that a processor evaluates the query in a streaming manner):

  (1 to 100000, <x/>) ! (. treat as xs:integer) = 1

Another example: Strict type checks would prevent a query processor from streaming results of functions if the return type cannot be statically determined:

  function($x) as xs:integer+ { 1 to 1000000000, $x }(123)[1]

As the examples indicate, I would clearly be in favor of allowing iterative type checking.