summaryrefslogtreecommitdiff
path: root/docs/core-spec
diff options
context:
space:
mode:
Diffstat (limited to 'docs/core-spec')
-rw-r--r--docs/core-spec/CoreLint.ott178
-rw-r--r--docs/core-spec/CoreSyn.ott77
-rw-r--r--docs/core-spec/OpSem.ott2
-rw-r--r--docs/core-spec/README2
-rw-r--r--docs/core-spec/core-spec.mng54
-rw-r--r--docs/core-spec/core-spec.pdfbin349150 -> 359837 bytes
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
Binary files differ
View Lorry Controller Status