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.

compiler/coreSyn/CoreLint.lhs

@@ -55,6 +55,18 @@ import MonadUtils
 import Data.Maybe
 \end{code}
 
+Note [GHC Formalism]
+~~~~~~~~~~~~~~~~~~~~
+This file implements the type-checking algorithm for System FC, the "official"
+name of the Core language. Type safety of FC is heart of the claim that
+executables produced by GHC do not have segmentation faults. Thus, it is
+useful to be able to reason about System FC independently of reading the code.
+To this purpose, there is a document ghc.pdf built in docs/core-spec that
+contains a formalism of the types and functions dealt with here. If you change
+just about anything in this file or you change other types/functions throughout
+the Core language (all signposted to this note), you should update that
+formalism. See docs/core-spec/README for more info about how to do so.
+
 %************************************************************************
 %*									*
 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
@@ -109,6 +121,8 @@ find an occurence of an Id, we fetch it from the in-scope set.
 \begin{code}
 lintCoreBindings :: CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
 --   Returns (warnings, errors)
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintCoreBindings binds
   = initL $ 
     addLoc TopLevelBindings $
@@ -135,6 +149,8 @@ lintCoreBindings binds
                   = compare (m1, nameOccName n1) (m2, nameOccName n2)
                   | otherwise = LT
 
+    -- If you edit this function, you may need to update the GHC formalism
+    -- See Note [GHC Formalism]
     lint_bind (Rec prs)		= mapM_ (lintSingleBinding TopLevel Recursive) prs
     lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
 \end{code}
@@ -173,6 +189,8 @@ Check a core binding, returning the list of variables bound.
 
 \begin{code}
 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
   = addLoc (RhsOf binder) $
          -- Check the rhs 
@@ -214,6 +232,9 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
     binder_ty                  = idType binder
     maybeDmdTy                 = idStrictness_maybe binder
     bndr_vars                  = varSetElems (idFreeVars binder)
+
+    -- If you edit this function, you may need to update the GHC formalism
+    -- See Note [GHC Formalism]
     lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
 	           | otherwise = return ()
 \end{code}
@@ -251,6 +272,8 @@ lintCoreExpr :: CoreExpr -> LintM OutType
 --
 -- The returned "type" can be a kind, if the expression is (Type ty)
 
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintCoreExpr (Var var)
   = do	{ checkL (not (var == oneTupleDataConId))
 		 (ptext (sLit "Illegal one-tuple"))
@@ -412,6 +435,8 @@ lintAltBinders :: OutType     -- Scrutinee type
 	       -> OutType     -- Constructor type
                -> [OutVar]    -- Binders
                -> LintM ()
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintAltBinders scrut_ty con_ty [] 
   = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty) 
 lintAltBinders scrut_ty con_ty (bndr:bndrs)
@@ -449,6 +474,9 @@ lintValApp arg fun_ty arg_ty
 \begin{code}
 checkTyKind :: OutTyVar -> OutType -> LintM ()
 -- Both args have had substitution applied
+
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 checkTyKind tyvar arg_ty
   | isSuperKind tyvar_kind  -- kind forall
   = lintKind arg_ty
@@ -522,7 +550,8 @@ lintCoreAlt :: OutType 		-- Type of scrutinee
             -> OutType          -- Type of the alternative
 	    -> CoreAlt
 	    -> LintM ()
-
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
   do { checkL (null args) (mkDefaultArgsMsg args)
      ; checkAltExpr rhs alt_ty }
@@ -574,6 +603,8 @@ lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 				 lintBinders vars $ \ vars' ->
 				 linterF (var':vars')
 
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 lintBinder var linterF
   | isId var  = lintIdBndr var linterF
@@ -640,6 +671,9 @@ lintTyBndrKind tv = lintKind (tyVarKind tv)
 -------------------
 lintType :: OutType -> LintM LintedKind
 -- The returned Kind has itself been linted
+
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintType (TyVarTy tv)
   = do { checkTyCoVarInScope tv
        ; return (tyVarKind tv) }
@@ -675,6 +709,8 @@ lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
 
 \begin{code}
 lintKind :: OutKind -> LintM ()
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintKind k = do { sk <- lintType k 
                 ; unless (isSuperKind sk) 
                          (addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
@@ -684,6 +720,8 @@ lintKind k = do { sk <- lintType k
 
 \begin{code}
 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintArrow what k1 k2   -- Eg lintArrow "type or kind `blah'" k1 k2
                        -- or lintarrow "coercion `blah'" k1 k2
   | isSuperKind k1 
@@ -720,6 +758,9 @@ lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
 --    We have an application (f arg_ty1 .. arg_tyn),
 --    where f :: fun_kind
 -- Takes care of linting the OutTypes
+
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lint_app doc kfn kas
     = foldlM go_app kfn kas
   where
@@ -762,6 +803,9 @@ lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType)
 -- Check the kind of a coercion term, returning the kind
 -- Post-condition: the returned OutTypes are lint-free
 --                 and have the same kind as each other
+
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 lintCoercion (Refl ty)
   = do { k <- lintType ty
        ; return (k, ty, ty) }
@@ -901,6 +945,9 @@ lintCoercion co@(AxiomInstCo (CoAxiom { co_ax_tvs = ktvs
 %************************************************************************
 
 \begin{code}
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism]
 newtype LintM a = 
    LintM { unLintM :: 
             [LintLocInfo] ->         -- Locations

compiler/coreSyn/CoreSyn.lhs

@@ -261,6 +261,9 @@ These data types are the heart of the compiler
 -- *  A type: this should only show up at the top level of an Arg
 --
 -- *  A coercion
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data Expr b
   = Var	  Id
   | Lit   Literal
@@ -281,9 +284,15 @@ type Arg b = Expr b
 -- | A case split alternative. Consists of the constructor leading to the alternative,
 -- the variables bound from the constructor, and the expression to be executed given that binding.
 -- The default alternative is @(DEFAULT, [], rhs)@
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 type Alt b = (AltCon, [b], Expr b)
 
 -- | A case alternative constructor (i.e. pattern match)
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data AltCon 
   = DataAlt DataCon   --  ^ A plain data constructor: @case e of { Foo x -> ... }@.
                       -- Invariant: the 'DataCon' is always from a @data@ type, and never from a @newtype@
@@ -296,6 +305,9 @@ data AltCon
    deriving (Eq, Ord, Data, Typeable)
 
 -- | Binding, used for top level bindings in a module and local bindings in a @let@.
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data Bind b = NonRec b (Expr b)
 	    | Rec [(b, (Expr b))]
   deriving (Data, Typeable)
@@ -423,6 +435,9 @@ unboxed type.
 
 \begin{code}
 -- | Allows attaching extra information to points in expressions
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data Tickish id =
     -- | An @{-# SCC #-}@ profiling annotation, either automatically
     -- added by the desugarer as a result of -auto-all, or added by
@@ -1049,6 +1064,9 @@ a list of CoreBind
    chunks.  
 
 \begin{code}
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 type CoreProgram = [CoreBind]	-- See Note [CoreProgram]
 
 -- | The common case for the type of binders and variables when
@@ -1213,6 +1231,8 @@ varsToCoreExprs vs = map varToCoreExpr vs
 \begin{code}
 -- | Extract every variable by this group
 bindersOf  :: Bind b -> [b]
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 bindersOf (NonRec binder _) = [binder]
 bindersOf (Rec pairs)       = [binder | (binder, _) <- pairs]
 

compiler/prelude/TysPrim.lhs

@@ -311,6 +311,8 @@ constraintKindTyCon   = mkKindTyCon constraintKindTyConName   superKind
 --------------------------
 -- ... and now their names
 
+-- If you edit these, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 superKindTyConName      = mkPrimTyConName (fsLit "BOX") superKindTyConKey superKindTyCon
 anyKindTyConName          = mkPrimTyConName (fsLit "AnyK") anyKindTyConKey anyKindTyCon
 liftedTypeKindTyConName   = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon

compiler/types/Coercion.lhs

@@ -114,6 +114,8 @@ import qualified Data.Data as Data hiding ( TyCon )
 -- | A 'Coercion' is concrete evidence of the equality/convertibility
 -- of two types.
 
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data Coercion 
   -- These ones mirror the shape of types
   = Refl Type  -- See Note [Refl invariant]
@@ -154,6 +156,8 @@ data Coercion
   | InstCo Coercion Type
   deriving (Data.Data, Data.Typeable)
 
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data LeftOrRight = CLeft | CRight 
                  deriving( Eq, Data.Data, Data.Typeable )
 

compiler/types/Kind.lhs

@@ -217,6 +217,8 @@ isSubKind :: Kind -> Kind -> Bool
 -- Sub-kinding is extremely simple and does not look
 -- under arrrows or type constructors
 
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
   | isPromotedTyCon kc1 || isPromotedTyCon kc2
     -- handles promoted kinds (List *, Nat, etc.)
@@ -230,6 +232,9 @@ isSubKind k1 k2 = eqKind k1 k2
 
 isSubKindCon :: TyCon -> TyCon -> Bool
 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
+
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 isSubKindCon kc1 kc2
   | kc1 == kc2              = True
   | isOpenTypeKindCon kc2   = isSubOpenTypeKindCon kc1 

compiler/types/TyCon.lhs

@@ -282,6 +282,9 @@ This is important. In an instance declaration we expect
 --
 -- This data type also encodes a number of primitive, built in type constructors such as those
 -- for function and tuple types.
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data TyCon
   = -- | The function type constructor, @(->)@
     FunTyCon {
@@ -708,6 +711,9 @@ so the coercion tycon CoT must have
 
 \begin{code}
 -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data CoAxiom
   = CoAxiom                   -- Type equality axiom.
     { co_ax_unique   :: Unique      -- unique identifier

compiler/types/Type.lhs

@@ -805,6 +805,8 @@ applyTys :: Type -> [KindOrType] -> Type
 -- This term should have type (Int -> Int), but notice that
 -- there are more type args than foralls in 'undefined's type.
 
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 applyTys ty args = applyTysD empty ty args
 
 applyTysD :: SDoc -> Type -> [Type] -> Type	-- Debug version

compiler/types/TypeRep.lhs

@@ -87,6 +87,9 @@ import qualified Data.Data        as Data hiding ( TyCon )
 
 \begin{code}
 -- | The key representation of types within the compiler
+
+-- If you edit this type, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
 data Type
   = TyVarTy Var	-- ^ Vanilla type or kind variable (*never* a coercion variable)
 

docs/core-spec/.gitignore

+*.aux
+*.log
+*.fdb_latexmk
+CoreOtt.tex
+core-spec.tex

docs/core-spec/CoreLint.ott

+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%  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