newtype coercion wrapping status

Fri Sep 6 18:47:43 CEST 2013

| Well, that is the case when we want to unwrap a newtype. But this is not
| the case here: We have a data type and we want to cast one of its type
| arguments. Clearly, we want to have
|         instance Coercible a b => Coercible [a] [b]
| right? The instance above is just an other instance (heh) of that form.

Bother.  You are right. I was thinking of newtypes, and your point was about data types. Sorry.

Re-reading, your message makes perfect sense.  But I hate it.  

And hang on!  One of our poster-child examples is

    module Map ( Map, insert, lookup, ... ) where
	data Map a b = MkMap [(a,b)]

So Map is abstract. But we ABSOLUTELY DO want to allow people to coerce (Map a b) to (Map a c) if a,c are coercible.  We were going to do that by role annotations. The exact syntax is still under debate (http://ghc.haskell.org/trac/ghc/ticket/8185), but you say something like

	data Map a at N b = MkMap [(a,b)]

and now the instance should look like

	instance Coercible b1 b2 => Coercible (Map a b1) (Map a b2)

Nothing to do with the visibility of Map's data constructors!

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.

OK?  This is far from obvious (since I was very confused about it), so worth writing up on the design page. As well as implementing.

Roles are in HEAD so you can use them right now.

Simon