cmmTopCodeGen no longer takes DynFlags as an argument
[ghc-hetmet.git] / compiler / coreSyn / CoreSyn.lhs
index ac32bc2..e754c6d 100644 (file)
@@ -3,46 +3,80 @@
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 
-CoreSyn: A data type for the Haskell compiler midsection
-
 \begin{code}
+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor #-}
+
+-- | CoreSyn holds all the main data types for use by for the Glasgow Haskell Compiler midsection
 module CoreSyn (
+       -- * Main data types
        Expr(..), Alt, Bind(..), AltCon(..), Arg, Note(..),
        CoreExpr, CoreAlt, CoreBind, CoreArg, CoreBndr,
        TaggedExpr, TaggedAlt, TaggedBind, TaggedArg, TaggedBndr(..),
 
-       mkLets, mkLams, 
-       mkApps, mkTyApps, mkValApps, mkVarApps,
-       mkLit, mkIntLitInt, mkIntLit, 
-       mkConApp, mkCast,
+        -- ** 'Expr' construction
+       mkLets, mkLams,
+       mkApps, mkTyApps, mkCoApps, mkVarApps,
+       
+       mkIntLit, mkIntLitInt,
+       mkWordLit, mkWordLitWord,
+       mkCharLit, mkStringLit,
+       mkFloatLit, mkFloatLitFloat,
+       mkDoubleLit, mkDoubleLitDouble,
+       
+       mkConApp, mkTyBind, mkCoBind,
        varToCoreExpr, varsToCoreExprs,
 
-       isTyVar, isId, cmpAltCon, cmpAlt, ltAlt,
+        isId, cmpAltCon, cmpAlt, ltAlt,
+       
+       -- ** Simple 'Expr' access functions and predicates
        bindersOf, bindersOfBinds, rhssOfBind, rhssOfAlts, 
        collectBinders, collectTyBinders, collectValBinders, collectTyAndValBinders,
-       collectArgs, coreExprCc,
-       mkTyBind, flattenBinds, 
+       collectArgs, coreExprCc, flattenBinds, 
 
-       isValArg, isTypeArg, valArgCount, valBndrCount, isRuntimeArg, isRuntimeVar,
+        isValArg, isTypeArg, isTyCoArg, valArgCount, valBndrCount,
+        isRuntimeArg, isRuntimeVar,
+        notSccNote,
 
-       -- Unfoldings
-       Unfolding(..),  UnfoldingGuidance(..),  -- Both abstract everywhere but in CoreUnfold.lhs
-       noUnfolding, evaldUnfolding, mkOtherCon,
-       unfoldingTemplate, maybeUnfoldingTemplate, otherCons, 
-       isValueUnfolding, isEvaldUnfolding, isCheapUnfolding, isCompulsoryUnfolding,
-       hasUnfolding, hasSomeUnfolding, neverUnfold,
+       -- * Unfolding data types
+        Unfolding(..),  UnfoldingGuidance(..), UnfoldingSource(..),
+        DFunArg(..), dfunArgExprs,
 
-       -- Seq stuff
+       -- ** Constructing 'Unfolding's
+       noUnfolding, evaldUnfolding, mkOtherCon,
+        unSaturatedOk, needSaturated, boringCxtOk, boringCxtNotOk,
+       
+       -- ** Predicates and deconstruction on 'Unfolding'
+       unfoldingTemplate, setUnfoldingTemplate, expandUnfolding_maybe,
+       maybeUnfoldingTemplate, otherCons, unfoldingArity,
+       isValueUnfolding, isEvaldUnfolding, isCheapUnfolding,
+        isExpandableUnfolding, isConLikeUnfolding, isCompulsoryUnfolding,
+        isStableUnfolding, isStableCoreUnfolding_maybe,
+        isClosedUnfolding, hasSomeUnfolding, 
+       canUnfold, neverUnfoldGuidance, isStableSource,
+
+       -- * Strictness
        seqExpr, seqExprs, seqUnfolding, 
 
-       -- Annotated expressions
-       AnnExpr, AnnExpr'(..), AnnBind(..), AnnAlt, 
+       -- * Annotated expression data types
+       AnnExpr, AnnExpr'(..), AnnBind(..), AnnAlt,
+       
+        -- ** Operations on annotated expressions
+        collectAnnArgs,
+
+       -- ** Operations on annotations
        deAnnotate, deAnnotate', deAnnAlt, collectAnnBndrs,
 
-       -- Core rules
+       -- * Core rule data types
        CoreRule(..),   -- CoreSubst, CoreTidy, CoreFVs, PprCore only
-       RuleName, seqRules, ruleArity,
-       isBuiltinRule, ruleName, isLocalRule, ruleIdName
+       RuleName, IdUnfoldingFun,
+       
+       -- ** Operations on 'CoreRule's 
+       seqRules, ruleArity, ruleName, ruleIdName, ruleActivation,
+       setRuleIdName,
+       isBuiltinRule, isLocalRule,
+
+       -- * Core vectorisation declarations data type
+       CoreVect(..)
     ) where
 
 #include "HsVersions.h"
@@ -59,7 +93,10 @@ import FastString
 import Outputable
 import Util
 
-infixl 4 `mkApps`, `mkValApps`, `mkTyApps`, `mkVarApps`
+import Data.Data
+import Data.Word
+
+infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`, `App`, `mkCoApps`
 -- Left associative, so that we can say (f `mkTyApps` xs `mkVarApps` ys)
 \end{code}
 
@@ -72,81 +109,182 @@ infixl 4 `mkApps`, `mkValApps`, `mkTyApps`, `mkVarApps`
 These data types are the heart of the compiler
 
 \begin{code}
-infixl 8 `App` -- App brackets to the left
-
-data Expr b    -- "b" for the type of binders, 
-  = Var          Id
-  | Lit   Literal
-  | App   (Expr b) (Arg b)             -- See Note [CoreSyn let/app invariant]
-  | Lam   b (Expr b)
-  | Let   (Bind b) (Expr b)            -- See [CoreSyn let/app invariant],
-                                       -- and [CoreSyn letrec invariant]
-  | Case  (Expr b) b Type [Alt b]      -- Binder gets bound to value of scrutinee
-                                       -- See Note [CoreSyn case invariants]
-  | Cast  (Expr b) Coercion
-  | Note  Note (Expr b)
-  | Type  Type                 -- This should only show up at the top
-                               -- level of an Arg
-
-type Arg b = Expr b            -- Can be a Type
-
-type Alt b = (AltCon, [b], Expr b)     -- (DEFAULT, [], rhs) is the default alternative
-
-data AltCon = DataAlt DataCon  -- Invariant: the DataCon is always from 
-                               -- a *data* type, and never from a *newtype*
-           | LitAlt  Literal
-           | DEFAULT
-        deriving (Eq, Ord)
-
-
+-- | This is the data type that represents GHCs core intermediate language. Currently
+-- GHC uses System FC <http://research.microsoft.com/~simonpj/papers/ext-f/> for this purpose,
+-- which is closely related to the simpler and better known System F <http://en.wikipedia.org/wiki/System_F>.
+--
+-- We get from Haskell source to this Core language in a number of stages:
+--
+-- 1. The source code is parsed into an abstract syntax tree, which is represented
+--    by the data type 'HsExpr.HsExpr' with the names being 'RdrName.RdrNames'
+--
+-- 2. This syntax tree is /renamed/, which attaches a 'Unique.Unique' to every 'RdrName.RdrName'
+--    (yielding a 'Name.Name') to disambiguate identifiers which are lexically identical. 
+--    For example, this program:
+--
+-- @
+--      f x = let f x = x + 1
+--            in f (x - 2)
+-- @
+--
+--    Would be renamed by having 'Unique's attached so it looked something like this:
+--
+-- @
+--      f_1 x_2 = let f_3 x_4 = x_4 + 1
+--                in f_3 (x_2 - 2)
+-- @
+--
+-- 3. The resulting syntax tree undergoes type checking (which also deals with instantiating
+--    type class arguments) to yield a 'HsExpr.HsExpr' type that has 'Id.Id' as it's names.
+--
+-- 4. Finally the syntax tree is /desugared/ from the expressive 'HsExpr.HsExpr' type into
+--    this 'Expr' type, which has far fewer constructors and hence is easier to perform
+--    optimization, analysis and code generation on.
+--
+-- The type parameter @b@ is for the type of binders in the expression tree.
+data Expr b
+  = Var          Id                            -- ^ Variables
+
+  | Lit   Literal                       -- ^ Primitive literals
+
+  | App   (Expr b) (Arg b)             -- ^ Applications: note that the argument may be a 'Type'.
+                                        --
+                                        -- See "CoreSyn#let_app_invariant" for another invariant
+
+  | Lam   b (Expr b)                    -- ^ Lambda abstraction
+
+  | Let   (Bind b) (Expr b)            -- ^ Recursive and non recursive @let@s. Operationally
+                                        -- this corresponds to allocating a thunk for the things
+                                        -- bound and then executing the sub-expression.
+                                        -- 
+                                        -- #top_level_invariant#
+                                        -- #letrec_invariant#
+                                        --
+                                        -- The right hand sides of all top-level and recursive @let@s
+                                        -- /must/ be of lifted type (see "Type#type_classification" for
+                                        -- the meaning of /lifted/ vs. /unlifted/).
+                                        --
+                                        -- #let_app_invariant#
+                                        -- The right hand side of of a non-recursive 'Let' 
+                                        -- _and_ the argument of an 'App',
+                                        -- /may/ be of unlifted type, but only if the expression 
+                                        -- is ok-for-speculation.  This means that the let can be floated 
+                                        -- around without difficulty. For example, this is OK:
+                                        --
+                                       -- > y::Int# = x +# 1#
+                                       --
+                                       -- But this is not, as it may affect termination if the 
+                                        -- expression is floated out:
+                                       --
+                                       -- > y::Int# = fac 4#
+                                       --
+                                       -- In this situation you should use @case@ rather than a @let@. The function
+                                       -- 'CoreUtils.needsCaseBinding' can help you determine which to generate, or
+                                       -- alternatively use 'MkCore.mkCoreLet' rather than this constructor directly,
+                                       -- which will generate a @case@ if necessary
+                                       --
+                                       -- #type_let#
+                                       -- We allow a /non-recursive/ let to bind a type variable, thus:
+                                       --
+                                       -- > Let (NonRec tv (Type ty)) body
+                                       --
+                                       -- This can be very convenient for postponing type substitutions until
+                                        -- the next run of the simplifier.
+                                        --
+                                        -- At the moment, the rest of the compiler only deals with type-let
+                                        -- in a Let expression, rather than at top level.  We may want to revist
+                                        -- this choice.
+
+  | Case  (Expr b) b Type [Alt b]      -- ^ Case split. Operationally this corresponds to evaluating
+                                        -- the scrutinee (expression examined) to weak head normal form
+                                        -- and then examining at most one level of resulting constructor (i.e. you
+                                        -- cannot do nested pattern matching directly with this).
+                                        --
+                                        -- The binder gets bound to the value of the scrutinee,
+                                        -- and the 'Type' must be that of all the case alternatives
+                                       --
+                                       -- #case_invariants#
+                                       -- This is one of the more complicated elements of the Core language, 
+                                       -- and comes with a number of restrictions:
+                                       --
+                                       -- The 'DEFAULT' case alternative must be first in the list, 
+                                        -- if it occurs at all.
+                                       --
+                                       -- The remaining cases are in order of increasing 
+                                       --      tag     (for 'DataAlts') or
+                                       --      lit     (for 'LitAlts').
+                                       -- This makes finding the relevant constructor easy, 
+                                        -- and makes comparison easier too.
+                                       --
+                                       -- The list of alternatives must be exhaustive. An /exhaustive/ case 
+                                       -- does not necessarily mention all constructors:
+                                       --
+                                       -- @
+                                        --      data Foo = Red | Green | Blue
+                                        -- ... case x of 
+                                        --      Red   -> True
+                                        --      other -> f (case x of 
+                                        --                      Green -> ...
+                                        --                      Blue  -> ... ) ...
+                                        -- @
+                                        --
+                                        -- The inner case does not need a @Red@ alternative, because @x@ 
+                                        -- can't be @Red@ at that program point.
+
+  | Cast  (Expr b) Coercion             -- ^ Cast an expression to a particular type. 
+                                        -- This is used to implement @newtype@s (a @newtype@ constructor or 
+                                        -- destructor just becomes a 'Cast' in Core) and GADTs.
+
+  | Note  Note (Expr b)                 -- ^ Notes. These allow general information to be
+                                        -- added to expressions in the syntax tree
+
+  | Type  Type                         -- ^ A type: this should only show up at the top
+                                        -- level of an Arg
+    
+  | Coercion Coercion                   -- ^ A coercion
+  deriving (Data, Typeable)
+
+-- | Type synonym for expressions that occur in function argument positions.
+-- Only 'Arg' should contain a 'Type' at top level, general 'Expr' should not
+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)@
+type Alt b = (AltCon, [b], Expr b)
+
+-- | A case alternative constructor (i.e. pattern match)
+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@
+           | LitAlt  Literal   -- ^ A literal: @case e of { 1 -> ... }@
+           | DEFAULT           -- ^ Trivial alternative: @case e of { _ -> ... }@
+        deriving (Eq, Ord, Data, Typeable)
+
+-- | Binding, used for top level bindings in a module and local bindings in a @let@.
 data Bind b = NonRec b (Expr b)
-             | Rec [(b, (Expr b))]
+           | Rec [(b, (Expr b))]
+  deriving (Data, Typeable)
 \end{code}
 
 -------------------------- CoreSyn INVARIANTS ---------------------------
 
 Note [CoreSyn top-level invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* The RHSs of all top-level lets must be of LIFTED type.
+See #toplevel_invariant#
 
 Note [CoreSyn letrec invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* The RHS of a letrec must be of LIFTED type.
+See #letrec_invariant#
 
 Note [CoreSyn let/app invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* The RHS of a non-recursive let, *and* the argument of an App,
-  may be of UNLIFTED type, but only if the expression 
-  is ok-for-speculation.  This means that the let can be floated around 
-  without difficulty.  e.g.
-       y::Int# = x +# 1#       ok
-       y::Int# = fac 4#        not ok [use case instead]
-This is intially enforced by DsUtils.mkDsLet and mkDsApp
+See #let_app_invariant#
+
+This is intially enforced by DsUtils.mkCoreLet and mkCoreApp
 
 Note [CoreSyn case invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Invariant: The DEFAULT case must be *first*, if it occurs at all
-
-Invariant: The remaining cases are in order of increasing 
-               tag     (for DataAlts)
-               lit     (for LitAlts)
-           This makes finding the relevant constructor easy,
-           and makes comparison easier too
-
-Invariant: The list of alternatives is ALWAYS EXHAUSTIVE,
-          meaning that it covers all cases that can occur
-
-    An "exhaustive" case does not necessarily mention all constructors:
-       data Foo = Red | Green | Blue
-
-       ...case x of 
-               Red   -> True
-               other -> f (case x of 
-                               Green -> ...
-                               Blue  -> ... )
-    The inner case does not need a Red alternative, because x can't be Red at
-    that program point.
-
+See #case_invariants#
 
 Note [CoreSyn let goal]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -157,33 +295,15 @@ Note [CoreSyn let goal]
 
 Note [Type let]
 ~~~~~~~~~~~~~~~
-We allow a *non-recursive* let to bind a type variable, thus
-       Let (NonRec tv (Type ty)) body
-This can be very convenient for postponing type substitutions until
-the next run of the simplifier.
-
-At the moment, the rest of the compiler only deals with type-let
-in a Let expression, rather than at top level.  We may want to revist
-this choice.
+See #type_let#
 
 \begin{code}
+
+-- | Allows attaching extra information to points in expressions rather than e.g. identifiers.
 data Note
-  = SCC CostCentre
-
-  | InlineMe           -- Instructs simplifer to treat the enclosed expression
-                       -- as very small, and inline it at its call sites
-
-  | CoreNote String     -- A generic core annotation, propagated but not used by GHC
-
--- NOTE: we also treat expressions wrapped in InlineMe as
--- 'cheap' and 'dupable' (in the sense of exprIsCheap, exprIsDupable)
--- What this means is that we obediently inline even things that don't
--- look like valuse.  This is sometimes important:
---     {-# INLINE f #-}
---     f = g . h
--- Here, f looks like a redex, and we aren't going to inline (.) because it's
--- inside an INLINE, so it'll stay looking like a redex.  Nevertheless, we 
--- should inline f even inside lambdas.  In effect, we should trust the programmer.
+  = SCC CostCentre      -- ^ A cost centre annotation for profiling
+  | CoreNote String     -- ^ A generic core annotation, propagated but not used by GHC
+  deriving (Data, Typeable)
 \end{code}
 
 
@@ -196,60 +316,73 @@ data Note
 The CoreRule type and its friends are dealt with mainly in CoreRules,
 but CoreFVs, Subst, PprCore, CoreTidy also inspect the representation.
 
-A Rule is 
-
-  "local"  if the function it is a rule for is defined in the
-          same module as the rule itself.
-
-  "orphan" if nothing on the LHS is defined in the same module
-          as the rule itself
-
 \begin{code}
-type RuleName = FastString
-
+-- | A 'CoreRule' is:
+--
+-- * \"Local\" if the function it is a rule for is defined in the
+--   same module as the rule itself.
+--
+-- * \"Orphan\" if nothing on the LHS is defined in the same module
+--   as the rule itself
 data CoreRule
   = Rule { 
-       ru_name :: RuleName,
-       ru_act  :: Activation,  -- When the rule is active
-       
+       ru_name :: RuleName,            -- ^ Name of the rule, for communication with the user
+       ru_act  :: Activation,          -- ^ When the rule is active
+
        -- Rough-matching stuff
        -- see comments with InstEnv.Instance( is_cls, is_rough )
-       ru_fn    :: Name,       -- Name of the Id at the head of this rule
-       ru_rough :: [Maybe Name],       -- Name at the head of each argument
+       ru_fn    :: Name,               -- ^ Name of the 'Id.Id' at the head of this rule
+       ru_rough :: [Maybe Name],       -- ^ Name at the head of each argument to the left hand side
        
        -- Proper-matching stuff
        -- see comments with InstEnv.Instance( is_tvs, is_tys )
-       ru_bndrs :: [CoreBndr], -- Forall'd variables
-       ru_args  :: [CoreExpr], -- LHS args
+       ru_bndrs :: [CoreBndr],         -- ^ Variables quantified over
+       ru_args  :: [CoreExpr],         -- ^ Left hand side arguments
        
        -- And the right-hand side
-       ru_rhs   :: CoreExpr,
+       ru_rhs   :: CoreExpr,           -- ^ Right hand side of the rule
+                                       -- Occurrence info is guaranteed correct
+                                       -- See Note [OccInfo in unfoldings and rules]
 
        -- Locality
-       ru_local :: Bool        -- The fn at the head of the rule is
+        ru_auto :: Bool,       -- ^ @True@  <=> this rule is auto-generated
+                               --   @False@ <=> generated at the users behest
+                               --   Main effect: reporting of orphan-hood
+
+       ru_local :: Bool        -- ^ @True@ iff the fn at the head of the rule is
                                -- defined in the same module as the rule
-                               -- and is not an implicit Id (like a record sel
-                               -- class op, or data con)
+                               -- and is not an implicit 'Id' (like a record selector,
+                               -- class operation, or data constructor)
+
                -- NB: ru_local is *not* used to decide orphan-hood
                --      c.g. MkIface.coreRuleToIfaceRule
     }
 
-  | BuiltinRule {              -- Built-in rules are used for constant folding
-       ru_name :: RuleName,    -- and suchlike.  It has no free variables.
-       ru_fn :: Name,          -- Name of the Id at 
-                               -- the head of this rule
-       ru_nargs :: Int,        -- Number of args that ru_try expects,
-                               -- including type args
-       ru_try  :: [CoreExpr] -> Maybe CoreExpr }
-               -- This function does the rewrite.  It given too many
-               -- arguments, it simply discards them; the returned CoreExpr
-               -- is just the rewrite of ru_fn applied to the first ru_nargs args
+  -- | Built-in rules are used for constant folding
+  -- and suchlike.  They have no free variables.
+  | BuiltinRule {               
+       ru_name  :: RuleName,   -- ^ As above
+       ru_fn    :: Name,       -- ^ As above
+       ru_nargs :: Int,        -- ^ Number of arguments that 'ru_try' consumes,
+                               -- if it fires, including type arguments
+       ru_try  :: IdUnfoldingFun -> [CoreExpr] -> Maybe CoreExpr
+               -- ^ This function does the rewrite.  It given too many
+               -- arguments, it simply discards them; the returned 'CoreExpr'
+               -- is just the rewrite of 'ru_fn' applied to the first 'ru_nargs' args
+    }
                -- See Note [Extra args in rule matching] in Rules.lhs
 
+type IdUnfoldingFun = Id -> Unfolding
+-- A function that embodies how to unfold an Id if you need
+-- to do that in the Rule.  The reason we need to pass this info in
+-- is that whether an Id is unfoldable depends on the simplifier phase
+
 isBuiltinRule :: CoreRule -> Bool
 isBuiltinRule (BuiltinRule {}) = True
 isBuiltinRule _                       = False
 
+-- | The number of arguments the 'ru_fn' must be applied 
+-- to before the rule can match on it
 ruleArity :: CoreRule -> Int
 ruleArity (BuiltinRule {ru_nargs = n}) = n
 ruleArity (Rule {ru_args = args})      = length args
@@ -257,11 +390,34 @@ ruleArity (Rule {ru_args = args})      = length args
 ruleName :: CoreRule -> RuleName
 ruleName = ru_name
 
+ruleActivation :: CoreRule -> Activation
+ruleActivation (BuiltinRule { })       = AlwaysActive
+ruleActivation (Rule { ru_act = act }) = act
+
+-- | The 'Name' of the 'Id.Id' at the head of the rule left hand side
 ruleIdName :: CoreRule -> Name
 ruleIdName = ru_fn
 
 isLocalRule :: CoreRule -> Bool
 isLocalRule = ru_local
+
+-- | Set the 'Name' of the 'Id.Id' at the head of the rule left hand side
+setRuleIdName :: Name -> CoreRule -> CoreRule
+setRuleIdName nm ru = ru { ru_fn = nm }
+\end{code}
+
+
+%************************************************************************
+%*                                                                      *
+\subsection{Vectorisation declarations}
+%*                                                                      *
+%************************************************************************
+
+Representation of desugared vectorisation declarations that are fed to the vectoriser (via
+'ModGuts').
+
+\begin{code}
+data CoreVect = Vect Id (Maybe CoreExpr)
 \end{code}
 
 
@@ -271,51 +427,197 @@ isLocalRule = ru_local
 %*                                                                     *
 %************************************************************************
 
-The @Unfolding@ type is declared here to avoid numerous loops, but it
-should be abstract everywhere except in CoreUnfold.lhs
+The @Unfolding@ type is declared here to avoid numerous loops
 
 \begin{code}
+-- | Records the /unfolding/ of an identifier, which is approximately the form the
+-- identifier would have if we substituted its definition in for the identifier.
+-- This type should be treated as abstract everywhere except in "CoreUnfold"
 data Unfolding
-  = NoUnfolding
-
-  | OtherCon [AltCon]          -- It ain't one of these
-                               -- (OtherCon xs) also indicates that something has been evaluated
-                               -- and hence there's no point in re-evaluating it.
-                               -- OtherCon [] is used even for non-data-type values
-                               -- to indicated evaluated-ness.  Notably:
-                               --      data C = C !(Int -> Int)
-                               --      case x of { C f -> ... }
-                               -- Here, f gets an OtherCon [] unfolding.
-
-  | CompulsoryUnfolding CoreExpr       -- There is no "original" definition,
-                                       -- so you'd better unfold.
-
-  | CoreUnfolding                      -- An unfolding with redundant cached information
-               CoreExpr                -- Template; binder-info is correct
-               Bool                    -- True <=> top level binding
-               Bool                    -- exprIsHNF template (cached); it is ok to discard a `seq` on
-                                       --      this variable
-               Bool                    -- True <=> doesn't waste (much) work to expand inside an inlining
-                                       --      Basically it's exprIsCheap
-               UnfoldingGuidance       -- Tells about the *size* of the template.
+  = NoUnfolding        -- ^ We have no information about the unfolding
+
+  | OtherCon [AltCon]  -- ^ It ain't one of these constructors.
+                      -- @OtherCon xs@ also indicates that something has been evaluated
+                      -- and hence there's no point in re-evaluating it.
+                      -- @OtherCon []@ is used even for non-data-type values
+                      -- to indicated evaluated-ness.  Notably:
+                      --
+                      -- > data C = C !(Int -> Int)
+                      -- > case x of { C f -> ... }
+                      --
+                      -- Here, @f@ gets an @OtherCon []@ unfolding.
+
+  | DFunUnfolding       -- The Unfolding of a DFunId  
+                       -- See Note [DFun unfoldings]
+                       --     df = /\a1..am. \d1..dn. MkD (op1 a1..am d1..dn)
+                       --                                 (op2 a1..am d1..dn)
+
+        Arity          -- Arity = m+n, the *total* number of args 
+                       --   (unusually, both type and value) to the dfun
+
+        DataCon        -- The dictionary data constructor (possibly a newtype datacon)
+
+        [DFunArg CoreExpr]  -- Specification of superclasses and methods, in positional order
+
+  | CoreUnfolding {            -- An unfolding for an Id with no pragma, 
+                                -- or perhaps a NOINLINE pragma
+                               -- (For NOINLINE, the phase, if any, is in the 
+                                -- InlinePragInfo for this Id.)
+       uf_tmpl       :: CoreExpr,        -- Template; occurrence info is correct
+       uf_src        :: UnfoldingSource, -- Where the unfolding came from
+       uf_is_top     :: Bool,          -- True <=> top level binding
+       uf_arity      :: Arity,         -- Number of value arguments expected
+       uf_is_value   :: Bool,          -- exprIsHNF template (cached); it is ok to discard 
+                                       --      a `seq` on this variable
+        uf_is_conlike :: Bool,          -- True <=> applicn of constructor or CONLIKE function
+                                        --      Cached version of exprIsConLike
+       uf_is_cheap   :: Bool,          -- True <=> doesn't waste (much) work to expand 
+                                        --          inside an inlining
+                                       --      Cached version of exprIsCheap
+       uf_expandable :: Bool,          -- True <=> can expand in RULE matching
+                                       --      Cached version of exprIsExpandable
+       uf_guidance   :: UnfoldingGuidance      -- Tells about the *size* of the template.
+    }
+  -- ^ An unfolding with redundant cached information. Parameters:
+  --
+  --  uf_tmpl: Template used to perform unfolding; 
+  --           NB: Occurrence info is guaranteed correct: 
+  --              see Note [OccInfo in unfoldings and rules]
+  --
+  --  uf_is_top: Is this a top level binding?
+  --
+  --  uf_is_value: 'exprIsHNF' template (cached); it is ok to discard a 'seq' on
+  --     this variable
+  --
+  --  uf_is_cheap:  Does this waste only a little work if we expand it inside an inlining?
+  --     Basically this is a cached version of 'exprIsCheap'
+  --
+  --  uf_guidance:  Tells us about the /size/ of the unfolding template
+
+------------------------------------------------
+data DFunArg e   -- Given (df a b d1 d2 d3)
+  = DFunPolyArg  e      -- Arg is (e a b d1 d2 d3)
+  | DFunConstArg e      -- Arg is e, which is constant
+  | DFunLamArg   Int    -- Arg is one of [a,b,d1,d2,d3], zero indexed
+  deriving( Functor )
+
+  -- 'e' is often CoreExpr, which are usually variables, but can
+  -- be trivial expressions instead (e.g. a type application).
+
+dfunArgExprs :: [DFunArg e] -> [e]
+dfunArgExprs [] = []
+dfunArgExprs (DFunPolyArg  e : as) = e : dfunArgExprs as
+dfunArgExprs (DFunConstArg e : as) = e : dfunArgExprs as
+dfunArgExprs (DFunLamArg {}  : as) =     dfunArgExprs as
+
+
+------------------------------------------------
+data UnfoldingSource
+  = InlineRhs          -- The current rhs of the function
+                      -- Replace uf_tmpl each time around
+
+  | InlineStable       -- From an INLINE or INLINABLE pragma 
+                       --   INLINE     if guidance is UnfWhen
+                       --   INLINABLE  if guidance is UnfIfGoodArgs/UnfoldNever
+                       -- (well, technically an INLINABLE might be made
+                       -- UnfWhen if it was small enough, and then
+                       -- it will behave like INLINE outside the current
+                       -- module, but that is the way automatic unfoldings
+                       -- work so it is consistent with the intended
+                       -- meaning of INLINABLE).
+                       --
+                      -- uf_tmpl may change, but only as a result of
+                       -- gentle simplification, it doesn't get updated
+                       -- to the current RHS during compilation as with
+                       -- InlineRhs.
+                       --
+                      -- See Note [InlineRules]
+
+  | InlineCompulsory   -- Something that *has* no binding, so you *must* inline it
+                      -- Only a few primop-like things have this property 
+                       -- (see MkId.lhs, calls to mkCompulsoryUnfolding).
+                       -- Inline absolutely always, however boring the context.
+
+  | InlineWrapper Id   -- This unfolding is a the wrapper in a 
+                      --     worker/wrapper split from the strictness analyser
+                      -- The Id is the worker-id
+                      -- Used to abbreviate the uf_tmpl in interface files
+                      --       which don't need to contain the RHS; 
+                      --       it can be derived from the strictness info
+
+
+
+-- | 'UnfoldingGuidance' says when unfolding should take place
+data UnfoldingGuidance
+  = UnfWhen {  -- Inline without thinking about the *size* of the uf_tmpl
+               -- Used (a) for small *and* cheap unfoldings
+               --      (b) for INLINE functions 
+                -- See Note [INLINE for small functions] in CoreUnfold
+      ug_unsat_ok  :: Bool,    -- True <=> ok to inline even if unsaturated
+      ug_boring_ok :: Bool      -- True <=> ok to inline even if the context is boring
+               -- So True,True means "always"
+    }
 
+  | UnfIfGoodArgs {    -- Arose from a normal Id; the info here is the
+                       -- result of a simple analysis of the RHS
 
-data UnfoldingGuidance
-  = UnfoldNever
-  | UnfoldIfGoodArgs   Int     -- and "n" value args
+      ug_args ::  [Int],  -- Discount if the argument is evaluated.
+                         -- (i.e., a simplification will definitely
+                         -- be possible).  One elt of the list per *value* arg.
+
+      ug_size :: Int,    -- The "size" of the unfolding.
+
+      ug_res :: Int      -- Scrutinee discount: the discount to substract if the thing is in
+    }                    -- a context (case (thing args) of ...),
+                         -- (where there are the right number of arguments.)
+
+  | UnfNever       -- The RHS is big, so don't inline it
+\end{code}
+
+
+Note [DFun unfoldings]
+~~~~~~~~~~~~~~~~~~~~~~
+The Arity in a DFunUnfolding is total number of args (type and value)
+that the DFun needs to produce a dictionary.  That's not necessarily 
+related to the ordinary arity of the dfun Id, esp if the class has
+one method, so the dictionary is represented by a newtype.  Example
 
-                       [Int]   -- Discount if the argument is evaluated.
-                               -- (i.e., a simplification will definitely
-                               -- be possible).  One elt of the list per *value* arg.
+     class C a where { op :: a -> Int }
+     instance C a -> C [a] where op xs = op (head xs)
 
-                       Int     -- The "size" of the unfolding; to be elaborated
-                               -- later. ToDo
+The instance translates to
 
-                       Int     -- Scrutinee discount: the discount to substract if the thing is in
-                               -- a context (case (thing args) of ...),
-                               -- (where there are the right number of arguments.)
+     $dfCList :: forall a. C a => C [a]  -- Arity 2!
+     $dfCList = /\a.\d. $copList {a} d |> co
+     $copList :: forall a. C a => [a] -> Int  -- Arity 2!
+     $copList = /\a.\d.\xs. op {a} d (head xs)
+
+Now we might encounter (op (dfCList {ty} d) a1 a2)
+and we want the (op (dfList {ty} d)) rule to fire, because $dfCList
+has all its arguments, even though its (value) arity is 2.  That's
+why we record the number of expected arguments in the DFunUnfolding.
+
+Note that although it's an Arity, it's most convenient for it to give
+the *total* number of arguments, both type and value.  See the use
+site in exprIsConApp_maybe.
+
+\begin{code}
+-- Constants for the UnfWhen constructor
+needSaturated, unSaturatedOk :: Bool
+needSaturated = False
+unSaturatedOk = True
+
+boringCxtNotOk, boringCxtOk :: Bool
+boringCxtOk    = True
+boringCxtNotOk = False
+
+------------------------------------------------
+noUnfolding :: Unfolding
+-- ^ There is no known 'Unfolding'
+evaldUnfolding :: Unfolding
+-- ^ This unfolding marks the associated thing as being evaluated
 
-noUnfolding, evaldUnfolding :: Unfolding
 noUnfolding    = NoUnfolding
 evaldUnfolding = OtherCon []
 
@@ -323,65 +625,165 @@ mkOtherCon :: [AltCon] -> Unfolding
 mkOtherCon = OtherCon
 
 seqUnfolding :: Unfolding -> ()
-seqUnfolding (CoreUnfolding e top b1 b2 g)
-  = seqExpr e `seq` top `seq` b1 `seq` b2 `seq` seqGuidance g
+seqUnfolding (CoreUnfolding { uf_tmpl = e, uf_is_top = top, 
+               uf_is_value = b1, uf_is_cheap = b2, 
+               uf_expandable = b3, uf_is_conlike = b4,
+                uf_arity = a, uf_guidance = g})
+  = seqExpr e `seq` top `seq` b1 `seq` a `seq` b2 `seq` b3 `seq` b4 `seq` seqGuidance g
+
 seqUnfolding _ = ()
 
 seqGuidance :: UnfoldingGuidance -> ()
-seqGuidance (UnfoldIfGoodArgs n ns a b) = n `seq` sum ns `seq` a `seq` b `seq` ()
-seqGuidance _                           = ()
+seqGuidance (UnfIfGoodArgs ns n b) = n `seq` sum ns `seq` b `seq` ()
+seqGuidance _                      = ()
 \end{code}
 
 \begin{code}
+isStableSource :: UnfoldingSource -> Bool
+-- Keep the unfolding template
+isStableSource InlineCompulsory   = True
+isStableSource InlineStable       = True
+isStableSource (InlineWrapper {}) = True
+isStableSource InlineRhs          = False
+-- | Retrieves the template of an unfolding: panics if none is known
 unfoldingTemplate :: Unfolding -> CoreExpr
-unfoldingTemplate (CoreUnfolding expr _ _ _ _) = expr
-unfoldingTemplate (CompulsoryUnfolding expr)   = expr
-unfoldingTemplate _ = panic "getUnfoldingTemplate"
+unfoldingTemplate = uf_tmpl
 
+setUnfoldingTemplate :: Unfolding -> CoreExpr -> Unfolding
+setUnfoldingTemplate unf rhs = unf { uf_tmpl = rhs }
+
+-- | Retrieves the template of an unfolding if possible
 maybeUnfoldingTemplate :: Unfolding -> Maybe CoreExpr
-maybeUnfoldingTemplate (CoreUnfolding expr _ _ _ _) = Just expr
-maybeUnfoldingTemplate (CompulsoryUnfolding expr)   = Just expr
-maybeUnfoldingTemplate _                            = Nothing
+maybeUnfoldingTemplate (CoreUnfolding { uf_tmpl = expr })       = Just expr
+maybeUnfoldingTemplate _                                       = Nothing
 
+-- | The constructors that the unfolding could never be: 
+-- returns @[]@ if no information is available
 otherCons :: Unfolding -> [AltCon]
 otherCons (OtherCon cons) = cons
 otherCons _               = []
 
+-- | Determines if it is certainly the case that the unfolding will
+-- yield a value (something in HNF): returns @False@ if unsure
 isValueUnfolding :: Unfolding -> Bool
        -- Returns False for OtherCon
-isValueUnfolding (CoreUnfolding _ _ is_evald _ _) = is_evald
-isValueUnfolding _                                = False
+isValueUnfolding (CoreUnfolding { uf_is_value = is_evald }) = is_evald
+isValueUnfolding _                                          = False
 
+-- | Determines if it possibly the case that the unfolding will
+-- yield a value. Unlike 'isValueUnfolding' it returns @True@
+-- for 'OtherCon'
 isEvaldUnfolding :: Unfolding -> Bool
        -- Returns True for OtherCon
-isEvaldUnfolding (OtherCon _)                    = True
-isEvaldUnfolding (CoreUnfolding _ _ is_evald _ _) = is_evald
-isEvaldUnfolding _                                = False
-
+isEvaldUnfolding (OtherCon _)                              = True
+isEvaldUnfolding (CoreUnfolding { uf_is_value = is_evald }) = is_evald
+isEvaldUnfolding _                                          = False
+
+-- | @True@ if the unfolding is a constructor application, the application
+-- of a CONLIKE function or 'OtherCon'
+isConLikeUnfolding :: Unfolding -> Bool
+isConLikeUnfolding (OtherCon _)                             = True
+isConLikeUnfolding (CoreUnfolding { uf_is_conlike = con })  = con
+isConLikeUnfolding _                                        = False
+
+-- | Is the thing we will unfold into certainly cheap?
 isCheapUnfolding :: Unfolding -> Bool
-isCheapUnfolding (CoreUnfolding _ _ _ is_cheap _) = is_cheap
-isCheapUnfolding _                                = False
+isCheapUnfolding (CoreUnfolding { uf_is_cheap = is_cheap }) = is_cheap
+isCheapUnfolding _                                          = False
 
-isCompulsoryUnfolding :: Unfolding -> Bool
-isCompulsoryUnfolding (CompulsoryUnfolding _) = True
-isCompulsoryUnfolding _                       = False
+isExpandableUnfolding :: Unfolding -> Bool
+isExpandableUnfolding (CoreUnfolding { uf_expandable = is_expable }) = is_expable
+isExpandableUnfolding _                                              = False
+
+expandUnfolding_maybe :: Unfolding -> Maybe CoreExpr
+-- Expand an expandable unfolding; this is used in rule matching 
+--   See Note [Expanding variables] in Rules.lhs
+-- The key point here is that CONLIKE things can be expanded
+expandUnfolding_maybe (CoreUnfolding { uf_expandable = True, uf_tmpl = rhs }) = Just rhs
+expandUnfolding_maybe _                                                       = Nothing
 
-hasUnfolding :: Unfolding -> Bool
-hasUnfolding (CoreUnfolding _ _ _ _ _) = True
-hasUnfolding (CompulsoryUnfolding _)   = True
-hasUnfolding _                         = False
+isStableCoreUnfolding_maybe :: Unfolding -> Maybe UnfoldingSource
+isStableCoreUnfolding_maybe (CoreUnfolding { uf_src = src })
+   | isStableSource src   = Just src
+isStableCoreUnfolding_maybe _ = Nothing
 
+isCompulsoryUnfolding :: Unfolding -> Bool
+isCompulsoryUnfolding (CoreUnfolding { uf_src = InlineCompulsory }) = True
+isCompulsoryUnfolding _                                             = False
+
+isStableUnfolding :: Unfolding -> Bool
+-- True of unfoldings that should not be overwritten 
+-- by a CoreUnfolding for the RHS of a let-binding
+isStableUnfolding (CoreUnfolding { uf_src = src }) = isStableSource src
+isStableUnfolding (DFunUnfolding {})              = True
+isStableUnfolding _                                = False
+
+unfoldingArity :: Unfolding -> Arity
+unfoldingArity (CoreUnfolding { uf_arity = arity }) = arity
+unfoldingArity _                                   = panic "unfoldingArity"
+
+isClosedUnfolding :: Unfolding -> Bool         -- No free variables
+isClosedUnfolding (CoreUnfolding {}) = False
+isClosedUnfolding (DFunUnfolding {}) = False
+isClosedUnfolding _                  = True
+
+-- | Only returns False if there is no unfolding information available at all
 hasSomeUnfolding :: Unfolding -> Bool
 hasSomeUnfolding NoUnfolding = False
 hasSomeUnfolding _           = True
 
-neverUnfold :: Unfolding -> Bool
-neverUnfold NoUnfolding                                = True
-neverUnfold (OtherCon _)                       = True
-neverUnfold (CoreUnfolding _ _ _ _ UnfoldNever) = True
-neverUnfold _                                   = False
+neverUnfoldGuidance :: UnfoldingGuidance -> Bool
+neverUnfoldGuidance UnfNever = True
+neverUnfoldGuidance _        = False
+
+canUnfold :: Unfolding -> Bool
+canUnfold (CoreUnfolding { uf_guidance = g }) = not (neverUnfoldGuidance g)
+canUnfold _                                  = False
 \end{code}
 
+Note [InlineRules]
+~~~~~~~~~~~~~~~~~
+When you say 
+      {-# INLINE f #-}
+      f x = <rhs>
+you intend that calls (f e) are replaced by <rhs>[e/x] So we
+should capture (\x.<rhs>) in the Unfolding of 'f', and never meddle
+with it.  Meanwhile, we can optimise <rhs> to our heart's content,
+leaving the original unfolding intact in Unfolding of 'f'. For example
+       all xs = foldr (&&) True xs
+       any p = all . map p  {-# INLINE any #-}
+We optimise any's RHS fully, but leave the InlineRule saying "all . map p",
+which deforests well at the call site.
+
+So INLINE pragma gives rise to an InlineRule, which captures the original RHS.
+
+Moreover, it's only used when 'f' is applied to the
+specified number of arguments; that is, the number of argument on 
+the LHS of the '=' sign in the original source definition. 
+For example, (.) is now defined in the libraries like this
+   {-# INLINE (.) #-}
+   (.) f g = \x -> f (g x)
+so that it'll inline when applied to two arguments. If 'x' appeared
+on the left, thus
+   (.) f g x = f (g x)
+it'd only inline when applied to three arguments.  This slightly-experimental
+change was requested by Roman, but it seems to make sense.
+
+See also Note [Inlining an InlineRule] in CoreUnfold.
+
+
+Note [OccInfo in unfoldings and rules]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In unfoldings and rules, we guarantee that the template is occ-analysed,
+so that the occurence info on the binders is correct.  This is important,
+because the Simplifier does not re-analyse the template when using it. If
+the occurrence info is wrong
+  - We may get more simpifier iterations than necessary, because
+    once-occ info isn't there
+  - More seriously, we may get an infinite loop if there's a Rec
+    without a loop breaker marked
+
 
 %************************************************************************
 %*                                                                     *
@@ -410,7 +812,7 @@ ltAlt :: Alt b -> Alt b -> Bool
 ltAlt a1 a2 = (a1 `cmpAlt` a2) == LT
 
 cmpAltCon :: AltCon -> AltCon -> Ordering
--- Compares AltCons within a single list of alternatives
+-- ^ Compares 'AltCon's within a single list of alternatives
 cmpAltCon DEFAULT      DEFAULT    = EQ
 cmpAltCon DEFAULT      _           = LT
 
@@ -424,26 +826,34 @@ cmpAltCon con1 con2 = WARN( True, text "Comparing incomparable AltCons" <+>
                      LT
 \end{code}
 
-
 %************************************************************************
 %*                                                                     *
 \subsection{Useful synonyms}
 %*                                                                     *
 %************************************************************************
 
-The common case
-
 \begin{code}
+-- | The common case for the type of binders and variables when
+-- we are manipulating the Core language within GHC
 type CoreBndr = Var
+-- | Expressions where binders are 'CoreBndr's
 type CoreExpr = Expr CoreBndr
+-- | Argument expressions where binders are 'CoreBndr's
 type CoreArg  = Arg  CoreBndr
+-- | Binding groups where binders are 'CoreBndr's
 type CoreBind = Bind CoreBndr
+-- | Case alternatives where binders are 'CoreBndr's
 type CoreAlt  = Alt  CoreBndr
 \end{code}
 
-Binders are ``tagged'' with a \tr{t}:
+%************************************************************************
+%*                                                                     *
+\subsection{Tagging}
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
+-- | Binders are /tagged/ with a t
 data TaggedBndr t = TB CoreBndr t      -- TB for "tagged binder"
 
 type TaggedBind t = Bind (TaggedBndr t)
@@ -466,41 +876,105 @@ instance Outputable b => OutputableBndr (TaggedBndr b) where
 %************************************************************************
 
 \begin{code}
+-- | Apply a list of argument expressions to a function expression in a nested fashion. Prefer to
+-- use 'CoreUtils.mkCoreApps' if possible
 mkApps    :: Expr b -> [Arg b]  -> Expr b
+-- | Apply a list of type argument expressions to a function expression in a nested fashion
 mkTyApps  :: Expr b -> [Type]   -> Expr b
-mkValApps :: Expr b -> [Expr b] -> Expr b
+-- | Apply a list of coercion argument expressions to a function expression in a nested fashion
+mkCoApps  :: Expr b -> [Coercion] -> Expr b
+-- | Apply a list of type or value variables to a function expression in a nested fashion
 mkVarApps :: Expr b -> [Var] -> Expr b
+-- | Apply a list of argument expressions to a data constructor in a nested fashion. Prefer to
+-- use 'MkCore.mkCoreConApps' if possible
+mkConApp      :: DataCon -> [Arg b] -> Expr b
 
 mkApps    f args = foldl App                      f args
 mkTyApps  f args = foldl (\ e a -> App e (Type a)) f args
-mkValApps f args = foldl (\ e a -> App e a)       f args
+mkCoApps  f args = foldl (\ e a -> App e (Coercion a)) f args
 mkVarApps f vars = foldl (\ e a -> App e (varToCoreExpr a)) f vars
+mkConApp con args = mkApps (Var (dataConWorkId con)) args
+
 
-mkLit         :: Literal -> Expr b
+-- | Create a machine integer literal expression of type @Int#@ from an @Integer@.
+-- If you want an expression of type @Int@ use 'MkCore.mkIntExpr'
 mkIntLit      :: Integer -> Expr b
+-- | Create a machine integer literal expression of type @Int#@ from an @Int@.
+-- If you want an expression of type @Int@ use 'MkCore.mkIntExpr'
 mkIntLitInt   :: Int     -> Expr b
-mkConApp      :: DataCon -> [Arg b] -> Expr b
+
+mkIntLit    n = Lit (mkMachInt n)
+mkIntLitInt n = Lit (mkMachInt (toInteger n))
+
+-- | Create a machine word literal expression of type  @Word#@ from an @Integer@.
+-- If you want an expression of type @Word@ use 'MkCore.mkWordExpr'
+mkWordLit     :: Integer -> Expr b
+-- | Create a machine word literal expression of type  @Word#@ from a @Word@.
+-- If you want an expression of type @Word@ use 'MkCore.mkWordExpr'
+mkWordLitWord :: Word -> Expr b
+
+mkWordLit     w = Lit (mkMachWord w)
+mkWordLitWord w = Lit (mkMachWord (toInteger w))
+
+-- | Create a machine character literal expression of type @Char#@.
+-- If you want an expression of type @Char@ use 'MkCore.mkCharExpr'
+mkCharLit :: Char -> Expr b
+-- | Create a machine string literal expression of type @Addr#@.
+-- If you want an expression of type @String@ use 'MkCore.mkStringExpr'
+mkStringLit :: String -> Expr b
+
+mkCharLit   c = Lit (mkMachChar c)
+mkStringLit s = Lit (mkMachString s)
+
+-- | Create a machine single precision literal expression of type @Float#@ from a @Rational@.
+-- If you want an expression of type @Float@ use 'MkCore.mkFloatExpr'
+mkFloatLit :: Rational -> Expr b
+-- | Create a machine single precision literal expression of type @Float#@ from a @Float@.
+-- If you want an expression of type @Float@ use 'MkCore.mkFloatExpr'
+mkFloatLitFloat :: Float -> Expr b
+
+mkFloatLit      f = Lit (mkMachFloat f)
+mkFloatLitFloat f = Lit (mkMachFloat (toRational f))
+
+-- | Create a machine double precision literal expression of type @Double#@ from a @Rational@.
+-- If you want an expression of type @Double@ use 'MkCore.mkDoubleExpr'
+mkDoubleLit :: Rational -> Expr b
+-- | Create a machine double precision literal expression of type @Double#@ from a @Double@.
+-- If you want an expression of type @Double@ use 'MkCore.mkDoubleExpr'
+mkDoubleLitDouble :: Double -> Expr b
+
+mkDoubleLit       d = Lit (mkMachDouble d)
+mkDoubleLitDouble d = Lit (mkMachDouble (toRational d))
+
+-- | Bind all supplied binding groups over an expression in a nested let expression. Prefer to
+-- use 'CoreUtils.mkCoreLets' if possible
 mkLets       :: [Bind b] -> Expr b -> Expr b
+-- | Bind all supplied binders over an expression in a nested lambda expression. Prefer to
+-- use 'CoreUtils.mkCoreLams' if possible
 mkLams       :: [b] -> Expr b -> Expr b
 
-mkLit lit        = Lit lit
-mkConApp con args = mkApps (Var (dataConWorkId con)) args
-
 mkLams binders body = foldr Lam body binders
 mkLets binds body   = foldr Let body binds
 
-mkIntLit    n = Lit (mkMachInt n)
-mkIntLitInt n = Lit (mkMachInt (toInteger n))
 
+-- | Create a binding group where a type variable is bound to a type. Per "CoreSyn#type_let",
+-- this can only be used to bind something in a non-recursive @let@ expression
+mkTyBind :: TyVar -> Type -> CoreBind
+mkTyBind tv ty      = NonRec tv (Type ty)
+
+-- | Create a binding group where a type variable is bound to a type. Per "CoreSyn#type_let",
+-- this can only be used to bind something in a non-recursive @let@ expression
+mkCoBind :: CoVar -> Coercion -> CoreBind
+mkCoBind cv co      = NonRec cv (Coercion co)
+
+-- | Convert a binder into either a 'Var' or 'Type' 'Expr' appropriately
 varToCoreExpr :: CoreBndr -> Expr b
-varToCoreExpr v | isId v    = Var v
-                | otherwise = Type (mkTyVarTy v)
+varToCoreExpr v | isTyVar v = Type (mkTyVarTy v)
+                | isCoVar v = Coercion (mkCoVarCo v)
+                | otherwise = ASSERT( isId v ) Var v
 
 varsToCoreExprs :: [CoreBndr] -> [Expr b]
 varsToCoreExprs vs = map varToCoreExpr vs
-
-mkCast   :: Expr b -> Coercion -> Expr b
-mkCast e co = Cast e co
 \end{code}
 
 
@@ -511,15 +985,12 @@ mkCast e co = Cast e co
 %************************************************************************
 
 \begin{code}
-mkTyBind :: TyVar -> Type -> CoreBind
-mkTyBind tv ty      = NonRec tv (Type ty)
-       -- Note [Type let]
-       -- A non-recursive let can bind a type variable
-
+-- | Extract every variable by this group
 bindersOf  :: Bind b -> [b]
 bindersOf (NonRec binder _) = [binder]
 bindersOf (Rec pairs)       = [binder | (binder, _) <- pairs]
 
+-- | 'bindersOf' applied to a list of binding groups
 bindersOfBinds :: [Bind b] -> [b]
 bindersOfBinds binds = foldr ((++) . bindersOf) [] binds
 
@@ -530,22 +1001,25 @@ rhssOfBind (Rec pairs)    = [rhs | (_,rhs) <- pairs]
 rhssOfAlts :: [Alt b] -> [Expr b]
 rhssOfAlts alts = [e | (_,_,e) <- alts]
 
-flattenBinds :: [Bind b] -> [(b, Expr b)]      -- Get all the lhs/rhs pairs
+-- | Collapse all the bindings in the supplied groups into a single
+-- list of lhs\/rhs pairs suitable for binding in a 'Rec' binding group
+flattenBinds :: [Bind b] -> [(b, Expr b)]
 flattenBinds (NonRec b r : binds) = (b,r) : flattenBinds binds
 flattenBinds (Rec prs1   : binds) = prs1 ++ flattenBinds binds
 flattenBinds []                          = []
 \end{code}
 
-We often want to strip off leading lambdas before getting down to
-business.  @collectBinders@ is your friend.
-
-We expect (by convention) type-, and value- lambdas in that
-order.
-
 \begin{code}
+-- | We often want to strip off leading lambdas before getting down to
+-- business. This function is your friend.
 collectBinders              :: Expr b -> ([b],         Expr b)
+-- | Collect as many type bindings as possible from the front of a nested lambda
 collectTyBinders                    :: CoreExpr -> ([TyVar],     CoreExpr)
+-- | Collect as many value bindings as possible from the front of a nested lambda
 collectValBinders                   :: CoreExpr -> ([Id],        CoreExpr)
+-- | Collect type binders from the front of the lambda first, 
+-- then follow up by collecting as many value bindings as possible
+-- from the resulting stripped expression
 collectTyAndValBinders              :: CoreExpr -> ([TyVar], [Id], CoreExpr)
 
 collectBinders expr
@@ -573,11 +1047,9 @@ collectValBinders expr
     go ids body                      = (reverse ids, body)
 \end{code}
 
-
-@collectArgs@ takes an application expression, returning the function
-and the arguments to which it is applied.
-
 \begin{code}
+-- | Takes a nested application expression and returns the the function
+-- being applied and the arguments to which it is applied
 collectArgs :: Expr b -> (Expr b, [Arg b])
 collectArgs expr
   = go expr []
@@ -586,10 +1058,9 @@ collectArgs expr
     go e        as = (e, as)
 \end{code}
 
-coreExprCc gets the cost centre enclosing an expression, if any.
-It looks inside lambdas because (scc "foo" \x.e) = \x.scc "foo" e
-
 \begin{code}
+-- | Gets the cost centre enclosing an expression, if any.
+-- It looks inside lambdas because @(scc \"foo\" \\x.e) = \\x. scc \"foo\" e@
 coreExprCc :: Expr b -> CostCentre
 coreExprCc (Note (SCC cc) _)   = cc
 coreExprCc (Note _ e)          = coreExprCc e
@@ -597,8 +1068,6 @@ coreExprCc (Lam _ e)           = coreExprCc e
 coreExprCc _                   = noCostCentre
 \end{code}
 
-
-
 %************************************************************************
 %*                                                                     *
 \subsection{Predicates}
@@ -611,25 +1080,43 @@ i.e. if type applications are actual lambdas because types are kept around
 at runtime.  Similarly isRuntimeArg.  
 
 \begin{code}
+-- | Will this variable exist at runtime?
 isRuntimeVar :: Var -> Bool
 isRuntimeVar = isId 
 
+-- | Will this argument expression exist at runtime?
 isRuntimeArg :: CoreExpr -> Bool
 isRuntimeArg = isValArg
 
+-- | Returns @False@ iff the expression is a 'Type' or 'Coercion'
+-- expression at its top level
 isValArg :: Expr b -> Bool
-isValArg (Type _) = False
-isValArg _        = True
+isValArg e = not (isTypeArg e)
+
+-- | Returns @True@ iff the expression is a 'Type' or 'Coercion'
+-- expression at its top level
+isTyCoArg :: Expr b -> Bool
+isTyCoArg (Type {})     = True
+isTyCoArg (Coercion {}) = True
+isTyCoArg _             = False
 
+-- | Returns @True@ iff the expression is a 'Type' expression at its
+-- top level.  Note this does NOT include 'Coercion's.
 isTypeArg :: Expr b -> Bool
-isTypeArg (Type _) = True
-isTypeArg _        = False
+isTypeArg (Type {}) = True
+isTypeArg _         = False
 
+-- | The number of binders that bind values rather than types
 valBndrCount :: [CoreBndr] -> Int
 valBndrCount = count isId
 
+-- | The number of argument expressions that are values rather than types at their top level
 valArgCount :: [Arg b] -> Int
 valArgCount = count isValArg
+
+notSccNote :: Note -> Bool
+notSccNote (SCC {}) = False
+notSccNote _        = True
 \end{code}
 
 
@@ -647,9 +1134,10 @@ seqExpr (App f a)       = seqExpr f `seq` seqExpr a
 seqExpr (Lam b e)       = seqBndr b `seq` seqExpr e
 seqExpr (Let b e)       = seqBind b `seq` seqExpr e
 seqExpr (Case e b t as) = seqExpr e `seq` seqBndr b `seq` seqType t `seq` seqAlts as
-seqExpr (Cast e co)     = seqExpr e `seq` seqType co
+seqExpr (Cast e co)     = seqExpr e `seq` seqCo co
 seqExpr (Note n e)      = seqNote n `seq` seqExpr e
-seqExpr (Type t)        = seqType t
+seqExpr (Type t)       = seqType t
+seqExpr (Coercion co)   = seqCo co
 
 seqExprs :: [CoreExpr] -> ()
 seqExprs [] = ()
@@ -685,17 +1173,17 @@ seqRules (Rule { ru_bndrs = bndrs, ru_args = args, ru_rhs = rhs } : rules)
 seqRules (BuiltinRule {} : rules) = seqRules rules
 \end{code}
 
-
-
 %************************************************************************
 %*                                                                     *
-\subsection{Annotated core; annotation at every node in the tree}
+\subsection{Annotated core}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
+-- | Annotated core: allows annotation at every node in the tree
 type AnnExpr bndr annot = (annot, AnnExpr' bndr annot)
 
+-- | A clone of the 'Expr' type but allowing annotation at every tree node
 data AnnExpr' bndr annot
   = AnnVar     Id
   | AnnLit     Literal
@@ -703,28 +1191,44 @@ data AnnExpr' bndr annot
   | AnnApp     (AnnExpr bndr annot) (AnnExpr bndr annot)
   | AnnCase    (AnnExpr bndr annot) bndr Type [AnnAlt bndr annot]
   | AnnLet     (AnnBind bndr annot) (AnnExpr bndr annot)
-  | AnnCast     (AnnExpr bndr annot) Coercion
+  | AnnCast     (AnnExpr bndr annot) (annot, Coercion)
+                  -- Put an annotation on the (root of) the coercion
   | AnnNote    Note (AnnExpr bndr annot)
   | AnnType    Type
+  | AnnCoercion Coercion
 
+-- | A clone of the 'Alt' type but allowing annotation at every tree node
 type AnnAlt bndr annot = (AltCon, [bndr], AnnExpr bndr annot)
 
+-- | A clone of the 'Bind' type but allowing annotation at every tree node
 data AnnBind bndr annot
   = AnnNonRec bndr (AnnExpr bndr annot)
   | AnnRec    [(bndr, AnnExpr bndr annot)]
 \end{code}
 
 \begin{code}
+-- | Takes a nested application expression and returns the the function
+-- being applied and the arguments to which it is applied
+collectAnnArgs :: AnnExpr b a -> (AnnExpr b a, [AnnExpr b a])
+collectAnnArgs expr
+  = go expr []
+  where
+    go (_, AnnApp f a) as = go f (a:as)
+    go e              as = (e, as)
+\end{code}
+
+\begin{code}
 deAnnotate :: AnnExpr bndr annot -> Expr bndr
 deAnnotate (_, e) = deAnnotate' e
 
 deAnnotate' :: AnnExpr' bndr annot -> Expr bndr
-deAnnotate' (AnnType t)           = Type t
+deAnnotate' (AnnType t)          = Type t
+deAnnotate' (AnnCoercion co)      = Coercion co
 deAnnotate' (AnnVar  v)           = Var v
 deAnnotate' (AnnLit  lit)         = Lit lit
 deAnnotate' (AnnLam  binder body) = Lam binder (deAnnotate body)
 deAnnotate' (AnnApp  fun arg)     = App (deAnnotate fun) (deAnnotate arg)
-deAnnotate' (AnnCast e co)        = Cast (deAnnotate e) co
+deAnnotate' (AnnCast e (_,co))    = Cast (deAnnotate e) co
 deAnnotate' (AnnNote note body)   = Note note (deAnnotate body)
 
 deAnnotate' (AnnLet bind body)
@@ -741,6 +1245,7 @@ deAnnAlt (con,args,rhs) = (con,args,deAnnotate rhs)
 \end{code}
 
 \begin{code}
+-- | As 'collectBinders' but for 'AnnExpr' rather than 'Expr'
 collectAnnBndrs :: AnnExpr bndr annot -> ([bndr], AnnExpr bndr annot)
 collectAnnBndrs e
   = collect [] e