question about subtyping and type annotations

I'm unclear on the semantic model for type annotations, and I can't
find a clear answer in the specifications or in the test suite.

I gather (and Saxon agrees) that:
   100 instance of xs:byte ==> false
because 100 has "type annotation" xs:integer, which is not a sub-type
of xs:byte.

Using the cast xs:byte creates a value with type annotation xs:byte:
   xs:byte(100) instance of xs:byte ==> true

What about xs:integer(xs:byte(100))?  I would expect this to return
a value with type annotation xs:integer, but Saxon (b8-6-1) disagrees:
   xs:integer(xs:byte(100)) instance of xs:byte ==> true ????

This implies that if the argument already conforms to the casted-to-type
then it it returned changed.  That is certainly a possible behavior,
but another behavior is that casting to xs:integer returns a value
with annotation xs:integer.  That seems more consistent to me.

The formal semantics just refers to chapter 17 of Functions and
Operators, which mainly specifies which conversions are valid.
The formal semantics should probably specify the resulting "formal
values" after a cast.

Either way, this should be tested in the test suite.  I didn't
find it (using a quick grep).
-- 
	--Per Bothner
[email protected]   http://per.bothner.com/