Re: unsafeCoerce and type aliases under type applications

On Sun, Dec 04, 2011 at 11:17:25AM +0100, Joachim Breitner wrote:

Hi,

Am Sonntag, den 04.12.2011, 00:50 -0500 schrieb wren ng thornton:

...

On 12/3/11 9:07 PM, Felipe Almeida Lessa wrote:

...

On Sat, Dec 3, 2011 at 5:39 PM, Joachim Breitner wrote:

...

have used unsafeCoerce to change the type inside a container to a "type" alias in real code, but your post makes me wonder: Under what circumstances is that safe? Is that documented somehow? Can a tool or the compiler decide for us whether it is safe?

AFAIK, newtypes are safe, and for everything else you're on your own. =)

N.B., newtypes are safe in the sense of congruent rewriting; i.e., if X is a newtype of Y, then we can rewrite X to Y (or Y to X) in any subterm of the type term (just like if X = Y or X ~ Y). It's not just at the top-level of the type term.

that is what I would expect at first glance, but at least some type features break this behavior:

So the question remains: Under which circumstances is newtypes coercing within a type term using unsafeCoerce safe?

Intuitively, it is safe to do newtype coercing as long as the newtype is treated "parametrically" by the context, i.e. it never appears as the argument to a type family. In principle this analysis could be done in an automated way; actually, the fact that GHC *doesn't* do this analysis means that GeneralizedNewtypeDeriving is unsound in the presence of type families; see http://hackage.haskell.org/trac/ghc/ticket/1496. For one approach to solving this see "Generative type abstraction and type-level computation" (POPL 2011) by Weirich, Vytiniotis, Peyton-Jones, and Zdancewic. It isn't implemented yet, but once it (or something like it) is, it may not be too hard to expose the ability to explicitly do congruent newtype coercing to the user. -Brent