newtype coercion wrapping status

[Richard Eisenberg]

On Sep 6, 2013, at 12:47 PM, Simon Peyton-Jones <simonpj at microsoft.com> wrote:

> 
> So
> 
> * for newtypes
>       newtype N a = MkN <rep-ty> 
>  the coercion is between (N a) and its representation type <rep_ty>.
>  The coercion is allowed if the data constructor MkN is in scope
> 
> * for data types (T a), the coercion is between (T a) and (T b),
>  The coercion is allowed if the roles allow it.
> 
> The two are handled quite differently.

This makes me say "Yikes!"

I've always lived under the impression that changing the word "newtype" to "data" should have exactly 0 effect on the compile-time behavior of Haskell programs. Yet, you're proposing that

> module Foo (T) where   -- MkT is *not* exported
>
> newtype T a = MkT [a]

is different from the same with "newtype" replaced with "data". To wit, in the "data" version, the instance (Coercible a b => Coercible (T a) (T b)) would exist, but this would not be derivable in the "newtype" version. Right?

A related issue is that, even with roles, I don't think GeneralizedNewtypeDeriving (GND) is in the Safe Haskell subset because it can break abstraction barriers -- you can use GND even when a newtype's constructor is not in scope. The above proposal for coercions will have the same problem.

What to do? Map should certainly not export its constructor(s). Yet, we want (Coercible a b => Coercible (Map x a) (Map x b)). It seems that the writer of Map would have to explicitly export this instance. This goes at odds with the idea of "there aren't any instances of Coercible, really", but otherwise I have a hard time seeing how this would all work.

Am I missing something here?

Richard