Proposed change to Dynamic library: mark it unsafe

[Alastair David Reid]

This morning, there was a bug report on the ghc bug list reporting
that they were able to crash ghci using a bad instance of typeOf (a
method in Dynamic/Typeable).  The report recognised that the problem
was in the instance decl but wasn't sure exactly what was wrong or
what the rules were.  This report got me thinking...

The Haskell libraries are fairly consistent about using the word
"unsafe" on any function which could break type safety, referential
transparency, etc. if misused.  An exception to this is the typeOf
method which the Dynamic library blindly assumes you have defined
correctly.  Lacking the hint that this is an "unsafe" feature,
beginners could well believe that any definition they use will work
(meaning "not crash Haskell") when, in fact, there are a bunch of
subtle issues in how it interacts with polymorphism.

An obvious fix would be to change the method name from "typeOf" to
"unsafeTypeOf" - reflecting the fact that a bad definition breaks type
safety and can lead to segmentation faults.  But this wrongly labels
uses of typeOf as being unsafe when it's definitions which are
(potentially) unsafe.  We can avoid this problem by separating
definitions from uses.

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.

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.

-- 
Alastair Reid        reid@cs.utah.edu        http://www.cs.utah.edu/~reid/