{-# 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
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
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.Types.Evidence( mkTcCoVarCo )
import GHC.Core.Type
import GHC.Core.TyCon( isTypeFamilyTyCon )
import GHC.Types.Id
import GHC.Types.Var( EvVar )
import GHC.Types.Var.Set
import GHC.Types.Basic ( RuleName )
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 GhcRn] -> TcM [LRuleDecls GhcTc]
tcRules [LRuleDecls GhcRn]
decls = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b ann.
(a -> TcM b)
-> GenLocated (SrcSpanAnn' ann) a
-> TcRn (GenLocated (SrcSpanAnn' ann) b)
wrapLocMA RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
tcRuleDecls) [LRuleDecls GhcRn]
decls
tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
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 { [GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (RuleDecl GhcTc)]
tc_decls <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b ann.
(a -> TcM b)
-> GenLocated (SrcSpanAnn' ann) a
-> TcRn (GenLocated (SrcSpanAnn' ann) b)
wrapLocMA RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
tcRule) [LRuleDecl GhcRn]
decls
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HsRules { rds_ext :: XCRuleDecls GhcTc
rds_ext = NoExtField
noExtField
, rds_src :: SourceText
rds_src = SourceText
src
, rds_rules :: [LRuleDecl GhcTc]
rds_rules = [GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (RuleDecl GhcTc)]
tc_decls } }
tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
tcRule (HsRule { rd_ext :: forall pass. RuleDecl pass -> XHsRule pass
rd_ext = XHsRule GhcRn
ext
, rd_name :: forall pass. RuleDecl pass -> XRec pass (SourceText, RuleName)
rd_name = rname :: XRec GhcRn (SourceText, RuleName)
rname@(L SrcSpan
_ (SourceText
_,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 -> XRec pass (HsExpr pass)
rd_lhs = XRec GhcRn (HsExpr GhcRn)
lhs
, rd_rhs :: forall pass. RuleDecl pass -> XRec pass (HsExpr pass)
rd_rhs = XRec GhcRn (HsExpr GhcRn)
rhs })
= forall a. SDoc -> TcM a -> TcM a
addErrCtxt (RuleName -> SDoc
ruleCtxt RuleName
name) forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcRn ()
traceTc String
"---- Rule ------" (GenLocated SrcSpan (SourceText, RuleName) -> SDoc
pprFullRuleName XRec GhcRn (SourceText, RuleName)
rname)
; (TcLevel
tc_lvl, ([TcTyVar],
GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc),
WantedConstraints,
GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc),
WantedConstraints, Type)
stuff) <- forall a. TcM a -> TcM (TcLevel, a)
pushTcLevelM forall a b. (a -> b) -> a -> b
$
Maybe [LHsTyVarBndr () GhcRn]
-> [LRuleBndr GhcRn]
-> XRec GhcRn (HsExpr GhcRn)
-> XRec GhcRn (HsExpr GhcRn)
-> TcM
([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
WantedConstraints, Type)
generateRuleConstraints Maybe [LHsTyVarBndr () (NoGhcTc GhcRn)]
ty_bndrs [LRuleBndr GhcRn]
tm_bndrs XRec GhcRn (HsExpr GhcRn)
lhs XRec GhcRn (HsExpr GhcRn)
rhs
; let ([TcTyVar]
id_bndrs, GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc)
lhs', WantedConstraints
lhs_wanted
, GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc)
rhs', WantedConstraints
rhs_wanted, Type
rule_ty) = ([TcTyVar],
GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc),
WantedConstraints,
GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc),
WantedConstraints, Type)
stuff
; String -> SDoc -> TcRn ()
traceTc String
"tcRule 1" ([SDoc] -> SDoc
vcat [ GenLocated SrcSpan (SourceText, RuleName) -> SDoc
pprFullRuleName XRec GhcRn (SourceText, RuleName)
rname
, forall a. Outputable a => a -> SDoc
ppr WantedConstraints
lhs_wanted
, 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
; let tpl_ids :: [TcTyVar]
tpl_ids = [TcTyVar]
lhs_evs forall a. [a] -> [a] -> [a]
++ [TcTyVar]
id_bndrs
; CandidatesQTvs
forall_tkvs <- [Type] -> TcM CandidatesQTvs
candidateQTyVarsOfTypes (Type
rule_ty forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> Type
idType [TcTyVar]
tpl_ids)
; [TcTyVar]
qtkvs <- CandidatesQTvs -> TcM [TcTyVar]
quantifyTyVars CandidatesQTvs
forall_tkvs
; String -> SDoc -> TcRn ()
traceTc String
"tcRule" ([SDoc] -> SDoc
vcat [ GenLocated SrcSpan (SourceText, RuleName) -> SDoc
pprFullRuleName XRec GhcRn (SourceText, RuleName)
rname
, forall a. Outputable a => a -> SDoc
ppr CandidatesQTvs
forall_tkvs
, forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
qtkvs
, forall a. Outputable a => a -> SDoc
ppr Type
rule_ty
, [SDoc] -> SDoc
vcat [ forall a. Outputable a => a -> SDoc
ppr TcTyVar
id SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (TcTyVar -> Type
idType TcTyVar
id) | TcTyVar
id <- [TcTyVar]
tpl_ids ]
])
; let skol_info :: SkolemInfo
skol_info = RuleName -> SkolemInfo
RuleSkol RuleName
name
; (Bag Implication
lhs_implic, TcEvBinds
lhs_binds) <- TcLevel
-> SkolemInfo
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl SkolemInfo
skol_info [TcTyVar]
qtkvs
[TcTyVar]
lhs_evs WantedConstraints
residual_lhs_wanted
; (Bag Implication
rhs_implic, TcEvBinds
rhs_binds) <- TcLevel
-> SkolemInfo
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl SkolemInfo
skol_info [TcTyVar]
qtkvs
[TcTyVar]
lhs_evs WantedConstraints
rhs_wanted
; Bag Implication -> TcRn ()
emitImplications (Bag Implication
lhs_implic forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Implication
rhs_implic)
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HsRule { rd_ext :: XHsRule GhcTc
rd_ext = XHsRule GhcRn
ext
, rd_name :: XRec GhcTc (SourceText, RuleName)
rd_name = XRec GhcRn (SourceText, RuleName)
rname
, rd_act :: Activation
rd_act = Activation
act
, rd_tyvs :: Maybe [LHsTyVarBndr () (NoGhcTc GhcTc)]
rd_tyvs = Maybe [LHsTyVarBndr () (NoGhcTc GhcRn)]
ty_bndrs
, rd_tmvs :: [LRuleBndr GhcTc]
rd_tmvs = forall a b. (a -> b) -> [a] -> [b]
map (forall e. e -> Located e
noLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall pass. XCRuleBndr pass -> LIdP pass -> RuleBndr pass
RuleBndr forall a. EpAnn a
noAnn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a an. a -> LocatedAn an a
noLocA)
([TcTyVar]
qtkvs forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tpl_ids)
, rd_lhs :: LHsExpr GhcTc
rd_lhs = TcEvBinds -> LHsExpr GhcTc -> LHsExpr GhcTc
mkHsDictLet TcEvBinds
lhs_binds GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc)
lhs'
, rd_rhs :: LHsExpr GhcTc
rd_rhs = TcEvBinds -> LHsExpr GhcTc -> LHsExpr GhcTc
mkHsDictLet TcEvBinds
rhs_binds GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc)
rhs' } }
generateRuleConstraints :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
-> LHsExpr GhcRn -> LHsExpr GhcRn
-> TcM ( [TcId]
, LHsExpr GhcTc, WantedConstraints
, LHsExpr GhcTc, WantedConstraints
, TcType )
generateRuleConstraints :: Maybe [LHsTyVarBndr () GhcRn]
-> [LRuleBndr GhcRn]
-> XRec GhcRn (HsExpr GhcRn)
-> XRec GhcRn (HsExpr GhcRn)
-> TcM
([TcTyVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
WantedConstraints, Type)
generateRuleConstraints Maybe [LHsTyVarBndr () GhcRn]
ty_bndrs [LRuleBndr GhcRn]
tm_bndrs XRec GhcRn (HsExpr GhcRn)
lhs XRec GhcRn (HsExpr GhcRn)
rhs
= do { (([TcTyVar]
tv_bndrs, [TcTyVar]
id_bndrs), WantedConstraints
bndr_wanted) <- forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints forall a b. (a -> b) -> a -> b
$
Maybe [LHsTyVarBndr () GhcRn]
-> [LRuleBndr GhcRn] -> TcM ([TcTyVar], [TcTyVar])
tcRuleBndrs Maybe [LHsTyVarBndr () GhcRn]
ty_bndrs [LRuleBndr GhcRn]
tm_bndrs
; forall r. [TcTyVar] -> TcM r -> TcM r
tcExtendTyVarEnv [TcTyVar]
tv_bndrs forall a b. (a -> b) -> a -> b
$
forall r. [TcTyVar] -> TcM r -> TcM r
tcExtendIdEnv [TcTyVar]
id_bndrs forall a b. (a -> b) -> a -> b
$
do {
((GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc)
lhs', Type
rule_ty), WantedConstraints
lhs_wanted) <- forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (XRec GhcRn (HsExpr GhcRn) -> TcM (LHsExpr GhcTc, Type)
tcInferRho XRec GhcRn (HsExpr GhcRn)
lhs)
; (GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc)
rhs', WantedConstraints
rhs_wanted) <- forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints forall a b. (a -> b) -> a -> b
$
XRec GhcRn (HsExpr GhcRn) -> Type -> TcM (LHsExpr GhcTc)
tcCheckMonoExpr XRec GhcRn (HsExpr GhcRn)
rhs Type
rule_ty
; let all_lhs_wanted :: WantedConstraints
all_lhs_wanted = WantedConstraints
bndr_wanted WantedConstraints -> WantedConstraints -> WantedConstraints
`andWC` WantedConstraints
lhs_wanted
; forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
id_bndrs, GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc)
lhs', WantedConstraints
all_lhs_wanted, GenLocated (SrcSpanAnn' (EpAnn AnnListItem)) (HsExpr GhcTc)
rhs', WantedConstraints
rhs_wanted, Type
rule_ty) } }
tcRuleBndrs :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
-> TcM ([TcTyVar], [Id])
tcRuleBndrs :: Maybe [LHsTyVarBndr () GhcRn]
-> [LRuleBndr GhcRn] -> TcM ([TcTyVar], [TcTyVar])
tcRuleBndrs (Just [LHsTyVarBndr () GhcRn]
bndrs) [LRuleBndr GhcRn]
xs
= do { ([VarBndr TcTyVar ()]
tybndrs1,([TcTyVar]
tys2,[TcTyVar]
tms)) <- forall flag a.
OutputableBndrFlag flag 'Renamed =>
[LHsTyVarBndr flag GhcRn]
-> TcM a -> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Skol [LHsTyVarBndr () GhcRn]
bndrs forall a b. (a -> b) -> a -> b
$
[LRuleBndr GhcRn] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
xs
; let tys1 :: [TcTyVar]
tys1 = forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr TcTyVar ()]
tybndrs1
; forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
tys1 forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tys2, [TcTyVar]
tms) }
tcRuleBndrs Maybe [LHsTyVarBndr () GhcRn]
Nothing [LRuleBndr GhcRn]
xs
= [LRuleBndr GhcRn] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
xs
tcRuleTmBndrs :: [LRuleBndr GhcRn] -> TcM ([TcTyVar],[Id])
tcRuleTmBndrs :: [LRuleBndr GhcRn] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs [] = forall (m :: * -> *) a. Monad m => a -> m a
return ([],[])
tcRuleTmBndrs (L SrcSpan
_ (RuleBndr XCRuleBndr GhcRn
_ (L SrcSpanAnnN
_ Name
name)) : [LRuleBndr GhcRn]
rule_bndrs)
= do { Type
ty <- TcM Type
newOpenFlexiTyVarTy
; ([TcTyVar]
tyvars, [TcTyVar]
tmvars) <- [LRuleBndr GhcRn] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
rule_bndrs
; forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
tyvars, HasDebugCallStack => Name -> Type -> Type -> TcTyVar
mkLocalId Name
name Type
Many Type
ty forall a. a -> [a] -> [a]
: [TcTyVar]
tmvars) }
tcRuleTmBndrs (L SrcSpan
_ (RuleBndrSig XRuleBndrSig GhcRn
_ (L SrcSpanAnnN
_ Name
name) HsPatSigType GhcRn
rn_ty) : [LRuleBndr GhcRn]
rule_bndrs)
= do { let ctxt :: UserTypeCtxt
ctxt = Name -> UserTypeCtxt
RuleSigCtxt Name
name
; ([(Name, TcTyVar)]
_ , [(Name, TcTyVar)]
tvs, Type
id_ty) <- UserTypeCtxt
-> HoleMode
-> HsPatSigType GhcRn
-> ContextKind
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
tcHsPatSigType UserTypeCtxt
ctxt HoleMode
HM_Sig HsPatSigType GhcRn
rn_ty ContextKind
OpenKind
; let id :: TcTyVar
id = HasDebugCallStack => Name -> Type -> Type -> TcTyVar
mkLocalId Name
name Type
Many Type
id_ty
; ([TcTyVar]
tyvars, [TcTyVar]
tmvars) <- forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, TcTyVar)]
tvs forall a b. (a -> b) -> a -> b
$
[LRuleBndr GhcRn] -> TcM ([TcTyVar], [TcTyVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
rule_bndrs
; forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Name, TcTyVar)]
tvs forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tyvars, TcTyVar
id forall a. a -> [a] -> [a]
: [TcTyVar]
tmvars) }
ruleCtxt :: FastString -> SDoc
ruleCtxt :: RuleName -> SDoc
ruleCtxt RuleName
name = String -> SDoc
text String
"When checking the rewrite rule" SDoc -> SDoc -> SDoc
<+>
SDoc -> SDoc
doubleQuotes (RuleName -> SDoc
ftext RuleName
name)
simplifyRule :: RuleName
-> TcLevel
-> WantedConstraints
-> WantedConstraints
-> TcM ( [EvVar]
, WantedConstraints)
simplifyRule :: RuleName
-> TcLevel
-> WantedConstraints
-> WantedConstraints
-> TcM ([TcTyVar], WantedConstraints)
simplifyRule RuleName
name TcLevel
tc_lvl WantedConstraints
lhs_wanted WantedConstraints
rhs_wanted
= do {
; WantedConstraints
lhs_clone <- WantedConstraints -> TcM WantedConstraints
cloneWC WantedConstraints
lhs_wanted
; WantedConstraints
rhs_clone <- WantedConstraints -> TcM WantedConstraints
cloneWC WantedConstraints
rhs_wanted
; forall a. TcLevel -> TcM a -> TcM a
setTcLevel TcLevel
tc_lvl forall a b. (a -> b) -> a -> b
$
forall a. TcS a -> TcM a
runTcSDeriveds forall a b. (a -> b) -> a -> b
$
do { WantedConstraints
_ <- WantedConstraints -> TcS WantedConstraints
solveWanteds WantedConstraints
lhs_clone
; WantedConstraints
_ <- WantedConstraints -> TcS WantedConstraints
solveWanteds WantedConstraints
rhs_clone
; forall (m :: * -> *) a. Monad m => a -> m a
return () }
; 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
; [TcTyVar]
quant_evs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Ct -> TcM TcTyVar
mk_quant_ev (forall a. Bag a -> [a]
bagToList Cts
quant_cts)
; String -> SDoc -> TcRn ()
traceTc String
"simplifyRule" forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"LHS of rule" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
doubleQuotes (RuleName -> SDoc
ftext RuleName
name)
, String -> SDoc
text String
"lhs_wanted" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr WantedConstraints
lhs_wanted
, String -> SDoc
text String
"rhs_wanted" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr WantedConstraints
rhs_wanted
, String -> SDoc
text String
"quant_cts" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Cts
quant_cts
, String -> SDoc
text String
"residual_lhs_wanted" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr WantedConstraints
residual_lhs_wanted
]
; 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 -> TcM 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
ev_id
HoleDest CoercionHole
hole ->
do { TcTyVar
ev_id <- forall gbl lcl. Type -> TcRnIf gbl lcl TcTyVar
newEvVar Type
pred
; CoercionHole -> Coercion -> TcRn ()
fillCoercionHole CoercionHole
hole (TcTyVar -> Coercion
mkTcCoVarCo TcTyVar
ev_id)
; forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
ev_id }
mk_quant_ev Ct
ct = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mk_quant_ev" (forall a. Outputable a => a -> SDoc
ppr Ct
ct)
getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
getRuleQuantCts WantedConstraints
wc
= TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc TcTyCoVarSet
emptyVarSet WantedConstraints
wc
where
float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc TcTyCoVarSet
skol_tvs (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes })
= ( Cts
simple_yes Cts -> Cts -> Cts
`andCts` Cts
implic_yes
, WantedConstraints
emptyWC { wc_simple :: Cts
wc_simple = Cts
simple_no, wc_impl :: Bag Implication
wc_impl = Bag Implication
implics_no, wc_holes :: Bag Hole
wc_holes = Bag Hole
holes })
where
(Cts
simple_yes, Cts
simple_no) = forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag (TcTyCoVarSet -> Ct -> Bool
rule_quant_ct TcTyCoVarSet
skol_tvs) Cts
simples
(Cts
implic_yes, Bag Implication
implics_no) = forall acc x y.
(acc -> x -> (acc, y)) -> acc -> Bag x -> (acc, Bag y)
mapAccumBagL (TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
float_implic TcTyCoVarSet
skol_tvs)
forall a. Bag a
emptyBag Bag Implication
implics
float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
float_implic TcTyCoVarSet
skol_tvs Cts
yes1 Implication
imp
= (Cts
yes1 Cts -> Cts -> Cts
`andCts` Cts
yes2, Implication
imp { ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
no })
where
(Cts
yes2, WantedConstraints
no) = TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
float_wc TcTyCoVarSet
new_skol_tvs (Implication -> WantedConstraints
ic_wanted Implication
imp)
new_skol_tvs :: TcTyCoVarSet
new_skol_tvs = TcTyCoVarSet
skol_tvs TcTyCoVarSet -> [TcTyVar] -> TcTyCoVarSet
`extendVarSetList` Implication -> [TcTyVar]
ic_skols Implication
imp
rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
rule_quant_ct TcTyCoVarSet
skol_tvs Ct
ct
| EqPred EqRel
_ Type
t1 Type
t2 <- Type -> Pred
classifyPredType (Ct -> Type
ctPred Ct
ct)
, Bool -> Bool
not (Type -> Type -> Bool
ok_eq Type
t1 Type
t2)
= Bool
False
| Bool
otherwise
= Ct -> TcTyCoVarSet
tyCoVarsOfCt Ct
ct TcTyCoVarSet -> TcTyCoVarSet -> Bool
`disjointVarSet` TcTyCoVarSet
skol_tvs
ok_eq :: Type -> Type -> Bool
ok_eq Type
t1 Type
t2
| Type
t1 HasDebugCallStack => 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
= case Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty of
Just TyCon
tc -> TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
Maybe TyCon
Nothing -> Bool
False