GitLab

Simon Peyton Jones pushed to branch wip/T25965 at Glasgow Haskell Compiler / GHC

Commits:

2e204269

by Andreas Klebinger at 2025-04-22T12:20:41+02:00

Simplifier: Constant fold invald tagToEnum# calls to bottom expr.

When applying tagToEnum# to a out-of-range value it's best to simply
constant fold it to a bottom expression. That potentially allows more
dead code elimination and makes debugging easier.

Fixes #25976

7250fc0c

by Matthew Pickering at 2025-04-22T16:24:04-04:00

Move -fno-code note into Downsweep module

This note was left behind when all the code which referred to it was
moved into the GHC.Driver.Downsweep module

d2dc89b4

by Matthew Pickering at 2025-04-22T16:24:04-04:00

Apply editing notes to Note [-fno-code mode] suggested by sheaf

These notes were suggested in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/14241

04f7475e

by Simon Peyton Jones at 2025-04-22T22:13:27+01:00

Fix infelicities in the Specialiser

On the way to #23109 (unary classes) I discovered some infelicities
(or maybe tiny bugs, I forget) in the type-class specialiser.

I also tripped over #25965, an outright bug in the rule matcher

Specifically:

* Refactor: I enhanced `wantCallsFor`, whih previously always said
`True`, to discard calls of class-ops, data constructors etc.  This is
a bit more efficient; and it means we don't need to worry about
filtering them out later.

* Fix: I tidied up some tricky logic that eliminated redundant
  specialisations.  It wasn't working correctly.  See the expanded
  Note [Specialisations already covered], and
  (MP3) in Note [Specialising polymorphic dictionaries].

  See also the new top-level `alreadyCovered`
  function, which now goes via `GHC.Core.Rules.ruleLhsIsMoreSpecific`

  I also added a useful Note [The (CI-KEY) invariant]

* Fix #25965: fixed a tricky bug in the `go_fam_fam` in
  `GHC.Core.Unify.uVarOrFam`, which allows matching to succeed
  without binding all type varibles.

  I enhanced Note [Apartness and type families] some more

* #25703. This ticket "just works" with -fpolymorphic-specialisation;
  but I was surprised that it worked! In this MR I added documentation
  to Note [Interesting dictionary arguments] to explain; and tests to
  ensure it stays fixed.

15 changed files:

compiler/GHC/Core/Opt/ConstantFold.hs
compiler/GHC/Core/Opt/Specialise.hs
compiler/GHC/Core/Rules.hs
compiler/GHC/Core/Unify.hs
compiler/GHC/Driver/Downsweep.hs
compiler/GHC/Driver/Make.hs
compiler/GHC/Tc/Solver/Equality.hs
compiler/GHC/Types/Basic.hs
+ testsuite/tests/simplCore/should_compile/T25703.hs
+ testsuite/tests/simplCore/should_compile/T25703.stderr
+ testsuite/tests/simplCore/should_compile/T25703a.hs
+ testsuite/tests/simplCore/should_compile/T25703a.stderr
+ testsuite/tests/simplCore/should_compile/T25965.hs
+ testsuite/tests/simplCore/should_compile/T25976.hs
testsuite/tests/simplCore/should_compile/all.T

Changes:

compiler/GHC/Core/Opt/ConstantFold.hs

@@ -69,7 +69,6 @@ import GHC.Cmm.MachOp ( FMASign(..) )
  import GHC.Cmm.Type ( Width(..) )
  import GHC.Data.FastString
 -import GHC.Data.Maybe      ( orElse )
  import GHC.Utils.Outputable
  import GHC.Utils.Misc
@@ -1997,6 +1996,14 @@ because we don't expect the user to call tagToEnum# at all; we merely
  generate calls in derived instances of Enum.  So we compromise: a
  rewrite rule rewrites a bad instance of tagToEnum# to an error call,
  and emits a warning.
++
 +We also do something similar if we can see that the argument of tagToEnum is out
 +of bounds, e.g. `tagToEnum# 99# :: Bool`.
 +Replacing this with an error expression is better for two reasons:
 +* It allow us to eliminate more dead code in cases like `case tagToEnum# 99# :: Bool of ...`
 +* Should we actually end up executing the relevant code at runtime the user will
 +  see a meaningful error message, instead of a segfault or incorrect result.
 +See #25976.
  -}
  tagToEnumRule :: RuleM CoreExpr
@@ -2008,9 +2015,13 @@ tagToEnumRule = do
      Just (tycon, tc_args) | isEnumerationTyCon tycon -> do
        let tag = fromInteger i
            correct_tag dc = (dataConTagZ dc) == tag
 -      (dc:rest) <- return $ filter correct_tag (tyConDataCons_maybe tycon `orElse` [])
 -      massert (null rest)
 -      return $ mkTyApps (Var (dataConWorkId dc)) tc_args
 +      Just dataCons <- pure $ tyConDataCons_maybe tycon
 +      case filter correct_tag dataCons of
 +        (dc:rest) -> do
 +          massert (null rest)
 +          pure $ mkTyApps (Var (dataConWorkId dc)) tc_args
 +        -- Literal is out of range, e.g. tagToEnum @Bool #4
 +        [] -> pure $ mkImpossibleExpr ty "tagToEnum: Argument out of range"
      -- See Note [tagToEnum#]
      _ -> warnPprTrace True "tagToEnum# on non-enumeration type" (ppr ty) $

compiler/GHC/Core/Opt/Specialise.hs

@@ -1243,14 +1243,15 @@ specExpr env (Let bind body)
  --     Note [Fire rules in the specialiser]
  fireRewriteRules :: SpecEnv -> InExpr -> [OutExpr] -> (InExpr, [OutExpr])
  fireRewriteRules env (Var f) args
 -  | Just (rule, expr) <- specLookupRule env f args InitialPhase (getRules (se_rules env) f)
 +  | let rules = getRules (se_rules env) f
 +  , Just (rule, expr) <- specLookupRule env f args activeInInitialPhase rules
    , let rest_args    = drop (ruleArity rule) args -- See Note [Extra args in the target]
          zapped_subst = Core.zapSubst (se_subst env)
          expr'        = simpleOptExprWith defaultSimpleOpts zapped_subst expr
                         -- simplOptExpr needed because lookupRule returns
                         --   (\x y. rhs) arg1 arg2
 -  , (fun, args) <- collectArgs expr'
 -  = fireRewriteRules env fun (args++rest_args)
 +  , (fun', args') <- collectArgs expr'
 +  = fireRewriteRules env fun' (args'++rest_args)
  fireRewriteRules _ fun args = (fun, args)
  --------------
@@ -1620,7 +1621,7 @@ specCalls :: Bool              -- True  =>  specialising imported fn
  -- This function checks existing rules, and does not create
  -- duplicate ones. So the caller does not need to do this filtering.
 --- See 'already_covered'
 +-- See `alreadyCovered`
  type SpecInfo = ( [CoreRule]       -- Specialisation rules
                  , [(Id,CoreExpr)]  -- Specialised definition
@@ -1644,15 +1645,13 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs
    = -- pprTrace "specCalls: some" (vcat
      --   [ text "function" <+> ppr fn
 -    --   , text "calls:" <+> ppr calls_for_me
 -    --   , text "subst" <+> ppr (se_subst env) ]) $
 +    --    , text "calls:" <+> ppr calls_for_me
 +    --    , text "subst" <+> ppr (se_subst env) ]) $
      foldlM spec_call ([], [], emptyUDs) calls_for_me
    | otherwise   -- No calls or RHS doesn't fit our preconceptions
 -  = warnPprTrace (not (exprIsTrivial rhs) && notNull calls_for_me && not (isClassOpId fn))
 +  = warnPprTrace (not (exprIsTrivial rhs) && notNull calls_for_me)
            "Missed specialisation opportunity for" (ppr fn $$ trace_doc) $
 -          -- isClassOpId: class-op Ids never inline; we specialise them
 -          -- through fireRewriteRules. So don't complain about missed opportunities
            -- Note [Specialisation shape]
      -- pprTrace "specCalls: none" (ppr fn <+> ppr calls_for_me) $
      return ([], [], emptyUDs)
@@ -1664,6 +1663,10 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs
      fn_unf    = realIdUnfolding fn  -- Ignore loop-breaker-ness here
      inl_prag  = idInlinePragma fn
      inl_act   = inlinePragmaActivation inl_prag
 +    is_active = isActive (beginPhase inl_act) :: Activation -> Bool
 +         -- is_active: inl_act is the activation we are going to put in the new
 +         --   SPEC rule; so we want to see if it is covered by another rule with
 +         --   that same activation.
      is_local  = isLocalId fn
      is_dfun   = isDFunId fn
      dflags    = se_dflags env
@@ -1674,16 +1677,6 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs
      (rhs_bndrs, rhs_body) = collectBindersPushingCo rhs
                              -- See Note [Account for casts in binding]
 -    already_covered :: SpecEnv -> [CoreRule] -> [CoreExpr] -> Bool
 -    already_covered env new_rules args      -- Note [Specialisations already covered]
 -       = isJust (specLookupRule env fn args (beginPhase inl_act)
 -                                (new_rules ++ existing_rules))
 -         -- Rules: we look both in the new_rules (generated by this invocation
 -         --   of specCalls), and in existing_rules (passed in to specCalls)
 -         -- inl_act: is the activation we are going to put in the new SPEC
 -         --   rule; so we want to see if it is covered by another rule with
 -         --   that same activation.
+-
      ----------------------------------------------------------
          -- Specialise to one particular call pattern
      spec_call :: SpecInfo                         -- Accumulating parameter
@@ -1717,8 +1710,12 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs
  --                , ppr dx_binds ]) $
  --             return ()
 +           ; let all_rules = rules_acc ++ existing_rules
 +                 -- all_rules: we look both in the rules_acc (generated by this invocation
 +                 --   of specCalls), and in existing_rules (passed in to specCalls)
             ; if not useful  -- No useful specialisation
 -                || already_covered rhs_env2 rules_acc rule_lhs_args
 +                || alreadyCovered rhs_env2 rule_bndrs fn rule_lhs_args is_active all_rules
 +                   -- See (SC1) in Note [Specialisations already covered]
               then return spec_acc
               else
          do { -- Run the specialiser on the specialised RHS
@@ -1780,7 +1777,7 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs
                   spec_fn_details
                     = case idDetails fn of
                         JoinId join_arity _ -> JoinId (join_arity - join_arity_decr) Nothing
 -                       DFunId is_nt        -> DFunId is_nt
 +                       DFunId unary        -> DFunId unary
                         _                   -> VanillaId
             ; spec_fn <- newSpecIdSM (idName fn) spec_fn_ty spec_fn_details spec_fn_info
@@ -1804,6 +1801,8 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs
                                         , ppr spec_fn  <+> dcolon <+> ppr spec_fn_ty
                                         , ppr rhs_bndrs, ppr call_args
                                         , ppr spec_rule
 +                                       , text "acc" <+> ppr rules_acc
 +                                       , text "existing" <+> ppr existing_rules
+                                        ]
             ; -- pprTrace "spec_call: rule" _rule_trace_doc
@@ -1812,19 +1811,35 @@ specCalls spec_imp env existing_rules calls_for_me fn rhs
                      , spec_uds           `thenUDs` uds_acc
                      ) } }
 +alreadyCovered :: SpecEnv
 +               -> [Var] -> Id -> [CoreExpr]   -- LHS of possible new rule
 +               -> (Activation -> Bool)        -- Which rules are active
 +               -> [CoreRule] -> Bool
 +-- Note [Specialisations already covered] esp (SC2)
 +alreadyCovered env bndrs fn args is_active rules
 +  = case specLookupRule env fn args is_active rules of
 +      Nothing             -> False
 +      Just (rule, _)
 +        | isAutoRule rule -> -- Discard identical rules
 +                             -- We know that (fn args) is an instance of RULE
 +                             -- Check if RULE is an instance of (fn args)
 +                             ruleLhsIsMoreSpecific in_scope bndrs args rule
 +        | otherwise       -> True  -- User rules dominate
 +  where
 +    in_scope = substInScopeSet (se_subst env)
++
  -- Convenience function for invoking lookupRule from Specialise
  -- The SpecEnv's InScopeSet should include all the Vars in the [CoreExpr]
  specLookupRule :: SpecEnv -> Id -> [CoreExpr]
 -               -> CompilerPhase  -- Look up rules as if we were in this phase
 +               -> (Activation -> Bool)  -- Which rules are active
                 -> [CoreRule] -> Maybe (CoreRule, CoreExpr)
 -specLookupRule env fn args phase rules
 +specLookupRule env fn args is_active rules
    = lookupRule ropts in_scope_env is_active fn args rules
    where
      dflags       = se_dflags env
      in_scope     = substInScopeSet (se_subst env)
      in_scope_env = ISE in_scope (whenActiveUnfoldingFun is_active)
      ropts        = initRuleOpts dflags
 -    is_active    = isActive phase
  {- Note [Specialising DFuns]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2323,21 +2338,24 @@ This plan is implemented in the Rec case of specBindItself.
  Note [Specialisations already covered]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  We obviously don't want to generate two specialisations for the same
 -argument pattern.  There are two wrinkles
+-
 -1. We do the already-covered test in specDefn, not when we generate
 -the CallInfo in mkCallUDs.  We used to test in the latter place, but
 -we now iterate the specialiser somewhat, and the Id at the call site
 -might therefore not have all the RULES that we can see in specDefn
+-
 -2. What about two specialisations where the second is an *instance*
 -of the first?  If the more specific one shows up first, we'll generate
 -specialisations for both.  If the *less* specific one shows up first,
 -we *don't* currently generate a specialisation for the more specific
 -one.  (See the call to lookupRule in already_covered.)  Reasons:
 -  (a) lookupRule doesn't say which matches are exact (bad reason)
 -  (b) if the earlier specialisation is user-provided, it's
 -      far from clear that we should auto-specialise further
 +argument pattern.  Wrinkles
++
 +(SC1) We do the already-covered test in specDefn, not when we generate
 +    the CallInfo in mkCallUDs.  We used to test in the latter place, but
 +    we now iterate the specialiser somewhat, and the Id at the call site
 +    might therefore not have all the RULES that we can see in specDefn
++
 +(SC2) What about two specialisations where the second is an *instance*
 +   of the first?  It's a bit arbitrary, but here's what we do:
 +   * If the existing one is user-specified, via a SPECIALISE pragma, we
 +     suppress the further specialisation.
 +   * If the existing one is auto-generated, we generate a second RULE
 +     for the more specialised version.
 +   The latter is important because we don't want the accidental order
 +   of calls to determine what specialisations we generate.
++
 +(SC3) Annoyingly, we /also/ eliminate duplicates in `filterCalls`.
 +   See (MP3) in Note [Specialising polymorphic dictionaries]
  Note [Auto-specialisation and RULES]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2800,12 +2818,10 @@ non-dictionary bindings too.
  Note [Specialising polymorphic dictionaries]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-
  Note June 2023: This has proved to be quite a tricky optimisation to get right
  see (#23469, #23109, #21229, #23445) so it is now guarded by a flag
  `-fpolymorphic-specialisation`.
+-
  Consider
      class M a where { foo :: a -> Int }
@@ -2845,11 +2861,26 @@ Here are the moving parts:
        function.
  (MP3) If we have f :: forall m. Monoid m => blah, and two calls
 -        (f @(Endo b)      (d :: Monoid (Endo b))
 -        (f @(Endo (c->c)) (d :: Monoid (Endo (c->c)))
 +        (f @(Endo b)      (d1 :: Monoid (Endo b))
 +        (f @(Endo (c->c)) (d2 :: Monoid (Endo (c->c)))
        we want to generate a specialisation only for the first.  The second
        is just a substitution instance of the first, with no greater specialisation.
 -      Hence the call to `remove_dups` in `filterCalls`.
 +      Hence the use of `removeDupCalls` in `filterCalls`.
++
 +      You might wonder if `d2` might be more specialised than `d1`; but no.
 +      This `removeDupCalls` thing is at the definition site of `f`, and both `d1`
 +      and `d2` are in scope. So `d1` is simply more polymorphic than `d2`, but
 +      is just as specialised.
++
 +      This distinction is sadly lost once we build a RULE, so `alreadyCovered`
 +      can't be so clever.  E.g if we have an existing RULE
 +            forall @a (d1:Ord Int) (d2: Eq a). f @a @Int d1 d2 = ...
 +      and a putative new rule
 +            forall (d1:Ord Int) (d2: Eq Int). f @Int @Int d1 d2 = ...
 +      we /don't/ want the existing rule to subsume the new one.
++
 +      So we sadly put up with having two rather different places where we
 +      eliminate duplicates: `alreadyCovered` and `removeDupCalls`.
  All this arose in #13873, in the unexpected form that a SPECIALISE
  pragma made the program slower!  The reason was that the specialised
@@ -2947,16 +2978,29 @@ data CallInfoSet = CIS Id (Bag CallInfo)
    -- The list of types and dictionaries is guaranteed to
    -- match the type of f
    -- The Bag may contain duplicate calls (i.e. f @T and another f @T)
 -  -- These dups are eliminated by already_covered in specCalls
 +  -- These dups are eliminated by alreadyCovered in specCalls
  data CallInfo
 -  = CI { ci_key  :: [SpecArg]   -- All arguments
 +  = CI { ci_key  :: [SpecArg]   -- Arguments of the call
 +                                -- See Note [The (CI-KEY) invariant]
++
         , ci_fvs  :: IdSet       -- Free Ids of the ci_key call
                                  -- /not/ including the main id itself, of course
                                  -- NB: excluding tyvars:
                                  --     See Note [Specialising polymorphic dictionaries]
+     }
 +{- Note [The (CI-KEY) invariant]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +Invariant (CI-KEY):
 +   In the `ci_key :: [SpecArg]` field of `CallInfo`,
 +     * The list is non-empty
 +     * The least element is always a `SpecDict`
++
 +In this way the RULE has as few args as possible, which broadens its
 +applicability, since rules only fire when saturated.
 +-}
++
  type DictExpr = CoreExpr
  ciSetFilter :: (CallInfo -> Bool) -> CallInfoSet -> CallInfoSet
@@ -3045,10 +3089,7 @@ mkCallUDs' env f args
      ci_key :: [SpecArg]
      ci_key = dropWhileEndLE (not . isSpecDict) $
               zipWith mk_spec_arg args pis
 -             -- Drop trailing args until we get to a SpecDict
 -             -- In this way the RULE has as few args as possible,
 -             -- which broadens its applicability, since rules only
 -             -- fire when saturated
 +             -- Establish (CI-KEY): drop trailing args until we get to a SpecDict
      mk_spec_arg :: OutExpr -> PiTyBinder -> SpecArg
      mk_spec_arg arg (Named bndr)
@@ -3086,34 +3127,76 @@ site, so we only look through ticks that RULE matching looks through
  -}
  wantCallsFor :: SpecEnv -> Id -> Bool
 -wantCallsFor _env _f = True
 - -- We could reduce the size of the UsageDetails by being less eager
 - -- about collecting calls for LocalIds: there is no point for
 - -- ones that are lambda-bound.  We can't decide this by looking at
 - -- the (absence of an) unfolding, because unfoldings for local
 - -- functions are discarded by cloneBindSM, so no local binder will
 - -- have an unfolding at this stage.  We'd have to keep a candidate
 - -- set of let-binders.
 - --
 - -- Not many lambda-bound variables have dictionary arguments, so
 - -- this would make little difference anyway.
 - --
 - -- For imported Ids we could check for an unfolding, but we have to
 - -- do so anyway in canSpecImport, and it seems better to have it
 - -- all in one place.  So we simply collect usage info for imported
 - -- overloaded functions.
+-
 -{- Note [Interesting dictionary arguments]
 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -Consider this
 -         \a.\d:Eq a.  let f = ... in ...(f d)...
 -There really is not much point in specialising f wrt the dictionary d,
 -because the code for the specialised f is not improved at all, because
 -d is lambda-bound.  We simply get junk specialisations.
+-
 -What is "interesting"?  Just that it has *some* structure.  But what about
 -variables?  We look in the variable's /unfolding/.  And that means
 -that we must be careful to ensure that dictionaries have unfoldings,
 +-- See Note [wantCallsFor]
 +wantCallsFor _env f
 +  = case idDetails f of
 +      RecSelId {}      -> False
 +      DataConWorkId {} -> False
 +      DataConWrapId {} -> False
 +      ClassOpId {}     -> False
 +      PrimOpId {}      -> False
 +      FCallId {}       -> False
 +      TickBoxOpId {}   -> False
 +      CoVarId {}       -> False
++
 +      DFunId {}        -> True
 +      VanillaId {}     -> True
 +      JoinId {}        -> True
 +      WorkerLikeId {}  -> True
 +      RepPolyId {}     -> True
++
 +{- Note [wantCallsFor]
 +~~~~~~~~~~~~~~~~~~~~~~
 +`wantCallsFor env f` says whether the Specialiser should collect calls for
 +function `f`; other thing being equal, the fewer calls we collect the better. It
 +is False for things we can't specialise:
++
 +* ClassOpId: never inline and we don't have a defn to specialise; we specialise
 +  them through fireRewriteRules.
 +* PrimOpId: are never overloaded
 +* Data constructors: we never specialise them
++
 +We could reduce the size of the UsageDetails by being less eager about
 +collecting calls for some LocalIds: there is no point for ones that are
 +lambda-bound.  We can't decide this by looking at the (absence of an) unfolding,
 +because unfoldings for local functions are discarded by cloneBindSM, so no local
 +binder will have an unfolding at this stage.  We'd have to keep a candidate set
 +of let-binders.
++
 +Not many lambda-bound variables have dictionary arguments, so this would make
 +little difference anyway.
++
 +For imported Ids we could check for an unfolding, but we have to do so anyway in
 +canSpecImport, and it seems better to have it all in one place.  So we simply
 +collect usage info for imported overloaded functions.
++
 +Note [Interesting dictionary arguments]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +In `mkCallUDs` we only use `SpecDict` for dictionaries of which
 +`interestingDict` holds.  Otherwise we use `UnspecArg`.  Two reasons:
++
 +* Consider this
 +       \a.\d:Eq a.  let f = ... in ...(f d)...
 +  There really is not much point in specialising f wrt the dictionary d,
 +  because the code for the specialised f is not improved at all, because
 +  d is lambda-bound.  We simply get junk specialisations.
++
 +* Consider this (#25703):
 +     f :: (Eq a, Show b) => a -> b -> INt
 +     goo :: forall x. (Eq x) => x -> blah
 +     goo @x (d:Eq x) (arg:x) = ...(f @x @Int d $fShowInt)...
 +  If we built a `ci_key` with a (SpecDict d) for `d`, we would end up
 +  discarding the call at the `\d`.  But if we use `UnspecArg` for that
 +  uninteresting `d`, we'll get a `ci_key` of
 +      f @x @Int UnspecArg (SpecDict $fShowInt)
 +  and /that/ can float out to f's definition and specialise nicely.
 +  Hooray.  (NB: the call can float only if `-fpolymorphic-specialisation`
 +  is on; otherwise it'll be trapped by the `\@x -> ...`.)(
++
 +What is "interesting"?  (See `interestingDict`.)  Just that it has *some*
 +structure.  But what about variables?  We look in the variable's /unfolding/.
 +And that means that we must be careful to ensure that dictionaries /have/
 +unfoldings,
  * cloneBndrSM discards non-Stable unfoldings
  * specBind updates the unfolding after specialisation
@@ -3159,7 +3242,7 @@ Now `f` turns into:
            meth @a dc ....
  When we specialise `f`, at a=Int say, that superclass selection can
 -nfire (via rewiteClassOps), but that info (that 'dc' is now a
 +fire (via rewiteClassOps), but that info (that 'dc' is now a
  particular dictionary `C`, of type `C Int`) must be available to
  the call `meth @a dc`, so that we can fire the `meth` class-op, and
  thence specialise `wombat`.
@@ -3286,7 +3369,11 @@ dumpUDs :: [CoreBndr] -> UsageDetails -> (UsageDetails, OrdList DictBind)
  -- Used at a lambda or case binder; just dump anything mentioning the binder
  dumpUDs bndrs uds@(MkUD { ud_binds = orig_dbs, ud_calls = orig_calls })
    | null bndrs = (uds, nilOL)  -- Common in case alternatives
 -  | otherwise  = -- pprTrace "dumpUDs" (ppr bndrs $$ ppr free_uds $$ ppr dump_dbs) $
 +  | otherwise  = -- pprTrace "dumpUDs" (vcat
 +                 --    [ text "bndrs" <+> ppr bndrs
 +                 --    , text "uds" <+> ppr uds
 +                 --    , text "free_uds" <+> ppr free_uds
 +                 --    , text "dump-dbs" <+> ppr dump_dbs ]) $
                   (free_uds, dump_dbs)
    where
      free_uds = uds { ud_binds = free_dbs, ud_calls = free_calls }
@@ -3325,20 +3412,17 @@ callsForMe fn uds@MkUD { ud_binds = orig_dbs, ud_calls = orig_calls }
      calls_for_me = case lookupDVarEnv orig_calls fn of
                          Nothing -> []
                          Just cis -> filterCalls cis orig_dbs
 -         -- filterCalls: drop calls that (directly or indirectly)
 -         -- refer to fn.  See Note [Avoiding loops (DFuns)]
  ----------------------
  filterCalls :: CallInfoSet -> FloatedDictBinds -> [CallInfo]
 --- Remove dominated calls (Note [Specialising polymorphic dictionaries])
 --- and loopy DFuns (Note [Avoiding loops (DFuns)])
 +-- Remove
 +--   (a) dominated calls: (MP3) in Note [Specialising polymorphic dictionaries]
 +--   (b) loopy DFuns: Note [Avoiding loops (DFuns)]
  filterCalls (CIS fn call_bag) (FDB { fdb_binds = dbs })
 -  | isDFunId fn  -- Note [Avoiding loops (DFuns)] applies only to DFuns
 -  = filter ok_call de_dupd_calls
 -  | otherwise         -- Do not apply it to non-DFuns
 -  = de_dupd_calls  -- See Note [Avoiding loops (non-DFuns)]
 +  | isDFunId fn  = filter ok_call de_dupd_calls  -- Deals with (b)
 +  | otherwise    = de_dupd_calls
    where
 -    de_dupd_calls = remove_dups call_bag
 +    de_dupd_calls = removeDupCalls call_bag -- Deals with (a)
      dump_set = foldl' go (unitVarSet fn) dbs
        -- This dump-set could also be computed by splitDictBinds
@@ -3352,10 +3436,10 @@ filterCalls (CIS fn call_bag) (FDB { fdb_binds = dbs })
      ok_call (CI { ci_fvs = fvs }) = fvs `disjointVarSet` dump_set
 -remove_dups :: Bag CallInfo -> [CallInfo]
 +removeDupCalls :: Bag CallInfo -> [CallInfo]
  -- Calls involving more generic instances beat more specific ones.
  -- See (MP3) in Note [Specialising polymorphic dictionaries]
 -remove_dups calls = foldr add [] calls
 +removeDupCalls calls = foldr add [] calls
    where
      add :: CallInfo -> [CallInfo] -> [CallInfo]
      add ci [] = [ci]
@@ -3364,12 +3448,20 @@ remove_dups calls = foldr add [] calls
                        | otherwise               = ci2 : add ci1 cis
  beats_or_same :: CallInfo -> CallInfo -> Bool
 +-- (beats_or_same ci1 ci2) is True if specialising on ci1 subsumes ci2
 +-- That is: ci1's types are less specialised than ci2
 +--          ci1   specialises on the same dict args as ci2
  beats_or_same (CI { ci_key = args1 }) (CI { ci_key = args2 })
    = go args1 args2
    where
 -    go [] _ = True
 +    go []           []           = True
      go (arg1:args1) (arg2:args2) = go_arg arg1 arg2 && go args1 args2
 -    go (_:_)        []           = False
++
 +    -- If one or the other runs dry, the other must still have a SpecDict
 +    -- because of the (CI-KEY) invariant.  So neither subsumes the other;
 +    -- one is more specialised (faster code) but the other is more generally
 +    -- applicable.
 +    go  _ _ = False
      go_arg (SpecType ty1) (SpecType ty2) = isJust (tcMatchTy ty1 ty2)
      go_arg UnspecType     UnspecType     = True

compiler/GHC/Core/Rules.hs

@@ -9,7 +9,7 @@
  -- The 'CoreRule' datatype itself is declared elsewhere.
  module GHC.Core.Rules (
          -- ** Looking up rules
 -        lookupRule, matchExprs,
 +        lookupRule, matchExprs, ruleLhsIsMoreSpecific,
          -- ** RuleBase, RuleEnv
          RuleBase, RuleEnv(..), mkRuleEnv, emptyRuleEnv,
@@ -587,8 +587,8 @@ findBest :: InScopeSet -> (Id, [CoreExpr])
  findBest _        _      (rule,ans)   [] = (rule,ans)
  findBest in_scope target (rule1,ans1) ((rule2,ans2):prs)
 -  | isMoreSpecific in_scope rule1 rule2 = findBest in_scope target (rule1,ans1) prs
 -  | isMoreSpecific in_scope rule2 rule1 = findBest in_scope target (rule2,ans2) prs
 +  | ruleIsMoreSpecific in_scope rule1 rule2 = findBest in_scope target (rule1,ans1) prs
 +  | ruleIsMoreSpecific in_scope rule2 rule1 = findBest in_scope target (rule2,ans2) prs
    | debugIsOn = let pp_rule rule
                        = ifPprDebug (ppr rule)
                                     (doubleQuotes (ftext (ruleName rule)))
@@ -603,15 +603,25 @@ findBest in_scope target (rule1,ans1) ((rule2,ans2):prs)
    where
      (fn,args) = target
 -isMoreSpecific :: InScopeSet -> CoreRule -> CoreRule -> Bool
 --- The call (rule1 `isMoreSpecific` rule2)
 +ruleIsMoreSpecific :: InScopeSet -> CoreRule -> CoreRule -> Bool
 +-- The call (rule1 `ruleIsMoreSpecific` rule2)
  -- sees if rule2 can be instantiated to look like rule1
 --- See Note [isMoreSpecific]
 -isMoreSpecific _        (BuiltinRule {}) _                = False
 -isMoreSpecific _        (Rule {})        (BuiltinRule {}) = True
 -isMoreSpecific in_scope (Rule { ru_bndrs = bndrs1, ru_args = args1 })
 -                        (Rule { ru_bndrs = bndrs2, ru_args = args2 })
 -  = isJust (matchExprs in_scope_env bndrs2 args2 args1)
 +-- See Note [ruleIsMoreSpecific]
 +ruleIsMoreSpecific in_scope rule1 rule2
 +  = case rule1 of
 +       BuiltinRule {} -> False
 +       Rule { ru_bndrs = bndrs1, ru_args = args1 }
 +                      -> ruleLhsIsMoreSpecific in_scope bndrs1 args1 rule2
++
 +ruleLhsIsMoreSpecific :: InScopeSet
 +                      -> [Var] -> [CoreExpr]  -- LHS of a possible new rule
 +                      -> CoreRule             -- An existing rule
 +                      -> Bool                 -- New one is more specific
 +ruleLhsIsMoreSpecific in_scope bndrs1 args1 rule2
 +  = case rule2 of
 +       BuiltinRule {} -> True
 +       Rule { ru_bndrs = bndrs2, ru_args = args2 }
 +                      -> isJust (matchExprs in_scope_env bndrs2 args2 args1)
    where
     full_in_scope = in_scope `extendInScopeSetList` bndrs1
     in_scope_env  = ISE full_in_scope noUnfoldingFun
@@ -620,9 +630,9 @@ isMoreSpecific in_scope (Rule { ru_bndrs = bndrs1, ru_args = args1 })
  noBlackList :: Activation -> Bool
  noBlackList _ = False           -- Nothing is black listed
 -{- Note [isMoreSpecific]
 +{- Note [ruleIsMoreSpecific]
  ~~~~~~~~~~~~~~~~~~~~~~~~
 -The call (rule1 `isMoreSpecific` rule2)
 +The call (rule1 `ruleIsMoreSpecific` rule2)
  sees if rule2 can be instantiated to look like rule1.
  Wrinkle:
@@ -825,7 +835,7 @@ bound on the LHS:
    The rule looks like
      forall (a::*) (d::Eq Char) (x :: Foo a Char).
 -         f (Foo a Char) d x = True
 +         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 :: *).

compiler/GHC/Core/Unify.hs

@@ -331,35 +331,57 @@ Wrinkles
     `DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`.  See
     `go_fam` in `uVarOrFam`
 -(ATF6) You might think that when /matching/ the um_fam_env will always be empty,
 -   because type-class-instance and type-family-instance heads can't include type
 -   families.  E.g.   instance C (F a) where ...   -- Illegal
+-
 -   But you'd be wrong: when "improving" type family constraint we may have a
 -   type family on the LHS of a match. Consider
 +(ATF6) When /matching/ can we ever have a type-family application on the LHS, in
 +   the template?  You might think not, because type-class-instance and
 +   type-family-instance heads can't include type families.  E.g.
 +            instance C (F a) where ...  -- Illegal
++
 +   But you'd be wrong: even when matching, we can see type families in the LHS template:
 +   * In `checkValidClass`, in `check_dm` we check that the default method has the
 +      right type, using matching, both ways.  And that type may have type-family
 +      applications in it. Example in test CoOpt_Singletons.
++
 +   * In the specialiser: see the call to `tcMatchTy` in
 +     `GHC.Core.Opt.Specialise.beats_or_same`
++
 +   * With -fpolymorphic-specialsation, we might get a specialiation rule like
 +         RULE forall a (d :: Eq (Maybe (F a))) .
 +                 f @(Maybe (F a)) d = ...
 +     See #25965.
++
 +   * A user-written RULE could conceivably have a type-family application
 +     in the template.  It might not be a good rule, but I don't think we currently
 +     check for this.
++
 +    In all these cases we are only interested in finding a substitution /for
 +    type variables/ that makes the match work.  So we simply want to recurse into
 +    the arguments of the type family.  E.g.
 +       Template:   forall a.  Maybe (F a)
 +       Target:     Mabybe (F Int)
 +    We want to succeed with substitution [a :-> Int].  See (ATF9).
++
 +    Conclusion: where we enter via `tcMatchTy`, `tcMatchTys`, `tc_match_tys`,
 +    etc, we always end up in `tc_match_tys_x`.  There we invoke the unifier
 +    but we do not distinguish between `SurelyApart` and `MaybeApart`. So in
 +    these cases we can set `um_bind_fam_fun` to `neverBindFam`.
++
 +(ATF7) There is one other, very special case of matching where we /do/ want to
 +   bind type families in `um_fam_env`, namely in GHC.Tc.Solver.Equality, the call
 +   to `tcUnifyTyForInjectivity False` in `improve_injective_wanted_top`.
 +   Consider
 +   of a match. Consider
        type family G6 a = r | r -> a
        type instance G6 [a]  = [G a]
        type instance G6 Bool = Int
 -   and the Wanted constraint [W] G6 alpha ~ [Int].  We /match/ each type instance
 -   RHS against [Int]!  So we try
 -        [G a] ~ [Int]
 +   and suppose we haev a Wanted constraint
 +      [W] G6 alpha ~ [Int]
 +.  According to Section 5.2 of "Injective type families for Haskell", we /match/
 +   the RHS each type instance [Int].  So we try
 +        Template: [G a]    Target: [Int]
     and we want to succeed with MaybeApart, so that we can generate the improvement
 -   constraint  [W] alpha ~ [beta]  where beta is fresh.
 -   See Section 5.2 of "Injective type families for Haskell".
+-
 -   A second place that we match with type-fams on the LHS is in `checkValidClass`.
 -   In `check_dm` we check that the default method has the right type, using matching,
 -   both ways.  And that type may have type-family applications in it. Example in
 -   test CoOpt_Singletons.
+-
 -(ATF7) You might think that (ATF6) is a very special case, and in /other/ uses of
 -  matching, where we enter via `tc_match_tys_x` we will never see a type-family
 -  in the template. But actually we do see that case in the specialiser: see
 -  the call to `tcMatchTy` in `GHC.Core.Opt.Specialise.beats_or_same`
+-
 -  Also: a user-written RULE could conceivably have a type-family application
 -  in the template.  It might not be a good rule, but I don't think we currently
 -  check for this.
 +   constraint
 +        [W] alpha ~ [beta]
 +   where beta is fresh.  We do this by binding [G a :-> Int]
  (ATF8) The treatment of type families is governed by
           um_bind_fam_fun :: BindFamFun
@@ -399,6 +421,8 @@ Wrinkles
    Key point: when decomposing (F tys1 ~ F tys2), we should /also/ extend the
    type-family substitution.
 +  (ATF11-1) All this cleverness only matters when unifying, not when matching
++
  (ATF12) There is a horrid exception for the injectivity check. See (UR1) in
    in Note [Specification of unification].
@@ -595,7 +619,7 @@ tc_match_tys_x :: HasDebugCallStack
                 -> [Type]
                 -> Maybe Subst
  tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2
 -  = case tc_unify_tys alwaysBindFam  -- (ATF7) in Note [Apartness and type families]
 +  = case tc_unify_tys neverBindFam  -- (ATF7) in Note [Apartness and type families]
                        bind_tv
                        False  -- Matching, not unifying
                        False  -- Not an injectivity check
@@ -1857,6 +1881,7 @@ uVarOrFam env ty1 ty2 kco
        = go_fam_fam tc1 tys1 tys2 kco
        -- Now check if we can bind the (F tys) to the RHS
 +      -- This can happen even when matching: see (ATF7)
        | BindMe <- um_bind_fam_fun env tc1 tys1 rhs
        = -- ToDo: do we need an occurs check here?
          do { extendFamEnv tc1 tys1 rhs
@@ -1881,11 +1906,6 @@ uVarOrFam env ty1 ty2 kco
      -- go_fam_fam: LHS and RHS are both saturated type-family applications,
      --             for the same type-family F
      go_fam_fam tc tys1 tys2 kco
 -      | tcEqTyConAppArgs tys1 tys2
 -      -- Detect (F tys ~ F tys); otherwise we'd build an infinite substitution
 -      = return ()
+-
 -      | otherwise
         -- Decompose (F tys1 ~ F tys2): (ATF9)
         -- Use injectivity information of F: (ATF10)
         -- But first bind the type-fam if poss: (ATF11)
@@ -1902,13 +1922,19 @@ uVarOrFam env ty1 ty2 kco
         (inj_tys1, noninj_tys1) = partitionByList inj tys1
         (inj_tys2, noninj_tys2) = partitionByList inj tys2
 -       bind_fam_if_poss | BindMe <- um_bind_fam_fun env tc tys1 rhs1
 -                        = extendFamEnv tc tys1 rhs1
 -                        | um_unif env
 -                        , BindMe <- um_bind_fam_fun env tc tys2 rhs2
 -                        = extendFamEnv tc tys2 rhs2
 -                        | otherwise
 -                        = return ()
 +       bind_fam_if_poss
 +         | not (um_unif env)  -- Not when matching (ATF11-1)
 +         = return ()
 +         | tcEqTyConAppArgs tys1 tys2   -- Detect (F tys ~ F tys);
 +         = return ()                    -- otherwise we'd build an infinite substitution
 +         | BindMe <- um_bind_fam_fun env tc tys1 rhs1
 +         = extendFamEnv tc tys1 rhs1
 +         | um_unif env
 +         , BindMe <- um_bind_fam_fun env tc tys2 rhs2
 +         = extendFamEnv tc tys2 rhs2
 +         | otherwise
 +         = return ()
++
         rhs1 = mkTyConApp tc tys2 `mkCastTy` mkSymCo kco
         rhs2 = mkTyConApp tc tys1 `mkCastTy` kco
@@ -1993,7 +2019,7 @@ data UMState = UMState
    -- in um_foralls; i.e. variables bound by foralls inside the types being unified
    -- When /matching/ um_fam_env is usually empty; but not quite always.
 -  -- See (ATF6) and (ATF7) of Note [Apartness and type families]
 +  -- See (ATF7) of Note [Apartness and type families]
  newtype UM a
    = UM' { unUM :: UMState -> UnifyResultM (UMState, a) }

compiler/GHC/Driver/Downsweep.hs

@@ -947,6 +947,71 @@ enableCodeGenWhen logger tmpfs staticLife dynLife unit_env mod_graph = do
                                   hostFullWays
          in dflags_c
 +{- Note [-fno-code mode]
 +~~~~~~~~~~~~~~~~~~~~~~~~
 +GHC offers the flag -fno-code for the purpose of parsing and typechecking a
 +program without generating object files. This is intended to be used by tooling
 +and IDEs to provide quick feedback on any parser or type errors as cheaply as
 +possible.
++
 +When GHC is invoked with -fno-code, no object files or linked output will be
 +generated. As many errors and warnings as possible will be generated, as if
 +-fno-code had not been passed. The session DynFlags will have
 +backend == NoBackend.
++
 +-fwrite-interface
 +~~~~~~~~~~~~~~~~
 +Whether interface files are generated in -fno-code mode is controlled by the
 +-fwrite-interface flag. The -fwrite-interface flag is a no-op if -fno-code is
 +not also passed. Recompilation avoidance requires interface files, so passing
 +-fno-code without -fwrite-interface should be avoided. If -fno-code were
 +re-implemented today, there would be no need for -fwrite-interface as it
 +would considered always on; this behaviour is as it is for backwards compatibility.
++
 +================================================================
 +IN SUMMARY: ALWAYS PASS -fno-code AND -fwrite-interface TOGETHER
 +================================================================
++
 +Template Haskell
 +~~~~~~~~~~~~~~~~
 +A module using Template Haskell may invoke an imported function from inside a
 +splice. This will cause the type-checker to attempt to execute that code, which
 +would fail if no object files had been generated. See #8025. To rectify this,
 +during the downsweep we patch the DynFlags in the ModSummary of any home module
 +that is imported by a module that uses Template Haskell to generate object
 +code.
++
 +The flavour of the generated code depends on whether `-fprefer-byte-code` is enabled
 +or not in the module which needs the code generation. If the module requires byte-code then
 +dependencies will generate byte-code, otherwise they will generate object files.
 +In the case where some modules require byte-code and some object files, both are
 +generated by enabling `-fbyte-code-and-object-code`, the test "fat015" tests these
 +configurations.
++
 +The object files (and interface files if -fwrite-interface is disabled) produced
 +for Template Haskell are written to temporary files.
++
 +Note that since Template Haskell can run arbitrary IO actions, -fno-code mode
 +is no more secure than running without it.
++
 +Potential TODOS:
 +~~~~~
 +* Remove -fwrite-interface and have interface files always written in -fno-code
 +  mode
 +* Both .o and .dyn_o files are generated for template haskell, but we only need
 +  .dyn_o. Fix it.
 +* In make mode, a message like
 +  Compiling A (A.hs, /tmp/ghc_123.o)
 +  is shown if downsweep enabled object code generation for A. Perhaps we should
 +  show "nothing" or "temporary object file" instead. Note that one
 +  can currently use -keep-tmp-files and inspect the generated file with the
 +  current behaviour.
 +* Offer a -no-codedir command line option, and write what were temporary
 +  object files there. This would speed up recompilation.
 +* Use existing object files (if they are up to date) instead of always
 +  generating temporary ones.
 +-}
++
  -- | Populate the Downsweep cache with the root modules.
  mkRootMap
    :: [ModuleNodeInfo]

compiler/GHC/Driver/Make.hs

@@ -1246,70 +1246,6 @@ addSptEntries hsc_env mlinkable =
       , spt <- bc_spt_entries bco
+      ]
 -{- Note [-fno-code mode]
 -~~~~~~~~~~~~~~~~~~~~~~~~
 -GHC offers the flag -fno-code for the purpose of parsing and typechecking a
 -program without generating object files. This is intended to be used by tooling
 -and IDEs to provide quick feedback on any parser or type errors as cheaply as
 -possible.
+-
 -When GHC is invoked with -fno-code no object files or linked output will be
 -generated. As many errors and warnings as possible will be generated, as if
 --fno-code had not been passed. The session DynFlags will have
 -backend == NoBackend.
+-
 --fwrite-interface
 -~~~~~~~~~~~~~~~~
 -Whether interface files are generated in -fno-code mode is controlled by the
 --fwrite-interface flag. The -fwrite-interface flag is a no-op if -fno-code is
 -not also passed. Recompilation avoidance requires interface files, so passing
 --fno-code without -fwrite-interface should be avoided. If -fno-code were
 -re-implemented today, -fwrite-interface would be discarded and it would be
 -considered always on; this behaviour is as it is for backwards compatibility.
+-
 -================================================================
 -IN SUMMARY: ALWAYS PASS -fno-code AND -fwrite-interface TOGETHER
 -================================================================
+-
 -Template Haskell
 -~~~~~~~~~~~~~~~~
 -A module using template haskell may invoke an imported function from inside a
 -splice. This will cause the type-checker to attempt to execute that code, which
 -would fail if no object files had been generated. See #8025. To rectify this,
 -during the downsweep we patch the DynFlags in the ModSummary of any home module
 -that is imported by a module that uses template haskell, to generate object
 -code.
+-
 -The flavour of the generated code depends on whether `-fprefer-byte-code` is enabled
 -or not in the module which needs the code generation. If the module requires byte-code then
 -dependencies will generate byte-code, otherwise they will generate object files.
 -In the case where some modules require byte-code and some object files, both are
 -generated by enabling `-fbyte-code-and-object-code`, the test "fat015" tests these
 -configurations.
+-
 -The object files (and interface files if -fwrite-interface is disabled) produced
 -for template haskell are written to temporary files.
+-
 -Note that since template haskell can run arbitrary IO actions, -fno-code mode
 -is no more secure than running without it.
+-
 -Potential TODOS:
 -~~~~~
 -* Remove -fwrite-interface and have interface files always written in -fno-code
 -  mode
 -* Both .o and .dyn_o files are generated for template haskell, but we only need
 -  .dyn_o. Fix it.
 -* In make mode, a message like
 -  Compiling A (A.hs, /tmp/ghc_123.o)
 -  is shown if downsweep enabled object code generation for A. Perhaps we should
 -  show "nothing" or "temporary object file" instead. Note that one
 -  can currently use -keep-tmp-files and inspect the generated file with the
 -  current behaviour.
 -* Offer a -no-codedir command line option, and write what were temporary
 -  object files there. This would speed up recompilation.
 -* Use existing object files (if they are up to date) instead of always
 -  generating temporary ones.
 --}
  -- Note [When source is considered modified]
  -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

compiler/GHC/Tc/Solver/Equality.hs

@@ -3017,6 +3017,7 @@ improve_wanted_top_fun_eqs fam_tc lhs_tys rhs_ty
  improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon -> [TcType] -> Xi -> TcS [TypeEqn]
  -- Interact with top-level instance declarations
 +-- See Section 5.2 in the Injective Type Families paper
  improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
    = concatMapM do_one branches
    where
@@ -3035,6 +3036,7 @@ improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
      do_one branch@(CoAxBranch { cab_tvs = branch_tvs, cab_lhs = branch_lhs_tys, cab_rhs = branch_rhs })
        | let in_scope1 = in_scope `extendInScopeSetList` branch_tvs
        , Just subst <- tcUnifyTyForInjectivity False in_scope1 branch_rhs rhs_ty
 +                      -- False: matching, not unifying
        = do { let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst
                   unsubstTvs = filterOut inSubst branch_tvs
                   -- The order of unsubstTvs is important; it must be

compiler/GHC/Types/Basic.hs

@@ -85,7 +85,7 @@ module GHC.Types.Basic (
          CompilerPhase(..), PhaseNum, beginPhase, nextPhase, laterPhase,
          Activation(..), isActive, competesWith,
 -        isNeverActive, isAlwaysActive, activeInFinalPhase,
 +        isNeverActive, isAlwaysActive, activeInFinalPhase, activeInInitialPhase,
          activateAfterInitial, activateDuringFinal, activeAfter,
          RuleMatchInfo(..), isConLike, isFunLike,

testsuite/tests/simplCore/should_compile/T25703.hs

 +module T25703 where
++
 +f :: (Eq a, Show b) => a -> b -> Int
 +f x y = f x y
++
 +goo :: forall x. (Eq x) => x -> Int
 +goo arg = f arg (3::Int)

testsuite/tests/simplCore/should_compile/T25703.stderr

	1	+Rule fired: SPEC f @_ @Int (T25703)
	2	+Rule fired: SPEC f @_ @Int (T25703)

testsuite/tests/simplCore/should_compile/T25703a.hs

 +{-# LANGUAGE DataKinds #-}
 +{-# LANGUAGE GADTs #-}
++
 +{-# OPTIONS_GHC -O2 -fspecialise-aggressively #-}
++
 +-- This pragma is just here to pretend that the function body of 'foo' is huge
 +-- and should never be inlined.
 +{-# OPTIONS_GHC -funfolding-use-threshold=-200 #-}
++
 +module T25703a where
++
 +import Data.Kind
 +import Data.Type.Equality
 +import Data.Proxy
 +import GHC.TypeNats
++
 +-- Pretend this is some big dictionary that absolutely must get
 +-- specialised away for performance reasons.
 +type C :: Nat -> Constraint
 +class C i where
 +  meth :: Proxy i -> Double
 +instance C 0 where
 +  meth _ = 0.1
 +instance C 1 where
 +  meth _ = 1.1
 +instance C 2 where
 +  meth _ = 2.1
++
 +{-# INLINEABLE foo #-}
 +foo :: forall a (n :: Nat) (m :: Nat)
 +    .  ( Eq a, C n, C m )
 +    => a -> ( Proxy n, Proxy m ) -> Int -> Double
 +-- Pretend this is a big complicated function, too big to inline,
 +-- for which we absolutely must specialise away the 'C n', 'C m'
 +-- dictionaries for performance reasons.
 +foo a b c
 +  = if a == a
 +    then meth @n Proxy + fromIntegral c
 +    else 2 * meth @m Proxy
++
 +-- Runtime dispatch to a specialisation of 'foo'
 +foo_spec :: forall a (n :: Nat) (m :: Nat)
 +         .  ( Eq a, KnownNat n, KnownNat m )
 +         => a -> ( Proxy n, Proxy m ) -> Int -> Double
 +foo_spec a b c
 +  | Just Refl <- sameNat @n @0 Proxy Proxy
 +  , Just Refl <- sameNat @m @0 Proxy Proxy
 +  = foo @a @0 @0 a b c
 +  | Just Refl <- sameNat @n @0 Proxy Proxy
 +  , Just Refl <- sameNat @m @1 Proxy Proxy
 +  = foo @a @0 @1 a b c
 +  | Just Refl <- sameNat @n @1 Proxy Proxy
 +  , Just Refl <- sameNat @m @1 Proxy Proxy
 +  = foo @a @1 @1 a b c
 +  | Just Refl <- sameNat @n @0 Proxy Proxy
 +  , Just Refl <- sameNat @m @2 Proxy Proxy
 +  = foo @a @0 @2 a b c
 +  | Just Refl <- sameNat @n @1 Proxy Proxy
 +  , Just Refl <- sameNat @m @2 Proxy Proxy
 +  = foo @a @1 @2 a b c
 +  | Just Refl <- sameNat @n @2 Proxy Proxy
 +  , Just Refl <- sameNat @m @2 Proxy Proxy
 +  = foo @a @2 @2 a b c
 +  | otherwise
 +  = error $ unlines
 +      [ "f: no specialisation"
 +      , "n: " ++ show (natVal @n Proxy)
 +      , "m: " ++ show (natVal @m Proxy)
 +      ]

testsuite/tests/simplCore/should_compile/T25703a.stderr

 +Rule fired: SPEC foo @_ @2 @2 (T25703a)
 +Rule fired: SPEC foo @_ @1 @2 (T25703a)
 +Rule fired: SPEC foo @_ @0 @2 (T25703a)
 +Rule fired: SPEC foo @_ @1 @1 (T25703a)
 +Rule fired: SPEC foo @_ @0 @1 (T25703a)
 +Rule fired: SPEC foo @_ @0 @0 (T25703a)

testsuite/tests/simplCore/should_compile/T25965.hs

 +{-# LANGUAGE TypeFamilies #-}
 +{-# OPTIONS_GHC -O -fpolymorphic-specialisation #-}
++
 +module Foo where
++
 +type family F a
++
 +data T a = T1
++
 +instance Eq (T a) where { (==) x y = False }
++
 +foo :: Eq a => a -> Bool
 +foo x | x==x = True
 +      | otherwise = foo x
++
 +bar :: forall b. b -> T (F b) -> Bool
 +bar y x = foo x
++

testsuite/tests/simplCore/should_compile/T25976.hs

 +{-# LANGUAGE MagicHash #-}
++
 +module T25976 where
++
 +import GHC.PrimOps (tagToEnum#)
++
 +-- Spoiler - it's all dead code since tagToEnum 3# is undefined
 +main = case (tagToEnum# 4# :: Bool) of
 +  True -> print "Dead Code"
 +  False -> print "Dead Code"

testsuite/tests/simplCore/should_compile/all.T

@@ -541,3 +541,10 @@ test('T25883', normal, compile_grep_core, [''])
  test('T25883b', normal, compile_grep_core, [''])
  test('T25883c', normal, compile_grep_core, [''])
  test('T25883d', [extra_files(['T25883d_import.hs'])], multimod_compile_filter, ['T25883d', '-O -ddump-simpl -dno-typeable-binds -dsuppress-all -dsuppress-uniques', r'grep -e "y ="'])
++
 +test('T25976', [grep_errmsg('Dead Code')], compile, ['-O -ddump-simpl -dsuppress-uniques -dno-typeable-binds'])
++
 +test('T25965', normal, compile, ['-O'])
 +test('T25703',  [grep_errmsg(r'SPEC')], compile, ['-O -fpolymorphic-specialisation -ddump-rule-firings'])
 +test('T25703a', [grep_errmsg(r'SPEC')], compile, ['-O -fpolymorphic-specialisation -ddump-rule-firings'])
++