Interaction of type annotations with literals in the formal semantics

I have a question concerning the typing of literals and its interaction with 
type annotations (for instance in let expressions) in the formal semantics.

The static rule for integer literals is

  --------------------------------------------------
  statenv |- integerLiteral : xs:integer

Now suppose we have the following type definition:

  define type feet restricts xs:integer

Is the following expression well-typed? 

  let $x as feet := 15 return $x

I believe it is not, since the literal 15 is given the type xs:integer by the 
literal typing rule above. The typing rule for let specifies that 
"xs:integer" should be a subtype of "feet".  By definition, "xs:integer" is a 
subtype of type "feet" iff every value that matches "xs:integer" also matches 
"feet".  However, the value "15 of type xs:integer" will not match type 
"feet", since there is only one matching rule for atomic values:

  statEnv |- AtomicTypeName1 derives from AtomicTypeName2   
------------------------------------------------------------------------------------------------------
  statEnv |- AtomicValue of type AtomicTypeName1 matches AtomicTypeName2

In our case, the value "xs:integer" is not derived from "feet". Obviously, the 
value is matched by type "xs:integer". Hence, "xs:integer" is not a subtype 
of "feet", and the expression above is ill-typed. 

Is my reasoning correct? If so, does this signal an error in the static 
semantics or is there something inherently "wrong" with the expression above 
(justifying the ill-typedness)? 

--Stijn Vansummeren

Limburgs Universitair Centrum
Universitaire Campus 
Gebouw D
3590 Diepenbeek
Belgium