Proposal:

Replace the class:

class Typeable a where typeOf :: a -> Type

with:

typeOf :: Typeable a => a -> Type typeOf = unsafeTypeOf

class Typeable a where unsafeTypeOf :: a -> Type

All existing calls of typeOf should be left as they are. All existing instance declarations should be changed to define unsafeTypeOf instead.

Hmmm. I normally associate something called 'unsafeBlah' with being unsafe to use, not unsafe to define, so this seems a little odd. But I don't have any better suggestions, and I agree that there ought to be at least some indication that there's potential unsafety here.

We also need to clarify the rules for writing correct definitions. I propose the following concise (but non-constructive) rules:

1) New instances must preserve the invariant that for all values x and y with monomorphic types,

typeOf x == typeOf y iff x and y have the same type.

It is not sufficient for the types of x and y to have the same representation or to be isomorphic - they have to be considered identical by the Haskell type system. [This last sentence is redundant but may be helpful.]

2) For any (possibly bottom) value x whose type is an instance of Typeable,

typeOf x /= _|_ and does not raise an exception

Examples of valid and invalid definitions would also be useful.

Fully agree. The documentation is in CVS and you have commit access, I believe :-) (at least for the old libs, I haven't brought any docs across to the new libraries yet). Cheers, Simon