Be more cautious about inferred roles

[matt-noonan]

@enobayram discovered in the justified-containers library that using phantom roles for phantom type parameters in GDP-style interfaces leads to a back-door:

https://github.com/matt-noonan/justified-containers/issues/8

The solution is to ensure that the phantom type variables used for gdp things always have role nominal. For example, the inferred role of p in data Proof p = QED is phantom, so a user(!) could write coerce :: Proof TRUE -> Proof FALSE. That's bad.

Instead, we should write:

{-# LANGUAGE RoleAnnotations #-}
data Proof p = QED
type role Proof nominal

The same goes for library-defined predicates and names, like data IsCons xs or newtype Head xs = Head Defn. The role of xs in each case needs to be explicitly annotated as nominal, or else the user could coerce the IsCons xs fact from a non-empty xs to nil. Gross.

[matt-noonan]

As for introducing existentially-quantified names, there are two approaches:

type a ~~ name = Named name a
newtype Named name a = Named a
type role Named nominal representational

or

type role Named nominal nominal

At first glance, it isn't quite clear to me which one of these is correct. Probably the nominal / nominal one.

[enobayram]

I'd say nominal / nominal, because, for instance if a is, say, supposed to be a sorted list w.r.t its elements' own Ord instance, representational would stop the show.

[enobayram]

I think this is a very sneaky issue, since in certain programming styles one could bump into this issue without even trying. For example if one is using newtypes like Product for their Monoid instances inside Maps, they would probably like to use coerce for simplicity and efficiency. If the same container happens to contain a gdp somewhere in it, all bets are off.

[matt-noonan]

Fixed in 6e09928.