| 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@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