role signatures in libraries

[Richard Eisenberg]

Hi libraries,

It seems that the syntax and semantics of role annotations has settled, and so it's time to add role annotations to various libraries. Here are the key ideas:

tl;dr: Add nominal role annotations for abstract datatypes whose data has an invariant based on a class instance. Set and Map are top candidates.

- We have three notions of equality: nominal, representational, and phantom.

- Type equality as we know it is called *nominal*.

- A newtype is considered *representationally* equal to its representation type.
   * Thus, if we have `newtype Age = MkAge Int`, `Age` and `Int` are representationally equal.

- Any two types are "phantomly" equal.
   * See below for an illustrative example of why this notion is useful.

- Every type parameter of every datatype and class is assigned a role. A parameter's role says what notion of equality must hold to show that two instantiations of the datatype are representationally equal.
   * Say we have `Bar a` where a's role is nominal. That means that `Bar Age` is *not* representationally equal to `Bar Int`.
   * Say we have `Foo a` where a's role is representational. That means that `Foo Age` is representationally equal to `Foo Int`.
   * Say we have `Quux a` where a's role is phantom. That means that `Quux Int` is representationally equal to `Quux Bool`.

- Datatype roles are inferred to be the most permissive possible.
   * `data Bar a = MkBar (F a)` where `F` is a type family: a's role will be inferred to be nominal.
   * `data Foo a = MkFoo a`: a's role will be inferred to be representational.
   * `data Quux a = MkQuux String`: a's role will be inferred to be phantom.

- Class roles are inferred to be nominal.
   * This choice follows from the idea that the dictionaries for `Ord Int` and `Ord Age` should not be assumed to be the same.

- A role annotation can be used to change a parameter's role. The syntax is a top-level declaration `type role <typename> <list of roles>`. You need the extension RoleAnnotations to use these. Role names are spelled out (nominal, representational, phantom) and are in lower-case.
   * If we wanted, say, Quux's parameter's role to be representational, we could say `type role Quux representational`.

- Role annotations must be in the same module as a type is defined in.

- Roles can be left out by inserting `_`. This causes the role to be inferred.

- Role annotations cannot be used to undercut type safety. They are checked to make sure they meet this requirement.

- The new function `coerce` (in GHC.Exts) allows for 0-cost conversion between representationally equal types.
   * This means that converting [Quux Bool] to [Quux Int] is now free. This is why phantom equality is interesting.

- You should consider adding a role annotation on any type that has an invariant based on class instances.
   * For example, the information stored in a Set is ordered according to the data's Ord instance. So, there should probably be an annotation `type role Set nominal`.
   * As a further example, the data stored in a Map cares about the Ord instance of its first parameter but not its second. So, we would probably want `type role Map nominal representational`.

Note that the new roles stuff does *not* allow programmers to do more bad things than they could previously. A sufficiently clever use of GeneralizedNewtypeDeriving could invalidate any instance-based invariants you wished to impose. However, we now have the power to stop these leaks of abstraction. We also have, in `coerce`, an easier way to take advantage of any remaining holes, making it even more important to close the gaps.

The user manual is updated with respect to all the roles stuff -- you may want to see there for more info.

Please let me know if you have any questions about this!
Richard