Well, the point is that you can name however many different refinements you want over the same data structure and the coercions have no dynamic content.

so I could write

`datatype nat = NatZero of Z | NatSucc of Nat S`and then write (assuming I put in a map function for the NewXTag functor as I neglected to do; say smap : ('a -> 'b) -> 'a S.stag -> 'b S.stag)

fun staticEvenToNat (Succ (x : odd S)) = NatSucc(smap staticOddToNat odd)
| staticEvenToNat Zero = NatZero
and staticOddToNat (x : even S) = NatSucc(smap staticEvenToNat x)

which is a

*proof* that the even and odd refinements are subrefinements of the trivial refinement on nats (although this is still a nontrivial refinement on the larger type xrec!) and then I can do something like

(* val evenToNat : even xrec -> nat xrec *)
fun evenToNat e = coe EvenToNat e

which is operationally equivalent to the identity function.