1 | | For Richard E TODO: Write this page. |
2 | | Deadline: Aug 2, 2013. |
| 1 | = Roles Implementation = |
| 2 | |
| 3 | This page describes how roles are implemented in GHC. If you're looking for how |
| 4 | to use roles in a Haskell program, see [wiki:Roles]. |
| 5 | |
| 6 | == The `Role` datatype == |
| 7 | |
| 8 | The `Role` datatype, defined in `CoAxiom` to avoid mentioning it in an hs-boot |
| 9 | file, is defined thusly: |
| 10 | |
| 11 | {{{ |
| 12 | data Role = Nominal | Representational | Phantom |
| 13 | deriving (Eq, Data.Data, Data.Typeable) |
| 14 | }}} |
| 15 | |
| 16 | Two types are nominally equal when they have the same name. This is the usual |
| 17 | equality in Haskell or Core. Two types are representationally equal when they |
| 18 | have the same representation. (If a type is higher-kinded, all nominally equal |
| 19 | instantiations lead to representationally equal types.) Any two types are |
| 20 | "phantomly" equal. |
| 21 | |
| 22 | == Roles on `Coercion`s == |
| 23 | |
| 24 | Every coercion proves an equality at a certain role. There are subtle rules |
| 25 | governing what compositions are allowed. See |
| 26 | [[http://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf?raw=true|the core spec]] for the details, or look at `coercionRole`. To facilitate this, |
| 27 | a few of the `Coercion` constructors needed to be changed: |
| 28 | |
| 29 | * `Refl` now takes a role and a type, proving reflexive equality at the given role. |
| 30 | * `TyConAppCo` also takes a role. The choice of this role affects which roles the |
| 31 | arguments must be at. If the role is nominal, all arguments must be nominal. |
| 32 | If the role is phantom, all arguments must be phantom. But, if the role is |
| 33 | representational, the argument roles must correspond to `tyConRoles` called |
| 34 | on the tycon in the `TyConAppCo`. The idea is that different tycons have |
| 35 | different requirements in order to prove representational equality. See the |
| 36 | section below discussing roles with tycons. Note that, now, the interpretation |
| 37 | of a `TyConAppCo` may differ from that of nested `AppCo`s. |
| 38 | * `CoVarCo`s extract their role from their type. |
| 39 | * `UnivCo` is a new "universal" coercion. It takes a role and two types and witnesses |
| 40 | equality between those types at that role. It replaces the old `UnsafeCo`. |
| 41 | `UnivCo` at role P is needed in `TyConAppCo`s at role P. |
| 42 | * The role produced by `NthCo` is essentially the inverse of the `TyConAppCo` story. |
| 43 | If `NthCo`'s parameter is N or P, the result has the same role. If it's R, though, |
| 44 | the result's role is determined by `tyConRoles` once again. |
| 45 | * `SubCo` implements sub-roling: its argument is N and it produces R. |
| 46 | |
| 47 | Because coercions can be produced at any of the three roles, most functions that |
| 48 | produce them now take a `Role` parameter, indicating what role to produce. These, |
| 49 | in turn, make use of `maybeSubCo2` and `maybeSubCo`, which convert among the roles; |
| 50 | they are documented in the source. |
| 51 | |
| 52 | The functions `mkTyConAppCo` (and, in turn `mkFunCo`) now have a bit of a delicate |
| 53 | requirement on their arguments: the argument types must "match" the desired role. |
| 54 | Thus, if the desired role is R, the arguments must have the roles indicated by |
| 55 | `tyConRoles`. In practice, it is not hard to ensure this precondition, but you |
| 56 | do have to be aware of it. |
| 57 | |
| 58 | == Roles on `TcCoercion`s == |
| 59 | |
| 60 | The type checker operates solely on `TcCoercion`s. What roles do these have? Because |
| 61 | the type checker thinks only about nominal equality, it would make sense for all |
| 62 | `TcCoercion`s to have role N. But, sometimes the type checker needs to pass around |
| 63 | a coercion produced by a newtype (for example, in implicit-parameter handling). |
| 64 | So, they need to handle R coercions as well. But, we never lint a `TcCoercion`, so |
| 65 | we don't quite need to be as careful with them. |
| 66 | |
| 67 | The solution is that, when desugaring to `Coercion`s, we pass in a `Role` |
| 68 | parameter, indicating how we should interpret the `TcCoercion`. (Casts always |
| 69 | use R equality.) Because we hopefully never ask for nominal equality from a |
| 70 | newtype axiom, this works in practice. If a problem arises, it will most likely |
| 71 | take the form of a `maybeSubCo2` panic. |
| 72 | |
| 73 | == Roles with `TyCon`s == |
| 74 | |
| 75 | Every `TyCon`'s parameters are now each assigned a role. The interpretation is |
| 76 | this: if a parameter a of tycon T has role r, then a coercion at role r can be |
| 77 | lifted into a representational coercion of T a. Thus, N is the most |
| 78 | restrictive, and P is the most permissive. These roles are user-visible, so |
| 79 | they are described on the [wiki:Roles] page. |
| 80 | |
| 81 | Kind variables are all assigned role N. We must be careful when comparing a |
| 82 | tycon's roles against the role annotations, because role annotations are only |
| 83 | on ''type'' variables, never ''kind'' variables. So, we often have to drop |
| 84 | the kind-variable roles when doing the comparison. |
| 85 | |
| 86 | == `eqPrimTyCon` vs `eqReprPrimTyCon` == |
| 87 | |
| 88 | The type of a nominal coercion is headed by `eqPrimTyCon`, spelled `~#`. In |
| 89 | order to support NewtypeWrappers, we must also have a way of storing |
| 90 | representational coercions. Their types are headed by `eqReprPrimTyCon`, spelled |
| 91 | `~R#`. |