I don't like the Kawa "coercion" semantic for type declarations; I don't
think it is wrong per se, but I much prefer Common Lisps "assertion"
semantics. That is, in Common Lisp, if I declare that a variable has a
certain type, the compiler can do just about anything, provided the
program works correctly when the variable has that type. Common
behaviours are:

(a) Doing nothing.

(b) Complaining if the variable does not have that type.

(c) Assuming that the variable has that type and and acting in a way
that will be dangerous if it does not.

These are often offered as compilation options. They seem to offer a
wider range of useful behaviour and a wider range of trade-offs between
safety and optimization.

The "assertion" semantics also more naturally extend to limited ranges
(e.g., asserting that an integer is non-zero) or using unions of types.

Regards,

Alan
--
Dr Alan Watson
Centro de Radioastronomía y Astrofísica
Universidad Astronómico Nacional de México