{-# 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.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
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)
; (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
; let tpl_ids :: [TcTyVar]
tpl_ids = [TcTyVar]
lhs_evs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
id_bndrs
; 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 ]
])
; (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
, 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
; [(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 {
((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) } }
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
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)
= 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
; ([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)
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
; 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
; () -> TcS ()
forall a. a -> TcS a
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 <- (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 ->
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)
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
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
= case Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty of
Just TyCon
tc -> TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
Maybe TyCon
Nothing -> Bool
False