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.

2 files changed, 68 insertions, 1 deletions

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index e315b7573e..c3f456bcb6 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/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
diff --git a/compiler/coreSyn/CoreSyn.lhs b/compiler/coreSyn/CoreSyn.lhs
index 711c14895a..685975f982 100644
--- a/compiler/coreSyn/CoreSyn.lhs
+++ b/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]