Implement "roles" into GHC.

Roles are a solution to the GeneralizedNewtypeDeriving type-safety
problem.

Roles were first described in the "Generative type abstraction" paper,
by Stephanie Weirich, Dimitrios Vytiniotis, Simon PJ, and Steve Zdancewic.
The implementation is a little different than that paper. For a quick
primer, check out Note [Roles] in Coercion. Also see
http://ghc.haskell.org/trac/ghc/wiki/Roles
and
http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
For a more formal treatment, check out docs/core-spec/core-spec.pdf.

This fixes Trac #1496, #4846, #7148.

6 files changed, 247 insertions, 66 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index c452877ad5..c2dba49612 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -1,3 +1,9 @@
+%%
+%% CoreLint.ott
+%%
+%% defines formal version of core typing rules
+%%
+%% See accompanying README file
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Static semantics  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -54,7 +60,7 @@ t = literalType lit
 G |-tm lit : t
 
 G |-tm e : s
-G |-co g : s ~#k t
+G |-co g : s ~Rep k t
 ------------------- :: Cast
 G |-tm e |> g : t
 
@@ -115,7 +121,7 @@ G |-ty t : k2
 ---------------------------------------------------- :: Case
 G |-tm case e as z_s return t of </ alti // i /> : t
 
-G |-co g : t1 ~#k t2
+G |-co g : t1 ~Nom k t2
 -------------------- :: Coercion
 G |-tm g : t1 ~#k t2
 
@@ -144,88 +150,101 @@ G |-ki k ok
 ---------------------------------------- :: TyVar
 G |-bnd alpha_k ok
 
-defn G  |- co g : t1 ~# k t2 ::  :: lintCoercion :: 'Co_'
+defn G  |- co g : t1 ~ R k t2 ::  :: lintCoercion :: 'Co_'
   {{ com Coercion typing, \coderef{coreSyn/CoreLint.lhs}{lintCoercion} }}
-  {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{\sim_{\#}^{[[k]]} } [[t2]] }}
+  {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{\sim_{[[R]]}^{[[k]]} } [[t2]] }}
 by
 
 G |-ty t : k
 ---------------------- :: Refl
-G |-co <t> : t ~#k t
+G |-co <t>_R : t ~R k t
 
-G |-co g1 : s1 ~#k1 t1
-G |-co g2 : s2 ~#k2 t2
+G |-co g1 : s1 ~R k1 t1
+G |-co g2 : s2 ~R k2 t2
 G |-arrow k1 -> k2 : k
 ------------------------- :: TyConAppCoFunTy
-G |-co (->) g1 g2 : (s1 -> s2) ~#k (t1 -> t2)
+G |-co (->)_R g1 g2 : (s1 -> s2) ~R k (t1 -> t2)
 
 T /= (->)
-</ G |-co gi : si ~#ki ti // i />
+</ Ri // i /> = tyConRolesX R T
+</ G |-co gi : si ~Ri ki ti // i />
 G |-app </ (si : ki) // i /> : tyConKind T ~> k
 --------------------------------- :: TyConAppCo
-G |-co T </ gi // i /> : T </ si // i />  ~#k T </ ti // i />
+G |-co T_R </ gi // i /> : T </ si // i />  ~R k T </ ti // i />
 
-G |-co g1 : s1 ~#k1 t1
-G |-co g2 : s2 ~#k2 t2
+G |-co g1 : s1 ~R k1 t1
+G |-co g2 : s2 ~Nom k2 t2
 G |-app (s2 : k2) : k1 ~> k
 --------------------- :: AppCo
-G |-co g1 g2 : (s1 s2) ~#k (t1 t2)
+G |-co g1 g2 : (s1 s2) ~R k (t1 t2)
+
+G |-co g1 : s1 ~Ph k1 t1
+G |-co g2 : s2 ~Ph k2 t2
+G |-app (s2 : k2) : k1 ~> k
+--------------------- :: AppCoPhantom
+G |-co g1 g2 : (s1 s2) ~Ph k (t1 t2)
 
 G |-ki k1 ok
-G, z_k1 |-co g : s ~#k2 t
+G, z_k1 |-co g : s ~R k2 t
 --------------------------- :: ForAllCo
-G |-co forall z_k1. g : (forall z_k1.s) ~#k2 (forall z_k1.t)
+G |-co forall z_k1. g : (forall z_k1.s) ~R k2 (forall z_k1.t)
 
 z_(t ~#BOX t) elt G
 ----------------------- :: CoVarCoBox
-G |-co z_(t ~#BOX t) : t ~#BOX t
+G |-co z_(t ~#BOX t) : t ~Nom BOX t
 
 z_(s ~#k t) elt G
 k /= BOX
------------------------ :: CoVarCo
-G |-co z_(s ~#k t) : s ~#k t
+----------------------- :: CoVarCoNom
+G |-co z_(s ~#k t) : s ~Nom k t
+
+z_(s ~R#k t) elt G
+k /= BOX
+----------------------- :: CoVarCoRepr
+G |-co z_(s ~R#k t) : s ~Rep k t
 
 G |-ty t1 : k
------------------------------ :: UnsafeCo
-G |-co t1 ==>! t2 : t1 ~#k t2
+----------------------------- :: UnivCo
+G |-co t1 ==>!_R t2 : t1 ~R k t2
 
-G |-co g : t1 ~#k t2
+G |-co g : t1 ~R k t2
 ------------------------- :: SymCo
-G |-co sym g : t2 ~#k t1
+G |-co sym g : t2 ~R k t1
 
-G |-co g1 : t1 ~#k t2
-G |-co g2 : t2 ~#k t3
+G |-co g1 : t1 ~R k t2
+G |-co g2 : t2 ~R k t3
 ----------------------- :: TransCo
-G |-co g1 ; g2 : t1 ~#k t3
+G |-co g1 ; g2 : t1 ~R k t3
 
-G |-co g : (T </ sj // j />) ~#k (T </ tj // j />)
+G |-co g : (T </ sj // j />) ~R k (T </ tj // j />)
 length </ sj // j /> = length </ tj // j />
 i < length </ sj // j />
 G |-ty si : k
+R' = (tyConRolesX R T)[i]
 ---------------------- :: NthCo
-G |-co nth i g : si ~#k ti
+G |-co nth i g : si ~R' k ti
 
-G |-co g : (s1 s2) ~#k (t1 t2)
+G |-co g : (s1 s2) ~Nom k' (t1 t2)
 G |-ty s1 : k
 ----------------------- :: LRCoLeft
-G |-co Left g : s1 ~#k t1
+G |-co Left g : s1 ~Nom k t1
 
-G |-co g : (s1 s2) ~#k (t1 t2)
+G |-co g : (s1 s2) ~Nom k' (t1 t2)
 G |-ty s2 : k
 ----------------------- :: LRCoRight
-G |-co Right g : s2 ~#k t2
+G |-co Right g : s2 ~Nom k t2
 
-G |-co g : forall m.s ~#k forall n.t
+G |-co g : forall m.s ~R k forall n.t
 G |-ty t0 : k0
 m = z_k1
 k0 <: k1
 --------------------- :: InstCo
-G |-co g t0 : s[m |-> t0] ~#k t[n |-> t0]
+G |-co g t0 : s[m |-> t0] ~R k t[n |-> t0]
 
-C = T </ axBranchkk // kk />
+C = T_R0 </ axBranchkk // kk />
 0 <= ind < length </ axBranchkk // kk />
-forall </ ni // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind]
-</ G |-co gi : s'i ~#k'i t'i // i />
+forall </ ni_Ri // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind]
+</ G |-co gi : s'i ~Ri k'i t'i // i />
 </ substi @ // i /> = inits(</ [ ni |-> s'i ] // i />)
 </ ni = zi_ki // i />
 </ k'i <: substi(ki) // i />
@@ -234,7 +253,76 @@ no_conflict(C, </ s2j // j />, ind, ind-1)
 t2 = t1 </ [ni |-> t'i] // i />
 G |-ty t2 : k
 ------------------------------------------------------ :: AxiomInstCo
-G |-co C ind </ gi // i /> : T </ s2j // j /> ~#k t2
+G |-co C ind </ gi // i /> : T </ s2j // j /> ~R0 k t2
+
+defn validRoles T ::  :: checkValidRoles :: 'Cvr_'
+  {{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }}
+by  
+
+</ Ki // i /> = tyConDataCons T
+</ Rj // j /> = tyConRoles T
+</ validDcRoles </ Rj // j /> Ki // i />
+------------------------------------ :: DataCons
+validRoles T
+
+defn validDcRoles </ Raa // aa /> K :: :: check_dc_roles :: 'Cdr_'
+  {{ com Data constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{check\_dc\_roles} }}
+by
+
+forall </ naa // aa />. forall </ mbb // bb />. </ tcc // cc /> @ -> T </ naa // aa /> = dataConRepType K
+</ </ naa : Raa // aa />, </ mbb : Nom // bb /> |- tcc : Rep // cc />
+--------------------------------- :: Args
+validDcRoles </ Raa // aa /> K
+
+defn O |- t : R  ::   :: check_ty_roles :: 'Ctr_'
+  {{ com Type role validity, \coderef{typecheck/TcTyClsDecls.lhs}{check\_ty\_roles} }}
+  {{ tex [[O]] \labeledjudge{ctr} [[t]] : [[R]] }}
+by
+
+O(n) = R'
+R' <= R
+---------- :: TyVarTy
+O |- n : R
+
+</ Ri // i /> = tyConRoles T
+</ Ri elt { Nom, Rep } => O |- ti : Ri // i />
+-------------------------- :: TyConAppRep
+O |- T </ ti // i /> : Rep
+
+</ O |- ti : Nom // i />
+--------------------------- :: TyConAppNom
+O |- T </ ti // i /> : Nom
+
+O |- t1 : R
+O |- t2 : Nom
+-------------------------- :: AppTy
+O |- t1 t2 : R
+
+O |- t1 : R
+O |- t2 : R
+------------------- :: FunTy
+O |- t1 -> t2 : R
+
+O, n : Nom |- t : R
+--------------------- :: ForAllTy
+O |- forall n. t : R
+
+------------------ :: LitTy
+O |- lit : R
+
+defn R1 <= R2 ::  :: ltRole :: 'Rlt_'
+  {{ com Sub-role relation, \coderef{types/Coercion.lhs}{ltRole} }}
+  {{ tex [[R1]] \leq [[R2]] }}
+by
+
+-------- :: Nominal
+Nom <= R
+
+-------- :: Phantom
+R <= Ph
+
+------- :: Refl
+R <= R 
 
 defn G |- ki k ok ::  :: lintKind :: 'K_'
   {{ com Kind validity, \coderef{coreSyn/CoreLint.lhs}{lintKind} }}
@@ -410,24 +498,24 @@ by
 ------------------------------------------------ :: NoBranch
 no_conflict(C, </ si // i/>, ind, -1)
 
-C = T </ axBranchkk // kk />
-forall </ ni // i />. (</ tj // j /> ~> t') = (</ axBranchkk // kk />)[ind2]
+C = T_R </ axBranchkk // kk />
+forall </ ni_Ri // i />. (</ tj // j /> ~> t') = (</ axBranchkk // kk />)[ind2]
 apart(</ sj // j />, </ tj // j />)
 no_conflict(C, </ sj // j />, ind1, ind2-1)
 ------------------------------------------------ :: Incompat
 no_conflict(C, </ sj // j />, ind1, ind2)
 
-C = T </ axBranchkk // kk />
-forall </ ni // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1]
-forall </ n'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2]
+C = T_R </ axBranchkk // kk />
+forall </ ni_Ri // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1]
+forall </ n'i_R'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2]
 apart(</ tj // j />, </ t'j // j />)
 no_conflict(C, </ sj // j />, ind1, ind2-1)
 ------------------------------------------- :: CompatApart
 no_conflict(C, </ sj // j />, ind1, ind2)
 
-C = T </ axBranchkk // kk />
-forall </ ni // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1]
-forall </ n'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2]
+C = T_R </ axBranchkk // kk />
+forall </ ni_Ri // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1]
+forall </ n'i_R'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2]
 unify(</ tj // j />, </ t'j // j />) = subst
 subst(s) = subst(s')
 ----------------------------------------- :: CompatCoincident
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index e6fae08956..ca060f2f72 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -1,3 +1,9 @@
+%%
+%% CoreSyn.ott
+%%
+%% defines formal version of core syntax
+%%
+%% See accompanying README file
 
 embed {{ tex-preamble
   \newcommand{\coderef}[2]{\ghcfile{#1}:\texttt{#2}%
@@ -93,6 +99,8 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}
   | tyConKind T             :: M :: tyConKind     {{ com \coderef{types/TyCon.lhs}{tyConKind} }}
   | t1 ~# k t2              :: M :: unliftedEq    {{ com Metanotation for coercion types }}
     {{ tex [[t1]] \mathop{\sim_{\#}^{[[k]]} } [[t2]] }}
+  | t1 ~R# k t2             :: M :: unliftedREq   {{ com Metanotation for coercion types }}
+    {{ tex [[t1]] \mathop{\sim_{\mathsf{R}\#}^{[[k]]} } [[t2]] }}
   | literalType t           :: M :: literalType   {{ com \coderef{basicTypes/Literal.lhs}{literalType} }}
   | ( t )                   :: M :: parens        {{ com Parentheses }}
   | t [ n |-> s ]           :: M :: TySubst       {{ com Type substitution }}
@@ -106,14 +114,14 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}
 %% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 g {{ tex \gamma }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/Coercion.lhs}{Coercion} }}
-  | < t >                   ::   :: Refl          {{ com Reflexivity }}
-    {{ tex \langle [[t]] \rangle }}
-  | T </ gi // i />         ::   :: TyConAppCo    {{ com Type constructor application }}
+  | < t > _ R               ::   :: Refl          {{ com Reflexivity }}
+    {{ tex {\langle [[t]] \rangle}_{[[R]]} }}
+  | T RA  </ gi // i />     ::   :: TyConAppCo    {{ com Type constructor application }}
   | g1 g2                   ::   :: AppCo         {{ com Application }}
   | forall n . g            ::   :: ForAllCo      {{ com Polymorphism }}
   | n                       ::   :: CoVarCo       {{ com Variable }}
   | C ind </ gj // j />     ::   :: AxiomInstCo   {{ com Axiom application }}
-  | t1 ==>! t2              ::   :: UnsafeCo      {{ com Unsafe coercion }}
+  | t1 ==>! RA t2           ::   :: UnivCo        {{ com Universal coercion }}
   | sym g                   ::   :: SymCo         {{ com Symmetry }}
   | g1 ; g2                 ::   :: TransCo       {{ com Transitivity }}
   | nth I g                 ::   :: NthCo         {{ com Projection (0-indexed) }}
@@ -128,12 +136,21 @@ LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/Co
   | Right            ::   :: CRight               {{ com Right projection }}
 
 C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.lhs}{CoAxiom} }}
-  | T </ axBranchi // ; // i />    ::   :: CoAxiom  {{ com Axiom }}
+  | T RA </ axBranchi // ; // i /> ::   :: CoAxiom  {{ com Axiom }}
   | ( C )                          :: M :: Parens   {{ com Parentheses }}
 
+R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.lhs}{Role} }}
+  | Nom              ::   :: Nominal              {{ com Nominal }}
+    {{ tex \mathsf{N} }}
+  | Rep              ::   :: Representational     {{ com Representational }}
+    {{ tex \mathsf{R} }}
+  | Ph               ::   :: Phantom              {{ com Phantom }}
+    {{ tex \mathsf{P} }}
+  | role_list [ i ]  :: M :: RoleListIndex        {{ com Look up in list }}
+
 axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.lhs}{CoAxBranch} }}
-  | forall </ ni // i /> . ( </ tj // j /> ~> s )  ::   :: CoAxBranch  {{ com Axiom branch }}
-  | ( </ axBranchi // i /> ) [ ind ]               :: M :: lookup      {{ com List lookup }}
+  | forall </ ni RAi // i /> . ( </ tj // j /> ~> s )  ::   :: CoAxBranch  {{ com Axiom branch }}
+  | ( </ axBranchi // i /> ) [ ind ]                   :: M :: lookup      {{ com List lookup }}
 
 %% TYCONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -149,13 +166,14 @@ T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
   | dataConTyCon K :: M :: dataConTyCon    {{ com TyCon extracted from DataCon }}
 
 H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{prelude/TysPrim.lhs}{} }}
-  | Int#         ::   :: intPrimTyCon           {{ com Unboxed Int }}
-  | ( ~# )       ::   :: eqPrimTyCon            {{ com Unboxed equality }}
-  | BOX          ::   :: superKindTyCon         {{ com Sort of kinds }}
-  | *            ::   :: liftedTypeKindTyCon    {{ com Kind of lifted types }}
-  | #            ::   :: unliftedTypeKindTyCon  {{ com Kind of unlifted types }}
-  | OpenKind     ::   :: openTypeKindTyCon      {{ com Either $*$ or $\#$ }}
-  | Constraint   ::   :: constraintTyCon        {{ com Constraint }}
+  | Int#         ::   :: intPrimTyCon           {{ com Unboxed Int (\texttt{intPrimTyCon}) }}
+  | ( ~# )       ::   :: eqPrimTyCon            {{ com Unboxed equality (\texttt{eqPrimTyCon}) }}
+  | ( ~R# )      ::   :: eqReprPrimTyCon        {{ com Unboxed representational equality (\texttt{eqReprPrimTyCon}) }}
+  | BOX          ::   :: superKindTyCon         {{ com Sort of kinds (\texttt{superKindTyCon}) }}
+  | *            ::   :: liftedTypeKindTyCon    {{ com Kind of lifted types (\texttt{liftedTypeKindTyCon}) }}
+  | #            ::   :: unliftedTypeKindTyCon  {{ com Kind of unlifted types (\texttt{unliftedTypeKindTyCon}) }}
+  | OpenKind     ::   :: openTypeKindTyCon      {{ com Either $*$ or $\#$ (\texttt{openTypeKindTyCon}) }}
+  | Constraint   ::   :: constraintTyCon        {{ com Constraint (\texttt{constraintTyCon}) }}
 
 %% CONTEXTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -164,6 +182,10 @@ G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{co
   | </ Gi // , // i />       ::   :: Concat    {{ com Context concatenation }}
   | vars_of binding          :: M :: VarsOf    {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
 
+O {{ tex \Omega }} :: 'VarEnv_Role_' ::= {{ com Mapping from type variables to roles }}
+  | </ ni : Ri // i />       ::   :: List      {{ com List of bindings }}
+  | O1 , O2                  :: M :: Concat    {{ com Concatenate two lists }}
+
 S {{ tex \Sigma }} :: 'St_' ::= {{ com Runtime store }}
   | [ n |-> e ]            ::   :: Binding  {{ com Single binding }}
   | </ Si // , // i />     ::   :: Concat   {{ com Store concatentation }}
@@ -201,6 +223,17 @@ ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
 type_list :: 'TypeList_' ::= {{ com List of types }}
   | </ si // i />     ::   :: List
 
+RA {{ tex {\!\!\!{}_{\rho} } }} :: 'RoleAnnot_' ::= {{ com Role annotation }}
+  | _ R                    :: M :: annotation
+  {{ tex {}_{[[R]]} }}
+
+role_list :: 'RoleList_' ::= {{ com List of roles }}
+  | </ Ri // , // i />     ::   :: List
+  | tyConRolesX R T        :: M :: tyConRolesX
+  | tyConRoles T           :: M :: tyConRoles
+  | ( role_list )          :: M :: Parens
+  | { role_list }          :: M :: Braces
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Terminals  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -226,6 +259,7 @@ terminals :: 'terminals_' ::=
   | BOX          ::   :: BOX              {{ tex \Box }}
   | Int#         ::   :: int_hash         {{ tex {\textsf{Int} }_{\#} }}
   | ~#           ::   :: eq_hash          {{ tex \mathop{ {\sim}_{\#} } }}
+  | ~R#          ::   :: eq_repr_hash     {{ tex \mathop{ {\sim}_{\mathsf{R}\#} } }}
   | OpenKind     ::   :: OpenKind         {{ tex \textsf{OpenKind} }}
   | ok           ::   :: ok               {{ tex \textsf{ ok} }}
   | no_duplicates ::  :: no_duplicates    {{ tex \textsf{no\_duplicates } }}
@@ -257,6 +291,11 @@ terminals :: 'terminals_' ::=
   | no_conflict  ::   :: no_conflict      {{ tex \textsf{no\_conflict} }}
   | apart        ::   :: apart            {{ tex \textsf{apart} }}
   | unify        ::   :: unify            {{ tex \textsf{unify} }}
+  | tyConRolesX  ::   :: tyConRolesX      {{ tex \textsf{tyConRolesX} }}
+  | tyConRoles   ::   :: tyConRoles       {{ tex \textsf{tyConRoles} }}
+  | tyConDataCons ::  :: tyConDataCons    {{ tex \textsf{tyConDataCons} }}
+  | validRoles   ::   :: validRoles       {{ tex \textsf{validRoles} }}
+  | validDcRoles ::   :: validDcRoles     {{ tex \textsf{validDcRoles} }}
   | -->          ::   :: steps            {{ tex \longrightarrow }}
   | coercionKind ::   :: coercionKind     {{ tex \textsf{coercionKind} }}
 
@@ -303,6 +342,14 @@ formula :: 'formula_' ::=
   | C1 = C2                            ::   :: axiom_rewrite
   | apart ( </ ti // i /> , </ sj // j /> ) :: :: apart
   | unify ( </ ti // i /> , </ sj // j /> ) = subst :: :: unify
+  | role_list1 = role_list2            ::   :: eq_role_list
+  | R1 /= R2                           ::   :: role_neq
+  | R1 = R2                            ::   :: eq_role
+  | </ Ki // i /> = tyConDataCons T    ::   :: tyConDataCons
+  | O ( n ) = R                        ::   :: role_lookup
+  | R elt role_list                    ::   :: role_elt
+  | formula1 => formula2               ::   :: implication
+    {{ tex [[formula1]] \implies [[formula2]] }}
   | alt1 = alt2                        ::   :: alt_rewrite
   | e1 = e2                            ::   :: e_rewrite
   | no other case matches              ::   :: no_other_case
@@ -336,4 +383,6 @@ Subst_TmMapping <= Type_TySubstListPost
 
 Expr_Type <= formula_e_rewrite
 
+Coercion_TyConAppCo <= Coercion_AppCo
+
 Expr_Coercion <= Subst_TmMapping
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index 53e1f288a9..1c21ada0ec 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -83,7 +83,7 @@ S |- case e as n return t of </ alti // i /> --> u[n |-> e]
 
 T </ taa // aa /> ~#k T </ t'aa // aa /> = coercionKind g
 forall </ alphaaa_kaa // aa />. forall </ betabb_k'bb // bb />. </ t1cc // cc /> @-> T </ alphaaa_kaa // aa /> = dataConRepType K
-</ e'cc = ecc |> (t1cc @ </ [alphaaa_kaa |-> nth aa g] // aa /> </ [betabb_k'bb |-> <sbb>] // bb />) // cc />
+</ e'cc = ecc |> (t1cc @ </ [alphaaa_kaa |-> nth aa g] // aa /> </ [betabb_k'bb |-> <sbb>_Nom] // bb />) // cc />
 --------------------------- :: CasePush
 S |- case (K </ taa // aa /> </ sbb // bb /> </ ecc // cc />) |> g as n return t2 of </ alti // i /> --> case K </ t'aa // aa /> </ sbb // bb /> </ e'cc // cc /> as n return t2 of </ alti // i />
 
diff --git a/docs/core-spec/README b/docs/core-spec/README
index e193955490..1fb304d261 100644
--- a/docs/core-spec/README
+++ b/docs/core-spec/README
@@ -64,7 +64,7 @@ your notation to LaTeX. Three different homs are used:
   help disambiguate otherwise-ambiguous parses. Getting these right is hard,
   so if you have trouble, you're not alone.
 
-- In one place, it was necessary to use an @ symbol to disambiguate parses. The
+- In a few places, it is necessary to use an @ symbol to disambiguate parses. The
   @ symbol is not typeset and is used solely for disambiguation. Feel free to use
   it if necessary to disambiguate other parses.
 
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 246be067fc..2e8134c7a1 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -7,6 +7,7 @@
 \usepackage{xcolor}
 \usepackage{fullpage}
 \usepackage{multirow}
+\usepackage{url}
 
 \newcommand{\ghcfile}[1]{\textsl{#1}}
 \newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
@@ -19,7 +20,7 @@
 \setlength{\parindent}{0in}
 \setlength{\parskip}{1ex}
 
-\newcommand{\gram}[1]{\ottgrammartabular{#1\ottinterrule}}
+\newcommand{\gram}[1]{\ottgrammartabular{#1\ottafterlastrule}}
 
 \begin{document}
 
@@ -148,13 +149,21 @@ a term-level literal, but we are ignoring this distinction here.
 
 Invariants on coercions:
 \begin{itemize}
-\item $[[<t1 t2>]]$ is used; never $[[<t1> <t2>]]$.
-\item If $[[<T>]]$ is applied to some coercions, at least one of which is not
-reflexive, use $[[T </ gi // i />]]$, never $[[<T> g1 g2]] \ldots$.
-\item The $[[T]]$ in $[[T </gi//i/>]]$ is never a type synonym, though it could
+\item $[[<t1 t2>_R]]$ is used; never $[[<t1>_R <t2>_Nom]]$.
+\item If $[[<T>_R]]$ is applied to some coercions, at least one of which is not
+reflexive, use $[[T_R </ gi // i />]]$, never $[[<T>_R g1 g2]] \ldots$.
+\item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
 be a type function.
 \end{itemize}
 
+Roles label what equality relation a coercion is a witness of. Nominal equality
+means that two types are identical (have the same name); representational equality
+means that two types have the same representation (introduced by newtypes); and
+phantom equality includes all types. See \url{http://ghc.haskell.org/trac/ghc/wiki/Roles}
+for more background.
+
+\gram{\ottR}
+
 Is it a left projection or a right projection?
 
 \gram{\ottLorR}
@@ -285,12 +294,22 @@ a dead id and for one-tuples. These checks are omitted here.
 
 \subsection{Coercion typing}
 
+In the coercion typing judgment, the $\#$ marks are left off the equality
+operators to reduce clutter. This is not actually inconsistent, because
+the GHC function that implements this check, \texttt{lintCoercion}, actually
+returns four separate values (the kind, the two types, and the role), not
+a type with head $[[(~#)]]$ or $[[(~R#)]]$. Note that the difference between
+these two forms of equality is interpreted in the rules \ottdrulename{Co\_CoVarCoNom}
+and \ottdrulename{Co\_CoVarCoRepr}.
+
 \ottdefnlintCoercion{}
 
 In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
 the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of 
 folding the substitution over the kinds for kind-checking.
 
+See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$.
+
 \subsection{Name consistency}
 
 There are two very similar checks for names, one declared as a local function:
@@ -327,6 +346,31 @@ There are two very similar checks for names, one declared as a local function:
 
 \ottdefnisSubKind{}
 
+\subsection{Roles}
+\label{sec:tyconroles}
+
+During type-checking, role inference is carried out, assigning roles to the
+arguments of every type constructor. The function $[[tyConRoles]]$ extracts these
+roles. Also used in other judgments is $[[tyConRolesX]]$, which is the same as
+$[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to account
+for potential oversaturation.
+
+The checks encoded in the following
+judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
+when \texttt{-dcore-lint} is set.
+
+\ottdefncheckValidRoles{}
+
+\ottdefncheckXXdcXXroles{}
+
+In the following judgment, the role $[[R]]$ is an \emph{input}, not an output.
+
+\ottdefncheckXXtyXXroles{}
+
+These judgments depend on a sub-role relation:
+
+\ottdefnltRole{}
+
 \subsection{Branched axiom conflict checking}
 \label{sec:no_conflict}
 
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 180d9bed78..cb21286abb 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf