merged master into late-dmdlate-dmd

7 files changed, 521 insertions, 91 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index beaf52a7d9..f2799841dc 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,10 +121,14 @@ G |-ty t : k2
 ---------------------------------------------------- :: Case
 G |-tm case e as z_s return t of </ alti // i /> : t
 
-G |-co g : t1 ~#k t2
--------------------- :: Coercion
+G |-co g : t1 ~Nom k t2
+-------------------- :: CoercionNom
 G |-tm g : t1 ~#k t2
 
+G |-co g : t1 ~Rep k t2
+----------------------- :: CoercionRep
+G |-tm g : (~R#) k t1 t2
+
 defn G  |- name n ok ::  :: lintSingleBinding_lintBinder :: 'Name_'
   {{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }}
   {{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }}
@@ -144,97 +154,179 @@ 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 />
-no_conflict(C, </ s2j // j />, ind-1)
+no_conflict(C, </ s2j // j />, ind, ind-1)
 </ s2j = s1j </ [ni |-> s'i] // i/> // j />
 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} }}
@@ -403,16 +495,32 @@ Constraint <: *
 ------------------ :: LiftedConstraint
 * <: Constraint
 
-defn no_conflict ( C , </ sj // j /> , ind ) ::  :: check_no_conflict :: 'NoConflict_'
-  {{ com Branched axiom conflict checking, \coderef{coreSyn/CoreLint.lhs}{lintCoercion\#check\_no\_conflict} }}
+defn no_conflict ( C , </ sj // j /> , ind1 , ind2 ) ::  :: check_no_conflict :: 'NoConflict_'
+  {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.lhs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.lhs}{compatibleBranches} } }}
 by
 
 ------------------------------------------------ :: NoBranch
-no_conflict(C, </ si // i/>, -1)
+no_conflict(C, </ si // i/>, ind, -1)
 
-C = T </ axBranchkk // kk />
-forall </ ni // i />. (</ tj // j /> ~> t') = (</ axBranchkk // kk />)[ind]
+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 />, ind-1)
------------------------------------------------- :: Branch
-no_conflict(C, </ sj // j />, ind)
+no_conflict(C, </ sj // j />, ind1, ind2-1)
+------------------------------------------------ :: Incompat
+no_conflict(C, </ sj // j />, ind1, 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_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
+no_conflict(C, </ sj // j />, ind1, ind2)
\ No newline at end of file
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 4c59849bb6..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}%
@@ -16,7 +22,7 @@ metavar alpha {{ tex \alpha }}, beta {{ tex \beta }} ::=
 metavar N ::=   {{ com Type-level constructor names }}
 metavar K ::=   {{ com Term-level data constructor names }}
 
-indexvar i, j, kk {{ tex k }} ::= {{ com Indices to be used in lists }}
+indexvar i, j, kk {{ tex k }}, aa {{ tex a }}, bb {{ tex b }}, cc {{ tex c }} ::= {{ com Indices to be used in lists }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Syntax  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -34,12 +40,17 @@ z :: 'Name_' ::= {{ com Term or type name }}
 n, m :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.lhs}{Var} }}
   | z _ t           ::   :: IdOrTyVar   {{ com Name, labeled with type/kind }}
     {{ tex {[[z]]}^{[[t]]} }}
+  | K               :: M :: DataCon     {{ com Data constructor }}
 
 vars :: 'Vars_' ::= {{ com List of variables }}
-  | </ ni // , // i />   ::   :: List
-  | fv ( t )             :: M :: fv
+  | </ ni // , // i />       ::   :: List
+  | fv ( t )                 :: M :: fv_t
     {{ tex \textit{fv}([[t]]) }}
-  | empty                :: M :: empty
+  | fv ( e )                 :: M :: fv_e
+    {{ tex \textit{fv}([[e]]) }}
+  | empty                    :: M :: empty
+  | vars1 \inter vars2       :: M :: intersection
+    {{ tex [[vars1]] \cap [[vars2]] }}
 
 e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
   | n                                            ::   :: Var  {{ com Variable }}
@@ -53,7 +64,10 @@ e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
     {{ tex {[[e]]}_{\{[[tick]]\} } }}
   | t                                            ::   :: Type {{ com Type }}
   | g                                            ::   :: Coercion {{ com Coercion }}
-  | e [ n |-> t ]                                :: M :: TySubst {{ com Type substitution }}
+  | e subst                                      :: M :: Subst    {{ com Substitution }}
+  | ( e )                                        :: M :: Parens {{ com Parenthesized expression }}
+  | e </ ui // i />                              :: M :: Apps {{ com Nested application }}
+  | S ( n )                                      :: M :: Lookup {{ com Lookup in the runtime store }}
 
 binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
   | n = e                         ::   :: NonRec  {{ com Non-recursive binding }}
@@ -85,43 +99,58 @@ 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 }}
   | subst ( k )             :: M :: TySubstList   {{ com Type substitution list }}
   | t subst                 :: M :: TySubstListPost {{ com Type substitution list }}
   | dataConRepType K        :: M :: dataConRepType {{ com Type of DataCon }}
+  | forall </ ni // , // i /> . t
+                            :: M :: ForAllTys     {{ com Nested polymorphism }}
+  | </ ti // i /> @ -> t'   :: M :: FunTys        {{ com Nested arrows }}
 
 %% 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) }}
-    {{ tex \textsf{nth}_{[[i]]}\,[[g]] }}
+  | nth I g                 ::   :: NthCo         {{ com Projection (0-indexed) }}
+    {{ tex \textsf{nth}_{[[I]]}\,[[g]] }}
   | LorR g                  ::   :: LRCo          {{ com Left/right projection }}
   | g t                     ::   :: InstCo        {{ com Type application }}
   | ( g )                   :: M :: Parens        {{ com Parentheses }}
+  | t @ liftingsubst        :: M :: Lifted        {{ com Type lifted to coercion }}
 
 LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/Coercion.lhs}{LeftOrRight} }}
   | Left             ::   :: CLeft                {{ com Left projection }}
   | Right            ::   :: CRight               {{ com Right projection }}
 
 C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.lhs}{CoAxiom} }}
-  | T </ axBranchi // ; // i />    ::   :: CoAxiom  {{ com Axiom }}
-  | ( C )                              :: M :: Parens   {{ com Parentheses }}
+  | 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -137,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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -152,6 +182,14 @@ 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 }}
+
 %% UTILITY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 B {{ tex \mathbb{B} }} :: 'Bool_' ::= {{ com Booleans in metatheory }}
@@ -162,17 +200,39 @@ kinded_types {{ tex \overline{(\sigma_i : \kappa_i)}^i }} :: 'Kinded_Types_' ::=
   | </ ( si : ki ) // , // i />    ::   :: List
   | empty                          :: M :: empty
 
-subst :: 'Subst_' ::= {{ com List of type substitutions }}
-  | [ n |-> t ]        ::   :: Mapping
+subst :: 'Subst_' ::= {{ com List of substitutions }}
+  | [ n |-> t ]        ::   :: TyMapping
+  | [ n |-> e ]        ::   :: TmMapping
   | </ substi // i />  ::   :: List
 
-ind :: 'Ind_' ::= {{ com Indices, numbers }}
+liftingsubst :: 'LiftSubst_' ::= {{ com List of lifting substitutions }}
+  | [ n |-> g ]               ::   :: Mapping
+  | </ liftingsubsti // i />  ::   :: List
+
+ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
   | i                           ::   :: index
   | length </ ti // i />        :: M :: length_t
   | length </ axBranchi // i /> :: M :: length_axBranch
   | tyConArity T                :: M :: tyConArity
   | ind - 1                     :: M :: decrement
   | -1                          :: M :: minusOne
+  | 0                           :: M :: zero
+  | 1                           :: M :: one
+  | 2                           :: M :: two
+
+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  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -199,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 } }}
@@ -229,6 +290,14 @@ terminals :: 'terminals_' ::=
   | Constraint   ::   :: Constraint       {{ tex \textsf{Constraint} }}
   | 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} }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -264,12 +333,28 @@ formula :: 'formula_' ::=
   | k1 elt { </ ki // , // i /> }      ::   :: kind_elt
   | e is_a_type                        ::   :: is_a_type
     {{ tex \exists \tau \text{ s.t.~} [[e]] = \tau }}
-  | t is_a_coercion                    ::   :: is_a_coercion
+  | e is_a_coercion                    ::   :: is_a_coercion
+    {{ tex \exists \gamma \text{ s.t.~} [[e]] = \gamma }}
+  | t is_a_prop                        ::   :: is_a_prop
     {{ tex \exists \tau_1, \tau_2, \kappa \text{ s.t.~} [[t]] =
            \tau_1 \mathop{ {\sim}_{\#}^{\kappa} } \tau_2 }}
   | axBranch1 = axBranch2              ::   :: branch_rewrite
   | 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
+    {{ tex \text{no other case matches} }}
+  | t = coercionKind g                 ::   :: coercionKind
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Subrules and Parsing  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -289,8 +374,15 @@ TyCon_AlgTyCon right Coercion_AppCo
 TyCon_PromotedDataCon right Coercion_AppCo
 TyCon_PromotedTyCon right Coercion_AppCo
 
-Subst_Mapping <= Type_TySubstList
+Subst_TyMapping <= Type_TySubstList
+Subst_TmMapping <= Type_TySubstList
 Subst_List <= Type_TySubstList
 
-Subst_Mapping <= Type_TySubstListPost
+Subst_TyMapping <= Type_TySubstListPost
+Subst_TmMapping <= Type_TySubstListPost
+
+Expr_Type <= formula_e_rewrite
+
+Coercion_TyConAppCo <= Coercion_AppCo
 
+Expr_Coercion <= Subst_TmMapping
diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile
index 1a5b27cd75..402f9dbe4e 100644
--- a/docs/core-spec/Makefile
+++ b/docs/core-spec/Makefile
@@ -1,10 +1,11 @@
-OTT_FILES = CoreSyn.ott CoreLint.ott
+OTT_FILES = CoreSyn.ott CoreLint.ott OpSem.ott
 OTT_TEX   = CoreOtt.tex
 OTT_OPTS  = -tex_show_meta false
 TARGET    = core-spec
 
 $(TARGET).pdf: $(TARGET).tex $(OTT_TEX)
-	latexmk -pdf $<
+	latex -output-format=pdf $<
+	latex -output-format=pdf $<
 
 $(TARGET).tex: $(TARGET).mng $(OTT_FILES)
 	ott $(OTT_OPTS) -tex_filter $< $@ $(OTT_FILES)
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
new file mode 100644
index 0000000000..1c21ada0ec
--- /dev/null
+++ b/docs/core-spec/OpSem.ott
@@ -0,0 +1,97 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Dynamic semantics  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% The definitions in this file do *not* strictly correspond to any specific
+% code in GHC. They are here to provide a reasonable operational semantic
+% interpretation to the typing rules presented in the other ott files. Thus,
+% your mileage may vary. In particular, there has been *no* attempt to
+% write any formal proofs over these semantics.
+%
+% With that disclaimer disclaimed, these rules are a reasonable jumping-off
+% point for an analysis of FC's operational semantics. If you don't want to
+% worry about mutual recursion (and who does?), you can even drop the
+% environment S.
+
+grammar
+
+defns
+OpSem :: '' ::=
+
+defn S |- e --> e'  ::  :: step :: 'S_' {{ com Single step semantics }}
+{{ tex [[S]] \labeledjudge{op} [[e]] [[-->]] [[e']] }}
+by
+
+S(n) = e
+----------------- :: Var
+S |- n --> e
+
+S |- e1 --> e1'
+------------------- :: App
+S |- e1 e2 --> e1' e2
+
+----------------------------- :: Beta
+S |- (\n.e1) e2 --> e1[n |-> e2]
+
+g0 = sym (nth 0 g)
+g1 = nth 1 g
+not e2 is_a_type
+not e2 is_a_coercion
+----------------------------------------------- :: Push
+S |- ((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0)
+
+---------------------------------------- :: TPush
+S |- ((\n.e) |> g) t --> (\n.(e |> g n)) t
+
+g0 = nth 1 (nth 0 g)
+g1 = sym (nth 2 (nth 0 g))
+g2 = nth 1 g
+------------------------------- :: CPush
+S |- ((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1)
+
+----------------- :: LetNonRec
+S |- let n = e1 in e2 --> e2[n |-> e1]
+
+
+S, </ [ni |-> ei] // i /> |- u --> u'
+------------------------------------ :: LetRec
+S |- let rec </ ni = ei // i /> in u --> let rec </ ni = ei // i /> in u'
+
+fv(u) \inter </ ni // i /> = empty
+------------------------------------------ :: LetRecReturn
+S |- let rec </ ni = ei // i /> in u --> u
+
+
+S |- e --> e'
+--------------------------------------- :: Case
+S |- case e as n return t of </ alti // i /> --> case e' as n return t of </ alti // i />
+
+altj = K </ alphabb_kbb // bb /> </ xcc_tcc // cc /> -> u
+u' = u[n |-> e] </ [alphabb_kbb |-> sbb] // bb /> </ [xcc_tcc |-> ecc] // cc />
+-------------------------------------------------------------- :: MatchData
+S |- case K </ t'aa // aa /> </ sbb // bb /> </ ecc // cc /> as n return t of </ alti // i /> --> u'
+
+altj = lit -> u
+---------------------------------------------------------------- :: MatchLit
+S |- case lit as n return t of </ alti // i /> --> u[n |-> lit]
+
+altj = _ -> u
+no other case matches
+------------------------------------------------------------ :: MatchDefault
+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>_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 />
+
+S |- e --> e'
+------------------------ :: Cast
+S |- e |> g --> e' |> g
+
+S |- e --> e'
+------------------------------ :: Tick
+S |- e { tick } --> e' { tick }
+
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 4b1e986c6d..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}
 
@@ -29,11 +30,28 @@ System FC, as implemented in GHC\footnote{This
 document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}),
 but it should be maintained by anyone who edits the functions or data structures
 mentioned in this file. Please feel free to contact Richard for more information.}\\
-\Large\today
+\Large 2 August, 2013
 \end{center}
 
 \section{Introduction}
 
+This document presents the typing system of System FC, very closely to how it is
+implemented in GHC. Care is taken to include only those checks that are actually
+written in the GHC code. It should be maintained along with any changes to this
+type system.
+
+Who will use this? Any implementer of GHC who wants to understand more about the
+type system can look here to see the relationships among constructors and the
+different types used in the implementation of the type system. Note that the
+type system here is quite different from that of Haskell---these are the details
+of the internal language, only.
+
+At the end of this document is a \emph{hypothetical} operational semantics for GHC.
+It is hypothetical because GHC does not strictly implement a concrete operational
+semantics anywhere in its code. While all the typing rules can be traced back to
+lines of real code, the operational semantics do not, in general, have as clear
+a provenance.
+
 There are a number of details elided from this presentation. The goal of the
 formalism is to aid in reasoning about type safety, and checks that do not
 work toward this goal were omitted. For example, various scoping checks (other
@@ -64,7 +82,6 @@ variables:
 \gram{
 \ottz
 }
-foo
 
 \gram{
 \ottn
@@ -132,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}
@@ -150,6 +175,12 @@ Axioms:
 \ottaxBranch
 }
 
+The definition for $[[axBranch]]$ above does not include the list of
+incompatible branches (field \texttt{cab\_incomps} of \texttt{CoAxBranch}),
+as that would unduly clutter this presentation. Instead, as the list
+of incompatible branches can be computed at any time, it is checked for
+in the judgment $[[no_conflict]]$. See Section~\ref{sec:no_conflict}.
+
 \subsection{Type constructors}
 
 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
@@ -179,7 +210,7 @@ the context sometimes requires creating a new, fresh variable name and then
 applying a substitution. We elide these details in this formalism, but
 see \coderef{types/Type.lhs}{substTyVarBndr} for details.
 
-\section{Judgments}
+\section{Typing judgments}
 
 The following functions are used from GHC. Their names are descriptive, and they
 are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
@@ -263,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:
@@ -305,17 +346,108 @@ 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}
 
 The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make
 sure that a type family application cannot unify with any previous branch
-in the axiom.
+in the axiom. The actual code scans through only those branches that are
+flagged as incompatible. These branches are stored directly in the
+$[[axBranch]]$. However, it is cleaner in this presentation to simply
+check for compatibility here.
 
 \ottdefncheckXXnoXXconflict{}
 
-The judgment $[[apart]]$ checks to see whether two lists of types are surely apart.
-It checks to see if \coderef{types/Unify.lhs}{tcApartTys} returns \texttt{SurelyApart}.
-Two types are apart if neither type is a type family application and if they do not
-unify.
+The judgment $[[apart]]$ checks to see whether two lists of types are surely
+apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i />
+]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
+\emph{patterns} (as in a type family equation), first flattens the $[[ </ ti
+    // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to
+see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
+Flattening takes all type family applications and replaces them with fresh variables,
+taking care to map identical type family applications to the same fresh variable.
+
+The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
+It performs a standard unification, returning a substitution upon success.
+
+\section{Operational semantics}
+
+\subsection{Disclaimer}
+GHC does not implement an operational semantics in any concrete form. Most
+of the rules below are implied by algorithms in, for example, the simplifier
+and optimizer. Yet, there is no one place in GHC that states these rules,
+analogously to \texttt{CoreLint.lhs}.
+Nevertheless, these rules are included in this document to help the reader
+understand System FC.
+
+\subsection{The context $[[S]]$}
+We use a context $[[S]]$ to keep track of the values of variables in a (mutually)
+recursive group. Its definition is as follows:
+\[
+[[S]] \quad ::= \quad [[ empty ]] \ |\ [[S]], [[ [n |-> e] ]]
+\]
+The presence of the context $[[S]]$ is solely to deal with recursion. If your
+use of FC does not require modeling recursion, you will not need to track $[[S]]$.
+
+\subsection{Operational semantics rules}
+
+\ottdefnstep{}
+
+\subsection{Notes}
+
+\begin{itemize}
+\item The \ottdrulename{S\_LetRec} and \ottdrulename{S\_LetRecReturn} rules
+implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
+for all of the mutually recursive equations. Then, after perhaps many steps,
+when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
+in the $[[let]]\ [[rec]]$, the context is popped.
+\item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
+lists of arguments: two lists of types and a list of terms. The types passed
+in are the universally and, respectively, existentially quantified type variables
+to the constructor. The terms are the regular term arguments stored in an
+algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
+\item The rule \ottdrulename{S\_CasePush} is the most complex rule.
+\begin{itemize}
+\item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
+\item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
+extracts the two types (and their kind) from
+a coercion. It does not require a typing context, as it does not \emph{check} the
+coercion, just extracts its types.
+\item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
+constructor expressions, the parameters to the constructor are broken into three
+groups: universally quantified types, existentially quantified types, and terms.
+\item The substitutions in the last premise to the rule are unusual: they replace
+\emph{type} variables with \emph{coercions}. This substitution is called lifting
+and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
+essentially a pun on the fact that types and coercions have such similar structure.
+\item Note that the types $[[ </ sbb // bb /> ]]$---the existentially quantified
+types---do not change during this step.
+\end{itemize}
+\end{itemize}
 
 \end{document}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index be13ca22c5..4e4ca924fb 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf