Compiling GHC disabling the type checker

[roconnor at theorem.ca]

On Mon, 16 Oct 2006, Simon Marlow wrote:

> There's one restriction that I know of: you should be careful not to cast a 
> function value to a non-function type (except a polymorphic type), because 
> the two have incompatible representations when it comes to seq and case. 
> And of course, you should never cast an unboxed value to a boxed type or vice 
> versa. Apart from these, I think you should be fine to unsafeCoerce# away.

Coq's extraction mechinism uses the type () whenever it encounters a 
dependent type that it cannot make a Haskell type for.  Thus, all sorts of 
functions end up getting cast to () types.

Would it be safer to cast things to ``() -> ()'', or perhaps a single 
polymorphic variable ``a''?

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''