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@haskell.org] On Behalf Of | Joachim Breitner | Sent: 12 October 2013 11:52 | To: ghc-devs@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@joachim-breitner.de • http://www.joachim-breitner.de/ | Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C | Debian Developer: nomeata@debian.org