SPARK and static unit checking?

[Jacob Sparre Andersen <jspa@nykredit.dk>]

I have found a rather annoying (but in some ways very reasonable) rule
in SPARK:

   You are not allowed to (re)declare operators for a type.

This prevents me from using my standard trick for static unit type
checking:

   type Length is private;
   function "+" (L, R : Length) return Length; -- not SPARK
   ...
   Meter : constant Length;

   type Area is private;
   function "*" (L, R : Length) return Area; -- not SPARK
   ...

I have an idea for a (clumsy) solution:  Generate two packages with
the same types (name-wise).  The one as above, the other simply as:

   type Length is new Float;
   type Area is new Float;

Then I can use the liberal version with the SPARK tools, and swap the
restrictive in for the proper compilation.

Any proposals for an elegant solution?

Jacob
--
[ I left my signature generator at home. ]