core-spec: Add join points to formalism

5 files changed, 197 insertions, 46 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 50b11ce7e7..3a3468d53b 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -30,7 +30,7 @@ G |-sbind n <- e
 ---------------------- :: NonRec
 G |-bind n = e
 
-</ G |-sbind ni <- ei // i />
+</ G, </ ni // i /> |-sbind ni <- ei // i />
 ---------------------- :: Rec
 G |-bind rec </ ni = ei // i />
 
@@ -38,50 +38,64 @@ defn G  |- sbind n <- e ::  :: lintSingleBinding :: 'SBinding_' {{ com Single bi
   {{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }}
 by
 
-G |-tm e : t
+G; empty |-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_'
+defn G ; D |-sjbind l vars <- e : t ::  :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
+  {{ tex [[G]];[[D]] \labeledjudge{sjbind} [[l]] \, [[vars]] [[<-]] [[e]] : [[t]] }}
+by
+
+</ G'j $ // j /> = inits(</ nj // j />)
+G, </ nj // j /> ; D |-tm e : t
+G |-label p/I_s ok
+</ G, G'j |-name nj ok // j />
+</ mj // j /> = fv(s)
+</ mj elt G // j />
+split_I s = </ sj // j /> t
+----------------- :: SingleBinding
+G; D |-sjbind p/I_s </ nj // j /> <- e : t
+
+defn G ; D  |- tm e : t ::  :: lintCoreExpr :: 'Tm_'
   {{ com Expression typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreExpr} }}
-  {{ tex [[G]] \labeledjudge{tm} [[e]] : [[t]] }}
+  {{ tex [[G]]; [[D]] \labeledjudge{tm} [[e]] : [[t]] }}
 by
 
 x_t elt G
 not (t is_a_coercion_type)
 ------------------ :: Var
-G |-tm x_t : t
+G; D |-tm x_t : t
 
 t = literalType lit
 ------------------- :: Lit
-G |-tm lit : t
+G; D |-tm lit : t
 
-G |-tm e : s
+G; empty |-tm e : s
 G |-co g : s k1~Rep k2 t
 k2 elt { *, # }
 ------------------- :: Cast
-G |-tm e |> g : t
+G; D |-tm e |> g : t
 
-G |-tm e : t
+G; empty |-tm e : t
 ------------------- :: Tick
-G |-tm e {tick} : t
+G; D |-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
+G'; D |-tm e[alpha_k |-> s] : t
 --------------------------- :: LetTyKi
-G |-tm let alpha_k = s in e : t
+G; D |-tm let alpha_k = s in e : t
 
 G |-sbind x_s <- u
 G |-ty s : k
 k = * \/ k = #
-G, x_s |-tm e : t
+G, x_s ; D |-tm e : t
 ------------------------- :: LetNonRec
-G |-tm let x_s = u in e : t
+G; D |-tm let x_s = u in e : t
 
 </ G'i $ // i /> = inits(</ zi_si // i />)
 </ G, G'i |-ty si : ki // i />
@@ -89,54 +103,72 @@ G |-tm let x_s = u in e : t
 no_duplicates </ zi // i />
 G' = G, </ zi_si // i />
 </ G' |-sbind zi_si <- ui // i />
-G' |-tm e : t
+G'; D |-tm e : t
 ------------------------ :: LetRec
-G |-tm let rec </ zi_si = ui // i /> in e : t
+G; D |-tm let rec </ zi_si = ui // i /> in e : t
+
+G; D |-sjbind l </ ni // i /> <- u : t
+G; D, l |-tm e : t
+------------------------------------------- :: JoinNonRec
+G; D |-tm join l </ ni // i /> = u in e : t
+
+no_duplicates </ li // i />
+D' = D, </ li // i />
+</ G; D' |-sjbind l </ nj // j /> <- ui : t // i />
+G; D' |-tm e : t
+------------------------------------------------------------- :: JoinRec
+G; D |-tm join rec </ li </ nj // j /> = ui // i /> in e : t
 
 % lintCoreArg is incorporated in these next two rules
 
-G |-tm e : forall alpha_k.t
+G; empty |-tm e : forall alpha_k.t
 G |-subst alpha_k |-> s ok
 ---------------- :: AppType
-G |-tm e s : t[alpha_k |-> s]
+G; D |-tm e s : t[alpha_k |-> s]
 
 not (e2 is_a_type)
-G |-tm e1 : t1 -> t2
-G |-tm e2 : t1
+G; empty |-tm e1 : t1 -> t2
+G; empty |-tm e2 : t1
 ---------------- :: AppExpr
-G |-tm e1 e2 : t2
+G; D |-tm e1 e2 : t2
+
+p/I_s elt D
+split_I s = </ sj // j /> t
+</ G; empty |-tm ej : sj // j />
+--------------------- :: Jump
+G; D |-tm jump p/I_s </ ej // j /> : t
 
 not (k is_a_coercion_type)
 G |-ty t : k
-G, x_t |-tm e : s
+G, x_t; |-tm e : s
 ----------------- :: LamId
-G |-tm \x_t.e : t -> s
+G; D |-tm \x_t.e : t -> s
 
 G |-ki k ok
-G,alpha_k |-tm e : t
+G,alpha_k; |-tm e : t
 --------------------------- :: LamTy
-G |-tm \alpha_k.e : forall alpha_k. t
+G; D |-tm \alpha_k.e : forall alpha_k. t
 
 phi = s1 k1~#k2 s2
 G |-ki phi ok
-G,c_phi |-tm e : t
+G,c_phi; |-tm e : t
 -------------------------------- :: LamCo
-G |-tm \c_phi.e : forall c_phi.t
+G; D |-tm \c_phi.e : forall c_phi.t
 
-G |-tm e : s
+G; empty |-tm e : s
 s = * \/ s = #
 G |-ty t : TYPE s2
-</ G, z_s; s |-altern alti : t // i />
+</ G, z_s; D; s |-altern alti : t // i />
 ---------------------------------------------------- :: Case
-G |-tm case e as z_s return t of </ alti // i /> : t
+G; D |-tm case e as z_s return t of </ alti // i /> : t
 
 G |-co g : t1 k1~Nom k2 t2
 -------------------- :: Coercion
-G |-tm g : t1 k1~#k2 t2
+G; D |-tm g : t1 k1~#k2 t2
 
 G |-co g : t1 k1~Rep k2 t2
 ----------------------- :: CoercionRep
-G |-tm g : (~Rep#) k1 k2 t1 t2
+G; D |-tm g : (~Rep#) k1 k2 t1 t2
 
 defn G  |- name n ok ::  :: lintSingleBinding_lintBinder :: 'Name_'
   {{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }}
@@ -151,6 +183,19 @@ G |-name x_t ok
 ----------------- :: TyVar
 G |-name alpha_k ok
 
+defn G |- label l ok ::  :: lintSingleBinding_lintBinder_join :: 'Label_'
+  {{ com Label consistency check, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding\#lintBinder} }}
+  {{ tex [[G]] \labeledjudge{label} [[l]] [[ok]] }}
+by
+
+G |- ty t : k
+k = * \/ k = #
+split_I t = </ si // i /> t'
+G |- ty t' : k'
+k' = * \/ k' = #
+----------------- :: Label
+G |-label p / I _ t ok
+
 defn G |- bnd n ok ::  :: lintBinder :: 'Binding_'
   {{ com Binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintBinder} }}
   {{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }}
@@ -316,7 +361,7 @@ G |-ty t'2 : k0'
 G |-co mu </ ti // i /> $ </ gj // j /> : t'1 k0 ~R' k0' t'2
 
 defn G |- axk [ namesroles |-> gs ] ~> ( subst1 , subst2 ) ::  :: check_ki :: 'AxiomKind_'
-  {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.lhs}{check\_ki} }}
+  {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.lhs}{lintCoercion\#check\_ki} }}
   {{ tex [[G]] \labeledjudge{axk} [ [[namesroles]] [[|->]] [[gs]] ] [[~>]] ([[subst1]], [[subst2]]) }}
 by
 
@@ -477,19 +522,19 @@ G |-ty t : k
 ---------------------- :: Type
 G |-subst z_k |-> t ok
 
-defn G ; s |- altern alt : t ::  :: lintCoreAlt :: 'Alt_'
+defn G ; D ; s |- altern alt : t ::  :: lintCoreAlt :: 'Alt_'
   {{ com Case alternative consistency, \coderef{coreSyn/CoreLint.lhs}{lintCoreAlt} }}
-  {{ tex [[G]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
+  {{ tex [[G]];[[D]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
 by
 
-G |-tm e : t
+G; D |-tm e : t
 --------------------- :: DEFAULT
-G; s |-altern _ -> e : t
+G; D; s |-altern _ -> e : t
 
 s = literalType lit
-G |-tm e : t
+G; D |-tm e : t
 ---------------------------------------- :: LitAlt
-G; s |-altern lit -> e : t
+G; D; s |-altern lit -> e : t
 
 T = dataConTyCon K
 not (isNewTyCon T)
@@ -498,9 +543,9 @@ 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
+G'; D |-tm e : t
 --------------------------------------- :: DataAlt
-G; T </ sj // j /> |-altern K </ ni // i /> -> e : t
+G; D; T </ sj // j /> |-altern K </ ni // i /> -> e : t
 
 defn t' = t { </ si // , // i /> } ::  :: applyTys :: 'ApplyTys_'
   {{ com Telescope substitution, \coderef{types/Type.lhs}{applyTys} }}
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index c42e38a980..78118d532c 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -19,6 +19,7 @@ embed {{ tex-preamble
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 metavar x, c ::=   {{ com Term-level variable names }}
+metavar p ::=    {{ com Labels }}
 metavar alpha {{ tex \alpha }}, beta {{ tex \beta }} ::=
   {{ com Type-level variable names }}
 metavar N ::=   {{ com Type-level constructor names }}
@@ -45,6 +46,10 @@ n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable na
   | z $             :: M :: NoSupScript {{ com Name without an explicit type/kind }}
   | K               :: M :: DataCon     {{ com Data constructor }}
 
+l :: 'Label_' ::= {{ com Labels for join points, also \coderef{basicTypes/Var.lhs}{Var} }}
+  | p / I _ t     ::   :: Label   {{ com Label with join arity and type }}
+    {{ tex  {[[p]]}_{[[I]]}^{[[t]]} }}
+
 vars :: 'Vars_' ::= {{ com List of variables }}
   | </ ni // , // i />       ::   :: List
   | fv ( t )                 :: M :: fv_t
@@ -55,12 +60,18 @@ vars :: 'Vars_' ::= {{ com List of variables }}
   | vars1 \inter vars2       :: M :: intersection
     {{ tex [[vars1]] \cap [[vars2]] }}
 
+labels :: 'Labels_' ::= {{ com List of labels }}
+  | </ li // , // i />       ::   :: List
+  | empty                    :: M :: empty
+
 e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
   | n                                            ::   :: Var  {{ com \ctor{Var}: Variable }}
   | lit                                          ::   :: Lit  {{ com \ctor{Lit}: Literal }}
   | e1 e2                                        ::   :: App  {{ com \ctor{App}: Application }}
+  | jump l </ ui // i />                         ::   :: Jump {{ com \ctor{App}: Jump }}
   | \ n . e                                      ::   :: Lam  {{ com \ctor{Lam}: Abstraction }}
   | let binding in e                             ::   :: Let  {{ com \ctor{Let}: Variable binding }}
+  | join jbinding in e                           ::   :: Join {{ com \ctor{Let}: Join binding }}
   | case e as n return t of </ alti // | // i /> ::   :: Case {{ com \ctor{Case}: Pattern match }}
   | e |> g                                       ::   :: Cast {{ com \ctor{Cast}: Cast }}
   | e { tick }                                   ::   :: Tick {{ com \ctor{Tick}: Internal note }}
@@ -78,6 +89,10 @@ binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind}
   | n = e                         ::   :: NonRec  {{ com \ctor{NonRec}: Non-recursive binding }}
   | rec </ ni = ei // ;; // i /> ::   :: Rec     {{ com \ctor{Rec}: Recursive binding }}
 
+jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
+  | l </ ni // i /> = e     ::   :: NonRec {{ com \ctor{NonRec}: Non-recursive binding }}
+  | rec </ li </ nij // j /> = ei // i /> :: :: Rec {{ com \ctor{Rec}: Recursive binding }}
+
 alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }}
   | Kp </ ni // i /> -> e    ::   :: Alt  {{ com Constructor applied to fresh names }}
 
@@ -214,6 +229,12 @@ 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} }}
 
+D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
+  | l                        ::   :: Binding   {{ com Single binding }}
+  | </ Di // , // i />       ::   :: Concat    {{ com Context concatenation }}
+  | empty                    :: M :: Empty     {{ com Empty context }}
+  | labels_of binding        :: M :: LabelsOf  {{ 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 }}
@@ -255,6 +276,9 @@ ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
   | 1                           :: M :: one
   | 2                           :: M :: two
 
+terms :: 'Terms_' ::= {{ com List of terms }}
+  | </ ei // i />      ::   :: List
+
 types :: 'Types_' ::= {{ com List of types }}
   | </ ti // i />      ::   :: List
 
@@ -294,9 +318,11 @@ role_list {{ tex {\overline{\rho_j} }^j }} :: 'RoleList_' ::= {{ com List of rol
 terminals :: 'terminals_' ::=
   | \            ::   :: lambda           {{ tex \lambda }}
   | let          ::   :: let              {{ tex \keyword{let} }}
+  | join         ::   :: join             {{ tex \keyword{join} }}
   | in           ::   :: key_in           {{ tex \keyword{in} }}
   | rec          ::   :: rec              {{ tex \keyword{rec} }}
   | and          ::   :: key_and          {{ tex \keyword{and} }}
+  | jump         ::   :: jump             {{ tex \keyword{jump} }}
   | case         ::   :: case             {{ tex \keyword{case} }}
   | of           ::   :: of               {{ tex \keyword{of} }}
   | ->           ::   :: arrow            {{ tex \to }}
@@ -317,6 +343,7 @@ terminals :: 'terminals_' ::=
   | ok           ::   :: ok               {{ tex \textsf{ ok} }}
   | no_duplicates ::  :: no_duplicates    {{ tex \textsf{no\_duplicates } }}
   | vars_of      ::   :: vars_of          {{ tex \textsf{vars\_of } }}
+  | split        ::   :: split            {{ tex \mathop{\textsf{split} } }}
   | not          ::   :: not              {{ tex \neg }}
   | isUnLiftedTyCon :: :: isUnLiftedTyCon {{ tex \textsf{isUnLiftedTyCon} }}
   | compatibleUnBoxedTys :: :: compatibleUnBoxedTys {{ tex \textsf{compatibleUnBoxedTys} }}
@@ -366,6 +393,8 @@ terminals :: 'terminals_' ::=
   | Just         ::   :: Just             {{ tex \textsf{Just} }}
   | \\           ::   :: newline          {{ tex \\ }}
   | classifiesTypeWithValues :: :: ctwv   {{ tex \textsf{classifiesTypeWithValues} }}
+  | 0            ::   :: zero             {{ tex 0 }}
+  | +1           ::   :: succ             {{ tex +1 }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -375,6 +404,7 @@ formula :: 'formula_' ::=
   | judgement                          ::   :: judgement
   | formula1 ... formulai              ::   :: dots
   | G1 = G2                            ::   :: context_rewrite
+  | D1 = D2                            ::   :: join_context_rewrite
   | t1 = t2                            ::   :: type_rewrite
   | t1 /= t2                           ::   :: type_inequality
   | e1 /=e e2                          ::   :: expr_inequality
@@ -384,6 +414,7 @@ formula :: 'formula_' ::=
   | g1 = g2                            ::   :: co_rewrite
   | no_duplicates </ zi // i />        ::   :: no_duplicates_name
   | no_duplicates </ bindingi // i />  ::   :: no_duplicates_binding
+  | no_duplicates </ li // i />        ::   :: no_duplicates_label
   | not formula                        ::   :: not
   | isUnLiftedTyCon T                  ::   :: isUnLiftedTyCon
   | compatibleUnBoxedTys t1 t2         ::   :: compatibleUnBoxedTys
@@ -395,6 +426,7 @@ formula :: 'formula_' ::=
 }{\quad [[formula2]]} \end{array} }}
   | ( formula )                        ::   :: parens
   | n elt G                            ::   :: context_inclusion
+  | l elt D                            ::   :: join_context_inclusion
   | vars1 = vars2                      ::   :: vars_rewrite
   | </ Gi $ // i /> = inits ( </ nj // j /> ) :: :: context_folding
   | </ substi $ // i /> = inits ( </ [ nj |-> tj ] // j /> ) :: :: subst_folding
@@ -436,6 +468,8 @@ formula :: 'formula_' ::=
   | mu1 = mu2                          ::   :: mu_rewrite
   | classifiesTypeWithValues k         ::   :: classifies_type_with_values
   | z elt vars                         ::   :: in_vars
+  | split _ I s = types                ::   :: split_type
+    {{ tex \mathop{\textsf{split} }_{[[I]]} [[s]] = [[types]] }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Subrules and Parsing  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -461,6 +495,7 @@ Subst_TyMapping <= Type_TySubstListPost
 Subst_TmMapping <= Type_TySubstListPost
 
 Expr_Type <= formula_e_rewrite
+Expr_Jump <= Expr_Apps
 
 Coercion_TyConAppCo <= Coercion_AppCo
 
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index 8fb9b0e068..03be476bbb 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -13,6 +13,10 @@
 % 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.
+%
+% Join points are ignored here because operationally they work exactly the same
+% as regular bindings. Simply read "join" as "let" and "jump" as application to
+% see how a (well-typed!) program should run.
 
 grammar
 
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index d1d89055e7..580032129d 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -89,6 +89,10 @@ variables:
 \ottn
 }
 
+\gram{
+\ottl
+}
+
 We sometimes omit the type/kind annotation to a variable when it is obvious from context.
 
 \subsection{Expressions}
@@ -112,13 +116,39 @@ is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSy
 \item Types and coercions can only appear on the right-hand-side of an application.
 \item The $[[t]]$ form of an expression must not then turn out to be a coercion.
 In other words, the payload inside of a \texttt{Type} constructor must not turn out
-to be built with \texttt{CoercionTy}. 
+to be built with \texttt{CoercionTy}.
+\item Join points (introduced by $[[join]]$ expressions) follow the invariants
+laid out in \verb|Note [Invariants on join points]| in
+\ghcfile{coreSyn/CoreSyn.lhs}:
+\begin{enumerate}
+    \item All occurences must be tail calls. This is enforced in our typing
+    rules using the label environment $[[D]]$.
+    \item Each join point has a \emph{join arity}. In this document, we write
+    each label as $[[p/I_t]]$ for the name $[[p]]$, the type $[[t]]$, and the
+    join arity $[[I]]$. The right-hand side of the binding must begin with at
+    least $[[I]]$ lambdas. This is enforced implicitly in
+    \ottdrulename{Tm\_JoinNonRec} and \ottdrulename{Tm\_JoinRec} by the use of
+    $[[split]]$ meta-function.
+    \item If the binding is recursive, then all other bindings in the recursive
+    group must be join points. We enforce this in our reformulation of the
+    grammar; in the actual AST, a $[[join]]$ is simply a $[[let]]$ where each
+    identifier is flagged as a join id, so this invariant requires that this
+    flag must be consistent across a recursive binding.
+    \item The binding's type must not be polymorphic in its return type. This
+    is expressed in \ottdrulename{Label\_Label}; see
+    Section~\ref{sec:name_consistency}.
+\end{enumerate}
+
 \end{itemize}
 
 Bindings for $[[let]]$ statements:
 
 \gram{\ottbinding}
 
+Bindings for $[[join]]$ statements:
+
+\gram{\ottjbinding}
+
 Case alternatives:
 
 \gram{\ottalt}
@@ -275,15 +305,21 @@ synonym for $[[TYPE 'Unlifted]]$.
 \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
+This monad contains a context with a set of bound variables $[[G]]$ and a set
+of bound labels $[[D]]$. The formalism treats $[[G]]$ and $[[D]]$ as ordered
+lists, but GHC uses sets as its
 representation.
 
 \gram{
 \ottG
 }
 
-We assume the Barendregt variable convention that all new variables are
+\gram{
+\ottD
+}
+
+We assume the Barendregt variable convention that all new variables and labels
+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
@@ -313,12 +349,29 @@ Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs
 \end{array}
 \]
 
+Here is the definition of $[[split]]$, which has no direct analogue in the
+source but simplifies the presentation here:
+
+\[
+\begin{array}{ll}
+[[split]]_0 [[t]] &= [[t]] \\
+[[split]]_n ([[s -> t]]) &= [[s]] \; ([[split]]_{n-1} [[t]]) \\
+[[split]]_n ([[forall alpha _ k . t]]) &= [[k]] \; ([[split]]_{n-1} [[t]])
+\end{array}
+\]
+
+The idea is simply to peel off the leading $i$ argument types (which may be
+kinds for type arguments) from a given type and return them in a sequence, with
+the return type (given $i$ arguments) as the final element of the sequence.
+
 \subsection{Binding consistency}
 
 \ottdefnlintXXbind{}
 
 \ottdefnlintSingleBinding{}
 
+\ottdefnlintSingleBindingXXjoins{}
+
 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.
 
@@ -376,11 +429,19 @@ See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, a
 see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
 
 \subsection{Name consistency}
+\label{sec:name_consistency}
 
-There are two very similar checks for names, one declared as a local function:
+There are three very similar checks for names, two performed as part of
+\coderef{coreSyn/CoreLint.hs}{lintSingleBinding}:
 
 \ottdefnlintSingleBindingXXlintBinder{}
 
+\ottdefnlintSingleBindingXXlintBinderXXjoin{}
+
+The point of the extra checks on $[[t']]$ is that a join point's type cannot be
+polymorphic in its return type; see \texttt{Note [The polymorphism rule of join
+points]} in \ghcfile{coreSyn/CoreSyn.hs}.
+
 \ottdefnlintBinder{}
 
 \subsection{Substitution consistency}
@@ -477,6 +538,12 @@ Also note that this semantics implements call-by-name, not call-by-need. So
 while it describes the operational meaning of a term, it does not describe what
 subexpressions are shared, and when.
 
+\subsection{Join points}
+Dealing with join points properly here would be cumbersome and pointless, since
+by design they work no differently than functions as far as FC is concerned.
+Reading $[[join]]$ as $[[let]]$ and $[[jump]]$ as application should tell you
+all need to know.
+
 \subsection{Operational semantics rules}
 
 \ottdefnstep{}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index dde6c9eeba..1e139115cd 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf