Added GHC formalism to the GHC source tree.

As per a request from Simon PJ, I wrote up a formalism of the core
language in GHC, System FC. The writeup lives in docs/core-spec.
I also added comments to a number of files dealing with the core
language reminding authors to update the formalism when updating the
code. In the next commit will be a README file in docs/core-spec
with more details of how to do this.

6 files changed, 1013 insertions, 0 deletions

diff --git a/docs/core-spec/.gitignore b/docs/core-spec/.gitignore
new file mode 100644
index 0000000000..a1958037ad
--- /dev/null
+++ b/docs/core-spec/.gitignore
@@ -0,0 +1,5 @@
+*.aux
+*.log
+*.fdb_latexmk
+CoreOtt.tex
+core-spec.tex
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
new file mode 100644
index 0000000000..22949eddf3
--- /dev/null
+++ b/docs/core-spec/CoreLint.ott
@@ -0,0 +1,402 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Static semantics  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+defns
+CoreLint :: '' ::=
+
+defn |- prog program ::  :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreBindings} }}
+  {{ tex \labeledjudge{prog} [[program]] }}
+by
+
+G = </ vars_of bindingi // i />
+no_duplicates </ bindingi // i />
+</ G |-bind bindingi // i />
+--------------------- :: CoreBindings
+|-prog </ bindingi // i />
+
+defn G |- bind binding ::  :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{coreSyn/CoreLint.lhs}{lint\_bind} }}
+  {{ tex [[G]] \labeledjudge{bind} [[binding]] }}
+by
+
+G |-sbind n <- e
+---------------------- :: NonRec
+G |-bind n = e
+
+</ G |-sbind ni <- ei // i />
+---------------------- :: Rec
+G |-bind rec </ ni = ei // i />
+
+defn G  |- sbind n <- e ::  :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
+  {{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }}
+by
+
+G |-tm e : t
+G |-name z_t ok
+</ mi // i /> = fv(t)
+</ mi elt G // i />
+----------------- :: SingleBinding
+G |-sbind z_t <- e
+
+defn G  |- tm e : t ::  :: lintCoreExpr :: 'Tm_'
+  {{ com Expression typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreExpr} }}
+  {{ tex [[G]] \labeledjudge{tm} [[e]] : [[t]] }}
+by
+
+x_t elt G
+not (t is_a_coercion)
+------------------ :: Var
+G |-tm x_t : t
+
+t = literalType lit
+------------------- :: Lit
+G |-tm lit : t
+
+G |-tm e : s
+G |-co g : s ~#k t
+------------------- :: Cast
+G |-tm e |> g : t
+
+G |-tm e : t
+------------------- :: Tick
+G |-tm e {tick} : t
+
+G' = G, alpha_k
+G |-ki k ok
+G' |-subst alpha_k |-> s ok
+G' |-tm e[alpha_k |-> s] : t
+--------------------------- :: LetTyKi
+G |-tm let alpha_k = s in e : t
+
+G |-sbind x_s <- u
+G |-ty s : k
+G, x_s |-tm e : t
+------------------------- :: LetNonRec
+G |-tm let x_s = u in e : t
+
+</ G'i @ // i /> = inits(</ zi_si // i />)
+</ G, G'i |-ty si : ki // i />
+no_duplicates </ zi // i />
+G' = G, </ zi_si // i />
+</ G' |-sbind zi_si <- ui // i />
+G' |-tm e : t
+------------------------ :: LetRec
+G |-tm let rec </ zi_si = ui // i /> in e : t
+
+% lintCoreArg is incorporated in these next two rules
+
+G |-tm e1 : forall alpha_k.t
+G |-subst alpha_k |-> s ok
+---------------- :: AppType
+G |-tm e1 s : t[alpha_k |-> s]
+
+not (e2 is_a_type)
+G |-tm e1 : t1 -> t2
+G |-tm e2 : t1
+---------------- :: AppExpr
+G |-tm e1 e2 : t2
+
+G |-ty t : k
+G, x_t |-tm e : s
+----------------- :: LamId
+G |-tm \x_t.e : t -> s
+
+G' = G, alpha_k
+G |-ki k ok
+G' |-tm e : t
+--------------------------- :: LamTy
+G |-tm \alpha_k.e : forall alpha_k. t
+
+G |-tm e : s
+G |-ty s : k1
+G |-ty t : k2
+</ G, z_s; s |-altern alti : t // i />
+---------------------------------------------------- :: Case
+G |-tm case e as z_s return t of </ alti // i /> : t
+
+% Type case of lintCoreExpr omitted because it is irrelevant
+
+G |-co g : t1 ~#k t2
+-------------------- :: Coercion
+G |-tm g : t1 ~#k 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]] }}
+by
+
+G |-ty t : k
+----------------- :: Id
+G |-name x_t ok
+
+----------------- :: TyVar
+G |-name alpha_k ok
+
+defn G |- bnd n ok ::  :: lintBinder :: 'Binding_'
+  {{ com Binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintBinder} }}
+  {{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }}
+by
+
+G |-ty t : k
+--------------------------------- :: Id
+G |-bnd x_t ok
+
+G |-ki k ok
+---------------------------------------- :: TyVar
+G |-bnd alpha_k ok
+
+defn G  |- co g : t1 ~# k t2 ::  :: lintCoercion :: 'Co_'
+  {{ com Coercion typing, \coderef{coreSyn/CoreLint.lhs}{lintCoercion} }}
+  {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{\sim_{\#}^{[[k]]} } [[t2]] }}
+by
+
+G |-ty t : k
+---------------------- :: Refl
+G |-co <t> : t ~#k t
+
+G |-co g1 : s1 ~#k1 t1
+G |-co g2 : s2 ~#k2 t2
+G |-arrow k1 -> k2 : k
+------------------------- :: TyConAppCoFunTy
+G |-co (->) g1 g2 : (s1 -> s2) ~#k (t1 -> t2)
+
+T /= (->)
+</ G |-co gi : si ~#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 g1 : s1 ~#k1 t1
+G |-co g2 : s2 ~#k2 t2
+G |-app (s2 : k2) : k1 ~> k
+--------------------- :: AppCo
+G |-co g1 g2 : (s1 s2) ~#k (t1 t2)
+
+G |-ki k1 ok
+G, z_k1 |-co g : s ~#k2 t
+--------------------------- :: ForAllCo
+G |-co forall z_k1. g : (forall z_k1.s) ~#k2 (forall z_k1.t)
+
+z_(t ~#BOX t) elt G
+----------------------- :: CoVarCoBox
+G |-co z_(t ~#BOX t) : t ~#BOX t
+
+z_(s ~#k t) elt G
+k /= BOX
+----------------------- :: CoVarCo
+G |-co z_(s ~#k t) : s ~#k t
+
+G |-ty t1 : k
+----------------------------- :: UnsafeCo
+G |-co t1 ==>! t2 : t1 ~#k t2
+
+G |-co g : t1 ~#k t2
+------------------------- :: SymCo
+G |-co sym g : t2 ~#k t1
+
+G |-co g1 : t1 ~#k t2
+G |-co g2 : t2 ~#k t3
+----------------------- :: TransCo
+G |-co g1 ; g2 : t1 ~#k t3
+
+G |-co g : (T </ sj // j />) ~#k (T </ tj // j />)
+length </ sj // j /> = length </ tj // j />
+i < length </ sj // j />
+G |-ty si : k
+---------------------- :: NthCo
+G |-co nth i g : si ~#k ti
+
+G |-co g : (s1 s2) ~#k (t1 t2)
+G |-ty s1 : k
+----------------------- :: LRCoLeft
+G |-co Left g : s1 ~#k t1
+
+G |-co g : (s1 s2) ~#k (t1 t2)
+G |-ty s2 : k
+----------------------- :: LRCoRight
+G |-co Right g : s2 ~#k t2
+
+G |-co g : forall m.s ~#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 gi : si ~#ki ti // i />
+</ substi @ // i /> = inits(</ [ ni |-> si ] // i />)
+</ ni = zi_k'i // i />
+</ ki <: substi(k'i) // i />
+s' = s </ [ ni |-> si ] // i />
+t' = t </ [ ni |-> ti ] // i />
+G |-ty s' : k
+------------------------------------------------------ :: AxiomInstCo
+G |-co (forall </ ni // i />. (s ~ t)) </ gi // i /> : s' ~#k t'
+
+defn G |- ki k ok ::  :: lintKind :: 'K_'
+  {{ com Kind validity, \coderef{coreSyn/CoreLint.lhs}{lintKind} }}
+  {{ tex [[G]] \labeledjudge{k} [[k]] [[ok]] }}
+by
+
+G |-ty k : BOX
+-------------- :: Box
+G |-ki k ok
+
+defn G |- ty t : k ::  :: lintType :: 'Ty_'  
+  {{ com Kinding, \coderef{coreSyn/CoreLint.lhs}{lintType} }}
+  {{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }}
+by
+
+z_k elt G
+------------ :: TyVarTy
+G |-ty z_k : k
+
+G |-ty t1 : k1
+G |-ty t2 : k2
+G |-app (t2 : k2) : k1 ~> k
+--------------- :: AppTy
+G |-ty t1 t2 : k
+
+G |-ty t1 : k1
+G |-ty t2 : k2
+G |-arrow k1 -> k2 : k
+------------------- :: FunTy
+G |-ty t1 -> t2 : k
+
+not (isUnLiftedTyCon T) \/ length </ ti // i /> = tyConArity T
+</ G |-ty ti : ki // i />
+G |-app </ (ti : ki) // i /> : tyConKind T ~> k
+--------------------------- :: TyConApp
+G |-ty T </ ti // i /> : k
+
+G |-ki k1 ok
+G, z_k1 |-ty t : k2
+------------------------ :: ForAllTy
+G |-ty forall z_k1. t : k2
+
+G |-tylit lit : k
+-------------- :: LitTy
+G |-ty lit : k
+
+defn G |- subst n |-> t ok ::  :: checkTyKind :: 'Subst_'
+  {{ com Substitution consistency, \coderef{coreSyn/CoreLint.lhs}{checkTyKind} }}
+  {{ tex [[G]] \labeledjudge{subst} [[n]] [[|->]] [[t]] [[ok]] }}
+by
+
+G |-ki k ok
+------------------------ :: Kind
+G |-subst z_BOX |-> k ok
+
+k1 /= BOX
+G |-ty t : k2
+k2 <: k1
+---------------------- :: Type
+G |-subst z_k1 |-> t ok
+
+defn G ; s |- altern alt : t ::  :: lintCoreAlt :: 'Alt_'
+  {{ com Case alternative consistency, \coderef{coreSyn/CoreLint.lhs}{lintCoreAlt} }}
+  {{ tex [[G]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
+by
+
+G |-tm e : t
+--------------------- :: DEFAULT
+G; s |-altern _ -> e : t
+
+s = literalType lit
+G |-tm e : t
+---------------------------------------- :: LitAlt
+G; s |-altern lit -> e : t
+
+T = dataConTyCon K
+not (isNewTyCon T)
+t1 = dataConRepType K
+t2 = t1 {</ sj // j />}
+</ G |-bnd ni ok // i />
+G' = G, </ ni // i />
+G' |-altbnd </ ni // i /> : t2 ~> T </ sj // j />
+G' |-tm e : t
+--------------------------------------- :: DataAlt
+G; T </ sj // j /> |-altern K </ ni // i /> -> e : t
+
+defn t' = t { </ si // , // i /> } ::  :: applyTys :: 'ApplyTys_'
+  {{ com Telescope substitution, \coderef{types/Type.lhs}{applyTys} }}
+by
+
+--------------------- :: Empty
+t = t { }
+
+t' = t{</ si // i />}
+t'' = t'[n |-> s]
+-------------------------- :: Ty
+t'' = (forall n. t) { s, </ si // i /> }
+
+defn G |- altbnd vars : t1 ~> t2 ::  :: lintAltBinders :: 'AltBinders_'
+  {{ com Case alternative binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintAltBinders} }}
+  {{ tex [[G]] \labeledjudge{altbnd} [[vars]] : [[t1]] [[~>]] [[t2]] }}
+by
+
+------------------------- :: Empty
+G |-altbnd empty : t ~> t
+
+G |-subst beta_k' |-> alpha_k ok
+G |-altbnd </ ni // i /> : t[beta_k' |-> alpha_k] ~> s
+------------------------------------------------------ :: TyVar
+G |-altbnd alpha_k, </ ni // i /> : (forall beta_k'.t) ~> s
+
+G |-altbnd </ ni // i /> : t2 ~> s
+----------------------------------------------- :: Id
+G |-altbnd x_t1, </ ni // i /> : (t1 -> t2) ~> s
+
+defn G |- arrow k1 -> k2 : k ::  :: lintArrow :: 'Arrow_'
+  {{ com Arrow kinding, \coderef{coreSyn/CoreLint.lhs}{lintArrow} }}
+  {{ tex [[G]] \labeledjudge{\rightarrow} [[k1]] [[->]] [[k2]] : [[k]] }}
+by
+
+------------------------- :: Box
+G |-arrow BOX -> k2 : BOX
+
+k1 elt { *, #, Constraint }
+k2 elt { *, #, Constraint }
+------------------------- :: Kind
+G |-arrow k1 -> k2 : *
+
+defn G |- app kinded_types : k1 ~> k2 ::  :: lint_app :: 'App_'
+  {{ com Type application kinding, \coderef{coreSyn/CoreLint.lhs}{lint\_app} }}
+  {{ tex [[G]] \labeledjudge{app} [[kinded_types]] : [[k1]] [[~>]] [[k2]] }}
+by
+
+--------------------- :: Empty
+G |-app empty : k ~> k
+
+k <: k1
+G |-app </ (ti : ki) // i /> : k2 ~> k'
+---------------------------------------------------- :: FunTy
+G |-app (t : k), </ (ti : ki) // i /> : (k1 -> k2) ~> k'
+
+k <: k1
+G |-app </ (ti : ki) // i /> : k2[z_k1 |-> t] ~> k'
+-------------------------------------------------------- :: ForAllTy
+G |-app (t : k), </ (ti : ki) // i /> : (forall z_k1. k2) ~> k'
+
+defn k1 <: k2 ::  :: isSubKind :: 'SubKind_'
+  {{ com Sub-kinding, \coderef{types/Kind.lhs}{isSubKind} }}
+by
+
+------ :: Refl
+k <: k
+
+-------------------- :: UnliftedTypeKind
+# <: OpenKind
+
+------------------- :: LiftedTypeKind
+* <: OpenKind
+
+---------------------- :: Constraint
+Constraint <: OpenKind
+
+------------------- :: ConstraintLifted
+Constraint <: *
+
+------------------ :: LiftedConstraint
+* <: Constraint
\ No newline at end of file
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
new file mode 100644
index 0000000000..f3e8a61eb0
--- /dev/null
+++ b/docs/core-spec/CoreSyn.ott
@@ -0,0 +1,283 @@
+
+embed {{ tex-preamble
+  \newcommand{\coderef}[2]{\ghcfile{#1}:\texttt{#2}%
+}
+  \newcommand{\keyword}[1]{\textbf{#1} }
+  \newcommand{\labeledjudge}[1]{\vdash_{\!\!\mathsf{#1} } }
+}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Metavariables  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+metavar x ::=   {{ com Term-level variable names }}
+metavar alpha {{ tex \alpha }}, beta {{ tex \beta }} ::=
+  {{ com Type-level variable names }}
+metavar N ::=   {{ com Type-level constructor names }}
+metavar K ::=   {{ com Term-level data constructor names }}
+
+indexvar i, j ::= {{ com Indices to be used in lists }}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Syntax  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+grammar
+
+lit {{ tex \textsf{lit} }} :: 'Literal_' ::=
+  {{ com Literals, \coderef{basicTypes/Literal.lhs}{Literal} }}
+
+z :: 'Name_' ::= {{ com Term or type name }}
+  | alpha           ::   :: Type    {{ com Type-level name }}
+  | x               ::   :: Term    {{ com Term-level name }}
+
+n, m :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.lhs}{Var} }}
+  | z _ t           ::   :: IdOrTyVar   {{ com Name, labeled with type/kind }}
+    {{ tex {[[z]]}^{[[t]]} }}
+
+vars :: 'Vars_' ::= {{ com List of variables }}
+  | </ ni // , // i />   ::   :: List
+  | fv ( t )             :: M :: fv
+    {{ tex \textit{fv}([[t]]) }}
+  | empty                :: M :: empty
+
+e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
+  | n                                            ::   :: Var  {{ com Variable }}
+  | lit                                          ::   :: Lit  {{ com Literal }}
+  | e1 e2                                        ::   :: App  {{ com Application }}
+  | \ n . e                                      ::   :: Lam  {{ com Abstraction }}
+  | let binding in e                             ::   :: Let  {{ com Variable binding }}
+  | case e as n return t of </ alti // | // i /> ::   :: Case {{ com Pattern match }}
+  | e |> g                                       ::   :: Cast {{ com Cast }}
+  | e { tick }                                   ::   :: Tick {{ com Internal note }}
+    {{ tex {[[e]]}_{\{[[tick]]\} } }}
+  | t                                            ::   :: Type {{ com Type }}
+  | g                                            ::   :: Coercion {{ com Coercion }}
+  | e [ n |-> t ]                                :: M :: TySubst {{ com Type substitution }}
+
+binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
+  | n = e                         ::   :: NonRec  {{ com Non-recursive binding }}
+  | rec </ ni = ei // and // i /> ::   :: Rec     {{ com Recursive binding }}
+
+alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }}
+  | Kp </ ni // i /> -> e    ::   :: Alt  {{ com Constructor applied to fresh names }}
+
+tick :: 'Tickish_' ::= {{ com Internal notes, \coderef{coreSyn/CoreSyn.lhs}{Tickish} }}
+
+Kp {{ tex \mathbb{K} }} :: 'AltCon_' ::= {{ com Constructors used in patterns, \coderef{coreSyn/CoreSyn.lhs}{AltCon} }}
+  | K        ::   :: DataAlt         {{ com Data constructor }}
+  | lit      ::   :: LitAlt          {{ com Literal (such as an integer or character) }}
+  | _        ::   :: DEFAULT         {{ com Wildcard }}
+
+program :: 'CoreProgram_' ::= {{ com A System FC program, \coderef{coreSyn/CoreSyn.lhs}{CoreProgram} }}
+  | </ bindingi // i />  ::   :: CoreProgram  {{ com List of bindings }}
+
+%% TYPES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}
+  :: 'Type_' ::= {{ com Types/kinds, \coderef{types/TypeRep.lhs}{Type} }}
+  | n                       ::   :: TyVarTy       {{ com Variable }}
+  | t1 t2                   ::   :: AppTy         {{ com Application }}
+  | T </ ti // i />         ::   :: TyConApp      {{ com Application of type constructor }}
+  | t1 -> t2                ::   :: FunTy         {{ com Function }}
+  | forall n . t            ::   :: ForAllTy      {{ com Polymorphism }}
+  | lit                     ::   :: LitTy         {{ com Type-level literal }}
+  | 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]] }}
+  | 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 }}
+
+%% 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 }}
+  | g1 g2                   ::   :: AppCo         {{ com Application }}
+  | forall n . g            ::   :: ForAllCo      {{ com Polymorphism }}
+  | n                       ::   :: CoVarCo       {{ com Variable }}
+  | C </ gi // i />         ::   :: AxiomInstCo   {{ com Axiom application }}
+  | t1 ==>! t2              ::   :: UnsafeCo      {{ com Unsafe coercion }}
+  | sym g                   ::   :: SymCo         {{ com Symmetry }}
+  | g1 ; g2                 ::   :: TransCo       {{ com Transitivity }}
+  | 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 }}
+
+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} }}
+  | forall </ ni // i /> . ( s ~ t )   ::   :: CoAxiom  {{ com Axiom }}
+  | ( C )                              :: M :: Parens   {{ com Parentheses }}
+
+%% TYCONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
+  | ( -> )       ::   :: FunTyCon          {{ com Arrow }}
+
+  % the following also includes TupleTyCon, SynTyCon
+  | N _ k        ::   :: AlgTyCon          {{ com Named tycon: algebraic, tuples, and synonyms }}
+    {{ tex {[[N]]}^{[[k]]} }}
+  | H            ::   :: PrimTyCon         {{ com Primitive tycon }}
+  | ' K          ::   :: PromotedDataCon   {{ com Promoted data constructor }}
+  | ' T          ::   :: PromotedTyCon     {{ com Promoted type constructor }}
+  | 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 }}
+
+%% CONTEXTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
+  | n                        ::   :: Binding   {{ com Single binding }}
+  | </ Gi // , // i />       ::   :: Concat    {{ com Context concatenation }}
+  | vars_of binding          :: M :: VarsOf    {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
+
+%% UTILITY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+B {{ tex \mathbb{B} }} :: 'Bool_' ::= {{ com Booleans in metatheory }}
+  | false        ::   :: False
+  | true         ::   :: True
+
+kinded_types {{ tex \overline{(\sigma_i : \kappa_i)}^i }} :: 'Kinded_Types_' ::= {{ com List of types with kinds }}
+  | </ ( si : ki ) // , // i />    ::   :: List
+  | empty                          :: M :: empty
+
+subst :: 'Subst_' ::= {{ com List of type substitutions }}
+  | [ n |-> t ]        ::   :: Mapping
+  | </ substi // i />  ::   :: List
+
+nat {{ tex \mathbb{N} }} :: 'Nat_' ::= {{ com Natural numbers }}
+  | i                       ::   :: index
+  | length </ ti // i />    :: M :: length
+  | tyConArity T            :: M :: tyConArity
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Terminals  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+terminals :: 'terminals_' ::=
+  | \            ::   :: lambda           {{ tex \lambda }}
+  | let          ::   :: let              {{ tex \keyword{let} }}
+  | in           ::   :: key_in           {{ tex \keyword{in} }}
+  | rec          ::   :: rec              {{ tex \keyword{rec} }}
+  | and          ::   :: key_and          {{ tex \keyword{and} }}
+  | case         ::   :: case             {{ tex \keyword{case} }}
+  | of           ::   :: of               {{ tex \keyword{of} }}
+  | ->           ::   :: arrow            {{ tex \to }}
+  | |>           ::   :: cast             {{ tex \triangleright }}
+  | forall       ::   :: forall           {{ tex {\forall}\! }}
+  | ==>!         ::   :: unsafe
+    {{ tex \twoheadrightarrow\!\!\!\!\!\! \raisebox{-.3ex}{!} \,\,\,\,\, }}
+  | sym          ::   :: sym              {{ tex \textsf{sym} }}
+  | ;            ::   :: trans            {{ tex \fatsemi }}
+  | Left         ::   :: Left             {{ tex \textsf{left} }}
+  | Right        ::   :: Right            {{ tex \textsf{right} }}
+  | _            ::   :: wildcard         {{ tex \text{\textvisiblespace} }}
+  | BOX          ::   :: BOX              {{ tex \Box }}
+  | Int#         ::   :: int_hash         {{ tex {\textsf{Int} }_{\#} }}
+  | ~#           ::   :: eq_hash          {{ tex \mathop{ {\sim}_{\#} } }}
+  | OpenKind     ::   :: OpenKind         {{ tex \textsf{OpenKind} }}
+  | ok           ::   :: ok               {{ tex \textsf{ ok} }}
+  | no_duplicates ::  :: no_duplicates    {{ tex \textsf{no\_duplicates } }}
+  | vars_of      ::   :: vars_of          {{ tex \textsf{vars\_of } }}
+  | not          ::   :: not              {{ tex \neg }}
+  | isUnLiftedTyCon :: :: isUnLiftenTyCon {{ tex \textsf{isUnLiftedTyCon} }}
+  | false        ::   :: false            {{ tex \textsf{false} }}
+  | true         ::   :: true             {{ tex \textsf{true} }}
+  | \/           ::   :: or               {{ tex \vee }}
+  | /\           ::   :: and              {{ tex \mathop{\wedge} }}
+  | elt          ::   :: elt              {{ tex \in }}
+  | /=           ::   :: neq              {{ tex \neq }}
+  | literalType  ::   :: literalType      {{ tex \textsf{literalType} }}
+  | |->          ::   :: mapsto           {{ tex \mapsto }}
+  | <-           ::   :: assignment       {{ tex \leftarrow }}
+  | @            ::   :: marker           {{ tex  }}
+  | inits        ::   :: inits            {{ tex \textsf{inits} }}
+  | ~>           ::   :: squigarrow       {{ tex \rightsquigarrow }}
+  | tyConKind    ::   :: tyConKind        {{ tex \mathop{\textsf{tyConKind} } }}
+  | empty        ::   :: empty            {{ tex \cdot }}
+  | length       ::   :: length           {{ tex \mathsf{length} }}
+  | <:           ::   :: subkind          {{ tex \mathop{ {<} {:}\, } }}
+  | ~            ::   :: eq               {{ tex \sim }}
+  | tyConArity   ::   :: tyConArity       {{ tex \textsf{tyConArity} }}
+  | dataConTyCon ::   :: dataConTyCon     {{ tex \textsf{dataConTyCon} }}
+  | dataConRepType :: :: dataConRepType   {{ tex \textsf{dataConRepType} }}
+  | isNewTyCon   ::   :: isNewTyCon       {{ tex \textsf{isNewTyCon} }}
+  | Constraint   ::   :: Constraint       {{ tex \textsf{Constraint} }}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+formula :: 'formula_' ::=
+  | judgement                          ::   :: judgement
+  | formula1 ... formulai              ::   :: dots
+  | G1 = G2                            ::   :: context_rewrite
+  | t1 = t2                            ::   :: type_rewrite
+  | t1 /= t2                           ::   :: type_inequality
+  | e1 /=e e2                          ::   :: expr_inequality
+    {{ tex [[e1]] \neq [[e2]] }}
+  | rf                                 ::   :: rf_formula
+  | tlf                                ::   :: tlf_formula
+  | g1 = g2                            ::   :: co_rewrite
+  | no_duplicates </ zi // i />        ::   :: no_duplicates_name
+  | no_duplicates </ bindingi // i />  ::   :: no_duplicates_binding
+  | not formula                        ::   :: not
+  | isUnLiftedTyCon T                  ::   :: isUnLiftedTyCon
+  | formula1 /\ formula2               ::   :: and
+  | formula1 \/ formula2               ::   :: or
+  | ( formula )                        ::   :: parens
+  | n elt G                            ::   :: context_inclusion
+  | vars1 = vars2                      ::   :: vars_rewrite
+  | </ Gi @ // i /> = inits ( </ nj // j /> ) :: :: context_folding
+  | </ substi @ // i /> = inits ( </ [ nj |-> tj ] // j /> ) :: :: subst_folding
+  | nat1 = nat2                        ::   :: eq_nat
+  | nat1 < nat2                        ::   :: lt
+  | G |- tylit lit : k                 ::   :: lintTyLit
+    {{ tex [[G]] \labeledjudge{tylit} [[lit]] : [[k]] }}
+  | isNewTyCon T                       ::   :: isNewTyCon
+  | 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
+    {{ tex \exists \tau_1, \tau_2, \kappa \text{ s.t.~} [[t]] =
+           \tau_1 \mathop{ {\sim}_{\#}^{\kappa} } \tau_2 }}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  Subrules and Parsing  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+parsing
+
+TyCon_FunTyCon right Type_AppTy
+TyCon_PrimTyCon right Type_AppTy
+TyCon_AlgTyCon right Type_AppTy
+TyCon_PromotedDataCon right Type_AppTy
+TyCon_PromotedTyCon right Type_AppTy
+
+TyCon_FunTyCon right Coercion_AppCo
+TyCon_PrimTyCon right Coercion_AppCo
+TyCon_AlgTyCon right Coercion_AppCo
+TyCon_PromotedDataCon right Coercion_AppCo
+TyCon_PromotedTyCon right Coercion_AppCo
+
+Subst_Mapping <= Type_TySubstList
+Subst_List <= Type_TySubstList
+
+Subst_Mapping <= Type_TySubstListPost
\ No newline at end of file
diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile
new file mode 100644
index 0000000000..1a5b27cd75
--- /dev/null
+++ b/docs/core-spec/Makefile
@@ -0,0 +1,17 @@
+OTT_FILES = CoreSyn.ott CoreLint.ott
+OTT_TEX   = CoreOtt.tex
+OTT_OPTS  = -tex_show_meta false
+TARGET    = core-spec
+
+$(TARGET).pdf: $(TARGET).tex $(OTT_TEX)
+	latexmk -pdf $<
+
+$(TARGET).tex: $(TARGET).mng $(OTT_FILES)
+	ott $(OTT_OPTS) -tex_filter $< $@ $(OTT_FILES)
+
+$(OTT_TEX): $(OTT_FILES)
+	ott -tex_wrap false $(OTT_OPTS) -o $@ $^
+
+.PHONY: clean
+clean:
+	rm -f $(TARGET).pdf $(TARGET).tex $(OTT_TEX) *.aux *.fdb_latexmk *.log
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
new file mode 100644
index 0000000000..4a76e46c91
--- /dev/null
+++ b/docs/core-spec/core-spec.mng
@@ -0,0 +1,306 @@
+\documentclass{article}
+
+\usepackage{supertabular}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{stmaryrd}
+\usepackage{xcolor}
+\usepackage{fullpage}
+\usepackage{multirow}
+
+\newcommand{\ghcfile}[1]{\textsl{#1}}
+\newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
+
+\input{CoreOtt}
+
+% increase spacing between rules for ease of reading:
+\renewcommand{\ottusedrule}[1]{\[#1\]\\[1ex]}
+
+\setlength{\parindent}{0in}
+\setlength{\parskip}{1ex}
+
+\newcommand{\gram}[1]{\ottgrammartabular{#1\ottinterrule}}
+
+\begin{document}
+
+\begin{center}
+\LARGE
+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
+\end{center}
+
+\section{Introduction}
+
+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
+than basic context inclusion) appear in the GHC code but not here.
+
+\section{Grammar}
+
+\subsection{Metavariables}
+
+We will use the following metavariables:
+
+\ottmetavars{}\\
+
+\subsection{Literals}
+
+Literals do not play a major role, so we leave them abstract:
+
+\gram{\ottlit}
+
+We also leave abstract the function \coderef{basicTypes/Literal.lhs}{literalType}
+and the judgment \coderef{coreSyn/CoreLint.lhs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
+
+\subsection{Variables}
+
+GHC uses the same datatype to represent term-level variables and type-level
+variables:
+
+\gram{
+\ottz
+}
+foo
+
+\gram{
+\ottn
+}
+
+\subsection{Expressions}
+
+The datatype that represents expressions:
+
+\gram{\otte}
+
+There are a few key invariants about expressions:
+\begin{itemize}
+\item The right-hand sides of all top-level and recursive $[[let]]$s
+must be of lifted type.
+\item The right-hand side of a non-recursive $[[let]]$ and the argument
+of an application may be of unlifted type, but only if the expression
+is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.lhs}.
+\item We allow a non-recursive $[[let]]$ for bind a type variable.
+\item The $[[_]]$ case for a $[[case]]$ must come first.
+\item The list of case alternatives must be exhaustive.
+\item Types and coercions can only appear on the right-hand-side of an application.
+\end{itemize}
+
+Bindings for $[[let]]$ statements:
+
+\gram{\ottbinding}
+
+Case alternatives:
+
+\gram{\ottalt}
+
+Constructors as used in patterns:
+
+\gram{\ottKp}
+
+Notes that can be inserted into the AST. We leave these abstract:
+
+\gram{\otttick}
+
+A program is just a list of bindings:
+
+\gram{\ottprogram}
+
+\subsection{Types}
+
+\gram{\ottt}
+
+There are some invariants on types:
+\begin{itemize}
+\item The type $[[t1]]$ in the form $[[t1 t2]]$ must not be a type constructor
+$[[T]]$. It should be another application or a type variable.
+\item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp}) 
+does \emph{not} need to be saturated.
+\item A saturated application of $[[(->) t1 t2]]$ should be represented as 
+$[[t1 -> t2]]$. This is a different point in the grammar, not just pretty-printing.
+The constructor for a saturated $[[(->)]]$ is \texttt{FunTy}.
+\item A type-level literal is represented in GHC with a different datatype than
+a term-level literal, but we are ignoring this distinction here.
+\end{itemize}
+
+\subsection{Coercions}
+
+\gram{\ottg}
+
+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
+be a type function.
+\end{itemize}
+
+Is it a left projection or a right projection?
+
+\gram{\ottLorR}
+
+Axioms:
+
+\gram{\ottC}
+
+\subsection{Type constructors}
+
+Type constructors in GHC contain \emph{lots} of information. We leave most of it out
+for this formalism:
+
+\gram{\ottT}
+
+We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.lhs}.
+
+\gram{\ottH}
+
+\section{Contexts}
+
+The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
+This monad contains a context with a set of bound variables $[[G]]$. The
+formalism treats $[[G]]$ as an ordered list, but GHC uses a set as its
+representation.
+
+\gram{
+\ottG
+}
+
+We assume the Barendregt variable convention that all new variables are
+fresh in the context. In the implementation, of course, some work is done
+to guarantee this freshness. In particular, adding a new type variable to
+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}
+
+The following functions are used from GHC. Their names are descriptive, and they
+are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
+\coderef{types/TyCon.lhs}{tyConArity}, \coderef{basicTypes/DataCon.lhs}{dataConTyCon}, \coderef{types/TyCon.lhs}{isNewTyCon}, \coderef{basicTypes/DataCon.lhs}{dataConRepType}.
+
+\subsection{Program consistency}
+
+Check the entire bindings list in a context including the whole list. We extract
+the actual variables (with their types/kinds) from the bindings, check for duplicates,
+and then check each binding.
+
+\ottdefnlintCoreBindings{}
+
+Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs}{bindersOf}:
+
+\[
+\begin{array}{ll}
+[[vars_of n = e]] &= [[n]] \\
+[[vars_of rec </ ni = ei // i />]] &= [[</ ni // i />]]
+\end{array}
+\]
+
+\subsection{Binding consistency}
+
+\ottdefnlintXXbind{}
+
+\ottdefnlintSingleBinding{}
+
+In the GHC source, this function contains a number of other checks, such
+as for strictness and exportability. See the source code for further information.
+
+\subsection{Expression typing}
+
+\ottdefnlintCoreExpr{}
+
+%\arraylabel{\coderef{coreSyn/CoreLint.lhs}{checkCaseAlts}} \\
+%\multicolumn{2}{l}{[[checkCaseAlts]] \text{ checks ordering and exhaustivity constr%aints}} \\
+
+%\end{array}
+%\]
+
+\begin{itemize}
+\item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
+second premise ($[[</ G, G'i |-ty s'i : ki // i />]]$) is that we wish
+to check each substituted type $[[s'i]]$ in a context containing all the types
+that come before it in the list of bindings. The $[[G'i]]$ are contexts
+containing the names and kinds of all type variables (and term variables,
+for that matter) up to the $i$th binding. This logic is extracted from
+\coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
+
+\item There is one more case for $[[G |-tm e : t]]$, for type expressions.
+This is included in the GHC code but is elided
+here because the case is never used in practice. Type expressions
+can only appear in arguments to functions, and these are handled
+in \ottdrulename{Tm\_AppType}.
+
+\item The GHC source code checks all arguments in an application expression
+all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
+and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
+has been unfolded for presentation here.
+
+\item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
+(scoping) checks.
+
+\item The rule for $[[case]]$ statements also checks to make sure that
+the alternatives in the $[[case]]$ are well-formed with respect to the
+invariants listed above. These invariants do not affect the type or
+evaluation of the expression, so the check is omitted here.
+
+\item The GHC source code for \ottdrulename{Tm\_Var} contains checks for
+a dead id and for one-tuples. These checks are omitted here.
+\end{itemize}
+
+\subsection{Kinding}
+
+\ottdefnlintType{}
+
+\subsection{Kind validity}
+
+\ottdefnlintKind{}
+
+\subsection{Coercion typing}
+
+\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.
+
+\subsection{Name consistency}
+
+There are two very similar checks for names, one declared as a local function
+within \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding}:
+
+\ottdefnlintSingleBindingXXlintBinder{}
+
+\ottdefnlintBinder{}
+
+\subsection{Substitution consistency}
+
+\ottdefncheckTyKind{}
+
+\subsection{Case alternative consistency}
+
+\ottdefnlintCoreAlt{}
+
+\subsection{Telescope substitution}
+
+\ottdefnapplyTys{}
+
+\subsection{Case alternative binding consistency}
+
+\ottdefnlintAltBinders{}
+
+\subsection{Arrow kinding}
+
+\ottdefnlintArrow{}
+
+\subsection{Type application kinding}
+
+\ottdefnlintXXapp{}
+
+\subsection{Sub-kinding}
+
+\ottdefnisSubKind{}
+
+\end{document}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
new file mode 100644
index 0000000000..0e427c9c81
--- /dev/null
+++ b/docs/core-spec/core-spec.pdf