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.''