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


TcRules: Typechecking transformation rules
-}

{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeFamilies #-}

module TcRules ( tcRules ) where

import GhcPrelude

import HsSyn
import TcRnTypes
import TcRnMonad
import TcSimplify
import TcMType
import TcType
import TcHsType
import TcExpr
import TcEnv
import TcUnify( buildImplicationFor )
import TcEvidence( mkTcCoVarCo )
import Type
import TyCon( isTypeFamilyTyCon )
import Id
import Var( EvVar )
import VarSet
import BasicTypes       ( RuleName )
import SrcLoc
import Outputable
import FastString
import 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.
-}

tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTcId]
tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTcId]
tcRules decls :: [LRuleDecls GhcRn]
decls = (LRuleDecls GhcRn
 -> IOEnv (Env TcGblEnv TcLclEnv) (LRuleDecls GhcTcId))
-> [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTcId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((SrcSpanLess (LRuleDecls GhcRn)
 -> TcM (SrcSpanLess (LRuleDecls GhcTcId)))
-> LRuleDecls GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) (LRuleDecls GhcTcId)
forall a b.
(HasSrcSpan a, HasSrcSpan b) =>
(SrcSpanLess a -> TcM (SrcSpanLess b)) -> a -> TcM b
wrapLocM SrcSpanLess (LRuleDecls GhcRn)
-> TcM (SrcSpanLess (LRuleDecls GhcTcId))
RuleDecls GhcRn -> TcM (RuleDecls GhcTcId)
tcRuleDecls) [LRuleDecls GhcRn]
decls

tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTcId)
tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTcId)
tcRuleDecls (HsRules { rds_src :: forall pass. RuleDecls pass -> SourceText
rds_src = SourceText
src
                     , rds_rules :: forall pass. RuleDecls pass -> [LRuleDecl pass]
rds_rules = [LRuleDecl GhcRn]
decls })
   = do { [LRuleDecl GhcTcId]
tc_decls <- (LRuleDecl GhcRn
 -> IOEnv (Env TcGblEnv TcLclEnv) (LRuleDecl GhcTcId))
-> [LRuleDecl GhcRn]
-> IOEnv (Env TcGblEnv TcLclEnv) [LRuleDecl GhcTcId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((SrcSpanLess (LRuleDecl GhcRn)
 -> TcM (SrcSpanLess (LRuleDecl GhcTcId)))
-> LRuleDecl GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) (LRuleDecl GhcTcId)
forall a b.
(HasSrcSpan a, HasSrcSpan b) =>
(SrcSpanLess a -> TcM (SrcSpanLess b)) -> a -> TcM b
wrapLocM SrcSpanLess (LRuleDecl GhcRn)
-> TcM (SrcSpanLess (LRuleDecl GhcTcId))
RuleDecl GhcRn -> TcM (RuleDecl GhcTcId)
tcRule) [LRuleDecl GhcRn]
decls
        ; RuleDecls GhcTcId -> TcM (RuleDecls GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (RuleDecls GhcTcId -> TcM (RuleDecls GhcTcId))
-> RuleDecls GhcTcId -> TcM (RuleDecls GhcTcId)
forall a b. (a -> b) -> a -> b
$ HsRules :: forall pass.
XCRuleDecls pass
-> SourceText -> [LRuleDecl pass] -> RuleDecls pass
HsRules { rds_ext :: XCRuleDecls GhcTcId
rds_ext   = XCRuleDecls GhcTcId
NoExt
noExt
                           , rds_src :: SourceText
rds_src   = SourceText
src
                           , rds_rules :: [LRuleDecl GhcTcId]
rds_rules = [LRuleDecl GhcTcId]
tc_decls } }
tcRuleDecls (XRuleDecls _) = String -> TcM (RuleDecls GhcTcId)
forall a. String -> a
panic "tcRuleDecls"

tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTcId)
tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTcId)
tcRule (HsRule { rd_ext :: forall pass. RuleDecl pass -> XHsRule pass
rd_ext  = XHsRule GhcRn
ext
               , rd_name :: forall pass. RuleDecl pass -> Located (SourceText, RuleName)
rd_name = rname :: Located (SourceText, RuleName)
rname@(L _ (_,name :: 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 GhcRn)]
ty_bndrs
               , rd_tmvs :: forall pass. RuleDecl pass -> [LRuleBndr pass]
rd_tmvs = [LRuleBndr GhcRn]
tm_bndrs
               , rd_lhs :: forall pass. RuleDecl pass -> Located (HsExpr pass)
rd_lhs  = Located (HsExpr GhcRn)
lhs
               , rd_rhs :: forall pass. RuleDecl pass -> Located (HsExpr pass)
rd_rhs  = Located (HsExpr GhcRn)
rhs })
  = MsgDoc -> TcM (RuleDecl GhcTcId) -> TcM (RuleDecl GhcTcId)
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt (RuleName -> MsgDoc
ruleCtxt RuleName
name)  (TcM (RuleDecl GhcTcId) -> TcM (RuleDecl GhcTcId))
-> TcM (RuleDecl GhcTcId) -> TcM (RuleDecl GhcTcId)
forall a b. (a -> b) -> a -> b
$
    do { String -> MsgDoc -> TcRn ()
traceTc "---- Rule ------" (Located (SourceText, RuleName) -> MsgDoc
pprFullRuleName Located (SourceText, RuleName)
rname)

        -- Note [Typechecking rules]
       ; (tc_lvl :: TcLevel
tc_lvl, stuff :: ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
 LHsExpr GhcTcId, WantedConstraints, TcType)
stuff) <- TcM
  ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
   LHsExpr GhcTcId, WantedConstraints, TcType)
-> TcM
     (TcLevel,
      ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
       LHsExpr GhcTcId, WantedConstraints, TcType))
forall a. TcM a -> TcM (TcLevel, a)
pushTcLevelM (TcM
   ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
    LHsExpr GhcTcId, WantedConstraints, TcType)
 -> TcM
      (TcLevel,
       ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
        LHsExpr GhcTcId, WantedConstraints, TcType)))
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
-> TcM
     (TcLevel,
      ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
       LHsExpr GhcTcId, WantedConstraints, TcType))
forall a b. (a -> b) -> a -> b
$
                            Maybe [LHsTyVarBndr GhcRn]
-> [LRuleBndr GhcRn]
-> Located (HsExpr GhcRn)
-> Located (HsExpr GhcRn)
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
generateRuleConstraints Maybe [LHsTyVarBndr (NoGhcTc GhcRn)]
Maybe [LHsTyVarBndr GhcRn]
ty_bndrs [LRuleBndr GhcRn]
tm_bndrs Located (HsExpr GhcRn)
lhs Located (HsExpr GhcRn)
rhs

       ; let (tv_bndrs :: [TyVar]
tv_bndrs, id_bndrs :: [TyVar]
id_bndrs, lhs' :: LHsExpr GhcTcId
lhs', lhs_wanted :: WantedConstraints
lhs_wanted
                                , rhs' :: LHsExpr GhcTcId
rhs', rhs_wanted :: WantedConstraints
rhs_wanted, rule_ty :: TcType
rule_ty) = ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
 LHsExpr GhcTcId, WantedConstraints, TcType)
stuff

       ; String -> MsgDoc -> TcRn ()
traceTc "tcRule 1" ([MsgDoc] -> MsgDoc
vcat [ Located (SourceText, RuleName) -> MsgDoc
pprFullRuleName Located (SourceText, RuleName)
rname
                                  , WantedConstraints -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr WantedConstraints
lhs_wanted
                                  , WantedConstraints -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr WantedConstraints
rhs_wanted ])

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

       -- SimplfyRule Plan, step 4
       -- Now figure out what to quantify over
       -- c.f. TcSimplify.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-uconstrained tyvars of
       -- the LHS, lest they otherwise get defaulted to Any; but we do that
       -- during zonking (see TcHsSyn.zonkRule)

       ; let tpl_ids :: [TyVar]
tpl_ids = [TyVar]
lhs_evs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
id_bndrs
       ; TcTyVarSet
gbls  <- TcM TcTyVarSet
tcGetGlobalTyCoVars -- Even though top level, there might be top-level
                                      -- monomorphic bindings from the MR; test tc111
       ; CandidatesQTvs
forall_tkvs <- [TcType] -> TcM CandidatesQTvs
candidateQTyVarsOfTypes ([TcType] -> TcM CandidatesQTvs) -> [TcType] -> TcM CandidatesQTvs
forall a b. (a -> b) -> a -> b
$
                        (TcType -> TcType) -> [TcType] -> [TcType]
forall a b. (a -> b) -> [a] -> [b]
map ([TyVar] -> TcType -> TcType
mkSpecForAllTys [TyVar]
tv_bndrs) ([TcType] -> [TcType]) -> [TcType] -> [TcType]
forall a b. (a -> b) -> a -> b
$  -- don't quantify over lexical tyvars
                        TcType
rule_ty TcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
: (TyVar -> TcType) -> [TyVar] -> [TcType]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> TcType
idType [TyVar]
tpl_ids
       ; [TyVar]
qtkvs <- TcTyVarSet -> CandidatesQTvs -> TcM [TyVar]
quantifyTyVars TcTyVarSet
gbls CandidatesQTvs
forall_tkvs
       ; String -> MsgDoc -> TcRn ()
traceTc "tcRule" ([MsgDoc] -> MsgDoc
vcat [ Located (SourceText, RuleName) -> MsgDoc
pprFullRuleName Located (SourceText, RuleName)
rname
                                , CandidatesQTvs -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr CandidatesQTvs
forall_tkvs
                                , [TyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TyVar]
qtkvs
                                , [TyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TyVar]
tv_bndrs
                                , TcType -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcType
rule_ty
                                , [MsgDoc] -> MsgDoc
vcat [ TyVar -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyVar
id MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc
dcolon MsgDoc -> MsgDoc -> MsgDoc
<+> TcType -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyVar -> TcType
idType TyVar
id) | TyVar
id <- [TyVar]
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
       ; let all_qtkvs :: [TyVar]
all_qtkvs = [TyVar]
qtkvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
tv_bndrs
             skol_info :: SkolemInfo
skol_info = RuleName -> SkolemInfo
RuleSkol RuleName
name
       ; (lhs_implic :: Bag Implication
lhs_implic, lhs_binds :: TcEvBinds
lhs_binds) <- TcLevel
-> SkolemInfo
-> [TyVar]
-> [TyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl SkolemInfo
skol_info [TyVar]
all_qtkvs
                                         [TyVar]
lhs_evs WantedConstraints
residual_lhs_wanted
       ; (rhs_implic :: Bag Implication
rhs_implic, rhs_binds :: TcEvBinds
rhs_binds) <- TcLevel
-> SkolemInfo
-> [TyVar]
-> [TyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl SkolemInfo
skol_info [TyVar]
all_qtkvs
                                         [TyVar]
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 GhcTcId -> TcM (RuleDecl GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (RuleDecl GhcTcId -> TcM (RuleDecl GhcTcId))
-> RuleDecl GhcTcId -> TcM (RuleDecl GhcTcId)
forall a b. (a -> b) -> a -> b
$ HsRule :: forall pass.
XHsRule pass
-> Located (SourceText, RuleName)
-> Activation
-> Maybe [LHsTyVarBndr (NoGhcTc pass)]
-> [LRuleBndr pass]
-> Located (HsExpr pass)
-> Located (HsExpr pass)
-> RuleDecl pass
HsRule { rd_ext :: XHsRule GhcTcId
rd_ext = XHsRule GhcRn
XHsRule GhcTcId
ext
                         , rd_name :: Located (SourceText, RuleName)
rd_name = Located (SourceText, RuleName)
rname
                         , rd_act :: Activation
rd_act = Activation
act
                         , rd_tyvs :: Maybe [LHsTyVarBndr (NoGhcTc GhcTcId)]
rd_tyvs = Maybe [LHsTyVarBndr (NoGhcTc GhcRn)]
Maybe [LHsTyVarBndr (NoGhcTc GhcTcId)]
ty_bndrs -- preserved for ppr-ing
                         , rd_tmvs :: [LRuleBndr GhcTcId]
rd_tmvs = (TyVar -> LRuleBndr GhcTcId) -> [TyVar] -> [LRuleBndr GhcTcId]
forall a b. (a -> b) -> [a] -> [b]
map (RuleBndr GhcTcId -> LRuleBndr GhcTcId
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (RuleBndr GhcTcId -> LRuleBndr GhcTcId)
-> (TyVar -> RuleBndr GhcTcId) -> TyVar -> LRuleBndr GhcTcId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XCRuleBndr GhcTcId -> Located (IdP GhcTcId) -> RuleBndr GhcTcId
forall pass. XCRuleBndr pass -> Located (IdP pass) -> RuleBndr pass
RuleBndr XCRuleBndr GhcTcId
NoExt
noExt (GenLocated SrcSpan TyVar -> RuleBndr GhcTcId)
-> (TyVar -> GenLocated SrcSpan TyVar) -> TyVar -> RuleBndr GhcTcId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> GenLocated SrcSpan TyVar
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc) ([TyVar]
all_qtkvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
tpl_ids)
                         , rd_lhs :: LHsExpr GhcTcId
rd_lhs  = TcEvBinds -> LHsExpr GhcTcId -> LHsExpr GhcTcId
mkHsDictLet TcEvBinds
lhs_binds LHsExpr GhcTcId
lhs'
                         , rd_rhs :: LHsExpr GhcTcId
rd_rhs  = TcEvBinds -> LHsExpr GhcTcId -> LHsExpr GhcTcId
mkHsDictLet TcEvBinds
rhs_binds LHsExpr GhcTcId
rhs' } }
tcRule (XRuleDecl _) = String -> TcM (RuleDecl GhcTcId)
forall a. String -> a
panic "tcRule"

generateRuleConstraints :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn]
                        -> LHsExpr GhcRn -> LHsExpr GhcRn
                        -> TcM ( [TyVar]
                               , [TcId]
                               , LHsExpr GhcTc, WantedConstraints
                               , LHsExpr GhcTc, WantedConstraints
                               , TcType )
generateRuleConstraints :: Maybe [LHsTyVarBndr GhcRn]
-> [LRuleBndr GhcRn]
-> Located (HsExpr GhcRn)
-> Located (HsExpr GhcRn)
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
generateRuleConstraints ty_bndrs :: Maybe [LHsTyVarBndr GhcRn]
ty_bndrs tm_bndrs :: [LRuleBndr GhcRn]
tm_bndrs lhs :: Located (HsExpr GhcRn)
lhs rhs :: Located (HsExpr GhcRn)
rhs
  = do { ((tv_bndrs :: [TyVar]
tv_bndrs, id_bndrs :: [TyVar]
id_bndrs), bndr_wanted :: WantedConstraints
bndr_wanted) <- TcM ([TyVar], [TyVar])
-> TcM (([TyVar], [TyVar]), WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM ([TyVar], [TyVar])
 -> TcM (([TyVar], [TyVar]), WantedConstraints))
-> TcM ([TyVar], [TyVar])
-> TcM (([TyVar], [TyVar]), WantedConstraints)
forall a b. (a -> b) -> a -> b
$
                                                Maybe [LHsTyVarBndr GhcRn]
-> [LRuleBndr GhcRn] -> TcM ([TyVar], [TyVar])
tcRuleBndrs Maybe [LHsTyVarBndr GhcRn]
ty_bndrs [LRuleBndr GhcRn]
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. Trac #10072

       ; [TyVar]
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
forall r. [TyVar] -> TcM r -> TcM r
tcExtendTyVarEnv [TyVar]
tv_bndrs (TcM
   ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
    LHsExpr GhcTcId, WantedConstraints, TcType)
 -> TcM
      ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
       LHsExpr GhcTcId, WantedConstraints, TcType))
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
forall a b. (a -> b) -> a -> b
$
         [TyVar]
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
forall r. [TyVar] -> TcM r -> TcM r
tcExtendIdEnv    [TyVar]
id_bndrs (TcM
   ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
    LHsExpr GhcTcId, WantedConstraints, TcType)
 -> TcM
      ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
       LHsExpr GhcTcId, WantedConstraints, TcType))
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
forall a b. (a -> b) -> a -> b
$
    do { -- See Note [Solve order for RULES]
         ((lhs' :: LHsExpr GhcTcId
lhs', rule_ty :: TcType
rule_ty), lhs_wanted :: WantedConstraints
lhs_wanted) <- TcM (LHsExpr GhcTcId, TcType)
-> TcM ((LHsExpr GhcTcId, TcType), WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (Located (HsExpr GhcRn) -> TcM (LHsExpr GhcTcId, TcType)
tcInferRho Located (HsExpr GhcRn)
lhs)
       ; (rhs' :: LHsExpr GhcTcId
rhs',            rhs_wanted :: WantedConstraints
rhs_wanted) <- TcM (LHsExpr GhcTcId) -> TcM (LHsExpr GhcTcId, WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM (LHsExpr GhcTcId) -> TcM (LHsExpr GhcTcId, WantedConstraints))
-> TcM (LHsExpr GhcTcId)
-> TcM (LHsExpr GhcTcId, WantedConstraints)
forall a b. (a -> b) -> a -> b
$
                                          Located (HsExpr GhcRn) -> ExpRhoType -> TcM (LHsExpr GhcTcId)
tcMonoExpr Located (HsExpr GhcRn)
rhs (TcType -> ExpRhoType
mkCheckExpType TcType
rule_ty)
       ; let all_lhs_wanted :: WantedConstraints
all_lhs_wanted = WantedConstraints
bndr_wanted WantedConstraints -> WantedConstraints -> WantedConstraints
`andWC` WantedConstraints
lhs_wanted
       ; ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
 LHsExpr GhcTcId, WantedConstraints, TcType)
-> TcM
     ([TyVar], [TyVar], LHsExpr GhcTcId, WantedConstraints,
      LHsExpr GhcTcId, WantedConstraints, TcType)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVar]
tv_bndrs, [TyVar]
id_bndrs, LHsExpr GhcTcId
lhs', WantedConstraints
all_lhs_wanted, LHsExpr GhcTcId
rhs', WantedConstraints
rhs_wanted, TcType
rule_ty) } }

-- See Note [TcLevel in type checking rules]
tcRuleBndrs :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn]
            -> TcM ([TcTyVar], [Id])
tcRuleBndrs :: Maybe [LHsTyVarBndr GhcRn]
-> [LRuleBndr GhcRn] -> TcM ([TyVar], [TyVar])
tcRuleBndrs (Just bndrs :: [LHsTyVarBndr GhcRn]
bndrs) xs :: [LRuleBndr GhcRn]
xs
  = do { (tys1 :: [TyVar]
tys1,(tys2 :: [TyVar]
tys2,tms :: [TyVar]
tms)) <- [LHsTyVarBndr GhcRn]
-> TcM ([TyVar], [TyVar]) -> TcM ([TyVar], ([TyVar], [TyVar]))
forall a. [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TyVar], a)
bindExplicitTKBndrs_Skol [LHsTyVarBndr GhcRn]
bndrs (TcM ([TyVar], [TyVar]) -> TcM ([TyVar], ([TyVar], [TyVar])))
-> TcM ([TyVar], [TyVar]) -> TcM ([TyVar], ([TyVar], [TyVar]))
forall a b. (a -> b) -> a -> b
$
                              [LRuleBndr GhcRn] -> TcM ([TyVar], [TyVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
xs
       ; ([TyVar], [TyVar]) -> TcM ([TyVar], [TyVar])
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVar]
tys1 [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
tys2, [TyVar]
tms) }

tcRuleBndrs Nothing xs :: [LRuleBndr GhcRn]
xs
  = [LRuleBndr GhcRn] -> TcM ([TyVar], [TyVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
xs

-- See Note [TcLevel in type checking rules]
tcRuleTmBndrs :: [LRuleBndr GhcRn] -> TcM ([TcTyVar],[Id])
tcRuleTmBndrs :: [LRuleBndr GhcRn] -> TcM ([TyVar], [TyVar])
tcRuleTmBndrs [] = ([TyVar], [TyVar]) -> TcM ([TyVar], [TyVar])
forall (m :: * -> *) a. Monad m => a -> m a
return ([],[])
tcRuleTmBndrs (L _ (RuleBndr _ (L _ name :: IdP GhcRn
name)) : rule_bndrs :: [LRuleBndr GhcRn]
rule_bndrs)
  = do  { TcType
ty <- TcM TcType
newOpenFlexiTyVarTy
        ; (tyvars :: [TyVar]
tyvars, tmvars :: [TyVar]
tmvars) <- [LRuleBndr GhcRn] -> TcM ([TyVar], [TyVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
rule_bndrs
        ; ([TyVar], [TyVar]) -> TcM ([TyVar], [TyVar])
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVar]
tyvars, Name -> TcType -> TyVar
mkLocalId Name
IdP GhcRn
name TcType
ty TyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
: [TyVar]
tmvars) }
tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name :: IdP GhcRn
name) rn_ty :: LHsSigWcType GhcRn
rn_ty) : rule_bndrs :: [LRuleBndr GhcRn]
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 = Name -> UserTypeCtxt
RuleSigCtxt Name
IdP GhcRn
name
        ; (_ , tvs :: [(Name, TyVar)]
tvs, id_ty :: TcType
id_ty) <- UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM ([(Name, TyVar)], [(Name, TyVar)], TcType)
tcHsPatSigType UserTypeCtxt
ctxt LHsSigWcType GhcRn
rn_ty
        ; let id :: TyVar
id  = Name -> TcType -> TyVar
mkLocalIdOrCoVar Name
IdP GhcRn
name TcType
id_ty
                    -- See Note [Pattern signature binders] in TcHsType

              -- The type variables scope over subsequent bindings; yuk
        ; (tyvars :: [TyVar]
tyvars, tmvars :: [TyVar]
tmvars) <- [(Name, TyVar)] -> TcM ([TyVar], [TyVar]) -> TcM ([TyVar], [TyVar])
forall r. [(Name, TyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, TyVar)]
tvs (TcM ([TyVar], [TyVar]) -> TcM ([TyVar], [TyVar]))
-> TcM ([TyVar], [TyVar]) -> TcM ([TyVar], [TyVar])
forall a b. (a -> b) -> a -> b
$
                                   [LRuleBndr GhcRn] -> TcM ([TyVar], [TyVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
rule_bndrs
        ; ([TyVar], [TyVar]) -> TcM ([TyVar], [TyVar])
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TyVar) -> TyVar) -> [(Name, TyVar)] -> [TyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TyVar) -> TyVar
forall a b. (a, b) -> b
snd [(Name, TyVar)]
tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
tyvars, TyVar
id TyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
: [TyVar]
tmvars) }
tcRuleTmBndrs (L _ (XRuleBndr _) : _) = String -> TcM ([TyVar], [TyVar])
forall a. String -> a
panic "tcRuleTmBndrs"

ruleCtxt :: FastString -> SDoc
ruleCtxt :: RuleName -> MsgDoc
ruleCtxt name :: RuleName
name = String -> MsgDoc
text "When checking the transformation rule" MsgDoc -> MsgDoc -> MsgDoc
<+>
                MsgDoc -> MsgDoc
doubleQuotes (RuleName -> MsgDoc
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
          We do this 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 ([TyVar], WantedConstraints)
simplifyRule name :: RuleName
name tc_lvl :: TcLevel
tc_lvl lhs_wanted :: WantedConstraints
lhs_wanted rhs_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
$
         TcS () -> TcRn ()
forall a. TcS a -> TcM a
runTcSDeriveds    (TcS () -> TcRn ()) -> TcS () -> TcRn ()
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 (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 (quant_cts :: Cts
quant_cts, residual_lhs_wanted :: WantedConstraints
residual_lhs_wanted) = WantedConstraints -> (Cts, WantedConstraints)
getRuleQuantCts WantedConstraints
lhs_wanted

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

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

       ; ([TyVar], WantedConstraints) -> TcM ([TyVar], WantedConstraints)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVar]
quant_evs, WantedConstraints
residual_lhs_wanted) }

  where
    mk_quant_ev :: Ct -> TcM EvVar
    mk_quant_ev :: Ct -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
mk_quant_ev ct :: Ct
ct
      | CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_pred :: CtEvidence -> TcType
ctev_pred = TcType
pred } <- Ct -> CtEvidence
ctEvidence Ct
ct
      = case TcEvDest
dest of
          EvVarDest ev_id :: TyVar
ev_id -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
ev_id
          HoleDest hole :: CoercionHole
hole   -> -- See Note [Quantifying over coercion holes]
                             do { TyVar
ev_id <- TcType -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall gbl lcl. TcType -> TcRnIf gbl lcl TyVar
newEvVar TcType
pred
                                ; CoercionHole -> Coercion -> TcRn ()
fillCoercionHole CoercionHole
hole (TyVar -> Coercion
mkTcCoVarCo TyVar
ev_id)
                                ; TyVar -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
ev_id }
    mk_quant_ev ct :: Ct
ct = String -> MsgDoc -> IOEnv (Env TcGblEnv TcLclEnv) TyVar
forall a. HasCallStack => String -> MsgDoc -> a
pprPanic "mk_quant_ev" (Ct -> MsgDoc
forall a. Outputable a => a -> MsgDoc
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 TcUnify.implicationNeeded. Not doing so caused Trac #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 TcInteract 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 wc :: WantedConstraints
wc
  = TcTyVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc TcTyVarSet
emptyVarSet WantedConstraints
wc
  where
    float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
    float_wc :: TcTyVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc skol_tvs :: TcTyVarSet
skol_tvs (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics })
      = ( Cts
simple_yes Cts -> Cts -> Cts
`andCts` Cts
implic_yes
        , WC :: Cts -> Bag Implication -> WantedConstraints
WC { wc_simple :: Cts
wc_simple = Cts
simple_no, wc_impl :: Bag Implication
wc_impl = Bag Implication
implics_no })
     where
        (simple_yes :: Cts
simple_yes, simple_no :: Cts
simple_no) = (Ct -> Bool) -> Cts -> (Cts, Cts)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag (TcTyVarSet -> Ct -> Bool
rule_quant_ct TcTyVarSet
skol_tvs) Cts
simples
        (implic_yes :: Cts
implic_yes, implics_no :: 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 (TcTyVarSet -> Cts -> Implication -> (Cts, Implication)
float_implic TcTyVarSet
skol_tvs)
                                                Cts
forall a. Bag a
emptyBag Bag Implication
implics

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

    rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
    rule_quant_ct :: TcTyVarSet -> Ct -> Bool
rule_quant_ct skol_tvs :: TcTyVarSet
skol_tvs ct :: Ct
ct
      | EqPred _ t1 :: TcType
t1 t2 :: TcType
t2 <- TcType -> PredTree
classifyPredType (Ct -> TcType
ctPred Ct
ct)
      , Bool -> Bool
not (TcType -> TcType -> Bool
ok_eq TcType
t1 TcType
t2)
       = Bool
False        -- Note [RULE quantification over equalities]
      | Ct -> Bool
isHoleCt Ct
ct
      = Bool
False         -- Don't quantify over type holes, obviously
      | Bool
otherwise
      = Ct -> TcTyVarSet
tyCoVarsOfCt Ct
ct TcTyVarSet -> TcTyVarSet -> Bool
`disjointVarSet` TcTyVarSet
skol_tvs

    ok_eq :: TcType -> TcType -> Bool
ok_eq t1 :: TcType
t1 t2 :: TcType
t2
       | TcType
t1 HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` TcType
t2 = Bool
False
       | Bool
otherwise        = TcType -> Bool
is_fun_app TcType
t1 Bool -> Bool -> Bool
|| TcType -> Bool
is_fun_app TcType
t2

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