cmmTopCodeGen no longer takes DynFlags as an argument
[ghc-hetmet.git] / compiler / coreSyn / CoreSyn.lhs
index 3c905af..e754c6d 100644 (file)
@@ -4,7 +4,7 @@
 %
 
 \begin{code}
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor #-}
 
 -- | CoreSyn holds all the main data types for use by for the Glasgow Haskell Compiler midsection
 module CoreSyn (
@@ -15,7 +15,7 @@ module CoreSyn (
 
         -- ** 'Expr' construction
        mkLets, mkLams,
-       mkApps, mkTyApps, mkVarApps,
+       mkApps, mkTyApps, mkCoApps, mkVarApps,
        
        mkIntLit, mkIntLitInt,
        mkWordLit, mkWordLitWord,
@@ -23,22 +23,24 @@ module CoreSyn (
        mkFloatLit, mkFloatLitFloat,
        mkDoubleLit, mkDoubleLitDouble,
        
-       mkConApp, mkTyBind,
+       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, flattenBinds, 
 
-       isValArg, isTypeArg, valArgCount, valBndrCount, isRuntimeArg, isRuntimeVar,
+        isValArg, isTypeArg, isTyCoArg, valArgCount, valBndrCount,
+        isRuntimeArg, isRuntimeVar,
+        notSccNote,
 
        -- * Unfolding data types
-       Unfolding(..),  UnfoldingGuidance(..), UnfoldingSource(..),
-               -- Abstract everywhere but in CoreUnfold.lhs
-       
+        Unfolding(..),  UnfoldingGuidance(..), UnfoldingSource(..),
+        DFunArg(..), dfunArgExprs,
+
        -- ** Constructing 'Unfolding's
        noUnfolding, evaldUnfolding, mkOtherCon,
         unSaturatedOk, needSaturated, boringCxtOk, boringCxtNotOk,
@@ -48,8 +50,9 @@ module CoreSyn (
        maybeUnfoldingTemplate, otherCons, unfoldingArity,
        isValueUnfolding, isEvaldUnfolding, isCheapUnfolding,
         isExpandableUnfolding, isConLikeUnfolding, isCompulsoryUnfolding,
-       isInlineRule, isInlineRule_maybe, isClosedUnfolding, hasSomeUnfolding, 
-       isStableUnfolding, canUnfold, neverUnfoldGuidance, isInlineRuleSource,
+        isStableUnfolding, isStableCoreUnfolding_maybe,
+        isClosedUnfolding, hasSomeUnfolding, 
+       canUnfold, neverUnfoldGuidance, isStableSource,
 
        -- * Strictness
        seqExpr, seqExprs, seqUnfolding, 
@@ -57,6 +60,9 @@ module CoreSyn (
        -- * Annotated expression data types
        AnnExpr, AnnExpr'(..), AnnBind(..), AnnAlt,
        
+        -- ** Operations on annotated expressions
+        collectAnnArgs,
+
        -- ** Operations on annotations
        deAnnotate, deAnnotate', deAnnAlt, collectAnnBndrs,
 
@@ -65,9 +71,12 @@ module CoreSyn (
        RuleName, IdUnfoldingFun,
        
        -- ** Operations on 'CoreRule's 
-       seqRules, ruleArity, ruleName, ruleIdName, ruleActivation_maybe,
+       seqRules, ruleArity, ruleName, ruleIdName, ruleActivation,
        setRuleIdName,
-       isBuiltinRule, isLocalRule
+       isBuiltinRule, isLocalRule,
+
+       -- * Core vectorisation declarations data type
+       CoreVect(..)
     ) where
 
 #include "HsVersions.h"
@@ -87,7 +96,7 @@ import Util
 import Data.Data
 import Data.Word
 
-infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`
+infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`, `App`, `mkCoApps`
 -- Left associative, so that we can say (f `mkTyApps` xs `mkVarApps` ys)
 \end{code}
 
@@ -100,8 +109,6 @@ infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`
 These data types are the heart of the compiler
 
 \begin{code}
-infixl 8 `App` -- App brackets to the left
-
 -- | 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>.
@@ -137,11 +144,15 @@ infixl 8 `App`    -- App brackets to the left
 -- 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.
@@ -154,14 +165,16 @@ data Expr b
                                         -- 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',
+                                        -- 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:
+                                        -- 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:
+                                       -- But this is not, as it may affect termination if the 
+                                        -- expression is floated out:
                                        --
                                        -- > y::Int# = fac 4#
                                        --
@@ -181,6 +194,7 @@ data Expr b
                                         -- 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
@@ -190,15 +204,17 @@ data Expr b
                                         -- 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:
+                                       -- 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 '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.
+                                       -- 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:
@@ -212,14 +228,20 @@ data Expr b
                                         --                      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.
+                                        -- 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.
@@ -306,7 +328,7 @@ data CoreRule
   = Rule { 
        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.Id' at the head of this rule
@@ -323,6 +345,10 @@ data CoreRule
                                        -- See Note [OccInfo in unfoldings and rules]
 
        -- Locality
+        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 selector,
@@ -364,9 +390,9 @@ ruleArity (Rule {ru_args = args})      = length args
 ruleName :: CoreRule -> RuleName
 ruleName = ru_name
 
-ruleActivation_maybe :: CoreRule -> Maybe Activation
-ruleActivation_maybe (BuiltinRule { })       = Nothing
-ruleActivation_maybe (Rule { ru_act = act }) = Just act
+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
@@ -382,6 +408,20 @@ setRuleIdName nm ru = ru { ru_fn = nm }
 
 
 %************************************************************************
+%*                                                                      *
+\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}
+
+
+%************************************************************************
 %*                                                                     *
                Unfoldings
 %*                                                                     *
@@ -407,27 +447,32 @@ data Unfolding
                       --
                       -- Here, @f@ gets an @OtherCon []@ unfolding.
 
-  | DFunUnfolding DataCon [CoreExpr]   
-                        -- The Unfolding of a DFunId
+  | 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)
-                       -- where Arity = n, the number of dict args to the dfun
-                       -- The [CoreExpr] are the superclasses and methods [op1,op2], 
-                       -- in positional order.
-                       -- They are usually variables, but can be trivial expressions
-                       -- instead (e.g. a type application).  
-
-  | 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.)
+
+        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 <=> application of constructor or CONLIKE function
+       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
+       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
@@ -450,14 +495,49 @@ data Unfolding
   --  uf_guidance:  Tells us about the /size/ of the unfolding template
 
 ------------------------------------------------
-data UnfoldingSource 
-  = InlineCompulsory   -- Something that *has* no binding, so you *must* inline it
+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.
 
-  | InlineRule        -- From an {-# INLINE #-} pragma; See Note [InlineRules]
-
   | InlineWrapper Id   -- This unfolding is a the wrapper in a 
                       --     worker/wrapper split from the strictness analyser
                       -- The Id is the worker-id
@@ -465,10 +545,6 @@ data UnfoldingSource
                       --       which don't need to contain the RHS; 
                       --       it can be derived from the strictness info
 
-  | InlineRhs          -- The current rhs of the function
-
-   -- For InlineRhs, the uf_tmpl is replaced each time around
-   -- For all the others we leave uf_tmpl alone
 
 
 -- | 'UnfoldingGuidance' says when unfolding should take place
@@ -496,7 +572,37 @@ data UnfoldingGuidance
                          -- (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
+
+     class C a where { op :: a -> Int }
+     instance C a -> C [a] where op xs = op (head xs)
+
+The instance translates to
+
+     $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
@@ -533,11 +639,12 @@ seqGuidance _                      = ()
 \end{code}
 
 \begin{code}
-isInlineRuleSource :: UnfoldingSource -> Bool
-isInlineRuleSource InlineCompulsory   = True
-isInlineRuleSource InlineRule         = True
-isInlineRuleSource (InlineWrapper {}) = True
-isInlineRuleSource InlineRhs          = False
+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
@@ -596,19 +703,10 @@ expandUnfolding_maybe :: Unfolding -> Maybe CoreExpr
 expandUnfolding_maybe (CoreUnfolding { uf_expandable = True, uf_tmpl = rhs }) = Just rhs
 expandUnfolding_maybe _                                                       = Nothing
 
-isInlineRule :: Unfolding -> Bool
-isInlineRule (CoreUnfolding { uf_src = src }) = isInlineRuleSource src
-isInlineRule _                               = False
-
-isInlineRule_maybe :: Unfolding -> Maybe (UnfoldingSource, Bool)
-isInlineRule_maybe (CoreUnfolding { uf_src = src, uf_guidance = guide }) 
-   | isInlineRuleSource src
-   = Just (src, unsat_ok)
-   where
-     unsat_ok = case guide of
-                 UnfWhen unsat_ok _ -> unsat_ok
-                  _                  -> needSaturated
-isInlineRule_maybe _ = Nothing
+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
@@ -617,7 +715,7 @@ 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 }) = isInlineRuleSource src
+isStableUnfolding (CoreUnfolding { uf_src = src }) = isStableSource src
 isStableUnfolding (DFunUnfolding {})              = True
 isStableUnfolding _                                = False
 
@@ -783,6 +881,8 @@ instance Outputable b => OutputableBndr (TaggedBndr b) where
 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
+-- | 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
@@ -791,6 +891,7 @@ 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
+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
 
@@ -861,10 +962,16 @@ mkLets binds body   = foldr Let body binds
 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
@@ -981,15 +1088,23 @@ isRuntimeVar = isId
 isRuntimeArg :: CoreExpr -> Bool
 isRuntimeArg = isValArg
 
--- | Returns @False@ iff the expression is a 'Type' expression at its top level
+-- | 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
+-- | 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
@@ -998,6 +1113,10 @@ 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}
 
 
@@ -1015,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 [] = ()
@@ -1071,9 +1191,11 @@ 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)
@@ -1085,16 +1207,28 @@ data AnnBind 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)