Fix #12442.
[ghc.git] / compiler / specialise / Rules.hs
index a768896..7909bdc 100644 (file)
@@ -9,9 +9,6 @@
 -- | 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,
@@ -19,8 +16,8 @@ module Rules (
         -- ** Checking rule applications
         ruleCheckProgram,
 
-        -- ** Manipulating 'SpecInfo' rules
-        mkSpecInfo, extendSpecInfo, addSpecInfo,
+        -- ** Manipulating 'RuleInfo' rules
+        mkRuleInfo, extendRuleInfo, addRuleInfo,
         addIdSpecialisations,
 
         -- * Misc. CoreRule helpers
@@ -32,23 +29,30 @@ module Rules (
 #include "HsVersions.h"
 
 import CoreSyn          -- All of it
+import Module           ( Module, ModuleSet, elemModuleSet )
 import CoreSubst
 import OccurAnal        ( occurAnalyseExpr )
-import CoreFVs          ( exprFreeVars, exprsFreeVars, bindFreeVars, rulesFreeVars )
-import CoreUtils        ( exprType, eqExpr )
+import CoreFVs          ( exprFreeVars, exprsFreeVars, bindFreeVars
+                        , rulesFreeVarsDSet, exprsOrphNames, exprFreeVarsList )
+import CoreUtils        ( exprType, eqExpr, mkTick, mkTicks,
+                          stripTicksTopT, stripTicksTopE )
 import PprCore          ( pprRules )
-import Type             ( Type )
+import Type             ( Type, substTy, mkTCvSubst )
 import TcType           ( tcSplitTyConApp_maybe )
+import TysWiredIn       ( anyTypeOfKind )
 import Coercion
 import CoreTidy         ( tidyRules )
 import Id
-import IdInfo           ( SpecInfo( SpecInfo ) )
+import IdInfo           ( RuleInfo( RuleInfo ) )
+import Var
 import VarEnv
 import VarSet
-import Name             ( Name, NamedThing(..) )
+import Name             ( Name, NamedThing(..), nameIsLocalOrFrom )
+import NameSet
 import NameEnv
-import Unify            ( ruleMatchTyX, MatchEnv(..) )
-import BasicTypes       ( Activation, CompilerPhase, isActive )
+import UniqFM
+import Unify            ( ruleMatchTyKiX )
+import BasicTypes       ( Activation, CompilerPhase, isActive, pprRuleName )
 import StaticFlags      ( opt_PprStyle_Debug )
 import DynFlags         ( DynFlags )
 import Outputable
@@ -58,6 +62,7 @@ import Bag
 import Util
 import Data.List
 import Data.Ord
+import Control.Monad    ( guard )
 
 {-
 Note [Overall plumbing for rules]
@@ -160,16 +165,30 @@ might have a specialisation
 where pi' :: Lift Int# is the specialised version of pi.
 -}
 
-mkRule :: Bool -> Bool -> RuleName -> Activation
+mkRule :: Module -> 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
+mkRule this_mod 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_origin = this_mod,
+           ru_orphan = orph,
            ru_auto = is_auto, ru_local = is_local }
+  where
+        -- Compute orphanhood.  See Note [Orphans] in InstEnv
+        -- A rule is an orphan only if none of the variables
+        -- mentioned on its left-hand side are locally defined
+    lhs_names = extendNameSet (exprsOrphNames args) fn
+
+        -- Since rules get eventually attached to one of the free names
+        -- from the definition when compiling the ABI hash, we should make
+        -- it deterministic. This chooses the one with minimal OccName
+        -- as opposed to uniq value.
+    local_lhs_names = filterNameSet (nameIsLocalOrFrom this_mod) lhs_names
+    orph = chooseOrphanAnchor local_lhs_names
 
 --------------
 roughTopNames :: [CoreExpr] -> [Maybe Name]
@@ -194,6 +213,8 @@ roughTopName (App f _) = roughTopName f
 roughTopName (Var f)   | isGlobalId f   -- Note [Care with roughTopName]
                        , isDataConWorkId f || idArity f > 0
                        = Just (idName f)
+roughTopName (Tick t e) | tickishFloatable t
+                        = roughTopName e
 roughTopName _ = Nothing
 
 ruleCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
@@ -248,42 +269,47 @@ pprRulesForUser rules
 {-
 ************************************************************************
 *                                                                      *
-                SpecInfo: the rules in an IdInfo
+                RuleInfo: the rules in an IdInfo
 *                                                                      *
 ************************************************************************
 -}
 
--- | Make a 'SpecInfo' containing a number of 'CoreRule's, suitable
+-- | Make a 'RuleInfo' containing a number of 'CoreRule's, suitable
 -- for putting into an 'IdInfo'
-mkSpecInfo :: [CoreRule] -> SpecInfo
-mkSpecInfo rules = SpecInfo rules (rulesFreeVars rules)
+mkRuleInfo :: [CoreRule] -> RuleInfo
+mkRuleInfo rules = RuleInfo rules (rulesFreeVarsDSet rules)
 
-extendSpecInfo :: SpecInfo -> [CoreRule] -> SpecInfo
-extendSpecInfo (SpecInfo rs1 fvs1) rs2
-  = SpecInfo (rs2 ++ rs1) (rulesFreeVars rs2 `unionVarSet` fvs1)
+extendRuleInfo :: RuleInfo -> [CoreRule] -> RuleInfo
+extendRuleInfo (RuleInfo rs1 fvs1) rs2
+  = RuleInfo (rs2 ++ rs1) (rulesFreeVarsDSet rs2 `unionDVarSet` fvs1)
 
-addSpecInfo :: SpecInfo -> SpecInfo -> SpecInfo
-addSpecInfo (SpecInfo rs1 fvs1) (SpecInfo rs2 fvs2)
-  = SpecInfo (rs1 ++ rs2) (fvs1 `unionVarSet` fvs2)
+addRuleInfo :: RuleInfo -> RuleInfo -> RuleInfo
+addRuleInfo (RuleInfo rs1 fvs1) (RuleInfo rs2 fvs2)
+  = RuleInfo (rs1 ++ rs2) (fvs1 `unionDVarSet` fvs2)
 
 addIdSpecialisations :: Id -> [CoreRule] -> Id
 addIdSpecialisations id []
   = id
 addIdSpecialisations id rules
   = setIdSpecialisation id $
-    extendSpecInfo (idSpecialisation id) rules
+    extendRuleInfo (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]
+getRules :: RuleEnv -> Id -> [CoreRule]
 -- See Note [Where rules are found]
-getRules rule_base fn
-  = idCoreRules fn ++ imp_rules
+getRules (RuleEnv { re_base = rule_base, re_visible_orphs = orphs }) fn
+  = idCoreRules fn ++ filter (ruleIsVisible orphs) imp_rules
   where
     imp_rules = lookupNameEnv rule_base (idName fn) `orElse` []
 
+ruleIsVisible :: ModuleSet -> CoreRule -> Bool
+ruleIsVisible _ BuiltinRule{} = True
+ruleIsVisible vis_orphs Rule { ru_orphan = orph, ru_origin = origin }
+    = notOrphan orph || origin `elemModuleSet` vis_orphs
+
 {-
 Note [Where rules are found]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -312,10 +338,7 @@ but that isn't quite right:
 ************************************************************************
 -}
 
--- | 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
+-- RuleBase itself is defined in CoreSyn, along with CoreRule
 
 emptyRuleBase :: RuleBase
 emptyRuleBase = emptyNameEnv
@@ -335,8 +358,9 @@ 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 ]
+pprRuleBase rules = pprUFM rules $ \rss ->
+  vcat [ pprRules (tidyRules emptyTidyEnv rs)
+       | rs <- rss ]
 
 {-
 ************************************************************************
@@ -361,20 +385,28 @@ lookupRule dflags in_scope is_active fn args rules
   = -- pprTrace "matchRules" (ppr fn <+> ppr args $$ ppr rules ) $
     case go [] rules of
         []     -> Nothing
-        (m:ms) -> Just (findBest (fn,args) m ms)
+        (m:ms) -> Just (findBest (fn,args') m ms)
   where
     rough_args = map roughTopName args
 
+    -- Strip ticks from arguments, see note [Tick annotations in RULE
+    -- matching]. We only collect ticks if a rule actually matches -
+    -- this matters for performance tests.
+    args' = map (stripTicksTopE tickishFloatable) args
+    ticks = concatMap (stripTicksTopT tickishFloatable) args
+
     go :: [(CoreRule,CoreExpr)] -> [CoreRule] -> [(CoreRule,CoreExpr)]
-    go ms []           = ms
-    go ms (r:rs) = case (matchRule dflags in_scope is_active fn 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
+    go ms [] = ms
+    go ms (r:rs)
+      | Just e <- matchRule dflags in_scope is_active fn args' rough_args r
+      = go ((r,mkTicks ticks e):ms) rs
+      | otherwise
+      = -- 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)
@@ -391,10 +423,10 @@ findBest target (rule1,ans1) ((rule2,ans2):prs)
                         | 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)
+                                   text "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]) $
+                                text "Rule 1:" <+> pp_rule rule1,
+                                text "Rule 2:" <+> pp_rule rule2]) $
                 findBest target (rule1,ans1) prs
   | otherwise = findBest target (rule1,ans1) prs
   where
@@ -414,8 +446,8 @@ isMoreSpecific :: CoreRule -> CoreRule -> Bool
 isMoreSpecific (BuiltinRule {}) _                = False
 isMoreSpecific (Rule {})        (BuiltinRule {}) = True
 isMoreSpecific (Rule { ru_bndrs = bndrs1, ru_args = args1 })
-               (Rule { ru_bndrs = bndrs2, ru_args = args2 })
-  = isJust (matchN (in_scope, id_unfolding_fun) bndrs2 args2 args1)
+               (Rule { ru_bndrs = bndrs2, ru_args = args2, ru_name = rule_name2 })
+  = isJust (matchN (in_scope, id_unfolding_fun) rule_name2 bndrs2 args2 args1)
   where
    id_unfolding_fun _ = NoUnfolding     -- Don't expand in templates
    in_scope = mkInScopeSet (mkVarSet bndrs1)
@@ -452,7 +484,7 @@ matchRule :: DynFlags -> InScopeEnv -> (Activation -> Bool)
 -- then (f args) matches the rule, and the corresponding
 -- rewritten RHS is rhs
 --
--- The bndrs and rhs is occurrence-analysed
+-- The returned expression is occurrence-analysed
 --
 --      Example
 --
@@ -474,17 +506,17 @@ matchRule dflags rule_env _is_active fn args _rough_args
           (BuiltinRule { ru_try = match_fn })
 -- Built-in rules can't be switched off, it seems
   = case match_fn dflags rule_env fn args of
-        Just expr -> Just expr
         Nothing   -> Nothing
+        Just expr -> Just (occurAnalyseExpr expr)
+        -- We could do this when putting things into the rulebase, I guess
 
 matchRule _ in_scope is_active _ args rough_args
-          (Rule { ru_act = act, ru_rough = tpl_tops
-                , ru_bndrs = tpl_vars, ru_args = tpl_args
-                , ru_rhs = rhs })
+          (Rule { ru_name = rule_name, 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 in_scope tpl_vars tpl_args args of
+  = case matchN in_scope rule_name tpl_vars tpl_args args of
         Nothing                        -> Nothing
         Just (bind_wrapper, tpl_vals) -> Just (bind_wrapper $
                                                rule_fn `mkApps` tpl_vals)
@@ -494,8 +526,7 @@ matchRule _ in_scope is_active _ args rough_args
 
 ---------------------------------------
 matchN  :: InScopeEnv
-        -> [Var]                -- ^ Match template type variables
-        -> [CoreExpr]           -- ^ Match template
+        -> RuleName -> [Var] -> [CoreExpr]
         -> [CoreExpr]           -- ^ Target; can have more elements than the template
         -> Maybe (BindWrapper,  -- Floated bindings; see Note [Matching lets]
                   [CoreExpr])
@@ -503,15 +534,15 @@ matchN  :: InScopeEnv
 -- 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 (in_scope, id_unf) tmpl_vars tmpl_es target_es
+matchN (in_scope, id_unf) rule_name 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') }
+        ; let (_, matched_es) = mapAccumL lookup_tmpl subst tmpl_vars
+        ; return (rs_binds subst, matched_es) }
   where
-    (init_rn_env, tmpl_vars') = mapAccumL rnBndrL (mkRnEnv2 in_scope) tmpl_vars
-        -- See Note [Template binders]
+    init_rn_env = mkRnEnv2 (extendInScopeSetList in_scope tmpl_vars)
+                  -- See Note [Template binders]
 
-    init_menv = RV { rv_tmpls = mkVarSet tmpl_vars', rv_lcl = init_rn_env
+    init_menv = RV { rv_tmpls = mkVarSet tmpl_vars, rv_lcl = init_rn_env
                    , rv_fltR = mkEmptySubst (rnInScopeSet init_rn_env)
                    , rv_unf = id_unf }
 
@@ -520,46 +551,94 @@ matchN (in_scope, id_unf) tmpl_vars tmpl_es target_es
     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'
+    lookup_tmpl :: RuleSubst -> Var -> (RuleSubst, CoreExpr)
+    lookup_tmpl rs@(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 -> (rs, e)
+             _      -> unbound tmpl_var
+        | otherwise
+        = case lookupVarEnv tv_subst tmpl_var of
+             Just ty -> (rs, Type ty)
+             Nothing -> (rs { rs_tv_subst = extendVarEnv tv_subst tmpl_var fake_ty }, Type fake_ty)
+             -- See Note [Unbound template type variables]
+        where
+          fake_ty = anyTypeOfKind kind
+          cv_subst = to_co_env id_subst
+          kind = Type.substTy (mkTCvSubst in_scope (tv_subst, cv_subst))
+                              (tyVarKind tmpl_var)
+
+          to_co_env env = nonDetFoldUFM_Directly to_co emptyVarEnv env
+            -- It's OK to use nonDetFoldUFM_Directly because we forget the
+            -- order immediately by creating a new env
+          to_co uniq expr env
+            | Just co <- exprToCoercion_maybe expr
+            = extendVarEnv_Directly env uniq co
 
-    unbound var = pprPanic "Template variable unbound in rewrite rule"
-                        (ppr var $$ ppr tmpl_vars $$ ppr tmpl_vars' $$ ppr tmpl_es $$ ppr target_es)
+            | otherwise
+            = env
+
+    unbound var = pprPanic "Template variable unbound in rewrite rule" $
+                  vcat [ text "Variable:" <+> ppr var
+                       , text "Rule" <+> pprRuleName rule_name
+                       , text "Rule bndrs:" <+> ppr tmpl_vars
+                       , text "LHS args:" <+> ppr tmpl_es
+                       , text "Actual args:" <+> ppr target_es ]
+
+{- Note [Unbound template type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type synonyms with phantom args can give rise to unbound template type
+variables.  Consider this (Trac #10689, simplCore/should_compile/T10689):
+
+    type Foo a b = b
+
+    f :: Eq a => a -> Bool
+    f x = x==x
+
+    {-# RULES "foo" forall (x :: Foo a Char). f x = True #-}
+    finkle = f 'c'
+
+The rule looks like
+   foall (a::*) (d::Eq Char) (x :: Foo a Char).
+         f (Foo a Char) d x = True
+
+Matching the rule won't bind 'a', and legitimately so.  We fudge by
+pretending that 'a' is bound to (Any :: *).
 
-{-
 Note [Template binders]
 ~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following match:
+Consider the following match (example 1):
         Template:  forall x.  f x
-        Target:     f (x+1)
-This should succeed, because the template variable 'x' has
-nothing to do with the 'x' in the target.
+        Target:               f (x+1)
+This should succeed, because the template variable 'x' has nothing to
+do with the 'x' in the target.
 
-On reflection, this case probably does just work, but this might not
+Likewise this one (example 2):
         Template:  forall x. f (\x.x)
-        Target:    f (\y.y)
-Here we want to clone when we find the \x, but to know that x must be in scope
+        Target:              f (\y.y)
 
-To achive this, we use rnBndrL to rename the template variables if
-necessary; the renamed ones are the tmpl_vars'
+We achieve this simply by:
+  * Adding forall'd template binders to the in-scope set
+
+This works even if the template binder are already in scope
+(in the target) because
+
+  * The RuleSubst rs_tv_subst, rs_id_subst maps LHS template vars to
+    the target world.  It is not applied recursively.
+
+  * Having the template vars in the in-scope set ensures that in
+    example 2 above, the (\x.x) is cloned to (\x'. x').
+
+In the past we used rnBndrL to clone the template variables if
+they were already in scope.  But (a) that's not necessary and (b)
+it complicate the fancy footwork for Note [Unbound template type variables]
 
 
 ************************************************************************
 *                                                                      *
                    The main matcher
 *                                                                      *
-************************************************************************
-
-        ---------------------------------------------
-                The inner workings of matching
-        ---------------------------------------------
--}
+********************************************************************* -}
 
 -- * The domain of the TvSubstEnv and IdSubstEnv are the template
 --   variables passed into the match.
@@ -609,6 +688,14 @@ match :: RuleMatchEnv
       -> CoreExpr               -- Target
       -> Maybe RuleSubst
 
+-- We look through certain ticks. See note [Tick annotations in RULE matching]
+match renv subst e1 (Tick t e2)
+  | tickishFloatable t
+  = match renv subst' e1 e2
+  where subst' = subst { rs_binds = rs_binds subst . mkTick t }
+match _ _ e@Tick{} _
+  = pprPanic "Tick in rule" (ppr e)
+
 -- See the notes with Unify.match, which matches types
 -- Everything is very similar for terms
 
@@ -675,10 +762,11 @@ match renv subst (App f1 a1) (App f2 a2)
         ; match renv subst' a1 a2 }
 
 match renv subst (Lam x1 e1) e2
-  | Just (x2, e2) <- exprIsLambda_maybe (rvInScopeEnv renv) e2
+  | Just (x2, e2, ts) <- exprIsLambda_maybe (rvInScopeEnv renv) e2
   = let renv' = renv { rv_lcl = rnBndr2 (rv_lcl renv) x1 x2
                      , rv_fltR = delBndr (rv_fltR renv) x2 }
-    in  match renv' subst e1 e2
+        subst' = subst { rs_binds = rs_binds subst . flip (foldr mkTick) ts }
+    in  match renv' subst' e1 e2
 
 match renv subst (Case e1 x1 ty1 alts1) (Case e2 x2 ty2 alts2)
   = do  { subst1 <- match_ty renv subst ty1 ty2
@@ -706,22 +794,27 @@ match_co :: RuleMatchEnv
          -> Coercion
          -> Coercion
          -> Maybe RuleSubst
-match_co renv subst (CoVarCo cv) co
-  = match_var renv subst cv (Coercion co)
-match_co renv subst (Refl r1 ty1) co
-  = case co of
-       Refl r2 ty2
-         | r1 == r2 -> match_ty renv subst ty1 ty2
-       _            -> Nothing
-match_co renv subst (TyConAppCo r1 tc1 cos1) co2
-  = case co2 of
-       TyConAppCo r2 tc2 cos2
-         | r1 == r2 && tc1 == tc2
-         -> match_cos renv subst cos1 cos2
-       _ -> Nothing
-match_co _ _ co1 co2
-  = pprTrace "match_co: needs more cases" (ppr co1 $$ ppr co2) Nothing
+match_co renv subst co1 co2
+  | Just cv <- getCoVar_maybe co1
+  = match_var renv subst cv (Coercion co2)
+  | Just (ty1, r1) <- isReflCo_maybe co1
+  = do { (ty2, r2) <- isReflCo_maybe co2
+       ; guard (r1 == r2)
+       ; match_ty renv subst ty1 ty2 }
+match_co renv subst co1 co2
+  | Just (tc1, cos1) <- splitTyConAppCo_maybe co1
+  = case splitTyConAppCo_maybe co2 of
+      Just (tc2, cos2)
+        |  tc1 == tc2
+        -> match_cos renv subst cos1 cos2
+      _ -> Nothing
+match_co _ _ _co1 _co2
     -- Currently just deals with CoVarCo, TyConAppCo and Refl
+#ifdef DEBUG
+  = pprTrace "match_co: needs more cases" (ppr _co1 $$ ppr _co2) Nothing
+#else
+  = Nothing
+#endif
 
 match_cos :: RuleMatchEnv
          -> RuleSubst
@@ -729,13 +822,11 @@ match_cos :: RuleMatchEnv
          -> [Coercion]
          -> Maybe RuleSubst
 match_cos renv subst (co1:cos1) (co2:cos2) =
-    case match_co renv subst co1 co2 of
-       Just subst' -> match_cos renv subst' cos1 cos2
-       Nothing -> Nothing
+  do { subst' <- match_co renv subst co1 co2
+     ; match_cos renv subst' cos1 cos2 }
 match_cos _ subst [] [] = Just subst
 match_cos _ _ cos1 cos2 = pprTrace "match_cos: not same length" (ppr cos1 $$ ppr cos2) Nothing
 
-
 -------------
 rnMatchBndr2 :: RuleMatchEnv -> RuleSubst -> Var -> Var -> RuleMatchEnv
 rnMatchBndr2 renv subst x1 x2
@@ -768,7 +859,7 @@ match_alts _ _ _ _
 ------------------------------------------
 okToFloat :: RnEnv2 -> VarSet -> Bool
 okToFloat rn_env bind_fvs
-  = foldVarSet ((&&) . not_captured) True bind_fvs
+  = varSetAll not_captured bind_fvs
   where
     not_captured fv = not (inRnEnvR rn_env fv)
 
@@ -811,7 +902,7 @@ match_tmpl_var :: RuleMatchEnv
 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))
+  | any (inRnEnvR rn_env) (exprFreeVarsList e2)
   = Nothing     -- Occurs check failure
                 -- e.g. match forall a. (\x-> a x) against (\y. y y)
 
@@ -855,11 +946,11 @@ match_ty :: RuleMatchEnv
 -- 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
+  = do  { tv_subst'
+            <- Unify.ruleMatchTyKiX (rv_tmpls renv) (rv_lcl renv) 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 }
 
 {-
 Note [Expanding variables]
@@ -890,10 +981,17 @@ Hence, (a) the guard (not (isLocallyBoundR v2))
 
 Note [Tick annotations in RULE matching]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We used to look through Notes in both template and expression being
-matched.  This would be incorrect for ticks, which we cannot discard,
-so we do not look through Ticks at all.  cf Note [Notes in call
-patterns] in SpecConstr
+
+We used to unconditionally look through Notes in both template and
+expression being matched. This is actually illegal for counting or
+cost-centre-scoped ticks, because we have no place to put them without
+changing entry counts and/or costs. So now we just fail the match in
+these cases.
+
+On the other hand, where we are allowed to insert new cost into the
+tick scope, we can float them upwards to the rule application site.
+
+cf Note [Notes in call patterns] in SpecConstr
 
 Note [Matching lets]
 ~~~~~~~~~~~~~~~~~~~~
@@ -1016,7 +1114,7 @@ is so important.
 -- string for the purposes of error reporting
 ruleCheckProgram :: CompilerPhase               -- ^ Rule activation test
                  -> String                      -- ^ Rule pattern
-                 -> RuleBase                    -- ^ Database of rules
+                 -> RuleEnv                     -- ^ Database of rules
                  -> CoreProgram                 -- ^ Bindings to check in
                  -> SDoc                        -- ^ Resulting check message
 ruleCheckProgram phase rule_pat rule_base binds
@@ -1040,7 +1138,7 @@ data RuleCheckEnv = RuleCheckEnv {
     rc_is_active :: Activation -> Bool,
     rc_id_unf  :: IdUnfoldingFun,
     rc_pattern :: String,
-    rc_rule_base :: RuleBase
+    rc_rule_base :: RuleEnv
 }
 
 ruleCheckBind :: RuleCheckEnv -> CoreBind -> Bag SDoc
@@ -1091,9 +1189,9 @@ ruleAppCheck_help env fn args rules
                       rule_herald rule <> colon <+> rule_info dflags rule
 
     rule_herald (BuiltinRule { ru_name = name })
-        = ptext (sLit "Builtin rule") <+> doubleQuotes (ftext name)
+        = text "Builtin rule" <+> doubleQuotes (ftext name)
     rule_herald (Rule { ru_name = name })
-        = ptext (sLit "Rule") <+> doubleQuotes (ftext name)
+        = text "Rule" <+> doubleQuotes (ftext name)
 
     rule_info dflags rule
         | Just _ <- matchRule dflags (emptyInScopeSet, rc_id_unf env)