{-# LANGUAGE TypeFamilies #-}

{-
(c) The University of Glasgow 2006
(c) The AQUA Project, Glasgow University, 1993-1998

-}

-- | Typechecking rewrite rules
module GHC.Tc.Gen.Rule ( tcRules ) where

import GHC.Prelude

import GHC.Hs
import GHC.Tc.Types
import GHC.Tc.Utils.Monad
import GHC.Tc.Solver
import GHC.Tc.Solver.Monad ( runTcS )
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.TcType
import GHC.Tc.Gen.HsType
import GHC.Tc.Gen.Expr
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Unify( buildImplicationFor )

import GHC.Core.Type
import GHC.Core.Coercion( mkCoVarCo )
import GHC.Core.TyCon( isTypeFamilyTyCon )
import GHC.Core.Predicate

import GHC.Types.Id
import GHC.Types.Var( EvVar, tyVarName )
import GHC.Types.Var.Set
import GHC.Types.Basic ( RuleName, NonStandardDefaultingStrategy(..) )
import GHC.Types.SrcLoc
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.FastString
import GHC.Data.Bag

{-
Note [Typechecking rules]
~~~~~~~~~~~~~~~~~~~~~~~~~
We *infer* the typ of the LHS, and use that type to *check* the type of
the RHS.  That means that higher-rank rules work reasonably well. Here's
an example (test simplCore/should_compile/rule2.hs) produced by Roman:

   foo :: (forall m. m a -> m b) -> m a -> m b
   foo f = ...

   bar :: (forall m. m a -> m a) -> m a -> m a
   bar f = ...

   {-# RULES "foo/bar" foo = bar #-}

He wanted the rule to typecheck.

Note [TcLevel in type checking rules]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Bringing type variables into scope naturally bumps the TcLevel. Thus, we type
check the term-level binders in a bumped level, and we must accordingly bump
the level whenever these binders are in scope.

Note [Re-quantify type variables in rules]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this example from #17710:

  foo :: forall k (a :: k) (b :: k). Proxy a -> Proxy b
  foo x = Proxy
  {-# RULES "foo" forall (x :: Proxy (a :: k)). foo x = Proxy #-}

Written out in more detail, the "foo" rewrite rule looks like this:

  forall k (a :: k). forall (x :: Proxy (a :: k)). foo @k @a @b0 x = Proxy @k @b0

Where b0 is a unification variable. Where should b0 be quantified? We have to
quantify it after k, since (b0 :: k). But generalization usually puts inferred
type variables (such as b0) at the /front/ of the telescope! This creates a
conflict.

One option is to simply throw an error, per the principles of
Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType. This is what would happen
if we were generalising over a normal type signature. On the other hand, the
types in a rewrite rule aren't quite "normal", since the notions of specified
and inferred type variables aren't applicable.

A more permissive design (and the design that GHC uses) is to simply requantify
all of the type variables. That is, we would end up with this:

  forall k (a :: k) (b :: k). forall (x :: Proxy (a :: k)). foo @k @a @b x = Proxy @k @b

It's a bit strange putting the generalized variable `b` after the user-written
variables `k` and `a`. But again, the notion of specificity is not relevant to
rewrite rules, since one cannot "visibly apply" a rewrite rule. This design not
only makes "foo" typecheck, but it also makes the implementation simpler.

See also Note [Generalising in tcTyFamInstEqnGuts] in GHC.Tc.TyCl, which
explains a very similar design when generalising over a type family instance
equation.
-}

tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTc]
tcRules :: [LRuleDecls (GhcPass 'Renamed)] -> TcM [LRuleDecls GhcTc]
tcRules [LRuleDecls (GhcPass 'Renamed)]
decls = (GenLocated SrcSpanAnnA (RuleDecls (GhcPass 'Renamed))
 -> IOEnv
      (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (RuleDecls GhcTc)))
-> [GenLocated SrcSpanAnnA (RuleDecls (GhcPass 'Renamed))]
-> IOEnv
     (Env TcGblEnv TcLclEnv) [GenLocated SrcSpanAnnA (RuleDecls GhcTc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RuleDecls (GhcPass 'Renamed) -> TcM (RuleDecls GhcTc))
-> GenLocated SrcSpanAnnA (RuleDecls (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (RuleDecls GhcTc))
forall a b ann.
(a -> TcM b)
-> GenLocated (SrcSpanAnn' ann) a
-> TcRn (GenLocated (SrcSpanAnn' ann) b)
wrapLocMA RuleDecls (GhcPass 'Renamed) -> TcM (RuleDecls GhcTc)
tcRuleDecls) [LRuleDecls (GhcPass 'Renamed)]
[GenLocated SrcSpanAnnA (RuleDecls (GhcPass 'Renamed))]
decls

tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
tcRuleDecls :: RuleDecls (GhcPass 'Renamed) -> TcM (RuleDecls GhcTc)
tcRuleDecls (HsRules { rds_ext :: forall pass. RuleDecls pass -> XCRuleDecls pass
rds_ext = XCRuleDecls (GhcPass 'Renamed)
src
                     , rds_rules :: forall pass. RuleDecls pass -> [LRuleDecl pass]
rds_rules = [LRuleDecl (GhcPass 'Renamed)]
decls })
   = do { [GenLocated SrcSpanAnnA (RuleDecl GhcTc)]
tc_decls <- (GenLocated SrcSpanAnnA (RuleDecl (GhcPass 'Renamed))
 -> IOEnv
      (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (RuleDecl GhcTc)))
-> [GenLocated SrcSpanAnnA (RuleDecl (GhcPass 'Renamed))]
-> IOEnv
     (Env TcGblEnv TcLclEnv) [GenLocated SrcSpanAnnA (RuleDecl GhcTc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RuleDecl (GhcPass 'Renamed) -> TcM (RuleDecl GhcTc))
-> GenLocated SrcSpanAnnA (RuleDecl (GhcPass 'Renamed))
-> IOEnv
     (Env TcGblEnv TcLclEnv) (GenLocated SrcSpanAnnA (RuleDecl GhcTc))
forall a b ann.
(a -> TcM b)
-> GenLocated (SrcSpanAnn' ann) a
-> TcRn (GenLocated (SrcSpanAnn' ann) b)
wrapLocMA RuleDecl (GhcPass 'Renamed) -> TcM (RuleDecl GhcTc)
tcRule) [LRuleDecl (GhcPass 'Renamed)]
[GenLocated SrcSpanAnnA (RuleDecl (GhcPass 'Renamed))]
decls
        ; RuleDecls GhcTc -> TcM (RuleDecls GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (RuleDecls GhcTc -> TcM (RuleDecls GhcTc))
-> RuleDecls GhcTc -> TcM (RuleDecls GhcTc)
forall a b. (a -> b) -> a -> b
$ HsRules { rds_ext :: XCRuleDecls GhcTc
rds_ext   = XCRuleDecls (GhcPass 'Renamed)
XCRuleDecls GhcTc
src
                           , rds_rules :: [LRuleDecl GhcTc]
rds_rules = [LRuleDecl GhcTc]
[GenLocated SrcSpanAnnA (RuleDecl GhcTc)]
tc_decls } }

tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
tcRule :: RuleDecl (GhcPass 'Renamed) -> TcM (RuleDecl GhcTc)
tcRule (HsRule { rd_ext :: forall pass. RuleDecl pass -> XHsRule pass
rd_ext  = XHsRule (GhcPass 'Renamed)
ext
               , rd_name :: forall pass. RuleDecl pass -> XRec pass RuleName
rd_name = rname :: XRec (GhcPass 'Renamed) RuleName
rname@(L SrcAnn NoEpAnns
_ RuleName
name)
               , rd_act :: forall pass. RuleDecl pass -> Activation
rd_act  = Activation
act
               , rd_tyvs :: forall pass.
RuleDecl pass -> Maybe [LHsTyVarBndr () (NoGhcTc pass)]
rd_tyvs = Maybe [LHsTyVarBndr () (NoGhcTc (GhcPass 'Renamed))]
ty_bndrs
               , rd_tmvs :: forall pass. RuleDecl pass -> [LRuleBndr pass]
rd_tmvs = [LRuleBndr (GhcPass 'Renamed)]
tm_bndrs
               , rd_lhs :: forall pass. RuleDecl pass -> XRec pass (HsExpr pass)
rd_lhs  = XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
lhs
               , rd_rhs :: forall pass. RuleDecl pass -> XRec pass (HsExpr pass)
rd_rhs  = XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
rhs })
  = SDoc -> TcM (RuleDecl GhcTc) -> TcM (RuleDecl GhcTc)
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (RuleName -> SDoc
ruleCtxt RuleName
name)  (TcM (RuleDecl GhcTc) -> TcM (RuleDecl GhcTc))
-> TcM (RuleDecl GhcTc) -> TcM (RuleDecl GhcTc)
forall a b. (a -> b) -> a -> b
$
    do { String -> SDoc -> TcRn ()
traceTc String
"---- Rule ------" (SourceText -> GenLocated (SrcAnn NoEpAnns) RuleName -> SDoc
forall a. SourceText -> GenLocated a RuleName -> SDoc
pprFullRuleName ((HsRuleRn, SourceText) -> SourceText
forall a b. (a, b) -> b
snd (HsRuleRn, SourceText)
XHsRule (GhcPass 'Renamed)
ext) XRec (GhcPass 'Renamed) RuleName
GenLocated (SrcAnn NoEpAnns) RuleName
rname)
       ; SkolemInfo
skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (RuleName -> SkolemInfoAnon
RuleSkol RuleName
name)
        -- Note [Typechecking rules]
       ; (TcLevel
tc_lvl, ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
 WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
 WantedConstraints, Type)
stuff) <- TcM
  ([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
   WantedConstraints, Type)
-> TcM
     (TcLevel,
      ([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
       WantedConstraints, Type))
forall a. TcM a -> TcM (TcLevel, a)
pushTcLevelM (TcM
   ([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
    WantedConstraints, Type)
 -> TcM
      (TcLevel,
       ([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
        WantedConstraints, Type)))
-> TcM
     ([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
      WantedConstraints, Type)
-> TcM
     (TcLevel,
      ([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
       WantedConstraints, Type))
forall a b. (a -> b) -> a -> b
$
                            RuleName
-> Maybe [LHsTyVarBndr () (GhcPass 'Renamed)]
-> [LRuleBndr (GhcPass 'Renamed)]
-> XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
-> XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
-> TcM
     ([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
      WantedConstraints, Type)
generateRuleConstraints RuleName
name Maybe [LHsTyVarBndr () (NoGhcTc (GhcPass 'Renamed))]
Maybe [LHsTyVarBndr () (GhcPass 'Renamed)]
ty_bndrs [LRuleBndr (GhcPass 'Renamed)]
tm_bndrs XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
lhs XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
rhs

       ; let ([TcTyVar]
id_bndrs, GenLocated SrcSpanAnnA (HsExpr GhcTc)
lhs', WantedConstraints
lhs_wanted
                      , GenLocated SrcSpanAnnA (HsExpr GhcTc)
rhs', WantedConstraints
rhs_wanted, Type
rule_ty) = ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
 WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
 WantedConstraints, Type)
stuff

       ; String -> SDoc -> TcRn ()
traceTc String
"tcRule 1" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SourceText -> GenLocated (SrcAnn NoEpAnns) RuleName -> SDoc
forall a. SourceText -> GenLocated a RuleName -> SDoc
pprFullRuleName ((HsRuleRn, SourceText) -> SourceText
forall a b. (a, b) -> b
snd (HsRuleRn, SourceText)
XHsRule (GhcPass 'Renamed)
ext) XRec (GhcPass 'Renamed) RuleName
GenLocated (SrcAnn NoEpAnns) RuleName
rname
                                  , WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
lhs_wanted
                                  , WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
rhs_wanted ])

       ; ([TcTyVar]
lhs_evs, WantedConstraints
residual_lhs_wanted)
            <- RuleName
-> TcLevel
-> WantedConstraints
-> WantedConstraints
-> TcM ([TcTyVar], WantedConstraints)
simplifyRule RuleName
name TcLevel
tc_lvl WantedConstraints
lhs_wanted WantedConstraints
rhs_wanted

       -- SimplifyRule Plan, step 4
       -- Now figure out what to quantify over
       -- c.f. GHC.Tc.Solver.simplifyInfer
       -- We quantify over any tyvars free in *either* the rule
       --  *or* the bound variables.  The latter is important.  Consider
       --      ss (x,(y,z)) = (x,z)
       --      RULE:  forall v. fst (ss v) = fst v
       -- The type of the rhs of the rule is just a, but v::(a,(b,c))
       --
       -- We also need to get the completely-unconstrained tyvars of
       -- the LHS, lest they otherwise get defaulted to Any; but we do that
       -- during zonking (see GHC.Tc.Utils.Zonk.zonkRule)

       ; let tpl_ids :: [TcTyVar]
tpl_ids = [TcTyVar]
lhs_evs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
id_bndrs

       -- See Note [Re-quantify type variables in rules]
       ; CandidatesQTvs
forall_tkvs <- [Type] -> TcM CandidatesQTvs
candidateQTyVarsOfTypes (Type
rule_ty Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: (TcTyVar -> Type) -> [TcTyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> Type
idType [TcTyVar]
tpl_ids)
       ; let don't_default :: TyCoVarSet
don't_default = WantedConstraints -> TyCoVarSet
nonDefaultableTyVarsOfWC WantedConstraints
residual_lhs_wanted
       ; let weed_out :: DVarSet -> DVarSet
weed_out = (DVarSet -> TyCoVarSet -> DVarSet
`dVarSetMinusVarSet` TyCoVarSet
don't_default)
             quant_cands :: CandidatesQTvs
quant_cands = CandidatesQTvs
forall_tkvs { dv_kvs = weed_out (dv_kvs forall_tkvs)
                                       , dv_tvs = weed_out (dv_tvs forall_tkvs) }
       ; [TcTyVar]
qtkvs <- SkolemInfo
-> NonStandardDefaultingStrategy -> CandidatesQTvs -> TcM [TcTyVar]
quantifyTyVars SkolemInfo
skol_info NonStandardDefaultingStrategy
DefaultNonStandardTyVars CandidatesQTvs
quant_cands
       ; String -> SDoc -> TcRn ()
traceTc String
"tcRule" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SourceText -> GenLocated (SrcAnn NoEpAnns) RuleName -> SDoc
forall a. SourceText -> GenLocated a RuleName -> SDoc
pprFullRuleName ((HsRuleRn, SourceText) -> SourceText
forall a b. (a, b) -> b
snd (HsRuleRn, SourceText)
XHsRule (GhcPass 'Renamed)
ext) XRec (GhcPass 'Renamed) RuleName
GenLocated (SrcAnn NoEpAnns) RuleName
rname
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"forall_tkvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CandidatesQTvs -> SDoc
forall a. Outputable a => a -> SDoc
ppr CandidatesQTvs
forall_tkvs
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"quant_cands:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CandidatesQTvs -> SDoc
forall a. Outputable a => a -> SDoc
ppr CandidatesQTvs
quant_cands
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"don't_default:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyCoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVarSet
don't_default
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"residual_lhs_wanted:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
residual_lhs_wanted
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"qtkvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
qtkvs
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rule_ty:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rule_ty
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_bndrs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Maybe [GenLocated SrcSpanAnnA (HsTyVarBndr () (GhcPass 'Renamed))]
-> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe [LHsTyVarBndr () (NoGhcTc (GhcPass 'Renamed))]
Maybe [GenLocated SrcSpanAnnA (HsTyVarBndr () (GhcPass 'Renamed))]
ty_bndrs
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"qtkvs ++ tpl_ids:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([TcTyVar]
qtkvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tpl_ids)
                                , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tpl_id info:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>
                                  [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
id SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcTyVar -> Type
idType TcTyVar
id) | TcTyVar
id <- [TcTyVar]
tpl_ids ]
                  ])

       -- SimplfyRule Plan, step 5
       -- Simplify the LHS and RHS constraints:
       -- For the LHS constraints we must solve the remaining constraints
       -- (a) so that we report insoluble ones
       -- (b) so that we bind any soluble ones
       ; (Bag Implication
lhs_implic, TcEvBinds
lhs_binds) <- TcLevel
-> SkolemInfoAnon
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TcTyVar]
qtkvs
                                         [TcTyVar]
lhs_evs WantedConstraints
residual_lhs_wanted
       ; (Bag Implication
rhs_implic, TcEvBinds
rhs_binds) <- TcLevel
-> SkolemInfoAnon
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TcTyVar]
qtkvs
                                         [TcTyVar]
lhs_evs WantedConstraints
rhs_wanted
       ; Bag Implication -> TcRn ()
emitImplications (Bag Implication
lhs_implic Bag Implication -> Bag Implication -> Bag Implication
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Implication
rhs_implic)
       ; RuleDecl GhcTc -> TcM (RuleDecl GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (RuleDecl GhcTc -> TcM (RuleDecl GhcTc))
-> RuleDecl GhcTc -> TcM (RuleDecl GhcTc)
forall a b. (a -> b) -> a -> b
$ HsRule { rd_ext :: XHsRule GhcTc
rd_ext = XHsRule (GhcPass 'Renamed)
XHsRule GhcTc
ext
                         , rd_name :: XRec GhcTc RuleName
rd_name = XRec (GhcPass 'Renamed) RuleName
XRec GhcTc RuleName
rname
                         , rd_act :: Activation
rd_act = Activation
act
                         , rd_tyvs :: Maybe [LHsTyVarBndr () (NoGhcTc GhcTc)]
rd_tyvs = Maybe [LHsTyVarBndr () (NoGhcTc (GhcPass 'Renamed))]
Maybe [LHsTyVarBndr () (NoGhcTc GhcTc)]
ty_bndrs -- preserved for ppr-ing
                         , rd_tmvs :: [LRuleBndr GhcTc]
rd_tmvs = (TcTyVar -> LocatedAn NoEpAnns (RuleBndr GhcTc))
-> [TcTyVar] -> [LocatedAn NoEpAnns (RuleBndr GhcTc)]
forall a b. (a -> b) -> [a] -> [b]
map (RuleBndr GhcTc -> LocatedAn NoEpAnns (RuleBndr GhcTc)
forall a an. a -> LocatedAn an a
noLocA (RuleBndr GhcTc -> LocatedAn NoEpAnns (RuleBndr GhcTc))
-> (TcTyVar -> RuleBndr GhcTc)
-> TcTyVar
-> LocatedAn NoEpAnns (RuleBndr GhcTc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XCRuleBndr GhcTc -> LIdP GhcTc -> RuleBndr GhcTc
forall pass. XCRuleBndr pass -> LIdP pass -> RuleBndr pass
RuleBndr XCRuleBndr GhcTc
EpAnn [AddEpAnn]
forall a. EpAnn a
noAnn (GenLocated SrcSpanAnnN TcTyVar -> RuleBndr GhcTc)
-> (TcTyVar -> GenLocated SrcSpanAnnN TcTyVar)
-> TcTyVar
-> RuleBndr GhcTc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcTyVar -> GenLocated SrcSpanAnnN TcTyVar
forall a an. a -> LocatedAn an a
noLocA)
                                         ([TcTyVar]
qtkvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tpl_ids)
                         , rd_lhs :: LHsExpr GhcTc
rd_lhs  = TcEvBinds -> LHsExpr GhcTc -> LHsExpr GhcTc
mkHsDictLet TcEvBinds
lhs_binds LHsExpr GhcTc
GenLocated SrcSpanAnnA (HsExpr GhcTc)
lhs'
                         , rd_rhs :: LHsExpr GhcTc
rd_rhs  = TcEvBinds -> LHsExpr GhcTc -> LHsExpr GhcTc
mkHsDictLet TcEvBinds
rhs_binds LHsExpr GhcTc
GenLocated SrcSpanAnnA (HsExpr GhcTc)
rhs' } }

generateRuleConstraints :: FastString
                        -> Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
                        -> LHsExpr GhcRn -> LHsExpr GhcRn
                        -> TcM ( [TcId]
                               , LHsExpr GhcTc, WantedConstraints
                               , LHsExpr GhcTc, WantedConstraints
                               , TcType )
generateRuleConstraints :: RuleName
-> Maybe [LHsTyVarBndr () (GhcPass 'Renamed)]
-> [LRuleBndr (GhcPass 'Renamed)]
-> XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
-> XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
-> TcM
     ([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
      WantedConstraints, Type)
generateRuleConstraints RuleName
rule_name Maybe [LHsTyVarBndr () (GhcPass 'Renamed)]
ty_bndrs [LRuleBndr (GhcPass 'Renamed)]
tm_bndrs XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
lhs XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
rhs
  = do { (([TcTyVar]
tv_bndrs, [TcTyVar]
id_bndrs), WantedConstraints
bndr_wanted) <- TcM ([TcTyVar], [TcTyVar])
-> TcM (([TcTyVar], [TcTyVar]), WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM ([TcTyVar], [TcTyVar])
 -> TcM (([TcTyVar], [TcTyVar]), WantedConstraints))
-> TcM ([TcTyVar], [TcTyVar])
-> TcM (([TcTyVar], [TcTyVar]), WantedConstraints)
forall a b. (a -> b) -> a -> b
$
                                                RuleName
-> Maybe [LHsTyVarBndr () (GhcPass 'Renamed)]
-> [LRuleBndr (GhcPass 'Renamed)]
-> TcM ([TcTyVar], [TcTyVar])
tcRuleBndrs RuleName
rule_name Maybe [LHsTyVarBndr () (GhcPass 'Renamed)]
ty_bndrs [LRuleBndr (GhcPass 'Renamed)]
tm_bndrs
              -- bndr_wanted constraints can include wildcard hole
              -- constraints, which we should not forget about.
              -- It may mention the skolem type variables bound by
              -- the RULE.  c.f. #10072
       ; [(Name, TcTyVar)]
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(TcTyVar -> Name
tyVarName TcTyVar
tv, TcTyVar
tv) | TcTyVar
tv <- [TcTyVar]
tv_bndrs] (TcM
   ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
    WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
    WantedConstraints, Type)
 -> TcM
      ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
       WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
       WantedConstraints, Type))
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
forall a b. (a -> b) -> a -> b
$
         [TcTyVar]
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
forall a. [TcTyVar] -> TcM a -> TcM a
tcExtendIdEnv    [TcTyVar]
id_bndrs (TcM
   ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
    WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
    WantedConstraints, Type)
 -> TcM
      ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
       WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
       WantedConstraints, Type))
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
forall a b. (a -> b) -> a -> b
$
    do { -- See Note [Solve order for RULES]
         ((GenLocated SrcSpanAnnA (HsExpr GhcTc)
lhs', Type
rule_ty), WantedConstraints
lhs_wanted) <- TcM (GenLocated SrcSpanAnnA (HsExpr GhcTc), Type)
-> TcM
     ((GenLocated SrcSpanAnnA (HsExpr GhcTc), Type), WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
-> TcM (LHsExpr GhcTc, Type)
tcInferRho XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
lhs)
       ; (GenLocated SrcSpanAnnA (HsExpr GhcTc)
rhs',            WantedConstraints
rhs_wanted) <- TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc, WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc, WantedConstraints))
-> TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc, WantedConstraints)
forall a b. (a -> b) -> a -> b
$
                                          XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
-> Type -> TcM (LHsExpr GhcTc)
tcCheckMonoExpr XRec (GhcPass 'Renamed) (HsExpr (GhcPass 'Renamed))
rhs Type
rule_ty
       ; let all_lhs_wanted :: WantedConstraints
all_lhs_wanted = WantedConstraints
bndr_wanted WantedConstraints -> WantedConstraints -> WantedConstraints
`andWC` WantedConstraints
lhs_wanted
       ; ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
 WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
 WantedConstraints, Type)
-> TcM
     ([TcTyVar], GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, GenLocated SrcSpanAnnA (HsExpr GhcTc),
      WantedConstraints, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
id_bndrs, GenLocated SrcSpanAnnA (HsExpr GhcTc)
lhs', WantedConstraints
all_lhs_wanted, GenLocated SrcSpanAnnA (HsExpr GhcTc)
rhs', WantedConstraints
rhs_wanted, Type
rule_ty) } }

-- See Note [TcLevel in type checking rules]
tcRuleBndrs :: FastString -> Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
            -> TcM ([TcTyVar], [Id])
tcRuleBndrs :: RuleName
-> Maybe [LHsTyVarBndr () (GhcPass 'Renamed)]
-> [LRuleBndr (GhcPass 'Renamed)]
-> TcM ([TcTyVar], [TcTyVar])
tcRuleBndrs RuleName
rule_name (Just [LHsTyVarBndr () (GhcPass 'Renamed)]
bndrs) [LRuleBndr (GhcPass 'Renamed)]
xs
  = do { SkolemInfo
skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (RuleName -> SkolemInfoAnon
RuleSkol RuleName
rule_name)
       ; ([VarBndr TcTyVar ()]
tybndrs1,([TcTyVar]
tys2,[TcTyVar]
tms)) <- SkolemInfo
-> [LHsTyVarBndr () (GhcPass 'Renamed)]
-> TcM ([TcTyVar], [TcTyVar])
-> TcM ([VarBndr TcTyVar ()], ([TcTyVar], [TcTyVar]))
forall flag a.
OutputableBndrFlag flag 'Renamed =>
SkolemInfo
-> [LHsTyVarBndr flag (GhcPass 'Renamed)]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Skol SkolemInfo
skol_info [LHsTyVarBndr () (GhcPass 'Renamed)]
bndrs (TcM ([TcTyVar], [TcTyVar])
 -> TcM ([VarBndr TcTyVar ()], ([TcTyVar], [TcTyVar])))
-> TcM ([TcTyVar], [TcTyVar])
-> TcM ([VarBndr TcTyVar ()], ([TcTyVar], [TcTyVar]))
forall a b. (a -> b) -> a -> b
$
                                  RuleName
-> [LRuleBndr (GhcPass 'Renamed)] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs RuleName
rule_name [LRuleBndr (GhcPass 'Renamed)]
xs
       ; let tys1 :: [TcTyVar]
tys1 = [VarBndr TcTyVar ()] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr TcTyVar ()]
tybndrs1
       ; ([TcTyVar], [TcTyVar]) -> TcM ([TcTyVar], [TcTyVar])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
tys1 [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tys2, [TcTyVar]
tms) }

tcRuleBndrs RuleName
rule_name Maybe [LHsTyVarBndr () (GhcPass 'Renamed)]
Nothing [LRuleBndr (GhcPass 'Renamed)]
xs
  = RuleName
-> [LRuleBndr (GhcPass 'Renamed)] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs RuleName
rule_name [LRuleBndr (GhcPass 'Renamed)]
xs

-- See Note [TcLevel in type checking rules]
tcRuleTmBndrs :: FastString -> [LRuleBndr GhcRn] -> TcM ([TcTyVar],[Id])
tcRuleTmBndrs :: RuleName
-> [LRuleBndr (GhcPass 'Renamed)] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs RuleName
_ [] = ([TcTyVar], [TcTyVar]) -> TcM ([TcTyVar], [TcTyVar])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([],[])
tcRuleTmBndrs RuleName
rule_name (L SrcAnn NoEpAnns
_ (RuleBndr XCRuleBndr (GhcPass 'Renamed)
_ (L SrcSpanAnnN
_ Name
name)) : [LRuleBndr (GhcPass 'Renamed)]
rule_bndrs)
  = do  { Type
ty <- TcM Type
newOpenFlexiTyVarTy
        ; ([TcTyVar]
tyvars, [TcTyVar]
tmvars) <- RuleName
-> [LRuleBndr (GhcPass 'Renamed)] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs RuleName
rule_name [LRuleBndr (GhcPass 'Renamed)]
rule_bndrs
        ; ([TcTyVar], [TcTyVar]) -> TcM ([TcTyVar], [TcTyVar])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
tyvars, (() :: Constraint) => Name -> Type -> Type -> TcTyVar
Name -> Type -> Type -> TcTyVar
mkLocalId Name
name Type
ManyTy Type
ty TcTyVar -> [TcTyVar] -> [TcTyVar]
forall a. a -> [a] -> [a]
: [TcTyVar]
tmvars) }
tcRuleTmBndrs RuleName
rule_name (L SrcAnn NoEpAnns
_ (RuleBndrSig XRuleBndrSig (GhcPass 'Renamed)
_ (L SrcSpanAnnN
_ Name
name) HsPatSigType (GhcPass 'Renamed)
rn_ty) : [LRuleBndr (GhcPass 'Renamed)]
rule_bndrs)
--  e.g         x :: a->a
--  The tyvar 'a' is brought into scope first, just as if you'd written
--              a::*, x :: a->a
--  If there's an explicit forall, the renamer would have already reported an
--   error for each out-of-scope type variable used
  = do  { let ctxt :: UserTypeCtxt
ctxt = RuleName -> Name -> UserTypeCtxt
RuleSigCtxt RuleName
rule_name Name
name
        ; ([(Name, TcTyVar)]
_ , [(Name, TcTyVar)]
tvs, Type
id_ty) <- UserTypeCtxt
-> HoleMode
-> HsPatSigType (GhcPass 'Renamed)
-> ContextKind
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
tcHsPatSigType UserTypeCtxt
ctxt HoleMode
HM_Sig HsPatSigType (GhcPass 'Renamed)
rn_ty ContextKind
OpenKind
        ; let id :: TcTyVar
id  = (() :: Constraint) => Name -> Type -> Type -> TcTyVar
Name -> Type -> Type -> TcTyVar
mkLocalId Name
name Type
ManyTy Type
id_ty
                    -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType

              -- The type variables scope over subsequent bindings; yuk
        ; ([TcTyVar]
tyvars, [TcTyVar]
tmvars) <- [(Name, TcTyVar)]
-> TcM ([TcTyVar], [TcTyVar]) -> TcM ([TcTyVar], [TcTyVar])
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, TcTyVar)]
tvs (TcM ([TcTyVar], [TcTyVar]) -> TcM ([TcTyVar], [TcTyVar]))
-> TcM ([TcTyVar], [TcTyVar]) -> TcM ([TcTyVar], [TcTyVar])
forall a b. (a -> b) -> a -> b
$
                                   RuleName
-> [LRuleBndr (GhcPass 'Renamed)] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs RuleName
rule_name [LRuleBndr (GhcPass 'Renamed)]
rule_bndrs
        ; ([TcTyVar], [TcTyVar]) -> TcM ([TcTyVar], [TcTyVar])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TcTyVar) -> TcTyVar) -> [(Name, TcTyVar)] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TcTyVar) -> TcTyVar
forall a b. (a, b) -> b
snd [(Name, TcTyVar)]
tvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tyvars, TcTyVar
id TcTyVar -> [TcTyVar] -> [TcTyVar]
forall a. a -> [a] -> [a]
: [TcTyVar]
tmvars) }

ruleCtxt :: FastString -> SDoc
ruleCtxt :: RuleName -> SDoc
ruleCtxt RuleName
name = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"When checking the rewrite rule" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>
                SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
doubleQuotes (RuleName -> SDoc
forall doc. IsLine doc => RuleName -> doc
ftext RuleName
name)


{-
*********************************************************************************
*                                                                                 *
              Constraint simplification for rules
*                                                                                 *
***********************************************************************************

Note [The SimplifyRule Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Example.  Consider the following left-hand side of a rule
        f (x == y) (y > z) = ...
If we typecheck this expression we get constraints
        d1 :: Ord a, d2 :: Eq a
We do NOT want to "simplify" to the LHS
        forall x::a, y::a, z::a, d1::Ord a.
          f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
Instead we want
        forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
          f ((==) d2 x y) ((>) d1 y z) = ...

Here is another example:
        fromIntegral :: (Integral a, Num b) => a -> b
        {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
we *dont* want to get
        forall dIntegralInt.
           fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
because the scsel will mess up RULE matching.  Instead we want
        forall dIntegralInt, dNumInt.
          fromIntegral Int Int dIntegralInt dNumInt = id Int

Even if we have
        g (x == y) (y == z) = ..
where the two dictionaries are *identical*, we do NOT WANT
        forall x::a, y::a, z::a, d1::Eq a
          f ((==) d1 x y) ((>) d1 y z) = ...
because that will only match if the dict args are (visibly) equal.
Instead we want to quantify over the dictionaries separately.

In short, simplifyRuleLhs must *only* squash equalities, leaving
all dicts unchanged, with absolutely no sharing.

Also note that we can't solve the LHS constraints in isolation:
Example   foo :: Ord a => a -> a
          foo_spec :: Int -> Int
          {-# RULE "foo"  foo = foo_spec #-}
Here, it's the RHS that fixes the type variable

HOWEVER, under a nested implication things are different
Consider
  f :: (forall a. Eq a => a->a) -> Bool -> ...
  {-# RULES "foo" forall (v::forall b. Eq b => b->b).
       f b True = ...
    #-}
Here we *must* solve the wanted (Eq a) from the given (Eq a)
resulting from skolemising the argument type of g.  So we
revert to SimplCheck when going under an implication.


--------- So the SimplifyRule Plan is this -----------------------

* Step 0: typecheck the LHS and RHS to get constraints from each

* Step 1: Simplify the LHS and RHS constraints all together in one bag,
          but /discarding/ the simplified constraints. We do this only
          to discover all unification equalities.

* Step 2: Zonk the ORIGINAL (unsimplified) LHS constraints, to take
          advantage of those unifications

* Setp 3: Partition the LHS constraints into the ones we will
          quantify over, and the others.
          See Note [RULE quantification over equalities]

* Step 4: Decide on the type variables to quantify over

* Step 5: Simplify the LHS and RHS constraints separately, using the
          quantified constraints as givens

Note [Solve order for RULES]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In step 1 above, we need to be a bit careful about solve order.
Consider
   f :: Int -> T Int
   type instance T Int = Bool

   RULE f 3 = True

From the RULE we get
   lhs-constraints:  T Int ~ alpha
   rhs-constraints:  Bool ~ alpha
where 'alpha' is the type that connects the two.  If we glom them
all together, and solve the RHS constraint first, we might solve
with alpha := Bool.  But then we'd end up with a RULE like

    RULE: f 3 |> (co :: T Int ~ Bool) = True

which is terrible.  We want

    RULE: f 3 = True |> (sym co :: Bool ~ T Int)

So we are careful to solve the LHS constraints first, and *then* the
RHS constraints.  Actually much of this is done by the on-the-fly
constraint solving, so the same order must be observed in
tcRule.


Note [RULE quantification over equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Deciding which equalities to quantify over is tricky:
 * We do not want to quantify over insoluble equalities (Int ~ Bool)
    (a) because we prefer to report a LHS type error
    (b) because if such things end up in 'givens' we get a bogus
        "inaccessible code" error

 * But we do want to quantify over things like (a ~ F b), where
   F is a type function.

The difficulty is that it's hard to tell what is insoluble!
So we see whether the simplification step yielded any type errors,
and if so refrain from quantifying over *any* equalities.

Note [Quantifying over coercion holes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality constraints from the LHS will emit coercion hole Wanteds.
These don't have a name, so we can't quantify over them directly.
Instead, because we really do want to quantify here, invent a new
EvVar for the coercion, fill the hole with the invented EvVar, and
then quantify over the EvVar. Not too tricky -- just some
impedance matching, really.

Note [Simplify cloned constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At this stage, we're simplifying constraints only for insolubility
and for unification. Note that all the evidence is quickly discarded.
We use a clone of the real constraint. If we don't do this,
then RHS coercion-hole constraints get filled in, only to get filled
in *again* when solving the implications emitted from tcRule. That's
terrible, so we avoid the problem by cloning the constraints.

-}

simplifyRule :: RuleName
             -> TcLevel                 -- Level at which to solve the constraints
             -> WantedConstraints       -- Constraints from LHS
             -> WantedConstraints       -- Constraints from RHS
             -> TcM ( [EvVar]               -- Quantify over these LHS vars
                    , WantedConstraints)    -- Residual un-quantified LHS constraints
-- See Note [The SimplifyRule Plan]
-- NB: This consumes all simple constraints on the LHS, but not
-- any LHS implication constraints.
simplifyRule :: RuleName
-> TcLevel
-> WantedConstraints
-> WantedConstraints
-> TcM ([TcTyVar], WantedConstraints)
simplifyRule RuleName
name TcLevel
tc_lvl WantedConstraints
lhs_wanted WantedConstraints
rhs_wanted
  = do {
       -- Note [The SimplifyRule Plan] step 1
       -- First solve the LHS and *then* solve the RHS
       -- Crucially, this performs unifications
       -- Why clone?  See Note [Simplify cloned constraints]
       ; WantedConstraints
lhs_clone <- WantedConstraints -> TcM WantedConstraints
cloneWC WantedConstraints
lhs_wanted
       ; WantedConstraints
rhs_clone <- WantedConstraints -> TcM WantedConstraints
cloneWC WantedConstraints
rhs_wanted
       ; TcLevel -> TcRn () -> TcRn ()
forall a. TcLevel -> TcM a -> TcM a
setTcLevel TcLevel
tc_lvl (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         TcM ((), EvBindMap) -> TcRn ()
forall a. TcM a -> TcRn ()
discardResult     (TcM ((), EvBindMap) -> TcRn ()) -> TcM ((), EvBindMap) -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         TcS () -> TcM ((), EvBindMap)
forall a. TcS a -> TcM (a, EvBindMap)
runTcS            (TcS () -> TcM ((), EvBindMap)) -> TcS () -> TcM ((), EvBindMap)
forall a b. (a -> b) -> a -> b
$
         do { WantedConstraints
_ <- WantedConstraints -> TcS WantedConstraints
solveWanteds WantedConstraints
lhs_clone
            ; WantedConstraints
_ <- WantedConstraints -> TcS WantedConstraints
solveWanteds WantedConstraints
rhs_clone
                  -- Why do them separately?
                  -- See Note [Solve order for RULES]
            ; () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return () }

       -- Note [The SimplifyRule Plan] step 2
       ; WantedConstraints
lhs_wanted <- WantedConstraints -> TcM WantedConstraints
zonkWC WantedConstraints
lhs_wanted
       ; let (Cts
quant_cts, WantedConstraints
residual_lhs_wanted) = WantedConstraints -> (Cts, WantedConstraints)
getRuleQuantCts WantedConstraints
lhs_wanted

       -- Note [The SimplifyRule Plan] step 3
       ; [TcTyVar]
quant_evs <- (Ct -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Ct] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Ct -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
mk_quant_ev (Cts -> [Ct]
forall a. Bag a -> [a]
bagToList Cts
quant_cts)

       ; String -> SDoc -> TcRn ()
traceTc String
"simplifyRule" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"LHS of rule" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
doubleQuotes (RuleName -> SDoc
forall doc. IsLine doc => RuleName -> doc
ftext RuleName
name)
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"lhs_wanted" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
lhs_wanted
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rhs_wanted" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
rhs_wanted
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"quant_cts" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
quant_cts
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"residual_lhs_wanted" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
residual_lhs_wanted
              ]

       ; ([TcTyVar], WantedConstraints)
-> TcM ([TcTyVar], WantedConstraints)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
quant_evs, WantedConstraints
residual_lhs_wanted) }

  where
    mk_quant_ev :: Ct -> TcM EvVar
    mk_quant_ev :: Ct -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
mk_quant_ev Ct
ct
      | CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_pred :: CtEvidence -> Type
ctev_pred = Type
pred } <- Ct -> CtEvidence
ctEvidence Ct
ct
      = case TcEvDest
dest of
          EvVarDest TcTyVar
ev_id -> TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
ev_id
          HoleDest CoercionHole
hole   -> -- See Note [Quantifying over coercion holes]
                             do { TcTyVar
ev_id <- Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall gbl lcl. Type -> TcRnIf gbl lcl TcTyVar
newEvVar Type
pred
                                ; CoercionHole -> Coercion -> TcRn ()
fillCoercionHole CoercionHole
hole (TcTyVar -> Coercion
mkCoVarCo TcTyVar
ev_id)
                                ; TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
ev_id }
    mk_quant_ev Ct
ct = String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mk_quant_ev" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)


getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
-- Extract all the constraints we can quantify over,
--   also returning the depleted WantedConstraints
--
-- NB: we must look inside implications, because with
--     -fdefer-type-errors we generate implications rather eagerly;
--     see GHC.Tc.Utils.Unify.implicationNeeded. Not doing so caused #14732.
--
-- Unlike simplifyInfer, we don't leave the WantedConstraints unchanged,
--   and attempt to solve them from the quantified constraints.  That
--   nearly works, but fails for a constraint like (d :: Eq Int).
--   We /do/ want to quantify over it, but the short-cut solver
--   (see GHC.Tc.Solver.Interact Note [Shortcut solving]) ignores the quantified
--   and instead solves from the top level.
--
--   So we must partition the WantedConstraints ourselves
--   Not hard, but tiresome.

getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
getRuleQuantCts WantedConstraints
wc
  = TyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc TyCoVarSet
emptyVarSet WantedConstraints
wc
  where
    float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
    float_wc :: TyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc TyCoVarSet
skol_tvs (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics, wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
      = ( Cts
simple_yes Cts -> Cts -> Cts
`andCts` Cts
implic_yes
        , WantedConstraints
emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_errors = errs })
     where
        (Cts
simple_yes, Cts
simple_no) = (Ct -> Bool) -> Cts -> (Cts, Cts)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag (TyCoVarSet -> Ct -> Bool
rule_quant_ct TyCoVarSet
skol_tvs) Cts
simples
        (Cts
implic_yes, Bag Implication
implics_no) = (Cts -> Implication -> (Cts, Implication))
-> Cts -> Bag Implication -> (Cts, Bag Implication)
forall acc x y.
(acc -> x -> (acc, y)) -> acc -> Bag x -> (acc, Bag y)
mapAccumBagL (TyCoVarSet -> Cts -> Implication -> (Cts, Implication)
float_implic TyCoVarSet
skol_tvs)
                                                Cts
forall a. Bag a
emptyBag Bag Implication
implics

    float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
    float_implic :: TyCoVarSet -> Cts -> Implication -> (Cts, Implication)
float_implic TyCoVarSet
skol_tvs Cts
yes1 Implication
imp
      = (Cts
yes1 Cts -> Cts -> Cts
`andCts` Cts
yes2, Implication
imp { ic_wanted = no })
      where
        (Cts
yes2, WantedConstraints
no) = TyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc TyCoVarSet
new_skol_tvs (Implication -> WantedConstraints
ic_wanted Implication
imp)
        new_skol_tvs :: TyCoVarSet
new_skol_tvs = TyCoVarSet
skol_tvs TyCoVarSet -> [TcTyVar] -> TyCoVarSet
`extendVarSetList` Implication -> [TcTyVar]
ic_skols Implication
imp

    rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
    rule_quant_ct :: TyCoVarSet -> Ct -> Bool
rule_quant_ct TyCoVarSet
skol_tvs Ct
ct = case Type -> Pred
classifyPredType (Ct -> Type
ctPred Ct
ct) of
      EqPred EqRel
_ Type
t1 Type
t2
        | Bool -> Bool
not (Type -> Type -> Bool
ok_eq Type
t1 Type
t2)
        -> Bool
False        -- Note [RULE quantification over equalities]
      Pred
_ -> Ct -> TyCoVarSet
tyCoVarsOfCt Ct
ct TyCoVarSet -> TyCoVarSet -> Bool
`disjointVarSet` TyCoVarSet
skol_tvs

    ok_eq :: Type -> Type -> Bool
ok_eq Type
t1 Type
t2
       | Type
t1 (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
t2 = Bool
False
       | Bool
otherwise        = Type -> Bool
is_fun_app Type
t1 Bool -> Bool -> Bool
|| Type -> Bool
is_fun_app Type
t2

    is_fun_app :: Type -> Bool
is_fun_app Type
ty   -- ty is of form (F tys) where F is a type function
      = case Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty of
          Just TyCon
tc -> TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
          Maybe TyCon
Nothing -> Bool
False