[Haskell-cafe] Roles, GND, Data.Coerce

[David Terei]

All,

An issue that came up with GHC 7.8 was the design of Roles and
Data.Coerce, with it's ability to break module abstractions by
default, requiring programmers adopt explicit role annotations to
enforce some types of invariants for abstract data types.

Because of this issue, as of now, GND & Data.Coerce are still disabled
in Safe Haskell. We'd like to change this but need feedback from
everyone.

I've written up a wiki page with lots of information on the issue:

https://ghc.haskell.org/trac/ghc/wiki/SafeRoles

Please read, it has information on how Roles work, the problem it
raises and subtleties in the current system. Possible paths forward
are also there, but I'll include below.

Please be aware that this discussion is about Roles in general, not
specifically how when using -XSafe. Ideally we'd come up with a
solution that works regardless of if using Safe Haskell or not.

I personally like option (3), although it isn't clear to me how hairy
the implementation would be.

== Possible Paths Forward for Roles ==

1) Do Nothing -- Keep Roles & GND unchanged, keep them unsafe in Safe Haskell.

2) Accept as Safe -- Keep Roles & GND unchanged, accept them as safe
in Safe Haskell and warn users that they neednominal role annotations
on ADTs.

3) In-scope constructor restriction for lifting instances -- The
newtype constructor restriction for unwrapping instances could be
extended to both data types, and the lifting instances of Data.Coerce.
This is, GND & Coercing under a type constructor is allowed if (a) all
involved constructors are in scope, or (b) the constructors involved
have been explicitly declared to allow coercion without them being in
scope. I.e., (b) allows library authors to opt-into the current GHC
behavior. This would require new syntax, probably just an explicit
deriving Coercible statement.

4) Change default role to nominal -- This will prioritize safety over
GND, and the belief is that it may break a lot of code. Worse, that it
will be an ongoing tax as role annotations will be needed to enable
GND.

5) Nominal default when constructors aren't exported -- When a module
doesn't export all the constructors of a data type, then the type
parameters of the data type should default to nominal. This heuristic
seems to capture somewhat the intention of the user, but given the
practice of defining an Internal module that exports everything, it
seems of limited use.

6) Nominal default in future -- Add a new extension,
SafeNewtypeDeriving that switches the default role to nominal, but
continue to provide a deprecated GND extension to help with the
transition. The claims in support of representational roles as default
though believe that nominal by default has an ongoing, continuous tax,
not just a transition cost. So it isn't clear that any scheme like
this satisfies that argument.

7) Safe Haskell Specific -- Many of the above approaches could be
adopted in a Safe Haskell specific manner. This isn't ideal as it
makes safe-inference harder and Safe Haskell less likely to remain
viable going forward. Richard suggests one such idea.

==

The belief by many people seems to be that (4) and (6) would be too
much of burden. I'd like to avoid (7) if possible. It isn't clear to
me if (7) ends up better than (2).

I'm going to try to setup some infastructure for compiling Hackage so
that we can measure how impactful these changes would be.

Cheers,
David