{-# 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 = (Located (RuleDecls GhcRn)
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (RuleDecls GhcTc)))
-> [Located (RuleDecls GhcRn)]
-> IOEnv (Env TcGblEnv TcLclEnv) [Located (RuleDecls GhcTc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((RuleDecls GhcRn -> TcM (RuleDecls GhcTc))
-> Located (RuleDecls GhcRn)
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (RuleDecls GhcTc))
forall a b. (a -> TcM b) -> Located a -> TcM (Located b)
wrapLocM RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
tcRuleDecls) [Located (RuleDecls GhcRn)]
[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 { [Located (RuleDecl GhcTc)]
tc_decls <- (Located (RuleDecl GhcRn)
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (RuleDecl GhcTc)))
-> [Located (RuleDecl GhcRn)]
-> IOEnv (Env TcGblEnv TcLclEnv) [Located (RuleDecl GhcTc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((RuleDecl GhcRn -> TcM (RuleDecl GhcTc))
-> Located (RuleDecl GhcRn)
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (RuleDecl GhcTc))
forall a b. (a -> TcM b) -> Located a -> TcM (Located b)
wrapLocM RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
tcRule) [Located (RuleDecl GhcRn)]
[LRuleDecl GhcRn]
decls
; RuleDecls GhcTc -> TcM (RuleDecls GhcTc)
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 :: forall pass.
XCRuleDecls pass
-> SourceText -> [LRuleDecl pass] -> RuleDecls pass
HsRules { rds_ext :: XCRuleDecls GhcTc
rds_ext = NoExtField
XCRuleDecls GhcTc
noExtField
, rds_src :: SourceText
rds_src = SourceText
src
, rds_rules :: [LRuleDecl GhcTc]
rds_rules = [Located (RuleDecl GhcTc)]
[LRuleDecl 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 _ (_,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 })
= 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 ------" (Located (SourceText, RuleName) -> SDoc
pprFullRuleName Located (SourceText, RuleName)
XRec GhcRn (SourceText, RuleName)
rname)
; (TcLevel
tc_lvl, ([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
stuff) <- TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
(TcLevel,
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind))
forall a. TcM a -> TcM (TcLevel, a)
pushTcLevelM (TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
(TcLevel,
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)))
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
(TcLevel,
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind))
forall a b. (a -> b) -> a -> b
$
Maybe [LHsTyVarBndr () GhcRn]
-> [LRuleBndr GhcRn]
-> XRec GhcRn (HsExpr GhcRn)
-> XRec GhcRn (HsExpr GhcRn)
-> TcM
([EvVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
WantedConstraints, Kind)
generateRuleConstraints Maybe [LHsTyVarBndr () GhcRn]
Maybe [LHsTyVarBndr () (NoGhcTc GhcRn)]
ty_bndrs [LRuleBndr GhcRn]
tm_bndrs XRec GhcRn (HsExpr GhcRn)
lhs XRec GhcRn (HsExpr GhcRn)
rhs
; let ([EvVar]
id_bndrs, Located (HsExpr GhcTc)
lhs', WantedConstraints
lhs_wanted
, Located (HsExpr GhcTc)
rhs', WantedConstraints
rhs_wanted, Kind
rule_ty) = ([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
stuff
; String -> SDoc -> TcRn ()
traceTc String
"tcRule 1" ([SDoc] -> SDoc
vcat [ Located (SourceText, RuleName) -> SDoc
pprFullRuleName Located (SourceText, RuleName)
XRec GhcRn (SourceText, 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 ])
; ([EvVar]
lhs_evs, WantedConstraints
residual_lhs_wanted)
<- RuleName
-> TcLevel
-> WantedConstraints
-> WantedConstraints
-> TcM ([EvVar], WantedConstraints)
simplifyRule RuleName
name TcLevel
tc_lvl WantedConstraints
lhs_wanted WantedConstraints
rhs_wanted
; let tpl_ids :: [EvVar]
tpl_ids = [EvVar]
lhs_evs [EvVar] -> [EvVar] -> [EvVar]
forall a. [a] -> [a] -> [a]
++ [EvVar]
id_bndrs
; CandidatesQTvs
forall_tkvs <- [Kind] -> TcM CandidatesQTvs
candidateQTyVarsOfTypes (Kind
rule_ty Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: (EvVar -> Kind) -> [EvVar] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map EvVar -> Kind
idType [EvVar]
tpl_ids)
; [EvVar]
qtkvs <- CandidatesQTvs -> TcM [EvVar]
quantifyTyVars CandidatesQTvs
forall_tkvs
; String -> SDoc -> TcRn ()
traceTc String
"tcRule" ([SDoc] -> SDoc
vcat [ Located (SourceText, RuleName) -> SDoc
pprFullRuleName Located (SourceText, RuleName)
XRec GhcRn (SourceText, RuleName)
rname
, CandidatesQTvs -> SDoc
forall a. Outputable a => a -> SDoc
ppr CandidatesQTvs
forall_tkvs
, [EvVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [EvVar]
qtkvs
, Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr Kind
rule_ty
, [SDoc] -> SDoc
vcat [ EvVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvVar
id SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (EvVar -> Kind
idType EvVar
id) | EvVar
id <- [EvVar]
tpl_ids ]
])
; let skol_info :: SkolemInfo
skol_info = RuleName -> SkolemInfo
RuleSkol RuleName
name
; (Bag Implication
lhs_implic, TcEvBinds
lhs_binds) <- TcLevel
-> SkolemInfo
-> [EvVar]
-> [EvVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl SkolemInfo
skol_info [EvVar]
qtkvs
[EvVar]
lhs_evs WantedConstraints
residual_lhs_wanted
; (Bag Implication
rhs_implic, TcEvBinds
rhs_binds) <- TcLevel
-> SkolemInfo
-> [EvVar]
-> [EvVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl SkolemInfo
skol_info [EvVar]
qtkvs
[EvVar]
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 (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 :: forall pass.
XHsRule pass
-> XRec pass (SourceText, RuleName)
-> Activation
-> Maybe [LHsTyVarBndr () (NoGhcTc pass)]
-> [LRuleBndr pass]
-> XRec pass (HsExpr pass)
-> XRec pass (HsExpr pass)
-> RuleDecl pass
HsRule { rd_ext :: XHsRule GhcTc
rd_ext = XHsRule GhcRn
XHsRule GhcTc
ext
, rd_name :: XRec GhcTc (SourceText, RuleName)
rd_name = XRec GhcRn (SourceText, RuleName)
XRec GhcTc (SourceText, RuleName)
rname
, rd_act :: Activation
rd_act = Activation
act
, rd_tyvs :: Maybe [LHsTyVarBndr () (NoGhcTc GhcTc)]
rd_tyvs = Maybe [LHsTyVarBndr () (NoGhcTc GhcRn)]
Maybe [LHsTyVarBndr () (NoGhcTc GhcTc)]
ty_bndrs
, rd_tmvs :: [LRuleBndr GhcTc]
rd_tmvs = (EvVar -> Located (RuleBndr GhcTc))
-> [EvVar] -> [Located (RuleBndr GhcTc)]
forall a b. (a -> b) -> [a] -> [b]
map (RuleBndr GhcTc -> Located (RuleBndr GhcTc)
forall e. e -> Located e
noLoc (RuleBndr GhcTc -> Located (RuleBndr GhcTc))
-> (EvVar -> RuleBndr GhcTc) -> EvVar -> Located (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 NoExtField
XCRuleBndr GhcTc
noExtField (Located EvVar -> RuleBndr GhcTc)
-> (EvVar -> Located EvVar) -> EvVar -> RuleBndr GhcTc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvVar -> Located EvVar
forall e. e -> Located e
noLoc)
([EvVar]
qtkvs [EvVar] -> [EvVar] -> [EvVar]
forall a. [a] -> [a] -> [a]
++ [EvVar]
tpl_ids)
, rd_lhs :: LHsExpr GhcTc
rd_lhs = TcEvBinds -> LHsExpr GhcTc -> LHsExpr GhcTc
mkHsDictLet TcEvBinds
lhs_binds Located (HsExpr GhcTc)
LHsExpr GhcTc
lhs'
, rd_rhs :: LHsExpr GhcTc
rd_rhs = TcEvBinds -> LHsExpr GhcTc -> LHsExpr GhcTc
mkHsDictLet TcEvBinds
rhs_binds Located (HsExpr GhcTc)
LHsExpr 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
([EvVar], LHsExpr GhcTc, WantedConstraints, LHsExpr GhcTc,
WantedConstraints, Kind)
generateRuleConstraints Maybe [LHsTyVarBndr () GhcRn]
ty_bndrs [LRuleBndr GhcRn]
tm_bndrs XRec GhcRn (HsExpr GhcRn)
lhs XRec GhcRn (HsExpr GhcRn)
rhs
= do { (([EvVar]
tv_bndrs, [EvVar]
id_bndrs), WantedConstraints
bndr_wanted) <- TcM ([EvVar], [EvVar])
-> TcM (([EvVar], [EvVar]), WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM ([EvVar], [EvVar])
-> TcM (([EvVar], [EvVar]), WantedConstraints))
-> TcM ([EvVar], [EvVar])
-> TcM (([EvVar], [EvVar]), WantedConstraints)
forall a b. (a -> b) -> a -> b
$
Maybe [LHsTyVarBndr () GhcRn]
-> [LRuleBndr GhcRn] -> TcM ([EvVar], [EvVar])
tcRuleBndrs Maybe [LHsTyVarBndr () GhcRn]
ty_bndrs [LRuleBndr GhcRn]
tm_bndrs
; [EvVar]
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
forall r. [EvVar] -> TcM r -> TcM r
tcExtendTyVarEnv [EvVar]
tv_bndrs (TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind))
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
forall a b. (a -> b) -> a -> b
$
[EvVar]
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
forall r. [EvVar] -> TcM r -> TcM r
tcExtendIdEnv [EvVar]
id_bndrs (TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind))
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
forall a b. (a -> b) -> a -> b
$
do {
((Located (HsExpr GhcTc)
lhs', Kind
rule_ty), WantedConstraints
lhs_wanted) <- TcM (Located (HsExpr GhcTc), Kind)
-> TcM ((Located (HsExpr GhcTc), Kind), WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (XRec GhcRn (HsExpr GhcRn) -> TcM (LHsExpr GhcTc, Kind)
tcInferRho XRec GhcRn (HsExpr GhcRn)
lhs)
; (Located (HsExpr GhcTc)
rhs', WantedConstraints
rhs_wanted) <- TcM (Located (HsExpr GhcTc))
-> TcM (Located (HsExpr GhcTc), WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM (Located (HsExpr GhcTc))
-> TcM (Located (HsExpr GhcTc), WantedConstraints))
-> TcM (Located (HsExpr GhcTc))
-> TcM (Located (HsExpr GhcTc), WantedConstraints)
forall a b. (a -> b) -> a -> b
$
XRec GhcRn (HsExpr GhcRn) -> Kind -> TcM (LHsExpr GhcTc)
tcCheckMonoExpr XRec GhcRn (HsExpr GhcRn)
rhs Kind
rule_ty
; let all_lhs_wanted :: WantedConstraints
all_lhs_wanted = WantedConstraints
bndr_wanted WantedConstraints -> WantedConstraints -> WantedConstraints
`andWC` WantedConstraints
lhs_wanted
; ([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
-> TcM
([EvVar], Located (HsExpr GhcTc), WantedConstraints,
Located (HsExpr GhcTc), WantedConstraints, Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return ([EvVar]
id_bndrs, Located (HsExpr GhcTc)
lhs', WantedConstraints
all_lhs_wanted, Located (HsExpr GhcTc)
rhs', WantedConstraints
rhs_wanted, Kind
rule_ty) } }
tcRuleBndrs :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
-> TcM ([TcTyVar], [Id])
tcRuleBndrs :: Maybe [LHsTyVarBndr () GhcRn]
-> [LRuleBndr GhcRn] -> TcM ([EvVar], [EvVar])
tcRuleBndrs (Just [LHsTyVarBndr () GhcRn]
bndrs) [LRuleBndr GhcRn]
xs
= do { ([VarBndr EvVar ()]
tybndrs1,([EvVar]
tys2,[EvVar]
tms)) <- [LHsTyVarBndr () GhcRn]
-> TcM ([EvVar], [EvVar])
-> TcM ([VarBndr EvVar ()], ([EvVar], [EvVar]))
forall flag a.
OutputableBndrFlag flag =>
[LHsTyVarBndr flag GhcRn] -> TcM a -> TcM ([VarBndr EvVar flag], a)
bindExplicitTKBndrs_Skol [LHsTyVarBndr () GhcRn]
bndrs (TcM ([EvVar], [EvVar])
-> TcM ([VarBndr EvVar ()], ([EvVar], [EvVar])))
-> TcM ([EvVar], [EvVar])
-> TcM ([VarBndr EvVar ()], ([EvVar], [EvVar]))
forall a b. (a -> b) -> a -> b
$
[LRuleBndr GhcRn] -> TcM ([EvVar], [EvVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
xs
; let tys1 :: [EvVar]
tys1 = [VarBndr EvVar ()] -> [EvVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr EvVar ()]
tybndrs1
; ([EvVar], [EvVar]) -> TcM ([EvVar], [EvVar])
forall (m :: * -> *) a. Monad m => a -> m a
return ([EvVar]
tys1 [EvVar] -> [EvVar] -> [EvVar]
forall a. [a] -> [a] -> [a]
++ [EvVar]
tys2, [EvVar]
tms) }
tcRuleBndrs Maybe [LHsTyVarBndr () GhcRn]
Nothing [LRuleBndr GhcRn]
xs
= [LRuleBndr GhcRn] -> TcM ([EvVar], [EvVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
xs
tcRuleTmBndrs :: [LRuleBndr GhcRn] -> TcM ([TcTyVar],[Id])
tcRuleTmBndrs :: [LRuleBndr GhcRn] -> TcM ([EvVar], [EvVar])
tcRuleTmBndrs [] = ([EvVar], [EvVar]) -> TcM ([EvVar], [EvVar])
forall (m :: * -> *) a. Monad m => a -> m a
return ([],[])
tcRuleTmBndrs (L _ (RuleBndr _ (L _ name)) : [LRuleBndr GhcRn]
rule_bndrs)
= do { Kind
ty <- TcM Kind
newOpenFlexiTyVarTy
; ([EvVar]
tyvars, [EvVar]
tmvars) <- [LRuleBndr GhcRn] -> TcM ([EvVar], [EvVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
rule_bndrs
; ([EvVar], [EvVar]) -> TcM ([EvVar], [EvVar])
forall (m :: * -> *) a. Monad m => a -> m a
return ([EvVar]
tyvars, HasDebugCallStack => Name -> Kind -> Kind -> EvVar
Name -> Kind -> Kind -> EvVar
mkLocalId Name
name Kind
Many Kind
ty EvVar -> [EvVar] -> [EvVar]
forall a. a -> [a] -> [a]
: [EvVar]
tmvars) }
tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name) rn_ty) : [LRuleBndr GhcRn]
rule_bndrs)
= do { let ctxt :: UserTypeCtxt
ctxt = Name -> UserTypeCtxt
RuleSigCtxt Name
name
; ([(Name, EvVar)]
_ , [(Name, EvVar)]
tvs, Kind
id_ty) <- UserTypeCtxt
-> HoleMode
-> HsPatSigType GhcRn
-> ContextKind
-> TcM ([(Name, EvVar)], [(Name, EvVar)], Kind)
tcHsPatSigType UserTypeCtxt
ctxt HoleMode
HM_Sig HsPatSigType GhcRn
rn_ty ContextKind
OpenKind
; let id :: EvVar
id = HasDebugCallStack => Name -> Kind -> Kind -> EvVar
Name -> Kind -> Kind -> EvVar
mkLocalId Name
name Kind
Many Kind
id_ty
; ([EvVar]
tyvars, [EvVar]
tmvars) <- [(Name, EvVar)] -> TcM ([EvVar], [EvVar]) -> TcM ([EvVar], [EvVar])
forall r. [(Name, EvVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, EvVar)]
tvs (TcM ([EvVar], [EvVar]) -> TcM ([EvVar], [EvVar]))
-> TcM ([EvVar], [EvVar]) -> TcM ([EvVar], [EvVar])
forall a b. (a -> b) -> a -> b
$
[LRuleBndr GhcRn] -> TcM ([EvVar], [EvVar])
tcRuleTmBndrs [LRuleBndr GhcRn]
rule_bndrs
; ([EvVar], [EvVar]) -> TcM ([EvVar], [EvVar])
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, EvVar) -> EvVar) -> [(Name, EvVar)] -> [EvVar]
forall a b. (a -> b) -> [a] -> [b]
map (Name, EvVar) -> EvVar
forall a b. (a, b) -> b
snd [(Name, EvVar)]
tvs [EvVar] -> [EvVar] -> [EvVar]
forall a. [a] -> [a] -> [a]
++ [EvVar]
tyvars, EvVar
id EvVar -> [EvVar] -> [EvVar]
forall a. a -> [a] -> [a]
: [EvVar]
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 ([EvVar], 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
$
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
; () -> TcS ()
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
; [EvVar]
quant_evs <- (Ct -> IOEnv (Env TcGblEnv TcLclEnv) EvVar) -> [Ct] -> TcM [EvVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Ct -> IOEnv (Env TcGblEnv TcLclEnv) EvVar
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
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
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
lhs_wanted
, String -> SDoc
text String
"rhs_wanted" SDoc -> SDoc -> SDoc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
rhs_wanted
, String -> SDoc
text String
"quant_cts" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
quant_cts
, String -> SDoc
text String
"residual_lhs_wanted" SDoc -> SDoc -> SDoc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
residual_lhs_wanted
]
; ([EvVar], WantedConstraints) -> TcM ([EvVar], WantedConstraints)
forall (m :: * -> *) a. Monad m => a -> m a
return ([EvVar]
quant_evs, WantedConstraints
residual_lhs_wanted) }
where
mk_quant_ev :: Ct -> TcM EvVar
mk_quant_ev :: Ct -> IOEnv (Env TcGblEnv TcLclEnv) EvVar
mk_quant_ev Ct
ct
| CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_pred :: CtEvidence -> Kind
ctev_pred = Kind
pred } <- Ct -> CtEvidence
ctEvidence Ct
ct
= case TcEvDest
dest of
EvVarDest EvVar
ev_id -> EvVar -> IOEnv (Env TcGblEnv TcLclEnv) EvVar
forall (m :: * -> *) a. Monad m => a -> m a
return EvVar
ev_id
HoleDest CoercionHole
hole ->
do { EvVar
ev_id <- Kind -> IOEnv (Env TcGblEnv TcLclEnv) EvVar
forall gbl lcl. Kind -> TcRnIf gbl lcl EvVar
newEvVar Kind
pred
; CoercionHole -> Coercion -> TcRn ()
fillCoercionHole CoercionHole
hole (EvVar -> Coercion
mkTcCoVarCo EvVar
ev_id)
; EvVar -> IOEnv (Env TcGblEnv TcLclEnv) EvVar
forall (m :: * -> *) a. Monad m => a -> m a
return EvVar
ev_id }
mk_quant_ev Ct
ct = String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) EvVar
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
= 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) = (Ct -> Bool) -> Cts -> (Cts, Cts)
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) = (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 (TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
float_implic TcTyCoVarSet
skol_tvs)
Cts
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 -> [EvVar] -> TcTyCoVarSet
`extendVarSetList` Implication -> [EvVar]
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
_ Kind
t1 Kind
t2 <- Kind -> Pred
classifyPredType (Ct -> Kind
ctPred Ct
ct)
, Bool -> Bool
not (Kind -> Kind -> Bool
ok_eq Kind
t1 Kind
t2)
= Bool
False
| Bool
otherwise
= Ct -> TcTyCoVarSet
tyCoVarsOfCt Ct
ct TcTyCoVarSet -> TcTyCoVarSet -> Bool
`disjointVarSet` TcTyCoVarSet
skol_tvs
ok_eq :: Kind -> Kind -> Bool
ok_eq Kind
t1 Kind
t2
| Kind
t1 HasDebugCallStack => Kind -> Kind -> Bool
Kind -> Kind -> Bool
`tcEqType` Kind
t2 = Bool
False
| Bool
otherwise = Kind -> Bool
is_fun_app Kind
t1 Bool -> Bool -> Bool
|| Kind -> Bool
is_fun_app Kind
t2
is_fun_app :: Kind -> Bool
is_fun_app Kind
ty
= case Kind -> Maybe TyCon
tyConAppTyCon_maybe Kind
ty of
Just TyCon
tc -> TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
Maybe TyCon
Nothing -> Bool
False