{-# LANGUAGE TypeFamilies #-}
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.Solve( solveWanteds )
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.Tc.Zonk.TcType
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
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 (EpAnn ann) a -> TcRn (GenLocated (EpAnn 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 { maybe_tc_decls <- (GenLocated SrcSpanAnnA (RuleDecl (GhcPass 'Renamed))
-> IOEnv
(Env TcGblEnv TcLclEnv)
(GenLocated SrcSpanAnnA (Maybe (RuleDecl GhcTc))))
-> [GenLocated SrcSpanAnnA (RuleDecl (GhcPass 'Renamed))]
-> IOEnv
(Env TcGblEnv TcLclEnv)
[GenLocated SrcSpanAnnA (Maybe (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 (Maybe (RuleDecl GhcTc)))
-> GenLocated SrcSpanAnnA (RuleDecl (GhcPass 'Renamed))
-> IOEnv
(Env TcGblEnv TcLclEnv)
(GenLocated SrcSpanAnnA (Maybe (RuleDecl GhcTc)))
forall a b ann.
(a -> TcM b)
-> GenLocated (EpAnn ann) a -> TcRn (GenLocated (EpAnn ann) b)
wrapLocMA RuleDecl (GhcPass 'Renamed) -> TcM (Maybe (RuleDecl GhcTc))
tcRule) [LRuleDecl (GhcPass 'Renamed)]
[GenLocated SrcSpanAnnA (RuleDecl (GhcPass 'Renamed))]
decls
; let tc_decls = [SrcSpanAnnA
-> RuleDecl GhcTc -> GenLocated SrcSpanAnnA (RuleDecl GhcTc)
forall l e. l -> e -> GenLocated l e
L SrcSpanAnnA
loc RuleDecl GhcTc
rule | (L SrcSpanAnnA
loc (Just RuleDecl GhcTc
rule)) <- [GenLocated SrcSpanAnnA (Maybe (RuleDecl GhcTc))]
maybe_tc_decls]
; return $ HsRules { rds_ext = src
, rds_rules = tc_decls } }
tcRule :: RuleDecl GhcRn -> TcM (Maybe (RuleDecl GhcTc))
tcRule :: RuleDecl (GhcPass 'Renamed) -> TcM (Maybe (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 EpAnnCO
_ 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 (Maybe (RuleDecl GhcTc)) -> TcM (Maybe (RuleDecl GhcTc))
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (RuleName -> SDoc
ruleCtxt RuleName
name) (TcM (Maybe (RuleDecl GhcTc)) -> TcM (Maybe (RuleDecl GhcTc)))
-> TcM (Maybe (RuleDecl GhcTc)) -> TcM (Maybe (RuleDecl GhcTc))
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcRn ()
traceTc String
"---- Rule ------" (SourceText -> GenLocated EpAnnCO 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 EpAnnCO RuleName
rname)
; skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (RuleName -> SkolemInfoAnon
RuleSkol RuleName
name)
; (tc_lvl, stuff) <- pushTcLevelM $
generateRuleConstraints name ty_bndrs tm_bndrs lhs rhs
; let (id_bndrs, lhs', lhs_wanted
, rhs', rhs_wanted, rule_ty) = stuff
; traceTc "tcRule 1" (vcat [ pprFullRuleName (snd ext) rname
, ppr lhs_wanted
, ppr rhs_wanted ])
; (lhs_evs, residual_lhs_wanted, dont_default)
<- simplifyRule name tc_lvl lhs_wanted rhs_wanted
; let tpl_ids = [TcTyVar]
lhs_evs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
id_bndrs
; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids)
; let weed_out = (DVarSet -> TyCoVarSet -> DVarSet
`dVarSetMinusVarSet` TyCoVarSet
dont_default)
quant_cands = CandidatesQTvs
forall_tkvs { dv_kvs = weed_out (dv_kvs forall_tkvs)
, dv_tvs = weed_out (dv_tvs forall_tkvs) }
; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars quant_cands
; traceTc "tcRule" (vcat [ pprFullRuleName (snd ext) rname
, text "forall_tkvs:" <+> ppr forall_tkvs
, text "quant_cands:" <+> ppr quant_cands
, text "dont_default:" <+> ppr dont_default
, text "residual_lhs_wanted:" <+> ppr residual_lhs_wanted
, text "qtkvs:" <+> ppr qtkvs
, text "rule_ty:" <+> ppr rule_ty
, text "ty_bndrs:" <+> ppr ty_bndrs
, text "qtkvs ++ tpl_ids:" <+> ppr (qtkvs ++ tpl_ids)
, text "tpl_id info:" <+>
vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
])
; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
lhs_evs residual_lhs_wanted
; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) qtkvs
lhs_evs rhs_wanted
; emitImplications (lhs_implic `unionBags` rhs_implic)
; if anyBag insolubleImplic lhs_implic
then
return Nothing
else
return . Just $ HsRule { rd_ext = ext
, rd_name = rname
, rd_act = act
, rd_tyvs = ty_bndrs
, rd_tmvs = map (noLocA . RuleBndr noAnn . noLocA)
(qtkvs ++ tpl_ids)
, rd_lhs = mkHsDictLet lhs_binds lhs'
, rd_rhs = mkHsDictLet rhs_binds 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, TcType)
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 { ((tv_bndrs, id_bndrs), 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
; tcExtendNameTyVarEnv [(tyVarName tv, tv) | tv <- tv_bndrs] $
tcExtendIdEnv id_bndrs $
do {
((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
; (rhs', rhs_wanted) <- captureConstraints $
tcCheckMonoExpr rhs rule_ty
; let all_lhs_wanted = WantedConstraints
bndr_wanted WantedConstraints -> WantedConstraints -> WantedConstraints
`andWC` WantedConstraints
lhs_wanted
; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
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 { skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (RuleName -> SkolemInfoAnon
RuleSkol RuleName
rule_name)
; (tybndrs1,(tys2,tms)) <- bindExplicitTKBndrs_Skol skol_info bndrs $
tcRuleTmBndrs rule_name xs
; let tys1 = [VarBndr TcTyVar ()] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr TcTyVar ()]
tybndrs1
; return (tys1 ++ tys2, 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
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 EpAnnCO
_ (RuleBndr XCRuleBndr (GhcPass 'Renamed)
_ (L SrcSpanAnnN
_ Name
name)) : [LRuleBndr (GhcPass 'Renamed)]
rule_bndrs)
= do { ty <- TcM TcType
newOpenFlexiTyVarTy
; (tyvars, tmvars) <- tcRuleTmBndrs rule_name rule_bndrs
; return (tyvars, mkLocalId name ManyTy ty : tmvars) }
tcRuleTmBndrs RuleName
rule_name (L EpAnnCO
_ (RuleBndrSig XRuleBndrSig (GhcPass 'Renamed)
_ (L SrcSpanAnnN
_ Name
name) HsPatSigType (GhcPass 'Renamed)
rn_ty) : [LRuleBndr (GhcPass 'Renamed)]
rule_bndrs)
= do { let ctxt :: UserTypeCtxt
ctxt = RuleName -> Name -> UserTypeCtxt
RuleSigCtxt RuleName
rule_name Name
name
; (_ , tvs, id_ty) <- UserTypeCtxt
-> HoleMode
-> HsPatSigType (GhcPass 'Renamed)
-> ContextKind
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], TcType)
tcHsPatSigType UserTypeCtxt
ctxt HoleMode
HM_Sig HsPatSigType (GhcPass 'Renamed)
rn_ty ContextKind
OpenKind
; let id = HasDebugCallStack => Name -> TcType -> TcType -> TcTyVar
Name -> TcType -> TcType -> TcTyVar
mkLocalId Name
name TcType
ManyTy TcType
id_ty
; (tyvars, tmvars) <- tcExtendNameTyVarEnv tvs $
tcRuleTmBndrs rule_name rule_bndrs
; return (map snd tvs ++ tyvars, id : 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)
simplifyRule :: RuleName
-> TcLevel
-> WantedConstraints
-> WantedConstraints
-> TcM ( [EvVar]
, WantedConstraints
, TcTyVarSet )
simplifyRule :: RuleName
-> TcLevel
-> WantedConstraints
-> WantedConstraints
-> TcM ([TcTyVar], WantedConstraints, TyCoVarSet)
simplifyRule RuleName
name TcLevel
tc_lvl WantedConstraints
lhs_wanted WantedConstraints
rhs_wanted
= do {
; lhs_clone <- WantedConstraints -> TcM WantedConstraints
cloneWC WantedConstraints
lhs_wanted
; rhs_clone <- cloneWC rhs_wanted
; (dont_default, _)
<- setTcLevel tc_lvl $
runTcS $
do { lhs_wc <- solveWanteds lhs_clone
; _rhs_wc <- solveWanteds rhs_clone
; let dont_default = WantedConstraints -> TyCoVarSet
nonDefaultableTyVarsOfWC WantedConstraints
lhs_wc
; return dont_default }
; lhs_wanted <- liftZonkM $ zonkWC lhs_wanted
; let (quant_cts, residual_lhs_wanted) = getRuleQuantCts lhs_wanted
; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
; traceTc "simplifyRule" $
vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
, text "lhs_wanted" <+> ppr lhs_wanted
, text "rhs_wanted" <+> ppr rhs_wanted
, text "quant_cts" <+> ppr quant_cts
, text "residual_lhs_wanted" <+> ppr residual_lhs_wanted
, text "dont_default" <+> ppr dont_default
]
; return (quant_evs, residual_lhs_wanted, dont_default) }
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 -> TcType
ctev_pred = TcType
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 ->
do { ev_id <- TcType -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall gbl lcl. TcType -> TcRnIf gbl lcl TcTyVar
newEvVar TcType
pred
; fillCoercionHole hole (mkCoVarCo ev_id)
; return 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)
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 TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct) of
EqPred EqRel
_ TcType
t1 TcType
t2
| Bool -> Bool
not (TcType -> TcType -> Bool
ok_eq TcType
t1 TcType
t2)
-> Bool
False
Pred
_ -> Ct -> TyCoVarSet
tyCoVarsOfCt Ct
ct TyCoVarSet -> TyCoVarSet -> Bool
`disjointVarSet` TyCoVarSet
skol_tvs
ok_eq :: TcType -> TcType -> Bool
ok_eq TcType
t1 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 TcType
ty
= case TcType -> Maybe TyCon
tyConAppTyCon_maybe TcType
ty of
Just TyCon
tc -> TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
Maybe TyCon
Nothing -> Bool
False