Back to explicit Coercible instances?

[Simon Peyton-Jones]

I don’t really agree.  Here's why:

The exact rules you suggest for when "deriving(Coercible)" would be allowed, are the rules we can use for when we need a "from thin air" instance.

Moreover, I'm very keen to give a simple, precise answer to the question
	if s is coercible to t
	when is (T s) coercible to (T t)
I propose that the answer is given by precisely T's roles.  At the moment I don't see why we would want to do anything more complicated.

But I'm open to being persuaded otherwise

Simon

| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
| Joachim Breitner
| Sent: 12 October 2013 11:52
| To: ghc-devs at haskell.org
| Subject: Back to explicit Coercible instances?
| 
| Hi,
| 
| the recent discussion about roles and abstraction lets me wonder
| whether
| we should re-evaluate the question of where the Coercible instances
| come
| from.
| 
| Currently, upon use of "coerce", GHC will create Coercible instances
| out
| of thin air, as long as the roles agree, and checking some
| constructor-in-scope invariants. This is troublesome WRT. abstraction.
| 
| One alternative that was discussed before is explicit Coercible
| instances. That is, if I write a datatype
|         datatype MyList a = Cons a (MyList a) | MyNil
| then I have to explicitly write either
|                 deriving Coercible
| to get
|         instance Coercible a b => Coercible (MyList a) (MyList b)
| or – especially if I want to control which parameters are coercible –
| have to use standalone deriving and write
|         deriving instance Coercible a b => Coercible (MyList a) (MyList
|         b)
| 
| For something like Set, the user would not use “deriving Coercible”,
| but
| would use
|         deriving instance Coercible a b => Coercible (Set k a) (Set k
| b)
| 
| Manual instances of Coercible would be prohibited. The instances are
| checked for things like:
|  * do the roles allow the behaviour?
|  * are the constructors in scope (for standalone deriving)?
|  * are the arguments of the constructors coercible?
| The last check ensures that the user cannot break abstraction by
| wrapping an abstract datatype in a datatype of its own. But note that
| these instances (between the datacon argument types) are only checked,
| never actually used! Therefore we must sure that only sound instances
| exists, and that the user cannot bogus instances (e.g. one with all
| fields undefined).
| 
| This would imply a few differences:
|  * Already for syntactical reasons, there will be no instances for
| coercing constraints. As we have seen, this is a good thing.
|  * Would be no way to use a coercion within the abstraction boundaries,
| but not outside, because you either have the instance, or you don’t.
| 
| 
| And assuming GND would simply implement its classes by passing each
| method through "coerce", this would hopefully also yield a sensible
| design for GND.
| 
| 
| Greetings,
| Joachim
| 
| --
| Joachim “nomeata” Breitner
|   mail at joachim-breitner.de • http://www.joachim-breitner.de/
|   Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
|   Debian Developer: nomeata at debian.org