unsafeCoerce and type aliases under type applications

[Brent Yorgey]

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
> > > <mail at joachim-breitner.de>  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