-- | Functions for collecting together and applying rewrite rules to a module.
-- The 'CoreRule' datatype itself is declared elsewhere.
module Rules (
        -- * RuleBase
        RuleBase,

        -- ** Constructing
        emptyRuleBase, mkRuleBase, extendRuleBaseList,
        unionRuleBase, pprRuleBase,

        -- ** Checking rule applications
        ruleCheckProgram,

        -- ** Manipulating 'SpecInfo' rules
        mkSpecInfo, extendSpecInfo, addSpecInfo,
        addIdSpecialisations,

        -- * Misc. CoreRule helpers
        rulesOfBinds, getRules, pprRulesForUser,

        lookupRule, mkRule, roughTopNames
    ) where

#include "HsVersions.h"

import CoreSyn          -- All of it
import CoreSubst
import OccurAnal        ( occurAnalyseExpr )
import CoreFVs          ( exprFreeVars, exprsFreeVars, bindFreeVars, rulesFreeVars )
import CoreUtils        ( exprType, eqExpr )
import PprCore          ( pprRules )
import Type             ( Type )
import TcType           ( tcSplitTyConApp_maybe )
import Coercion
import CoreTidy         ( tidyRules )
import Id
import IdInfo           ( SpecInfo( SpecInfo ) )
import VarEnv
import VarSet
import Name             ( Name, NamedThing(..) )
import NameEnv
import Unify            ( ruleMatchTyX, MatchEnv(..) )
import BasicTypes       ( Activation, CompilerPhase, isActive )
import StaticFlags      ( opt_PprStyle_Debug )
import Outputable
import FastString
import Maybes
import Bag
import Util
import Data.List
import Data.Ord

mkRule :: Bool -> Bool -> RuleName -> Activation
       -> Name -> [CoreBndr] -> [CoreExpr] -> CoreExpr -> CoreRule
-- ^ Used to make 'CoreRule' for an 'Id' defined in the module being
-- compiled. See also 'CoreSyn.CoreRule'
mkRule is_auto is_local name act fn bndrs args rhs
  = Rule { ru_name = name, ru_fn = fn, ru_act = act,
           ru_bndrs = bndrs, ru_args = args,
           ru_rhs = occurAnalyseExpr rhs,
           ru_rough = roughTopNames args,
           ru_auto = is_auto, ru_local = is_local }

--------------
roughTopNames :: [CoreExpr] -> [Maybe Name]
-- ^ Find the \"top\" free names of several expressions.
-- Such names are either:
--
-- 1. The function finally being applied to in an application chain
--    (if that name is a GlobalId: see "Var#globalvslocal"), or
--
-- 2. The 'TyCon' if the expression is a 'Type'
--
-- This is used for the fast-match-check for rules;
--      if the top names don't match, the rest can't
roughTopNames args = map roughTopName args

roughTopName :: CoreExpr -> Maybe Name
roughTopName (Type ty) = case tcSplitTyConApp_maybe ty of
                               Just (tc,_) -> Just (getName tc)
                               Nothing     -> Nothing
roughTopName (Coercion _) = Nothing
roughTopName (App f _) = roughTopName f
roughTopName (Var f)   | isGlobalId f   -- Note [Care with roughTopName]
                       , isDataConWorkId f || idArity f > 0
                       = Just (idName f)
roughTopName _ = Nothing

ruleCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
-- ^ @ruleCantMatch tpl actual@ returns True only if @actual@
-- definitely can't match @tpl@ by instantiating @tpl@.
-- It's only a one-way match; unlike instance matching we
-- don't consider unification.
--
-- Notice that [_$_]
--      @ruleCantMatch [Nothing] [Just n2] = False@
--      Reason: a template variable can be instantiated by a constant
-- Also:
--      @ruleCantMatch [Just n1] [Nothing] = False@
--      Reason: a local variable @v@ in the actuals might [_$_]

ruleCantMatch (Just n1 : ts) (Just n2 : as) = n1 /= n2 || ruleCantMatch ts as
ruleCantMatch (_       : ts) (_       : as) = ruleCantMatch ts as
ruleCantMatch _              _              = False

pprRulesForUser :: [CoreRule] -> SDoc
-- (a) tidy the rules
-- (b) sort them into order based on the rule name
-- (c) suppress uniques (unless -dppr-debug is on)
-- This combination makes the output stable so we can use in testing
-- It's here rather than in PprCore because it calls tidyRules
pprRulesForUser rules
  = withPprStyle defaultUserStyle $
    pprRules $
    sortBy (comparing ru_name) $
    tidyRules emptyTidyEnv rules

-- | Make a 'SpecInfo' containing a number of 'CoreRule's, suitable
-- for putting into an 'IdInfo'
mkSpecInfo :: [CoreRule] -> SpecInfo
mkSpecInfo rules = SpecInfo rules (rulesFreeVars rules)

extendSpecInfo :: SpecInfo -> [CoreRule] -> SpecInfo
extendSpecInfo (SpecInfo rs1 fvs1) rs2
  = SpecInfo (rs2 ++ rs1) (rulesFreeVars rs2 `unionVarSet` fvs1)

addSpecInfo :: SpecInfo -> SpecInfo -> SpecInfo
addSpecInfo (SpecInfo rs1 fvs1) (SpecInfo rs2 fvs2)
  = SpecInfo (rs1 ++ rs2) (fvs1 `unionVarSet` fvs2)

addIdSpecialisations :: Id -> [CoreRule] -> Id
addIdSpecialisations id []
  = id
addIdSpecialisations id rules
  = setIdSpecialisation id $
    extendSpecInfo (idSpecialisation id) rules

-- | Gather all the rules for locally bound identifiers from the supplied bindings
rulesOfBinds :: [CoreBind] -> [CoreRule]
rulesOfBinds binds = concatMap (concatMap idCoreRules . bindersOf) binds

getRules :: RuleBase -> Id -> [CoreRule]
-- See Note [Where rules are found]
getRules rule_base fn
  = idCoreRules fn ++ imp_rules
  where
    imp_rules = lookupNameEnv rule_base (idName fn) `orElse` []

-- | Gathers a collection of 'CoreRule's. Maps (the name of) an 'Id' to its rules
type RuleBase = NameEnv [CoreRule]
        -- The rules are are unordered;
        -- we sort out any overlaps on lookup

emptyRuleBase :: RuleBase
emptyRuleBase = emptyNameEnv

mkRuleBase :: [CoreRule] -> RuleBase
mkRuleBase rules = extendRuleBaseList emptyRuleBase rules

extendRuleBaseList :: RuleBase -> [CoreRule] -> RuleBase
extendRuleBaseList rule_base new_guys
  = foldl extendRuleBase rule_base new_guys

unionRuleBase :: RuleBase -> RuleBase -> RuleBase
unionRuleBase rb1 rb2 = plusNameEnv_C (++) rb1 rb2

extendRuleBase :: RuleBase -> CoreRule -> RuleBase
extendRuleBase rule_base rule
  = extendNameEnv_Acc (:) singleton rule_base (ruleIdName rule) rule

pprRuleBase :: RuleBase -> SDoc
pprRuleBase rules = vcat [ pprRules (tidyRules emptyTidyEnv rs)
                         | rs <- nameEnvElts rules ]

-- | The main rule matching function. Attempts to apply all (active)
-- supplied rules to this instance of an application in a given
-- context, returning the rule applied and the resulting expression if
-- successful.
lookupRule :: (Activation -> Bool)      -- When rule is active
            -> IdUnfoldingFun           -- When Id can be unfolded
            -> InScopeSet
            -> Id -> [CoreExpr]
            -> [CoreRule] -> Maybe (CoreRule, CoreExpr)

-- See Note [Extra args in rule matching]
-- See comments on matchRule
lookupRule is_active id_unf in_scope fn args rules
  = -- pprTrace "matchRules" (ppr fn <+> ppr args $$ ppr rules ) $
    case go [] rules of
        []     -> Nothing
        (m:ms) -> Just (findBest (fn,args) m ms)
  where
    rough_args = map roughTopName args

    go :: [(CoreRule,CoreExpr)] -> [CoreRule] -> [(CoreRule,CoreExpr)]
    go ms []           = ms
    go ms (r:rs) = case (matchRule fn is_active id_unf in_scope args rough_args r) of
                        Just e  -> go ((r,e):ms) rs
                        Nothing -> -- pprTrace "match failed" (ppr r $$ ppr args $$
                                   --   ppr [ (arg_id, unfoldingTemplate unf)
                                   --       | Var arg_id <- args
                                   --       , let unf = idUnfolding arg_id
                                   --       , isCheapUnfolding unf] )
                                   go ms rs

findBest :: (Id, [CoreExpr])
         -> (CoreRule,CoreExpr) -> [(CoreRule,CoreExpr)] -> (CoreRule,CoreExpr)
-- All these pairs matched the expression
-- Return the pair the the most specific rule
-- The (fn,args) is just for overlap reporting

findBest _      (rule,ans)   [] = (rule,ans)
findBest target (rule1,ans1) ((rule2,ans2):prs)
  | rule1 `isMoreSpecific` rule2 = findBest target (rule1,ans1) prs
  | rule2 `isMoreSpecific` rule1 = findBest target (rule2,ans2) prs
  | debugIsOn = let pp_rule rule
                        | opt_PprStyle_Debug = ppr rule
                        | otherwise          = doubleQuotes (ftext (ru_name rule))
                in pprTrace "Rules.findBest: rule overlap (Rule 1 wins)"
                         (vcat [if opt_PprStyle_Debug then
                                   ptext (sLit "Expression to match:") <+> ppr fn <+> sep (map ppr args)
                                else empty,
                                ptext (sLit "Rule 1:") <+> pp_rule rule1,
                                ptext (sLit "Rule 2:") <+> pp_rule rule2]) $
                findBest target (rule1,ans1) prs
  | otherwise = findBest target (rule1,ans1) prs
  where
    (fn,args) = target

isMoreSpecific :: CoreRule -> CoreRule -> Bool
-- This tests if one rule is more specific than another
-- We take the view that a BuiltinRule is less specific than
-- anything else, because we want user-define rules to "win"
-- In particular, class ops have a built-in rule, but we
-- any user-specific rules to win
--   eg (Trac #4397)
--      truncate :: (RealFrac a, Integral b) => a -> b
--      {-# RULES "truncate/Double->Int" truncate = double2Int #-}
--      double2Int :: Double -> Int
--   We want the specific RULE to beat the built-in class-op rule
isMoreSpecific (BuiltinRule {}) _                = False
isMoreSpecific (Rule {})        (BuiltinRule {}) = True
isMoreSpecific (Rule { ru_bndrs = bndrs1, ru_args = args1 })
               (Rule { ru_bndrs = bndrs2, ru_args = args2 })
  = isJust (matchN id_unfolding_fun in_scope bndrs2 args2 args1)
  where
   id_unfolding_fun _ = NoUnfolding     -- Don't expand in templates
   in_scope = mkInScopeSet (mkVarSet bndrs1)
        -- Actually we should probably include the free vars
        -- of rule1's args, but I can't be bothered

noBlackList :: Activation -> Bool
noBlackList _ = False           -- Nothing is black listed

------------------------------------
matchRule :: Id -> (Activation -> Bool) -> IdUnfoldingFun
          -> InScopeSet
          -> [CoreExpr] -> [Maybe Name]
          -> CoreRule -> Maybe CoreExpr

-- If (matchRule rule args) returns Just (name,rhs)
-- then (f args) matches the rule, and the corresponding
-- rewritten RHS is rhs
--
-- The bndrs and rhs is occurrence-analysed
--
--      Example
--
-- The rule
--      forall f g x. map f (map g x) ==> map (f . g) x
-- is stored
--      CoreRule "map/map"
--               [f,g,x]                -- tpl_vars
--               [f,map g x]            -- tpl_args
--               map (f.g) x)           -- rhs
--
-- Then the call: matchRule the_rule [e1,map e2 e3]
--        = Just ("map/map", (\f,g,x -> rhs) e1 e2 e3)
--
-- Any 'surplus' arguments in the input are simply put on the end
-- of the output.

matchRule fn _is_active id_unf _in_scope args _rough_args
          (BuiltinRule { ru_try = match_fn })
-- Built-in rules can't be switched off, it seems
  = case match_fn fn id_unf args of
        Just expr -> Just expr
        Nothing   -> Nothing

matchRule _ is_active id_unf in_scope args rough_args
          (Rule { ru_act = act, ru_rough = tpl_tops,
                  ru_bndrs = tpl_vars, ru_args = tpl_args,
                  ru_rhs = rhs })
  | not (is_active act)               = Nothing
  | ruleCantMatch tpl_tops rough_args = Nothing
  | otherwise
  = case matchN id_unf in_scope tpl_vars tpl_args args of
        Nothing                        -> Nothing
        Just (bind_wrapper, tpl_vals) -> Just (bind_wrapper $
                                               rule_fn `mkApps` tpl_vals)
  where
    rule_fn = occurAnalyseExpr (mkLams tpl_vars rhs)
        -- We could do this when putting things into the rulebase, I guess

---------------------------------------
matchN  :: IdUnfoldingFun
        -> InScopeSet           -- ^ In-scope variables
        -> [Var]                -- ^ Match template type variables
        -> [CoreExpr]           -- ^ Match template
        -> [CoreExpr]           -- ^ Target; can have more elements than the template
        -> Maybe (BindWrapper,  -- Floated bindings; see Note [Matching lets]
                  [CoreExpr])
-- For a given match template and context, find bindings to wrap around
-- the entire result and what should be substituted for each template variable.
-- Fail if there are two few actual arguments from the target to match the template

matchN id_unf in_scope tmpl_vars tmpl_es target_es
  = do  { subst <- go init_menv emptyRuleSubst tmpl_es target_es
        ; return (rs_binds subst,
                  map (lookup_tmpl subst) tmpl_vars') }
  where
    (init_rn_env, tmpl_vars') = mapAccumL rnBndrL (mkRnEnv2 in_scope) tmpl_vars
        -- See Note [Template binders]

    init_menv = RV { rv_tmpls = mkVarSet tmpl_vars', rv_lcl = init_rn_env
                   , rv_fltR = mkEmptySubst (rnInScopeSet init_rn_env)
                   , rv_unf = id_unf }

    go _    subst []     _      = Just subst
    go _    _     _      []     = Nothing       -- Fail if too few actual args
    go menv subst (t:ts) (e:es) = do { subst1 <- match menv subst t e
                                     ; go menv subst1 ts es }

    lookup_tmpl :: RuleSubst -> Var -> CoreExpr
    lookup_tmpl (RS { rs_tv_subst = tv_subst, rs_id_subst = id_subst }) tmpl_var'
        | isId tmpl_var' = case lookupVarEnv id_subst tmpl_var' of
                             Just e -> e
                             _      -> unbound tmpl_var'
        | otherwise      = case lookupVarEnv tv_subst tmpl_var' of
                             Just ty -> Type ty
                             Nothing -> unbound tmpl_var'

    unbound var = pprPanic "Template variable unbound in rewrite rule"
                        (ppr var $$ ppr tmpl_vars $$ ppr tmpl_vars' $$ ppr tmpl_es $$ ppr target_es)

-- * The domain of the TvSubstEnv and IdSubstEnv are the template
--   variables passed into the match.
--
-- * The BindWrapper in a RuleSubst are the bindings floated out
--   from nested matches; see the Let case of match, below
--
data RuleEnv = RV { rv_tmpls :: VarSet          -- Template variables
                  , rv_lcl   :: RnEnv2          -- Renamings for *local bindings*
                                                --   (lambda/case)
                  , rv_fltR  :: Subst           -- Renamings for floated let-bindings
                                                --   domain disjoint from envR of rv_lcl
                                                -- See Note [Matching lets]
                  , rv_unf :: IdUnfoldingFun
                  }

data RuleSubst = RS { rs_tv_subst :: TvSubstEnv   -- Range is the
                    , rs_id_subst :: IdSubstEnv   --   template variables
                    , rs_binds    :: BindWrapper  -- Floated bindings
                    , rs_bndrs    :: VarSet       -- Variables bound by floated lets
                    }

type BindWrapper = CoreExpr -> CoreExpr
  -- See Notes [Matching lets] and [Matching cases]
  -- we represent the floated bindings as a core-to-core function

emptyRuleSubst :: RuleSubst
emptyRuleSubst = RS { rs_tv_subst = emptyVarEnv, rs_id_subst = emptyVarEnv
                    , rs_binds = \e -> e, rs_bndrs = emptyVarSet }

--      At one stage I tried to match even if there are more
--      template args than real args.

--      I now think this is probably a bad idea.
--      Should the template (map f xs) match (map g)?  I think not.
--      For a start, in general eta expansion wastes work.
--      SLPJ July 99


match :: RuleEnv
      -> RuleSubst
      -> CoreExpr               -- Template
      -> CoreExpr               -- Target
      -> Maybe RuleSubst

-- See the notes with Unify.match, which matches types
-- Everything is very similar for terms

-- Interesting examples:
-- Consider matching
--      \x->f      against    \f->f
-- When we meet the lambdas we must remember to rename f to f' in the
-- second expresion.  The RnEnv2 does that.
--
-- Consider matching
--      forall a. \b->b    against   \a->3
-- We must rename the \a.  Otherwise when we meet the lambdas we
-- might substitute [a/b] in the template, and then erroneously
-- succeed in matching what looks like the template variable 'a' against 3.

-- The Var case follows closely what happens in Unify.match
match renv subst (Var v1)    e2 = match_var renv subst v1 e2

match renv subst e1 (Var v2)      -- Note [Expanding variables]
  | not (inRnEnvR rn_env v2) -- Note [Do not expand locally-bound variables]
  , Just e2' <- expandUnfolding_maybe (rv_unf renv v2')
  = match (renv { rv_lcl = nukeRnEnvR rn_env }) subst e1 e2'
  where
    v2'    = lookupRnInScope rn_env v2
    rn_env = rv_lcl renv
        -- Notice that we look up v2 in the in-scope set
        -- See Note [Lookup in-scope]
        -- No need to apply any renaming first (hence no rnOccR)
        -- because of the not-inRnEnvR

match renv subst e1 (Let bind e2)
  | okToFloat (rv_lcl renv) (bindFreeVars bind)        -- See Note [Matching lets]
  = match (renv { rv_fltR = flt_subst' })
          (subst { rs_binds = rs_binds subst . Let bind'
                 , rs_bndrs = extendVarSetList (rs_bndrs subst) new_bndrs })
          e1 e2
  where
    flt_subst = addInScopeSet (rv_fltR renv) (rs_bndrs subst)
    (flt_subst', bind') = substBind flt_subst bind
    new_bndrs = bindersOf bind'

{- Disabled: see Note [Matching cases] below
match renv (tv_subst, id_subst, binds) e1
      (Case scrut case_bndr ty [(con, alt_bndrs, rhs)])
  | exprOkForSpeculation scrut  -- See Note [Matching cases]
  , okToFloat rn_env bndrs (exprFreeVars scrut)
  = match (renv { me_env = rn_env' })
          (tv_subst, id_subst, binds . case_wrap)
          e1 rhs
  where
    rn_env   = me_env renv
    rn_env'  = extendRnInScopeList rn_env bndrs
    bndrs    = case_bndr : alt_bndrs
    case_wrap rhs' = Case scrut case_bndr ty [(con, alt_bndrs, rhs')]
-}

match _ subst (Lit lit1) (Lit lit2)
  | lit1 == lit2
  = Just subst

match renv subst (App f1 a1) (App f2 a2)
  = do  { subst' <- match renv subst f1 f2
        ; match renv subst' a1 a2 }

match renv subst (Lam x1 e1) (Lam x2 e2)
  = match renv' subst e1 e2
  where
    renv' = renv { rv_lcl = rnBndr2 (rv_lcl renv) x1 x2
                 , rv_fltR = delBndr (rv_fltR renv) x2 }

-- This rule does eta expansion
--              (\x.M)  ~  N    iff     M  ~  N x
-- It's important that this is *after* the let rule,
-- so that      (\x.M)  ~  (let y = e in \y.N)
-- does the let thing, and then gets the lam/lam rule above
match renv subst (Lam x1 e1) e2
  = match renv' subst e1 (App e2 (varToCoreExpr new_x))
  where
    (rn_env', new_x) = rnEtaL (rv_lcl renv) x1
    renv' = renv { rv_lcl = rn_env' }

-- Eta expansion the other way
--      M  ~  (\y.N)    iff   M y     ~  N
match renv subst e1 (Lam x2 e2)
  = match renv' subst (App e1 (varToCoreExpr new_x)) e2
  where
    (rn_env', new_x) = rnEtaR (rv_lcl renv) x2
    renv' = renv { rv_lcl = rn_env' }

match renv subst (Case e1 x1 ty1 alts1) (Case e2 x2 ty2 alts2)
  = do  { subst1 <- match_ty renv subst ty1 ty2
        ; subst2 <- match renv subst1 e1 e2
        ; let renv' = rnMatchBndr2 renv subst x1 x2
        ; match_alts renv' subst2 alts1 alts2   -- Alts are both sorted
        }

match renv subst (Type ty1) (Type ty2)
  = match_ty renv subst ty1 ty2
match renv subst (Coercion co1) (Coercion co2)
  = match_co renv subst co1 co2

match renv subst (Cast e1 co1) (Cast e2 co2)
  = do  { subst1 <- match_co renv subst co1 co2
        ; match renv subst1 e1 e2 }

-- Everything else fails
match _ _ _e1 _e2 = -- pprTrace "Failing at" ((text "e1:" <+> ppr _e1) $$ (text "e2:" <+> ppr _e2)) $
                    Nothing

-------------
match_co :: RuleEnv
         -> RuleSubst
         -> Coercion
         -> Coercion
         -> Maybe RuleSubst
match_co renv subst (CoVarCo cv) co
  = match_var renv subst cv (Coercion co)
match_co renv subst (Refl ty1) co
  = case co of
       Refl ty2 -> match_ty renv subst ty1 ty2
       _        -> Nothing
match_co _ _ co1 _
  = pprTrace "match_co: needs more cases" (ppr co1) Nothing
    -- Currently just deals with CoVarCo and Refl

-------------
rnMatchBndr2 :: RuleEnv -> RuleSubst -> Var -> Var -> RuleEnv
rnMatchBndr2 renv subst x1 x2
  = renv { rv_lcl  = rnBndr2 rn_env x1 x2
         , rv_fltR = delBndr (rv_fltR renv) x2 }
  where
    rn_env = addRnInScopeSet (rv_lcl renv) (rs_bndrs subst)
    -- Typically this is a no-op, but it may matter if
    -- there are some floated let-bindings

------------------------------------------
match_alts :: RuleEnv
           -> RuleSubst
           -> [CoreAlt]         -- Template
           -> [CoreAlt]         -- Target
           -> Maybe RuleSubst
match_alts _ subst [] []
  = return subst
match_alts renv subst ((c1,vs1,r1):alts1) ((c2,vs2,r2):alts2)
  | c1 == c2
  = do  { subst1 <- match renv' subst r1 r2
        ; match_alts renv subst1 alts1 alts2 }
  where
    renv' = foldl mb renv (vs1 `zip` vs2)
    mb renv (v1,v2) = rnMatchBndr2 renv subst v1 v2

match_alts _ _ _ _
  = Nothing

------------------------------------------
okToFloat :: RnEnv2 -> VarSet -> Bool
okToFloat rn_env bind_fvs
  = foldVarSet ((&&) . not_captured) True bind_fvs
  where
    not_captured fv = not (inRnEnvR rn_env fv)

------------------------------------------
match_var :: RuleEnv
          -> RuleSubst
          -> Var                -- Template
          -> CoreExpr        -- Target
          -> Maybe RuleSubst
match_var renv@(RV { rv_tmpls = tmpls, rv_lcl = rn_env, rv_fltR = flt_env })
          subst v1 e2
  | v1' `elemVarSet` tmpls
  = match_tmpl_var renv subst v1' e2

  | otherwise   -- v1' is not a template variable; check for an exact match with e2
  = case e2 of  -- Remember, envR of rn_env is disjoint from rv_fltR
       Var v2 | v1' == rnOccR rn_env v2
              -> Just subst

              | Var v2' <- lookupIdSubst (text "match_var") flt_env v2
              , v1' == v2'
              -> Just subst

       _ -> Nothing

  where
    v1' = rnOccL rn_env v1
        -- If the template is
        --      forall x. f x (\x -> x) = ...
        -- Then the x inside the lambda isn't the
        -- template x, so we must rename first!

------------------------------------------
match_tmpl_var :: RuleEnv
               -> RuleSubst
               -> Var                -- Template
               -> CoreExpr              -- Target
               -> Maybe RuleSubst

match_tmpl_var renv@(RV { rv_lcl = rn_env, rv_fltR = flt_env })
               subst@(RS { rs_id_subst = id_subst, rs_bndrs = let_bndrs })
               v1' e2
  | any (inRnEnvR rn_env) (varSetElems (exprFreeVars e2))
  = Nothing     -- Occurs check failure
                -- e.g. match forall a. (\x-> a x) against (\y. y y)

  | Just e1' <- lookupVarEnv id_subst v1'
  = if eqExpr (rnInScopeSet rn_env) e1' e2'
    then Just subst
    else Nothing

  | otherwise
  =             -- Note [Matching variable types]
                -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
                -- However, we must match the *types*; e.g.
                --   forall (c::Char->Int) (x::Char).
                --      f (c x) = "RULE FIRED"
                -- We must only match on args that have the right type
                -- It's actually quite difficult to come up with an example that shows
                -- you need type matching, esp since matching is left-to-right, so type
                -- args get matched first.  But it's possible (e.g. simplrun008) and
                -- this is the Right Thing to do
    do { subst' <- match_ty renv subst (idType v1') (exprType e2)
       ; return (subst' { rs_id_subst = id_subst' }) }
  where
    -- e2' is the result of applying flt_env to e2
    e2' | isEmptyVarSet let_bndrs = e2
        | otherwise = substExpr (text "match_tmpl_var") flt_env e2

    id_subst' = extendVarEnv (rs_id_subst subst) v1' e2'
         -- No further renaming to do on e2',
         -- because no free var of e2' is in the rnEnvR of the envt

------------------------------------------
match_ty :: RuleEnv
         -> RuleSubst
         -> Type                -- Template
         -> Type                -- Target
         -> Maybe RuleSubst
-- Matching Core types: use the matcher in TcType.
-- Notice that we treat newtypes as opaque.  For example, suppose
-- we have a specialised version of a function at a newtype, say
--      newtype T = MkT Int
-- We only want to replace (f T) with f', not (f Int).

match_ty renv subst ty1 ty2
  = do  { tv_subst' <- Unify.ruleMatchTyX menv tv_subst ty1 ty2
        ; return (subst { rs_tv_subst = tv_subst' }) }
  where
    tv_subst = rs_tv_subst subst
    menv = ME { me_tmpls = rv_tmpls renv, me_env = rv_lcl renv }

-- | Report partial matches for rules beginning with the specified
-- string for the purposes of error reporting
ruleCheckProgram :: CompilerPhase               -- ^ Rule activation test
                 -> String                      -- ^ Rule pattern
                 -> RuleBase                    -- ^ Database of rules
                 -> CoreProgram                 -- ^ Bindings to check in
                 -> SDoc                        -- ^ Resulting check message
ruleCheckProgram phase rule_pat rule_base binds
  | isEmptyBag results
  = text "Rule check results: no rule application sites"
  | otherwise
  = vcat [text "Rule check results:",
          line,
          vcat [ p $$ line | p <- bagToList results ]
         ]
  where
    env = RuleCheckEnv { rc_is_active = isActive phase
                       , rc_id_unf    = idUnfolding     -- Not quite right
                                                        -- Should use activeUnfolding
                       , rc_pattern   = rule_pat
                       , rc_rule_base = rule_base }
    results = unionManyBags (map (ruleCheckBind env) binds)
    line = text (replicate 20 '-')

data RuleCheckEnv = RuleCheckEnv {
    rc_is_active :: Activation -> Bool,
    rc_id_unf  :: IdUnfoldingFun,
    rc_pattern :: String,
    rc_rule_base :: RuleBase
}

ruleCheckBind :: RuleCheckEnv -> CoreBind -> Bag SDoc
   -- The Bag returned has one SDoc for each call site found
ruleCheckBind env (NonRec _ r) = ruleCheck env r
ruleCheckBind env (Rec prs)    = unionManyBags [ruleCheck env r | (_,r) <- prs]

ruleCheck :: RuleCheckEnv -> CoreExpr -> Bag SDoc
ruleCheck _   (Var _)       = emptyBag
ruleCheck _   (Lit _)       = emptyBag
ruleCheck _   (Type _)      = emptyBag
ruleCheck _   (Coercion _)  = emptyBag
ruleCheck env (App f a)     = ruleCheckApp env (App f a) []
ruleCheck env (Tick _ e)  = ruleCheck env e
ruleCheck env (Cast e _)    = ruleCheck env e
ruleCheck env (Let bd e)    = ruleCheckBind env bd `unionBags` ruleCheck env e
ruleCheck env (Lam _ e)     = ruleCheck env e
ruleCheck env (Case e _ _ as) = ruleCheck env e `unionBags`
                                unionManyBags [ruleCheck env r | (_,_,r) <- as]

ruleCheckApp :: RuleCheckEnv -> Expr CoreBndr -> [Arg CoreBndr] -> Bag SDoc
ruleCheckApp env (App f a) as = ruleCheck env a `unionBags` ruleCheckApp env f (a:as)
ruleCheckApp env (Var f) as   = ruleCheckFun env f as
ruleCheckApp env other _      = ruleCheck env other

ruleCheckFun :: RuleCheckEnv -> Id -> [CoreExpr] -> Bag SDoc
-- Produce a report for all rules matching the predicate
-- saying why it doesn't match the specified application

ruleCheckFun env fn args
  | null name_match_rules = emptyBag
  | otherwise             = unitBag (ruleAppCheck_help env fn args name_match_rules)
  where
    name_match_rules = filter match (getRules (rc_rule_base env) fn)
    match rule = (rc_pattern env) `isPrefixOf` unpackFS (ruleName rule)

ruleAppCheck_help :: RuleCheckEnv -> Id -> [CoreExpr] -> [CoreRule] -> SDoc
ruleAppCheck_help env fn args rules
  =     -- The rules match the pattern, so we want to print something
    vcat [text "Expression:" <+> ppr (mkApps (Var fn) args),
          vcat (map check_rule rules)]
  where
    n_args = length args
    i_args = args `zip` [1::Int ..]
    rough_args = map roughTopName args

    check_rule rule = rule_herald rule <> colon <+> rule_info rule

    rule_herald (BuiltinRule { ru_name = name })
        = ptext (sLit "Builtin rule") <+> doubleQuotes (ftext name)
    rule_herald (Rule { ru_name = name })
        = ptext (sLit "Rule") <+> doubleQuotes (ftext name)

    rule_info rule
        | Just _ <- matchRule fn noBlackList (rc_id_unf env) emptyInScopeSet args rough_args rule
        = text "matches (which is very peculiar!)"

    rule_info (BuiltinRule {}) = text "does not match"

    rule_info (Rule { ru_act = act,
                      ru_bndrs = rule_bndrs, ru_args = rule_args})
        | not (rc_is_active env act)  = text "active only in later phase"
        | n_args < n_rule_args        = text "too few arguments"
        | n_mismatches == n_rule_args = text "no arguments match"
        | n_mismatches == 0           = text "all arguments match (considered individually), but rule as a whole does not"
        | otherwise                   = text "arguments" <+> ppr mismatches <+> text "do not match (1-indexing)"
        where
          n_rule_args  = length rule_args
          n_mismatches = length mismatches
          mismatches   = [i | (rule_arg, (arg,i)) <- rule_args `zip` i_args,
                              not (isJust (match_fn rule_arg arg))]

          lhs_fvs = exprsFreeVars rule_args     -- Includes template tyvars
          match_fn rule_arg arg = match renv emptyRuleSubst rule_arg arg
                where
                  in_scope = mkInScopeSet (lhs_fvs `unionVarSet` exprFreeVars arg)
                  renv = RV { rv_lcl   = mkRnEnv2 in_scope
                            , rv_tmpls = mkVarSet rule_bndrs
                            , rv_fltR  = mkEmptySubst in_scope
                            , rv_unf   = rc_id_unf env }