On Sep 6, 2013, at 12:47 PM, Simon Peyton-Jones
So
* for newtypes newtype N a = MkN <rep-ty> the coercion is between (N a) and its representation type
. 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