Note [Role inference]
The role inference algorithm datatype definitions to infer the roles on the parameters. Although these roles are stored in the tycons, we can perform this algorithm on the built tycons, as long as we don't peek at an as-yet-unknown roles field! Ah, the magic of laziness. First, we choose appropriate initial roles. For families and classes, roles (including initial roles) are N. For datatypes, we start with the role in the role annotation (if any), or otherwise use Phantom. This is done in initialRoleEnv1. The function irGroup then propagates role information until it reaches a fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a monad RoleM, which is a combination reader and state monad. In its state are the current RoleEnv, which gets updated by role propagation, and an update bit, which we use to know whether or not we've reached the fixpoint. The environment of RoleM contains the tycon whose parameters we are inferring, and a VarEnv from parameters to their positions, so we can update the RoleEnv. Between tycons, this reader information is missing; it is added by addRoleInferenceInfo. There are two kinds of tycons to consider: algebraic ones (excluding classes) and type synonyms. (Remember, families don't participate -- all their parameters are N.) An algebraic tycon processes each of its datacons, in turn. Note that a datacon's universally quantified parameters might be different from the parent tycon's parameters, so we use the datacon's univ parameters in the mapping from vars to positions. Note also that we don't want to infer roles for existentials (they're all at N, too), so we put them in the set of local variables. As an optimisation, we skip any tycons whose roles are already all Nominal, as there nowhere else for them to go. For synonyms, we just analyse their right-hand sides. irType walks through a type, looking for uses of a variable of interest and propagating role information. Because anything used under a phantom position is at phantom and anything used under a nominal position is at nominal, the irType function can assume that anything it sees is at representational. (The other possibilities are pruned when they're encountered.) The rest of the code is just plumbing. How do we know that this algorithm is correct? It should meet the following specification: Let Z be a role context -- a mapping from variables to roles. The following rules define the property (Z |- t : r), where t is a type and r is a role: Z(a) = r' r' <= r RCVar Z |- a : r RCConst Z |- T : r -- T is a type constructor Z |- t1 : r Z |- t2 : N RCApp Z |- t1 t2 : r forall i<=n. (r_i is R or N) implies Z |- t_i : r_i roles(T) = r_1 .. r_n RCDApp Z |- T t_1 .. t_n : R Z, a:N |- t : r RCAll Z |- forall a:k.t : r We also have the following rules: For all datacon_i in type T, where a_1 .. a_n are universally quantified and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p, then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R, then roles(T) = r_1 .. r_n roles(->) = R, R roles(~#) = N, N With -dcore-lint on, the output of this algorithm is checked in checkValidRoles, called from checkValidTycon.
References 0
This Note does not link to any other.
Referenced by 4
- GHC.Tc.TyCl.Utils call site ×2
- Decomposing newtypes a bit more aggressively GHC.Tc.Solver.Equality
- GHC.Tc.TyCl call site