Back to explicit Coercible instances?

[Joachim Breitner]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131012/7de64991/attachment.sig>