Upward static coercion
let x = 7;; -> val x : 7 = 7
x has the value 7 and is of the type 7 (the singleton containing the integer seven)
let y1 = (x : Int);; let y2 : Int = x;;
These two upward coercions give the same thing: the value 7 of type Int. This is possible because the singleton 7 is a subset of the integers set.
The static downward coercion is not possible
type Positive = 1--* let y = (7 : Int);;
let yp = (y : Positive);; -> This expression should have type: Positive but its inferred type is: Int which is not a subtype, as shown by the sample: *--0
But the dynamic downward coercion is possible:
let yp1 :? Positive = y;; let yp2 = (y :? Positive);;
An exception is raised at execution is coercion is not possible
let ybad = (y :? Char);; -> Uncaught CDuce exception: "Value 7 does not match type Empty\n"
The message contains "Empty" because the dynamic coercion give the conjunction type. This can be seen writing
(7 : 1--8) :? 5--10;;
which appears having the type 5--8
Note that for upward coercion the static nethod is more efficient and gives better error handling. Furthermnore, due to the conjunction mechanism, the upward coercion cannot be dynamic:
(7 : 1--8) :? Int;;
continues to be of type 1--8, not Int.