Add kind equalities to GHC.

This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

7 files changed, 389 insertions, 231 deletions

diff --git a/docs/core-spec/.gitignore b/docs/core-spec/.gitignore
index a1958037ad..dac3bd2547 100644
--- a/docs/core-spec/.gitignore
+++ b/docs/core-spec/.gitignore
@@ -3,3 +3,4 @@
 *.fdb_latexmk
 CoreOtt.tex
 core-spec.tex
+*.fls
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 7058e8a113..50b11ce7e7 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -51,7 +51,7 @@ defn G  |- tm e : t ::  :: lintCoreExpr :: 'Tm_'
 by
 
 x_t elt G
-not (t is_a_coercion)
+not (t is_a_coercion_type)
 ------------------ :: Var
 G |-tm x_t : t
 
@@ -60,7 +60,8 @@ t = literalType lit
 G |-tm lit : t
 
 G |-tm e : s
-G |-co g : s ~Rep k t
+G |-co g : s k1~Rep k2 t
+k2 elt { *, # }
 ------------------- :: Cast
 G |-tm e |> g : t
 
@@ -77,12 +78,14 @@ G |-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
 ------------------------- :: LetNonRec
 G |-tm let x_s = u in e : t
 
-</ G'i @ // i /> = inits(</ zi_si // i />)
+</ G'i $ // i /> = inits(</ zi_si // i />)
 </ G, G'i |-ty si : ki // i />
+</ ki = * \/ ki = # // i />
 no_duplicates </ zi // i />
 G' = G, </ zi_si // i />
 </ G' |-sbind zi_si <- ui // i />
@@ -92,10 +95,10 @@ 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 |-tm e : forall alpha_k.t
 G |-subst alpha_k |-> s ok
 ---------------- :: AppType
-G |-tm e1 s : t[alpha_k |-> s]
+G |-tm e s : t[alpha_k |-> s]
 
 not (e2 is_a_type)
 G |-tm e1 : t1 -> t2
@@ -103,31 +106,37 @@ G |-tm e2 : t1
 ---------------- :: AppExpr
 G |-tm e1 e2 : t2
 
+not (k is_a_coercion_type)
 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
+G,alpha_k |-tm e : t
 --------------------------- :: LamTy
 G |-tm \alpha_k.e : forall alpha_k. t
 
+phi = s1 k1~#k2 s2
+G |-ki phi ok
+G,c_phi |-tm e : t
+-------------------------------- :: LamCo
+G |-tm \c_phi.e : forall c_phi.t
+
 G |-tm e : s
-G |-ty s : k1
-G |-ty t : k2
+s = * \/ s = #
+G |-ty t : TYPE s2
 </ G, z_s; s |-altern alti : t // i />
 ---------------------------------------------------- :: Case
 G |-tm case e as z_s return t of </ alti // i /> : t
 
-G |-co g : t1 ~Nom k t2
--------------------- :: CoercionNom
-G |-tm g : t1 ~#k t2
+G |-co g : t1 k1~Nom k2 t2
+-------------------- :: Coercion
+G |-tm g : t1 k1~#k2 t2
 
-G |-co g : t1 ~Rep k t2
+G |-co g : t1 k1~Rep k2 t2
 ----------------------- :: CoercionRep
-G |-tm g : (~R#) k t1 t2
+G |-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} }}
@@ -135,6 +144,7 @@ defn G  |- name n ok ::  :: lintSingleBinding_lintBinder :: 'Name_'
 by
 
 G |-ty t : k
+k = * \/ k = #
 ----------------- :: Id
 G |-name x_t ok
 
@@ -147,6 +157,7 @@ defn G |- bnd n ok ::  :: lintBinder :: 'Binding_'
 by
 
 G |-ty t : k
+k = * \/ k = #
 --------------------------------- :: Id
 G |-bnd x_t ok
 
@@ -154,125 +165,169 @@ G |-ki k ok
 ---------------------------------------- :: TyVar
 G |-bnd alpha_k ok
 
-defn G  |- co g : t1 ~ R k t2 ::  :: lintCoercion :: 'Co_'
+defn G  |- co g : t1 k1 ~ R k2 t2 ::  :: lintCoercion :: 'Co_'
   {{ com Coercion typing, \coderef{coreSyn/CoreLint.lhs}{lintCoercion} }}
-  {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{\sim_{[[R]]}^{[[k]]} } [[t2]] }}
+  {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{ {}^{[[k1]]} {\sim}_{[[R]]}^{[[k2]]} } [[t2]] }}
 by
 
 G |-ty t : k
 ---------------------- :: Refl
-G |-co <t>_R : t ~R k t
+G |-co <t>_R : t k~R k t
 
-G |-co g1 : s1 ~R k1 t1
-G |-co g2 : s2 ~R k2 t2
+G |-co g1 : s1 k1~R k'1 t1
+G |-co g2 : s2 k2~R k'2 t2
 G |-arrow k1 -> k2 : k
+G |-arrow k'1 -> k'2 : k'
 ------------------------- :: TyConAppCoFunTy
-G |-co (->)_R g1 g2 : (s1 -> s2) ~R k (t1 -> t2)
+G |-co (->)_R g1 g2 : (s1 -> s2) k~R k' (t1 -> t2)
 
 T /= (->)
 </ Ri // i /> = take(length </ gi // i />, tyConRolesX R T)
-</ G |-co gi : si ~Ri ki ti // i />
-G |-app </ (si : ki) // i /> : tyConKind T ~> k
+</ G |-co gi : si k'i~Ri ki ti // i />
+G |-app </ (si : k'i) // i /> : tyConKind T ~> k'
+G |-app </ (ti : ki) // i /> : tyConKind T ~> k
 --------------------------------- :: TyConAppCo
-G |-co T_R </ gi // i /> : T </ si // i />  ~R k T </ ti // i />
+G |-co T_R </ gi // i /> : T </ si // i />  k'~R k T </ ti // i />
 
-G |-co g1 : s1 ~R k1 t1
-G |-co g2 : s2 ~Nom k2 t2
-G |-app (s2 : k2) : k1 ~> k
+G |-co g1 : s1 k1~R k2 s2
+G |-co g2 : t1 k1'~Nom k2' t2
+G |-app (t1 : k1') : k1 ~> k3
+G |-app (t2 : k2') : k2 ~> k4
 --------------------- :: AppCo
-G |-co g1 g2 : (s1 s2) ~R k (t1 t2)
+G |-co g1 g2 : (s1 t1) k3~R k4 (s2 t2)
 
-G |-co g1 : s1 ~Ph k1 t1
-G |-co g2 : s2 ~Ph k2 t2
-G |-app (s2 : k2) : k1 ~> k
+G |-co g1 : s1 k1 ~Ph k2 s2
+G |-co g2 : t1 k1' ~Ph k2' t2
+G |-app (t1 : k1') : k1 ~> k3
+G |-app (t2 : k2') : k2 ~> k4
 --------------------- :: AppCoPhantom
-G |-co g1 g2 : (s1 s2) ~Ph k (t1 t2)
-
-G |-ki k1 ok
-G, z_k1 |-co g : s ~R k2 t
---------------------------- :: ForAllCo
-G |-co forall z_k1. g : (forall z_k1.s) ~R k2 (forall z_k1.t)
+G |-co g1 g2 : (s1 t1) k3~Ph k4 (s2 t2)
 
-z_(t ~#BOX t) elt G
------------------------ :: CoVarCoBox
-G |-co z_(t ~#BOX t) : t ~Nom BOX t
+G |-co h : k1 *~Nom * k2
+G, z_k1 |-co g : t1 k3~R k4 t2
+------------------------------------------------------------------ :: ForAllCo
+G |-co forall z:h. g : (forall z_k1. t1) k3~R k4 (forall z_k2. (t2[z |-> z_k2 |> sym h]))
 
-z_(s ~#k t) elt G
-k /= BOX
+z_phi elt G
+phi = t1 k1~#k2 t2
 ----------------------- :: CoVarCoNom
-G |-co z_(s ~#k t) : s ~Nom k t
+G |-co z_phi : t1 k1 ~Nom k2 t2
 
-z_(s ~R#k t) elt G
-k /= BOX
------------------------ :: CoVarCoRepr
-G |-co z_(s ~R#k t) : s ~Rep k t
+z_phi elt G
+phi = t1 k1 ~Rep# k2 t2
+--------------------- :: CoVarCoRepr
+G |-co z_phi : t1 k1 ~Rep k2 t2
 
+G |-co h : k1 *~Nom * k2
 G |-ty t1 : k1
 G |-ty t2 : k2
-R <= Ph \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2
------------------------------------------------------------------------- :: UnivCo
-G |-co t1 ==>!_R t2 : t1 ~R k2 t2
+(R <= Ph \/ not (classifiesTypeWithValues k1)) \\/ (not (classifiesTypeWithValues k2) \/ compatibleUnBoxedTys t1 t2)
+------------------------------------------------------ :: UnivCoUnsafe
+G |-co UnsafeCoerceProv <t1, t2>_R^(h) : t1 k1~R k2 t2
+
+G |-co h : k1 *~Nom * k2
+G |-ty t1 : k1
+G |-ty t2 : k2
+-------------------------------------------------- :: UnivCoPhantom
+G |-co PhantomProv <t1,t2>_Ph^(h) : t1 k1~Ph k2 t2
+
+G |-co h : phi1 *~Nom * phi2
+G |-ty g1 : phi1
+G |-ty g2 : phi2
+-------------------------------------------------- :: UnivCoProofIrrel
+G |-co ProofIrrelProv <g1,g2>_R^(h) : g1 phi1~R phi2 g2
 
-G |-co g : t1 ~R k t2
+G |-co g : t1 k1~R k2 t2
 ------------------------- :: SymCo
-G |-co sym g : t2 ~R k t1
+G |-co sym g : t2 k2~R k1 t1
 
-G |-co g1 : t1 ~R k t2
-G |-co g2 : t2 ~R k t3
+G |-co g1 : t1 k1~R k2 t2
+G |-co g2 : t2 k2~R k3 t3
 ----------------------- :: TransCo
-G |-co g1 ; g2 : t1 ~R k t3
+G |-co g1 ; g2 : t1 k1~R k3 t3
 
-G |-co g : (T </ sj // j />) ~R k (T </ tj // j />)
+G |-co g : (T </ sj // j />) k1~R k1' (T </ tj // j />)
 length </ sj // j /> = length </ tj // j />
 i < length </ sj // j />
-G |-ty si : k
+G |-ty si : k2
+G |-ty ti : k2'
+not (si is_a_coercion)
+not (ti is_a_coercion)
 R' = (tyConRolesX R T)[i]
----------------------- :: NthCo
-G |-co nth i g : si ~R' k ti
+---------------------- :: NthCoTyCon
+G |-co nth i g : si k2~R' k2' ti
 
-G |-co g : (s1 s2) ~Nom k' (t1 t2)
-G |-ty s1 : k
+G |-co g : (forall z1_k1.t1) k3~R k4 (forall z2_k2.t2)
+--------------------------- :: NthCoForAll
+G |-co nth 0 g : k1 *~Nom * k2
+
+G |-co g : (s1 s2) k~Nom k' (t1 t2)
+G |-ty s1 : k1
+G |-ty t1 : k1'
 ----------------------- :: LRCoLeft
-G |-co Left g : s1 ~Nom k t1
+G |-co Left g : s1 k1~Nom k1' t1
 
-G |-co g : (s1 s2) ~Nom k' (t1 t2)
-G |-ty s2 : k
+G |-co g : (s1 s2) k~Nom k' (t1 t2)
+G |-ty s2 : k2
+G |-ty t2 : k2'
+not (s2 is_a_coercion)
+not (t2 is_a_coercion)
 ----------------------- :: LRCoRight
-G |-co Right g : s2 ~Nom k t2
+G |-co Right g : s2 k2~Nom k2' t2
 
-G |-co g : forall m.s ~R k forall n.t
-G |-ty t0 : k0
-m = z_k1
-k0 <: k1
+G |-co g : (forall z1_k1.t1) k3~R k4 (forall z2_k2.t2)
+G |-co h : s1 k1~Nom k2 s2
 --------------------- :: InstCo
-G |-co g t0 : s[m |-> t0] ~R k t[n |-> t0]
+G |-co g @ h : (t1[z1_k1 |-> s1]) k3~R k4 (t2[z2_k2 |-> s2])
 
 C = T_R0 </ axBranchkk // kk />
 0 <= ind < length </ axBranchkk // kk />
 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 />
+G |-axk [ </ ni_Ri // i /> |-> </ gi // i /> ] ~> (subst1, subst2)
+</ s2j = subst1(s1j) // j />
 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
+t2 = subst2(t1)
+s2 = T </ s2j // j />
+G |-ty s2 : k
+G |-ty t2 : k'
 ------------------------------------------------------ :: AxiomInstCo
-G |-co C ind </ gi // i /> : T </ s2j // j /> ~R0 k t2
+G |-co C ind </ gi // i /> : s2 k~R0 k' t2
+
+G |-co g : t1 k1~R k2 t2
+G |-ty t1 |> h : k1'
+---------------------------------- :: CoherenceCo
+G |-co g |> h : t1 |> h k1'~R k2 t2
+
+G |-co g : t1 k1~R k2 t2
+-------------------------- :: KindCo
+G |-co kind g : k1 *~Nom * k2
 
-G |-co g : s ~Nom k t
+G |-co g : s k' ~Nom k t
 ------------------------- :: SubCo
-G |-co sub g : s ~Rep k t
+G |-co sub g : s k' ~Rep k t
 
 mu = M(i, </ Rj // j />, R')
 </ G |-ty ti : ki // i />
-</ G |-co gj : sj ~Rj k'j s'j // j />
+</ G |-co gj : sj k''j ~Rj k'j s'j // j />
 Just (t'1, t'2) = coaxrProves mu </ ti // i /> </ (sj, s'j) // j />
 G |-ty t'1 : k0
-G |-ty t'2 : k0
+G |-ty t'2 : k0'
 --------------------------------------------------------------------- :: AxiomRuleCo
-G |-co mu </ ti // i /> </ gj // j /> : t'1 ~R' k0 t'2
+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} }}
+  {{ tex [[G]] \labeledjudge{axk} [ [[namesroles]] [[|->]] [[gs]] ] [[~>]] ([[subst1]], [[subst2]]) }}
+by
+
+--------------------------------------- :: Empty
+G |-axk [empty |-> empty] ~> (empty, empty)
+
+G |-axk [namesroles |-> gs] ~> (subst1, subst2)
+n = z_k
+G |-co g0 : t1 {subst1(k)}~R subst2(k) t2
+----------------------------- :: Arg
+G |-axk [ namesroles, n_R |-> gs, g0 ] ~> (subst1 [n |-> t1], subst2 [n |-> t2])
 
 defn validRoles T ::  :: checkValidRoles :: 'Cvr_'
   {{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }}
@@ -288,7 +343,7 @@ 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
+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
@@ -329,6 +384,13 @@ O |- forall n. t : R
 ------------------ :: LitTy
 O |- lit : R
 
+O |- t : R
+--------------- :: CastTy
+O |- t |> g : R
+
+------------ :: CoercionTy
+O |- g : Ph
+
 defn R1 <= R2 ::  :: ltRole :: 'Rlt_'
   {{ com Sub-role relation, \coderef{types/Coercion.lhs}{ltRole} }}
   {{ tex [[R1]] \leq [[R2]] }}
@@ -348,8 +410,12 @@ defn G |- ki k ok ::  :: lintKind :: 'K_'
   {{ tex [[G]] \labeledjudge{k} [[k]] [[ok]] }}
 by
 
-G |-ty k : BOX
--------------- :: Box
+G |-ty k : *
+-------------- :: Star
+G |-ki k ok
+
+G |-ty k : #
+-------------- :: Hash
 G |-ki k ok
 
 defn G |- ty t : k ::  :: lintType :: 'Ty_'
@@ -380,28 +446,36 @@ G |-app </ (ti : ki) // i /> : tyConKind T ~> k
 G |-ty T </ ti // i /> : k
 
 G |-ki k1 ok
-G, z_k1 |-ty t : k2
+G, z_k1 |-ty t : TYPE s
+not (z elt fv(s))
 ------------------------ :: ForAllTy
-G |-ty forall z_k1. t : k2
+G |-ty forall z_k1. t : TYPE s
 
 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} }}
+G |-ty t : k1
+G |-co g : k1 *~Nom * k2
+--------------------- :: CastTy
+G |-ty t |> g : k2
+
+G |-co g : t1 k1 ~Nom k2 t2
+-------------- :: CoercionTy_Nom
+G |-ty g : t1 k1 ~# k2 t2
+
+G |-co g : t1 k1 ~Rep k2 t2
+------------------- :: CoercionTy_Repr
+G |-ty g : (~Rep#) k1 k2 t1 t2
+
+defn G |- subst n |-> t ok ::  :: lintTyKind :: 'Subst_'
+  {{ com Substitution consistency, \coderef{coreSyn/CoreLint.lhs}{lintTyKind} }}
   {{ 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
+G |-ty t : k
 ---------------------- :: Type
-G |-subst z_k1 |-> t ok
+G |-subst z_k |-> t ok
 
 defn G ; s |- altern alt : t ::  :: lintCoreAlt :: 'Alt_'
   {{ com Case alternative consistency, \coderef{coreSyn/CoreLint.lhs}{lintCoreAlt} }}
@@ -453,8 +527,12 @@ 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 /> : t[z_phi |-> c_phi] ~> s
+------------------------------------------------------- :: IdCoercion
+G |-altbnd c_phi, </ ni // i /> : (forall z_phi.t) ~> s
+
 G |-altbnd </ ni // i /> : t2 ~> s
------------------------------------------------ :: Id
+----------------------------------------------- :: IdTerm
 G |-altbnd x_t1, </ ni // i /> : (t1 -> t2) ~> s
 
 defn G |- arrow k1 -> k2 : k ::  :: lintArrow :: 'Arrow_'
@@ -462,11 +540,8 @@ defn G |- arrow k1 -> k2 : k ::  :: lintArrow :: 'Arrow_'
   {{ tex [[G]] \labeledjudge{\rightarrow} [[k1]] [[->]] [[k2]] : [[k]] }}
 by
 
-------------------------- :: Box
-G |-arrow BOX -> k2 : BOX
-
-k1 elt { *, #, Constraint }
-k2 elt { *, #, Constraint }
+k1 elt { *, # }
+k2 = TYPE s
 ------------------------- :: Kind
 G |-arrow k1 -> k2 : *
 
@@ -478,37 +553,13 @@ 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'
+G |-app (t : k1), </ (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
+G |-app (t : k1), </ (ti : ki) // i /> : (forall z_k1. k2) ~> k'
 
 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} } }}
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 247fd05ae3..f96666185e 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -10,17 +10,18 @@ embed {{ tex-preamble
 }
   \newcommand{\keyword}[1]{\textbf{#1} }
   \newcommand{\labeledjudge}[1]{\vdash_{\!\!\mathsf{#1} } }
+  \newcommand{\ctor}[1]{\texttt{#1}%
+}
 }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Metavariables  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-metavar x ::=   {{ com Term-level variable names }}
+metavar x, c ::=   {{ 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 }}
 metavar M ::=   {{ com Axiom rule names }}
 
 indexvar i, j, kk {{ tex k }}, aa {{ tex a }}, bb {{ tex b }}, cc {{ tex c }} ::= {{ com Indices to be used in lists }}
@@ -38,9 +39,10 @@ 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} }}
+n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.lhs}{Var} }}
   | z _ t           ::   :: IdOrTyVar   {{ com Name, labeled with type/kind }}
     {{ tex {[[z]]}^{[[t]]} }}
+  | z $             :: M :: NoSupScript {{ com Name without an explicit type/kind }}
   | K               :: M :: DataCon     {{ com Data constructor }}
 
 vars :: 'Vars_' ::= {{ com List of variables }}
@@ -54,18 +56,18 @@ vars :: 'Vars_' ::= {{ com List of variables }}
     {{ tex [[vars1]] \cap [[vars2]] }}
 
 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 }}
+  | n                                            ::   :: Var  {{ com \ctor{Var}: Variable }}
+  | lit                                          ::   :: Lit  {{ com \ctor{Lit}: Literal }}
+  | e1 e2                                        ::   :: App  {{ com \ctor{App}: Application }}
+  | \ n . e                                      ::   :: Lam  {{ com \ctor{Lam}: Abstraction }}
+  | let binding in e                             ::   :: Let  {{ com \ctor{Let}: Variable 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 }}
     {{ tex {[[e]]}_{\{[[tick]]\} } }}
-  | t                                            ::   :: Type {{ com Type }}
-  | g                                            ::   :: Coercion {{ com Coercion }}
-  | e subst                                      :: M :: Subst    {{ com Substitution }}
+  | t                                            ::   :: Type {{ com \ctor{Type}: Type }}
+  | g                                            ::   :: Coercion {{ com \ctor{Coercion}: Coercion }}
+  | 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 }}
@@ -73,8 +75,8 @@ e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
     {{ tex \qquad \\ \multicolumn{1}{r}{[[e]]} }}
 
 binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
-  | n = e                         ::   :: NonRec  {{ com Non-recursive binding }}
-  | rec </ ni = ei // ;; // i />  ::   :: Rec     {{ com Recursive binding }}
+  | n = e                         ::   :: NonRec  {{ com \ctor{NonRec}: Non-recursive binding }}
+  | rec </ ni = 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 }}
@@ -82,68 +84,84 @@ alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }}
 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 }}
+  | K        ::   :: DataAlt         {{ com \ctor{DataAlt}: Data constructor }}
+  | lit      ::   :: LitAlt          {{ com \ctor{LitAlt}: Literal (such as an integer or character) }}
+  | _        ::   :: DEFAULT         {{ com \ctor{DEFAULT}: 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 }}
+t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
+  :: 'Type_' ::= {{ com Types/kinds, \coderef{types/TyCoRep.lhs}{Type} }}
+  | n                       ::   :: TyVarTy       {{ com \ctor{TyVarTy}: Variable }}
+  | t1 t2                   ::   :: AppTy         {{ com \ctor{AppTy}: Application }}
+  | T </ ti // i />         ::   :: TyConApp      {{ com \ctor{TyConApp}: Application of type constructor }}
+  | t1 -> t2                ::   :: FunTy         {{ com \ctor{ForAllTy (Anon ...) ...}: Function }}
+  | forall n . t            ::   :: ForAllTy      {{ com \ctor{ForAllTy (Named ...) ...}: Type and coercion polymorphism }}
+  | lit                     ::   :: LitTy         {{ com \ctor{LitTy}: Type-level literal }}
+  | t |> g                  ::   :: CastTy        {{ com \ctor{CastTy}: Kind cast }}
+  | g                       ::   :: CoercionTy    {{ com \ctor{CoercionTy}: Coercion used in type }}
   | 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} }}
+  | t1 k1 ~# k2 t2          :: M :: unliftedEq    {{ com Metanotation for coercion types }}
+    {{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\#}^{[[k2]]} } [[t2]] }}
+  | t1 k1 ~Rep# k2 t2         :: M :: unliftedREq   {{ com Metanotation for coercion types }}
+    {{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\mathsf{R}\#}^{[[k2]]} } [[t2]] }}
+  | literalType lit         :: M :: literalType   {{ com \coderef{basicTypes/Literal.lhs}{literalType} }}
   | ( t )                   :: M :: parens        {{ com Parentheses }}
+  | { t }                   :: M :: IParens       {{ com Invisible parentheses }}
+    {{ tex [[t]] }}
   | 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 }}
+  | </ ti // i /> $ -> t'   :: M :: FunTys        {{ com Nested arrows }}
 
 %% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-g {{ tex \gamma }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/Coercion.lhs}{Coercion} }}
-  | < t > _ R               ::   :: Refl          {{ com Reflexivity }}
+g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.lhs}{Coercion} }}
+  | < t > _ R               ::   :: Refl          {{ com \ctor{Refl}: 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 ==>! RA t2           ::   :: UnivCo        {{ com Universal coercion }}
-  | sym g                   ::   :: SymCo         {{ com Symmetry }}
-  | g1 ; g2                 ::   :: TransCo       {{ com Transitivity }}
-  | mu </ ti // i /> </ gj // j />
-                            ::   :: AxiomRuleCo   {{ com Axiom-rule application (for type-nats) }}
-  | 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 }}
-  | sub g                   ::   :: SubCo         {{ com Sub-role --- convert nominal to representational }}
+  | T RA </ gi // i />      ::   :: TyConAppCo    {{ com \ctor{TyConAppCo}: Type constructor application }}
+  | g1 g2                   ::   :: AppCo         {{ com \ctor{AppCo}: Application }}
+  | forall z : h . g        ::   :: ForAllCo      {{ com \ctor{ForAllCo}: Polymorphism }}
+    {{ tex [[forall]] [[z]]{:}[[h]].[[g]] }}
+  | n                       ::   :: CoVarCo       {{ com \ctor{CoVarCo}: Variable }}
+  | C ind </ gi // i />     ::   :: AxiomInstCo   {{ com \ctor{AxiomInstCo}: Axiom application }}
+  | prov < t1 , t2 > _ R ^ ( h ) ::  :: UnivCo    {{ com \ctor{UnivCo}: Universal coercion }}
+    {{ tex {}_{[[prov]]}{\langle [[t1]], [[t2]] \rangle}_{[[R]]}^{[[h]]} }}
+  | sym g                   ::   :: SymCo         {{ com \ctor{SymCo}: Symmetry }}
+  | g1 ; g2                 ::   :: TransCo       {{ com \ctor{TransCo}: Transitivity }}
+  | mu </ ti // i /> $ </ gj // j />
+                            ::   :: AxiomRuleCo   {{ com \ctor{AxiomRuleCo}: Axiom-rule application (for type-nats) }}
+  | nth I g                 ::   :: NthCo         {{ com \ctor{NthCo}: Projection (0-indexed) }}
+    {{ tex \textsf{nth}^{[[I]]}\,[[g]] }}
+  | LorR g                  ::   :: LRCo          {{ com \ctor{LRCo}: Left/right projection }}
+  | g @ h                   ::   :: InstCo        {{ com \ctor{InstCo}: Instantiation }}
+  | g |> h                  ::   :: CoherenceCo   {{ com \ctor{CoherenceCo}: Coherence }}
+  | kind g                  ::   :: KindCo        {{ com \ctor{KindCo}: Kind extraction }}
+  | sub g                   ::   :: SubCo         {{ com \ctor{SubCo}: Sub-role --- convert nominal to representational }}
   | ( g )                   :: M :: Parens        {{ com Parentheses }}
-  | t @ liftingsubst        :: M :: Lifted        {{ com Type lifted to coercion }}
+  | t $ liftingsubst        :: M :: Lifted        {{ com Type lifted to coercion }}
+
+prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.lhs}{UnivCoProvenance} }}
+  | UnsafeCoerceProv   ::   :: UnsafeCoerceProv  {{ com From \texttt{unsafeCoerce\#} }}
+    {{ tex \mathsf{unsafe} }}
+  | PhantomProv        ::   :: PhantomProv       {{ com From the need for a phantom coercion }}
+    {{ tex \mathsf{phant} }}
+  | ProofIrrelProv     ::   :: ProofIrrelProv    {{ com From proof irrelevance }}
+    {{ tex \mathsf{irrel} }}
 
-LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/Coercion.lhs}{LeftOrRight} }}
-  | Left             ::   :: CLeft                {{ com Left projection }}
-  | Right            ::   :: CRight               {{ com Right projection }}
+LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.lhs}{LeftOrRight} }}
+  | Left             ::   :: CLeft                {{ com \ctor{CLeft}: Left projection }}
+  | Right            ::   :: CRight               {{ com \ctor{CRight}: Right projection }}
 
 C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.lhs}{CoAxiom} }}
-  | T RA </ axBranchi // ; // i /> ::   :: CoAxiom  {{ com Axiom }}
-  | ( C )                          :: M :: Parens   {{ com Parentheses }}
+  | T RA </ axBranchi // ; // i />     ::   :: CoAxiom  {{ com \ctor{CoAxiom}: Axiom }}
+  | ( C )                              :: M :: Parens   {{ com Parentheses }}
 
 R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.lhs}{Role} }}
   | Nom              ::   :: Nominal              {{ com Nominal }}
@@ -155,8 +173,8 @@ R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.lhs}{Role}
   | role_list [ i ]  :: M :: RoleListIndex        {{ com Look up in list }}
 
 axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.lhs}{CoAxBranch} }}
-  | forall </ ni RAi // 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 \ctor{CoAxBranch}: Axiom branch }}
+  | ( </ axBranchi // i /> ) [ ind ]               :: M :: lookup      {{ com List lookup }}
 
 mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxiom.lhs}{CoAxiomRule} }}
   | M ( I , role_list , R' )   ::  :: CoAxiomRule  {{ com Named rule, with parameter info }}
@@ -165,25 +183,29 @@ mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxi
 %% TYCONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
-  | ( -> )       ::   :: FunTyCon          {{ com Arrow }}
+  | ( -> )       ::   :: FunTyCon          {{ com \ctor{FunTyCon}: Arrow }}
 
   % the following also includes TupleTyCon, SynTyCon
-  | N _ k        ::   :: AlgTyCon          {{ com Named tycon: algebraic, tuples, and synonyms }}
+  | N _ k        ::   :: AlgTyCon          {{ com \ctor{AlgTyCon}, \ctor{TupleTyCon}, \ctor{SynTyCon}: algebraic, tuples, families, and synonyms }}
     {{ tex {[[N]]}^{[[k]]} }}
-  | H            ::   :: PrimTyCon         {{ com Primitive tycon }}
-  | ' K          ::   :: PromotedDataCon   {{ com Promoted data constructor }}
-  | ' T          ::   :: PromotedTyCon     {{ com Promoted type constructor }}
+  | H            ::   :: PrimTyCon         {{ com \ctor{PrimTyCon}: Primitive tycon }}
+  | ' K          ::   :: PromotedDataCon   {{ com \ctor{PromotedDataCon}: Promoted data 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 (\texttt{intPrimTyCon}) }}
   | ( ~# )       ::   :: eqPrimTyCon            {{ com Unboxed equality (\texttt{eqPrimTyCon}) }}
-  | ( ~R# )      ::   :: eqReprPrimTyCon        {{ com Unboxed representational equality (\texttt{eqReprPrimTyCon}) }}
-  | BOX          ::   :: superKindTyCon         {{ com Sort of kinds (\texttt{superKindTyCon}) }}
+  | ( ~Rep# )      ::   :: eqReprPrimTyCon        {{ com Unboxed representational equality (\texttt{eqReprPrimTyCon}) }}
   | *            ::   :: 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}) }}
+  | TYPE         ::   :: TYPE                   {{ com TYPE (\texttt{tYPETyCon}) }}
+  | Levity       ::   :: Levity                 {{ com Levity (\texttt{LevityTyCon}) }}
+
+K :: 'DataCon_' ::= {{ com Data constructors, \coderef{basicTypes/DataCon.lhs}{DataCon} }}
+  | Lifted       ::   :: Lifted       {{ com \ctor{Lifted}, a lifted type }}
+  | Unlifted     ::   :: Unlifted     {{ com \ctor{Unlifted}, an unlifted type }}
 
 %% CONTEXTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -213,7 +235,9 @@ kinded_types {{ tex \overline{(\sigma_i : \kappa_i)}^i }} :: 'Kinded_Types_' ::=
 subst :: 'Subst_' ::= {{ com List of substitutions }}
   | [ n |-> t ]        ::   :: TyMapping
   | [ n |-> e ]        ::   :: TmMapping
+  | [ z |-> t ]        ::   :: TyMapping_Raw
   | </ substi // i />  ::   :: List
+  | empty              :: M :: Empty
 
 liftingsubst :: 'LiftSubst_' ::= {{ com List of lifting substitutions }}
   | [ n |-> g ]               ::   :: Mapping
@@ -231,12 +255,27 @@ ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
   | 1                           :: M :: one
   | 2                           :: M :: two
 
-type_list :: 'TypeList_' ::= {{ com List of types }}
-  | </ si // i />     ::   :: List
+types :: 'Types_' ::= {{ com List of types }}
+  | </ ti // i />      ::   :: List
+
+names {{ tex \overline{n_i}^i }} :: 'Names_' ::= {{ com List of names }}
+  | </ ni // , // i />      ::   :: List
+  | empty                   :: M :: Empty
+  | names , n               :: M :: Snoc
+
+namesroles {{ tex \overline{n_i \!\! {}_{\rho_i} }^i }} :: 'NamesRoles_' ::= {{ com List of names, annotated with roles }}
+  | </ ni RAi // , // i />    ::   :: List
+  | empty                     :: M :: Empty
+  | namesroles , n RA         :: M :: Snoc
+
+gs {{ tex \overline{\gamma} }} :: 'Cos_' ::= {{ com List of coercions }}
+  | </ gi // , // i />     ::   :: List
+  | empty                  :: M :: Empty
+  | gs , g                 :: M :: Snoc
 
-RA {{ tex {\!\!\!{}_{\rho} } }} :: 'RoleAnnot_' ::= {{ com Role annotation }}
+RA {{ tex {\!\!{}_{\rho} } }} :: 'RoleAnnot_' ::= {{ com Role annotation }}
   | _ R                    :: M :: annotation
-  {{ tex {\!\!\!{}_{[[R]]} } }}
+  {{ tex {\!\!{}_{[[R]]} } }}
   | _ ^^ R                 :: M :: spaced_annotation
   {{ tex {}_{[[R]]} }}
 
@@ -271,10 +310,9 @@ terminals :: 'terminals_' ::=
   | 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}_{\#} } }}
-  | ~R#          ::   :: eq_repr_hash     {{ tex \mathop{ {\sim}_{\mathsf{R}\#} } }}
+  | ~Rep#        ::   :: 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 } }}
@@ -291,21 +329,30 @@ terminals :: 'terminals_' ::=
   | literalType  ::   :: literalType      {{ tex \textsf{literalType} }}
   | |->          ::   :: mapsto           {{ tex \mapsto }}
   | <-           ::   :: assignment       {{ tex \leftarrow }}
-  | @            ::   :: marker           {{ tex  }}
+  | $            ::   :: 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} }}
+  | TYPE         ::   :: TYPE             {{ tex \textsf{TYPE} }}
+  | Levity       ::   :: Levity           {{ tex \textsf{Levity} }}
+  | Lifted       ::   :: Lifted           {{ tex \textsf{Lifted} }}
+  | Unlifted       ::   :: Unlifted           {{ tex \textsf{Unlifted} }}
   | no_conflict  ::   :: no_conflict      {{ tex \textsf{no\_conflict} }}
   | apart        ::   :: apart            {{ tex \textsf{apart} }}
+  | kind         ::   :: kind             {{ tex \textsf{kind} }}
+  | kapp         ::   :: kapp             {{ tex \textsf{kapp} }}
+  | sub          ::   :: sub              {{ tex \textsf{sub} }}
+  | #            ::   :: free             {{ tex \mathop{ \# } }}
+  | BOX          ::   :: BOX              {{ tex \square }}
+  | *            ::   :: star             {{ tex \star }}
   | unify        ::   :: unify            {{ tex \textsf{unify} }}
   | tyConRolesX  ::   :: tyConRolesX      {{ tex \textsf{tyConRolesX} }}
   | tyConRoles   ::   :: tyConRoles       {{ tex \textsf{tyConRoles} }}
@@ -318,6 +365,7 @@ terminals :: 'terminals_' ::=
   | coaxrProves  ::   :: coaxrProves      {{ tex \textsf{coaxrProves} }}
   | Just         ::   :: Just             {{ tex \textsf{Just} }}
   | \\           ::   :: newline          {{ tex \\ }}
+  | classifiesTypeWithValues :: :: ctwv   {{ tex \textsf{classifiesTypeWithValues} }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -341,11 +389,15 @@ formula :: 'formula_' ::=
   | compatibleUnBoxedTys t1 t2         ::   :: compatibleUnBoxedTys
   | formula1 /\ formula2               ::   :: and
   | formula1 \/ formula2               ::   :: or
+  | ( formula1 ) \\/ ( formula2 )      ::   :: newline
+    {{ tex \begin{array}{@{}l@{}%
+}[[formula1]] \vee \\ \multicolumn{1}{@{}r@{}%
+}{\quad [[formula2]]} \end{array} }}
   | ( 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
+  | </ Gi $ // i /> = inits ( </ nj // j /> ) :: :: context_folding
+  | </ substi $ // i /> = inits ( </ [ nj |-> tj ] // j /> ) :: :: subst_folding
   | ind1 = ind2                        ::   :: eq_ind
   | ind1 < ind2                        ::   :: lt
   | G |- tylit lit : k                 ::   :: lintTyLit
@@ -354,6 +406,9 @@ 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_type               ::   :: is_a_coercion_type
+    {{ tex \exists \tau_1, \tau_2, \kappa_1, \kappa_2 \text{ s.t.~} [[t]] =
+           \tau_1 \mathop{ {}^{\kappa_1} {\sim}_{\#}^{\kappa_2} } \tau_2 }}
   | e is_a_coercion                    ::   :: is_a_coercion
     {{ tex \exists \gamma \text{ s.t.~} [[e]] = \gamma }}
   | t is_a_prop                        ::   :: is_a_prop
@@ -378,7 +433,9 @@ formula :: 'formula_' ::=
   | t = coercionKind g                 ::   :: coercionKind
   | Just ( t1 , t2 ) = coaxrProves mu </ si // i /> </ ( s'j , s''j ) // j />
                                        ::   :: coaxrProves
-
+  | mu1 = mu2                          ::   :: mu_rewrite
+  | classifiesTypeWithValues k         ::   :: classifies_type_with_values
+  | z elt vars                         ::   :: in_vars
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Subrules and Parsing  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -390,13 +447,11 @@ 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_TyMapping <= Type_TySubstList
 Subst_TmMapping <= Type_TySubstList
@@ -409,4 +464,12 @@ Expr_Type <= formula_e_rewrite
 
 Coercion_TyConAppCo <= Coercion_AppCo
 
+Coercion_TyConAppCo <= Type_CoercionTy
+Coercion_CoVarCo <= Type_CoercionTy
+
+Type_unliftedEq left Var_IdOrTyVar
+
 Expr_Coercion <= Subst_TmMapping
+
+Type_CastTy <= Var_IdOrTyVar
+
diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile
index 402f9dbe4e..de0cac6e24 100644
--- a/docs/core-spec/Makefile
+++ b/docs/core-spec/Makefile
@@ -15,4 +15,4 @@ $(OTT_TEX): $(OTT_FILES)
 
 .PHONY: clean
 clean:
-	rm -f $(TARGET).pdf $(TARGET).tex $(OTT_TEX) *.aux *.fdb_latexmk *.log
+	rm -f $(TARGET).pdf $(TARGET).tex $(OTT_TEX) *.aux *.fdb_latexmk *.log *.fls
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index ed59e9538b..db8ce1cf5e 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -79,9 +79,9 @@ 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 />
+T </ taa // aa /> k'~#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 />
 
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 7830e890e1..0eec2eb38c 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -30,7 +30,7 @@ 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 23 April 2015
+\Large 23 October, 2015
 \end{center}
 
 \section{Introduction}
@@ -89,6 +89,8 @@ variables:
 \ottn
 }
 
+We sometimes omit the type/kind annotation to a variable when it is obvious from context.
+
 \subsection{Expressions}
 
 The datatype that represents expressions:
@@ -106,6 +108,9 @@ is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSy
 \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.
+\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}. 
 \end{itemize}
 
 Bindings for $[[let]]$ statements:
@@ -132,19 +137,37 @@ A program is just a list of bindings:
 
 \gram{\ottt}
 
+\ctor{ForAllTy}s are represented in two different ways, depending on whether
+the \ctor{ForAllTy} is anonymous (written $[[t1 -> t2]]$) or
+named (written $[[forall n . t]]$).
+
 There are some invariants on types:
 \begin{itemize}
+\item The name used in a type must be a type-level name (\ctor{TyVar}).
 \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}.
+The constructor for a saturated $[[(->)]]$ is \texttt{ForAllTy}.
 \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.
+\item A coercion used as a type should appear only in the right-hand side of
+  an application.
 \end{itemize}
 
+Note that the use of the $[[T </ ti // i />]]$ form and the $[[t1 -> t2]]$ form
+are purely representational. The metatheory would remain the same if these forms
+were removed in favor of $[[t1 t2]]$. Nevertheless, we keep all three forms in
+this documentation to accurately reflect the implementation.
+
+The \texttt{Named} variant of a \texttt{Binder} (the first argument to a
+\texttt{ForAllTy}) also tracks visibility of arguments. Visibility affects
+only source Haskell, and is omitted from this presentation.
+
+We use the notation $[[t1 k1~#k2 t2]]$ to stand for $[[(~#) k1 k2 t1 t2]]$.
+
 \subsection{Coercions}
 
 \gram{\ottg}
@@ -156,12 +179,22 @@ Invariants on coercions:
 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.
+\item Every non-reflexive coercion coerces between two distinct types.
+\item The name in a coercion must be a term-level name (\ctor{Id}).
+\item The contents of $[[<t>_R]]$ must not be a coercion. In other words,
+the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
 \end{itemize}
 
+The \texttt{UnivCo} constructor takes several arguments: the two types coerced
+between, a coercion relating these types' kinds, a role for the universal coercion,
+and a provenance. The provenance states what created the universal coercion:
+
+\gram{\ottprov}
+
 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}
+phantom equality includes all types. See \url{http://ghc.haskell.org/trac/ghc/wiki/Roles} and \url{http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/coercible.pdf}
 for more background.
 
 \gram{\ottR}
@@ -177,6 +210,9 @@ Axioms:
 \ottaxBranch
 }
 
+The left-hand sides $[[ </ tj // j /> ]]$ of different branches of one axiom must
+all have the same length.
+
 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
@@ -219,6 +255,21 @@ We include some representative primitive type constructors. There are many more
 
 \gram{\ottH}
 
+Note that although GHC contains distinct type constructors $[[*]]$
+and $[[Constraint]]$, this formalism treats only $[[*]]$. These two type
+constructors are considered wholly equivalent. In particular the function
+\texttt{eqType} returns \texttt{True} when comparing $[[*]]$ and $[[Constraint]]$.
+We need them both because they serve different functions in source Haskell.
+
+\paragraph{$[[TYPE]]$}
+The type system is rooted at the special constant $[[TYPE]]$ and the
+(quite normal) datatype \texttt{data Levity = Lifted | Unlifted}.
+The type of $[[TYPE]]$ is $[[Levity -> TYPE 'Lifted]]$. The idea is that
+$[[TYPE 'Lifted]]$ classifies lifted types and $[[TYPE 'Unlifted]]$
+classifies unlifted types. Indeed $[[*]]$ is just a plain old type
+synonym for $[[TYPE 'Lifted]]$, and $[[#]]$ is just a plain old type
+synonym for $[[TYPE 'Unlifted]]$.
+
 \section{Contexts}
 
 The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
@@ -275,19 +326,13 @@ as for strictness and exportability. See the source code for further information
 
 \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
+second premise ($[[</ G, G'i |-ty si : 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
@@ -318,17 +363,13 @@ a dead id and for one-tuples. These checks are omitted here.
 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
+returns five separate values (the two kinds, the two types, and the role), not
+a type with head $[[(~#)]]$ or $[[(~Rep#)]]$. 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]]$, and
 see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
 
@@ -342,7 +383,7 @@ There are two very similar checks for names, one declared as a local function:
 
 \subsection{Substitution consistency}
 
-\ottdefncheckTyKind{}
+\ottdefnlintTyKind{}
 
 \subsection{Case alternative consistency}
 
@@ -364,9 +405,9 @@ There are two very similar checks for names, one declared as a local function:
 
 \ottdefnlintXXapp{}
 
-\subsection{Sub-kinding}
+\subsection{Axiom argument kinding}
 
-\ottdefnisSubKind{}
+\ottdefncheckXXki{}
 
 \subsection{Roles}
 \label{sec:tyconroles}
@@ -462,7 +503,7 @@ algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
 \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
+extracts the two types (and their kinds) 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
@@ -472,6 +513,8 @@ groups: universally quantified types, existentially quantified types, and terms.
 \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.
+This operation is quite non-trivial. Please see \emph{System FC with Explicit
+Kind Equality} for details.
 \item Note that the types $[[ </ sbb // bb /> ]]$---the existentially quantified
 types---do not change during this step.
 \end{itemize}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 93242e9f72..ac548f63c1 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf