{-# LANGUAGE RecursiveDo #-}
module GHC.Tc.Solver.Solve (
simplifyWantedsTcM,
solveWanteds,
solveSimpleGivens,
solveSimpleWanteds,
setImplicationStatus
) where
import GHC.Prelude
import GHC.Tc.Solver.Dict
import GHC.Tc.Solver.Equality( solveEquality )
import GHC.Tc.Solver.Irred( solveIrred )
import GHC.Tc.Solver.Rewrite( rewrite, rewriteType )
import GHC.Tc.Errors.Types
import GHC.Tc.Utils.TcType
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.CtLoc( ctLocEnv, ctLocOrigin, setCtLocOrigin )
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc( mkGivenLoc )
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Tc.Utils.Monad as TcM
import GHC.Tc.Zonk.TcType as TcM
import GHC.Tc.Solver.Monad as TcS
import GHC.Core.Predicate
import GHC.Core.Reduction
import GHC.Core.Coercion
import GHC.Core.Class( classHasSCs )
import GHC.Types.Id( idType )
import GHC.Types.Var( EvVar, tyVarKind )
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Basic ( IntWithInf, intGtLimit )
import GHC.Data.Bag
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc
import GHC.Driver.Session
import Data.List( deleteFirstsBy )
import Control.Monad
import qualified Data.Semigroup as S
import Data.Void( Void )
simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
simplifyWantedsTcM [CtEvidence]
wanted
= do { String -> SDoc -> TcRn ()
traceTc String
"simplifyWantedsTcM {" ([CtEvidence] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
wanted)
; (result, _) <- TcS WantedConstraints -> TcM (WantedConstraints, EvBindMap)
forall a. TcS a -> TcM (a, EvBindMap)
runTcS (WantedConstraints -> TcS WantedConstraints
solveWanteds ([CtEvidence] -> WantedConstraints
mkSimpleWC [CtEvidence]
wanted))
; result <- TcM.liftZonkM $ TcM.zonkWC result
; traceTc "simplifyWantedsTcM }" (ppr result)
; return result }
solveWanteds :: WantedConstraints -> TcS WantedConstraints
solveWanteds :: WantedConstraints -> TcS WantedConstraints
solveWanteds wc :: WantedConstraints
wc@(WC { wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
= do { cur_lvl <- TcS TcLevel
TcS.getTcLevel
; traceTcS "solveWanteds {" $
vcat [ text "Level =" <+> ppr cur_lvl
, ppr wc ]
; dflags <- getDynFlags
; solved_wc <- simplify_loop 0 (solverIterations dflags) True wc
; errs' <- simplifyDelayedErrors errs
; let final_wc = WantedConstraints
solved_wc { wc_errors = errs' }
; ev_binds_var <- getTcEvBindsVar
; bb <- TcS.getTcEvBindsMap ev_binds_var
; traceTcS "solveWanteds }" $
vcat [ text "final wc =" <+> ppr final_wc
, text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
; return final_wc }
simplify_loop :: Int -> IntWithInf -> Bool
-> WantedConstraints -> TcS WantedConstraints
simplify_loop :: Int
-> IntWithInf -> Bool -> WantedConstraints -> TcS WantedConstraints
simplify_loop Int
n IntWithInf
limit Bool
definitely_redo_implications
wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics })
| WantedConstraints -> Bool
isSolvedWC WantedConstraints
wc
= WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc
| Bool
otherwise
= do { SDoc -> TcS ()
csTraceTcS (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"simplify_loop iteration=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
n
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
hsep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"definitely_redo =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
definitely_redo_implications SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma
, Int -> SDoc
forall doc. IsLine doc => Int -> doc
int (Cts -> Int
forall a. Bag a -> Int
lengthBag Cts
simples) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"simples to solve" ])
; String -> SDoc -> TcS ()
traceTcS String
"simplify_loop: wc =" (WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wc)
; (unifs1, wc1) <- TcS WantedConstraints -> TcS (Int, WantedConstraints)
forall a. TcS a -> TcS (Int, a)
reportUnifications (TcS WantedConstraints -> TcS (Int, WantedConstraints))
-> TcS WantedConstraints -> TcS (Int, WantedConstraints)
forall a b. (a -> b) -> a -> b
$
Cts -> TcS WantedConstraints
solveSimpleWanteds Cts
simples
; wc2 <- if not definitely_redo_implications
&& unifs1 == 0
&& isEmptyBag (wc_impl wc1)
then return (wc { wc_simple = wc_simple wc1 })
else do { implics2 <- solveNestedImplications $
implics `unionBags` (wc_impl wc1)
; return (wc { wc_simple = wc_simple wc1
, wc_impl = implics2 }) }
; unif_happened <- resetUnificationFlag
; csTraceTcS $ text "unif_happened" <+> ppr unif_happened
; maybe_simplify_again (n+1) limit unif_happened wc2 }
maybe_simplify_again :: Int -> IntWithInf -> Bool
-> WantedConstraints -> TcS WantedConstraints
maybe_simplify_again :: Int
-> IntWithInf -> Bool -> WantedConstraints -> TcS WantedConstraints
maybe_simplify_again Int
n IntWithInf
limit Bool
unif_happened wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples })
| Int
n Int -> IntWithInf -> Bool
`intGtLimit` IntWithInf
limit
= do {
TcRnMessage -> TcS ()
addErrTcS (TcRnMessage -> TcS ()) -> TcRnMessage -> TcS ()
forall a b. (a -> b) -> a -> b
$ Cts -> IntWithInf -> WantedConstraints -> TcRnMessage
TcRnSimplifierTooManyIterations Cts
simples IntWithInf
limit WantedConstraints
wc
; WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc }
| Bool
unif_happened
= Int
-> IntWithInf -> Bool -> WantedConstraints -> TcS WantedConstraints
simplify_loop Int
n IntWithInf
limit Bool
True WantedConstraints
wc
| WantedConstraints -> Bool
superClassesMightHelp WantedConstraints
wc
=
do { pending_given <- TcS [Ct]
getPendingGivenScs
; let (pending_wanted, simples1) = getPendingWantedScs simples
; if null pending_given && null pending_wanted
then return wc
else
do { new_given <- makeSuperClasses pending_given
; new_wanted <- makeSuperClasses pending_wanted
; solveSimpleGivens new_given
; traceTcS "maybe_simplify_again" (vcat [ text "pending_given" <+> ppr pending_given
, text "new_given" <+> ppr new_given
, text "pending_wanted" <+> ppr pending_wanted
, text "new_wanted" <+> ppr new_wanted ])
; simplify_loop n limit (not (null pending_given)) $
wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
| Bool
otherwise
= WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc
solveNestedImplications :: Bag Implication
-> TcS (Bag Implication)
solveNestedImplications :: Bag Implication -> TcS (Bag Implication)
solveNestedImplications Bag Implication
implics
| Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics
= Bag Implication -> TcS (Bag Implication)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bag Implication
forall a. Bag a
emptyBag)
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"solveNestedImplications starting {" SDoc
forall doc. IsOutput doc => doc
empty
; unsolved_implics <- (Implication -> TcS (Maybe Implication))
-> Bag Implication -> TcS (Bag (Maybe Implication))
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Implication -> TcS (Maybe Implication)
solveImplication Bag Implication
implics
; traceTcS "solveNestedImplications end }" $
vcat [ text "unsolved_implics =" <+> ppr unsolved_implics ]
; return (catBagMaybes unsolved_implics) }
solveImplication :: Implication
-> TcS (Maybe Implication)
solveImplication :: Implication -> TcS (Maybe Implication)
solveImplication imp :: Implication
imp@(Implic { ic_tclvl :: Implication -> TcLevel
ic_tclvl = TcLevel
tclvl
, ic_binds :: Implication -> EvBindsVar
ic_binds = EvBindsVar
ev_binds_var
, ic_given :: Implication -> [EvVar]
ic_given = [EvVar]
given_ids
, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanteds
, ic_info :: Implication -> SkolemInfoAnon
ic_info = SkolemInfoAnon
info
, ic_status :: Implication -> ImplicStatus
ic_status = ImplicStatus
status })
| ImplicStatus -> Bool
isSolvedStatus ImplicStatus
status
= Maybe Implication -> TcS (Maybe Implication)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication -> Maybe Implication
forall a. a -> Maybe a
Just Implication
imp)
| Bool
otherwise
= do { inerts <- TcS InertSet
getInertSet
; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
; (has_given_eqs, given_insols, residual_wanted)
<- nestImplicTcS ev_binds_var tclvl $
do { let loc = TcLevel -> SkolemInfoAnon -> CtLocEnv -> CtLoc
mkGivenLoc TcLevel
tclvl SkolemInfoAnon
info (Implication -> CtLocEnv
ic_env Implication
imp)
givens = CtLoc -> [EvVar] -> [Ct]
mkGivens CtLoc
loc [EvVar]
given_ids
; solveSimpleGivens givens
; residual_wanted <- solveWanteds wanteds
; (has_eqs, given_insols) <- getHasGivenEqs tclvl
; return (has_eqs, given_insols, residual_wanted) }
; traceTcS "solveImplication 2"
(ppr given_insols $$ ppr residual_wanted)
; let final_wanted = WantedConstraints
residual_wanted WantedConstraints -> InertIrreds -> WantedConstraints
`addInsols` InertIrreds
given_insols
; res_implic <- setImplicationStatus (imp { ic_given_eqs = has_given_eqs
, ic_wanted = final_wanted })
; evbinds <- TcS.getTcEvBindsMap ev_binds_var
; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
; traceTcS "solveImplication end }" $ vcat
[ text "has_given_eqs =" <+> ppr has_given_eqs
, text "res_implic =" <+> ppr res_implic
, text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
, text "implication tvcs =" <+> ppr tcvs ]
; return res_implic }
setImplicationStatus :: Implication -> TcS (Maybe Implication)
setImplicationStatus :: Implication -> TcS (Maybe Implication)
setImplicationStatus implic :: Implication
implic@(Implic { ic_status :: Implication -> ImplicStatus
ic_status = ImplicStatus
old_status
, ic_info :: Implication -> SkolemInfoAnon
ic_info = SkolemInfoAnon
info
, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wc
, ic_given :: Implication -> [EvVar]
ic_given = [EvVar]
givens })
| Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (ImplicStatus -> Bool
isSolvedStatus ImplicStatus
old_status)) (SkolemInfoAnon -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfoAnon
info) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
Bool -> Bool
not (WantedConstraints -> Bool
isSolvedWC WantedConstraints
pruned_wc)
= do { String -> SDoc -> TcS ()
traceTcS String
"setImplicationStatus(not-all-solved) {" (Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr Implication
implic)
; implic <- Implication -> TcS Implication
neededEvVars Implication
implic
; let new_status | WantedConstraints -> Bool
insolubleWC WantedConstraints
pruned_wc = ImplicStatus
IC_Insoluble
| Bool
otherwise = ImplicStatus
IC_Unsolved
new_implic = Implication
implic { ic_status = new_status
, ic_wanted = pruned_wc }
; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic)
; return $ Just new_implic }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"setImplicationStatus(all-solved) {" (Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr Implication
implic)
; implic@(Implic { ic_need_inner = need_inner
, ic_need_outer = need_outer }) <- Implication -> TcS Implication
neededEvVars Implication
implic
; bad_telescope <- checkBadTelescope implic
; let warn_givens = SkolemInfoAnon -> VarSet -> [EvVar] -> [EvVar]
findUnnecessaryGivens SkolemInfoAnon
info VarSet
need_inner [EvVar]
givens
discard_entire_implication
= [EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
warn_givens
Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
bad_telescope
Bool -> Bool -> Bool
&& WantedConstraints -> Bool
isEmptyWC WantedConstraints
pruned_wc
Bool -> Bool -> Bool
&& VarSet -> Bool
isEmptyVarSet VarSet
need_outer
final_status
| Bool
bad_telescope = ImplicStatus
IC_BadTelescope
| Bool
otherwise = IC_Solved { ics_dead :: [EvVar]
ics_dead = [EvVar]
warn_givens }
final_implic = Implication
implic { ic_status = final_status
, ic_wanted = pruned_wc }
; traceTcS "setImplicationStatus(all-solved) }" $
vcat [ text "discard:" <+> ppr discard_entire_implication
, text "new_implic:" <+> ppr final_implic ]
; return $ if discard_entire_implication
then Nothing
else Just final_implic }
where
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 } = WantedConstraints
wc
pruned_implics :: Bag Implication
pruned_implics = (Implication -> Bool) -> Bag Implication -> Bag Implication
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Implication -> Bool
keep_me Bag Implication
implics
pruned_wc :: WantedConstraints
pruned_wc = WC { wc_simple :: Cts
wc_simple = Cts
simples
, wc_impl :: Bag Implication
wc_impl = Bag Implication
pruned_implics
, wc_errors :: Bag DelayedError
wc_errors = Bag DelayedError
errs }
keep_me :: Implication -> Bool
keep_me :: Implication -> Bool
keep_me Implication
ic
| IC_Solved { ics_dead :: ImplicStatus -> [EvVar]
ics_dead = [EvVar]
dead_givens } <- Implication -> ImplicStatus
ic_status Implication
ic
, [EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
dead_givens
, Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag (WantedConstraints -> Bag Implication
wc_impl (Implication -> WantedConstraints
ic_wanted Implication
ic))
= Bool
False
| Bool
otherwise
= Bool
True
findUnnecessaryGivens :: SkolemInfoAnon -> VarSet -> [EvVar] -> [EvVar]
findUnnecessaryGivens :: SkolemInfoAnon -> VarSet -> [EvVar] -> [EvVar]
findUnnecessaryGivens SkolemInfoAnon
info VarSet
need_inner [EvVar]
givens
| Bool -> Bool
not (SkolemInfoAnon -> Bool
warnRedundantGivens SkolemInfoAnon
info)
= []
| Bool -> Bool
not ([EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
unused_givens)
= [EvVar]
unused_givens
| Bool
otherwise
= [EvVar]
redundant_givens
where
in_instance_decl :: Bool
in_instance_decl = case SkolemInfoAnon
info of { InstSkol {} -> Bool
True; SkolemInfoAnon
_ -> Bool
False }
unused_givens :: [EvVar]
unused_givens = (EvVar -> Bool) -> [EvVar] -> [EvVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut EvVar -> Bool
is_used [EvVar]
givens
is_used :: EvVar -> Bool
is_used EvVar
given = EvVar -> Bool
is_type_error EvVar
given
Bool -> Bool -> Bool
|| EvVar
given EvVar -> VarSet -> Bool
`elemVarSet` VarSet
need_inner
Bool -> Bool -> Bool
|| (Bool
in_instance_decl Bool -> Bool -> Bool
&& TcType -> Bool
is_improving (EvVar -> TcType
idType EvVar
given))
minimal_givens :: [EvVar]
minimal_givens = (EvVar -> TcType) -> [EvVar] -> [EvVar]
forall a. (a -> TcType) -> [a] -> [a]
mkMinimalBySCs EvVar -> TcType
evVarPred [EvVar]
givens
is_minimal :: EvVar -> Bool
is_minimal = (EvVar -> VarSet -> Bool
`elemVarSet` [EvVar] -> VarSet
mkVarSet [EvVar]
minimal_givens)
redundant_givens :: [EvVar]
redundant_givens
| Bool
in_instance_decl = []
| Bool
otherwise = (EvVar -> Bool) -> [EvVar] -> [EvVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut EvVar -> Bool
is_minimal [EvVar]
givens
is_type_error :: EvVar -> Bool
is_type_error EvVar
id = TcType -> Bool
isTopLevelUserTypeError (EvVar -> TcType
idType EvVar
id)
is_improving :: TcType -> Bool
is_improving TcType
pred
= (TcType -> Bool) -> [TcType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcType -> Bool
isImprovementPred (TcType
pred TcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
: TcType -> [TcType]
transSuperClasses TcType
pred)
checkBadTelescope :: Implication -> TcS Bool
checkBadTelescope :: Implication -> TcS Bool
checkBadTelescope (Implic { ic_info :: Implication -> SkolemInfoAnon
ic_info = SkolemInfoAnon
info
, ic_skols :: Implication -> [EvVar]
ic_skols = [EvVar]
skols })
| SkolemInfoAnon -> Bool
checkTelescopeSkol SkolemInfoAnon
info
= do{ skols <- (EvVar -> TcS EvVar) -> [EvVar] -> TcS [EvVar]
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 EvVar -> TcS EvVar
TcS.zonkTyCoVarKind [EvVar]
skols
; return (go emptyVarSet (reverse skols))}
| Bool
otherwise
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
where
go :: TyVarSet
-> [TcTyVar]
-> Bool
go :: VarSet -> [EvVar] -> Bool
go VarSet
_ [] = Bool
False
go VarSet
later_skols (EvVar
one_skol : [EvVar]
earlier_skols)
| TcType -> VarSet
tyCoVarsOfType (EvVar -> TcType
tyVarKind EvVar
one_skol) VarSet -> VarSet -> Bool
`intersectsVarSet` VarSet
later_skols
= Bool
True
| Bool
otherwise
= VarSet -> [EvVar] -> Bool
go (VarSet
later_skols VarSet -> EvVar -> VarSet
`extendVarSet` EvVar
one_skol) [EvVar]
earlier_skols
warnRedundantGivens :: SkolemInfoAnon -> Bool
warnRedundantGivens :: SkolemInfoAnon -> Bool
warnRedundantGivens (SigSkol UserTypeCtxt
ctxt TcType
_ [(Name, EvVar)]
_)
= case UserTypeCtxt
ctxt of
FunSigCtxt Name
_ ReportRedundantConstraints
rrc -> ReportRedundantConstraints -> Bool
reportRedundantConstraints ReportRedundantConstraints
rrc
ExprSigCtxt ReportRedundantConstraints
rrc -> ReportRedundantConstraints -> Bool
reportRedundantConstraints ReportRedundantConstraints
rrc
UserTypeCtxt
_ -> Bool
False
warnRedundantGivens (InstSkol {}) = Bool
True
warnRedundantGivens SkolemInfoAnon
_ = Bool
False
neededEvVars :: Implication -> TcS Implication
neededEvVars :: Implication -> TcS Implication
neededEvVars implic :: Implication
implic@(Implic { ic_given :: Implication -> [EvVar]
ic_given = [EvVar]
givens
, ic_binds :: Implication -> EvBindsVar
ic_binds = EvBindsVar
ev_binds_var
, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WC { wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics }
, ic_need_inner :: Implication -> VarSet
ic_need_inner = VarSet
old_needs })
= do { ev_binds <- EvBindsVar -> TcS EvBindMap
TcS.getTcEvBindsMap EvBindsVar
ev_binds_var
; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
; let seeds1 = (Implication -> VarSet -> VarSet)
-> VarSet -> Bag Implication -> VarSet
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Implication -> VarSet -> VarSet
add_implic_seeds VarSet
old_needs Bag Implication
implics
seeds2 = (EvBind -> VarSet -> VarSet) -> VarSet -> EvBindMap -> VarSet
forall a. (EvBind -> a -> a) -> a -> EvBindMap -> a
nonDetStrictFoldEvBindMap EvBind -> VarSet -> VarSet
add_wanted VarSet
seeds1 EvBindMap
ev_binds
seeds3 = VarSet
seeds2 VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
tcvs
need_inner = EvBindMap -> VarSet -> VarSet
findNeededEvVars EvBindMap
ev_binds VarSet
seeds3
live_ev_binds = (EvBind -> Bool) -> EvBindMap -> EvBindMap
filterEvBindMap (VarSet -> EvBind -> Bool
needed_ev_bind VarSet
need_inner) EvBindMap
ev_binds
need_outer = VarSet -> EvBindMap -> VarSet
varSetMinusEvBindMap VarSet
need_inner EvBindMap
live_ev_binds
VarSet -> [EvVar] -> VarSet
`delVarSetList` [EvVar]
givens
; TcS.setTcEvBindsMap ev_binds_var live_ev_binds
; traceTcS "neededEvVars" $
vcat [ text "old_needs:" <+> ppr old_needs
, text "seeds3:" <+> ppr seeds3
, text "tcvs:" <+> ppr tcvs
, text "ev_binds:" <+> ppr ev_binds
, text "live_ev_binds:" <+> ppr live_ev_binds ]
; return (implic { ic_need_inner = need_inner
, ic_need_outer = need_outer }) }
where
add_implic_seeds :: Implication -> VarSet -> VarSet
add_implic_seeds (Implic { ic_need_outer :: Implication -> VarSet
ic_need_outer = VarSet
needs }) VarSet
acc
= VarSet
needs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
acc
needed_ev_bind :: VarSet -> EvBind -> Bool
needed_ev_bind VarSet
needed (EvBind { eb_lhs :: EvBind -> EvVar
eb_lhs = EvVar
ev_var
, eb_info :: EvBind -> EvBindInfo
eb_info = EvBindInfo
info })
| EvBindGiven{} <- EvBindInfo
info = EvVar
ev_var EvVar -> VarSet -> Bool
`elemVarSet` VarSet
needed
| Bool
otherwise = Bool
True
add_wanted :: EvBind -> VarSet -> VarSet
add_wanted :: EvBind -> VarSet -> VarSet
add_wanted (EvBind { eb_info :: EvBind -> EvBindInfo
eb_info = EvBindInfo
info, eb_rhs :: EvBind -> EvTerm
eb_rhs = EvTerm
rhs }) VarSet
needs
| EvBindGiven{} <- EvBindInfo
info = VarSet
needs
| Bool
otherwise = EvTerm -> VarSet
evVarsOfTerm EvTerm
rhs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
needs
simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError)
simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError)
simplifyDelayedErrors = (DelayedError -> TcS (Maybe DelayedError))
-> Bag DelayedError -> TcS (Bag DelayedError)
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> Bag a -> m (Bag b)
mapMaybeBagM DelayedError -> TcS (Maybe DelayedError)
simpl_err
where
simpl_err :: DelayedError -> TcS (Maybe DelayedError)
simpl_err :: DelayedError -> TcS (Maybe DelayedError)
simpl_err (DE_Hole Hole
hole) = DelayedError -> Maybe DelayedError
forall a. a -> Maybe a
Just (DelayedError -> Maybe DelayedError)
-> (Hole -> DelayedError) -> Hole -> Maybe DelayedError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hole -> DelayedError
DE_Hole (Hole -> Maybe DelayedError)
-> TcS Hole -> TcS (Maybe DelayedError)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hole -> TcS Hole
simpl_hole Hole
hole
simpl_err err :: DelayedError
err@(DE_NotConcrete {}) = Maybe DelayedError -> TcS (Maybe DelayedError)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DelayedError -> TcS (Maybe DelayedError))
-> Maybe DelayedError -> TcS (Maybe DelayedError)
forall a b. (a -> b) -> a -> b
$ DelayedError -> Maybe DelayedError
forall a. a -> Maybe a
Just DelayedError
err
simpl_err (DE_Multiplicity TcCoercion
mult_co CtLoc
loc)
= do { mult_co' <- TcCoercion -> TcS TcCoercion
TcS.zonkCo TcCoercion
mult_co
; if isReflexiveCo mult_co' then
return Nothing
else
return $ Just (DE_Multiplicity mult_co' loc) }
simpl_hole :: Hole -> TcS Hole
simpl_hole :: Hole -> TcS Hole
simpl_hole h :: Hole
h@(Hole { hole_sort :: Hole -> HoleSort
hole_sort = HoleSort
ConstraintHole }) = Hole -> TcS Hole
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Hole
h
simpl_hole h :: Hole
h@(Hole { hole_ty :: Hole -> TcType
hole_ty = TcType
ty, hole_loc :: Hole -> CtLoc
hole_loc = CtLoc
loc })
= do { ty' <- CtLoc -> TcType -> TcS TcType
rewriteType CtLoc
loc TcType
ty
; traceTcS "simpl_hole" (ppr ty $$ ppr ty')
; return (h { hole_ty = ty' }) }
solveSimpleGivens :: [Ct] -> TcS ()
solveSimpleGivens :: [Ct] -> TcS ()
solveSimpleGivens [Ct]
givens
| [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
givens
= () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"solveSimpleGivens {" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens)
; [Ct] -> TcS ()
go [Ct]
givens
; String -> SDoc -> TcS ()
traceTcS String
"End solveSimpleGivens }" SDoc
forall doc. IsOutput doc => doc
empty }
where
go :: [Ct] -> TcS ()
go [Ct]
givens = do { Cts -> TcS ()
solveSimples ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
givens)
; new_givens <- TcS [Ct]
runTcPluginsGiven
; when (notNull new_givens) $
go new_givens }
solveSimpleWanteds :: Cts -> TcS WantedConstraints
solveSimpleWanteds :: Cts -> TcS WantedConstraints
solveSimpleWanteds Cts
simples
= do { String -> SDoc -> TcS ()
traceTcS String
"solveSimpleWanteds {" (Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
simples)
; dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
; traceTcS "solveSimpleWanteds end }" $
vcat [ text "iterations =" <+> ppr n
, text "residual =" <+> ppr wc ]
; return wc }
where
go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
go :: Int
-> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
go Int
n IntWithInf
limit WantedConstraints
wc
| Int
n Int -> IntWithInf -> Bool
`intGtLimit` IntWithInf
limit
= TcRnMessage -> TcS (Int, WantedConstraints)
forall a. TcRnMessage -> TcS a
failTcS (TcRnMessage -> TcS (Int, WantedConstraints))
-> TcRnMessage -> TcS (Int, WantedConstraints)
forall a b. (a -> b) -> a -> b
$ Cts -> IntWithInf -> WantedConstraints -> TcRnMessage
TcRnSimplifierTooManyIterations Cts
simples IntWithInf
limit WantedConstraints
wc
| Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag (WantedConstraints -> Cts
wc_simple WantedConstraints
wc)
= (Int, WantedConstraints) -> TcS (Int, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n,WantedConstraints
wc)
| Bool
otherwise
= do {
wc1 <- WantedConstraints -> TcS WantedConstraints
solve_simple_wanteds WantedConstraints
wc
; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
; if rerun_plugin
then do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
; go (n+1) limit wc2 }
else return (n, wc2) }
solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints
solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints
solve_simple_wanteds (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples1, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics1, wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
= TcS WantedConstraints -> TcS WantedConstraints
forall a. TcS a -> TcS a
nestTcS (TcS WantedConstraints -> TcS WantedConstraints)
-> TcS WantedConstraints -> TcS WantedConstraints
forall a b. (a -> b) -> a -> b
$
do { Cts -> TcS ()
solveSimples Cts
simples1
; (implics2, unsolved) <- TcS (Bag Implication, Cts)
getUnsolvedInerts
; return (WC { wc_simple = unsolved
, wc_impl = implics1 `unionBags` implics2
, wc_errors = errs }) }
solveSimples :: Cts -> TcS ()
solveSimples :: Cts -> TcS ()
solveSimples Cts
cts
= {-# SCC "solveSimples" #-}
do { Cts -> TcS ()
emitWork Cts
cts; TcS ()
solve_loop }
where
solve_loop :: TcS ()
solve_loop
= {-# SCC "solve_loop" #-}
do { sel <- TcS (Maybe Ct)
selectNextWorkItem
; case sel of
Maybe Ct
Nothing -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Ct
ct -> do { Ct -> TcS ()
solveOne Ct
ct
; TcS ()
solve_loop } }
solveOne :: Ct -> TcS ()
solveOne :: Ct -> TcS ()
solveOne Ct
workItem
= do { wl <- TcS WorkList
getWorkList
; inerts <- getInertSet
; tclevel <- TcS.getTcLevel
; traceTcS "----------------------------- " empty
; traceTcS "Start solver pipeline {" $
vcat [ text "tclevel =" <+> ppr tclevel
, text "work item =" <+> ppr workItem
, text "inerts =" <+> ppr inerts
, text "rest of worklist =" <+> ppr wl ]
; bumpStepCountTcS
; solve workItem }
where
solve :: Ct -> TcS ()
solve :: Ct -> TcS ()
solve Ct
ct
= do { String -> SDoc -> TcS ()
traceTcS String
"solve {" (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"workitem = " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
; res <- SolverStage Void -> TcS (StopOrContinue Void)
forall a. SolverStage a -> TcS (StopOrContinue a)
runSolverStage (Ct -> SolverStage Void
solveCt Ct
ct)
; traceTcS "end solve }" (ppr res)
; case res of
StartAgain Ct
ct -> do { String -> SDoc -> TcS ()
traceTcS String
"Go round again" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
; Ct -> TcS ()
solve Ct
ct }
Stop CtEvidence
ev SDoc
s -> do { CtEvidence -> SDoc -> TcS ()
traceFireTcS CtEvidence
ev SDoc
s
; String -> SDoc -> TcS ()
traceTcS String
"End solver pipeline }" SDoc
forall doc. IsOutput doc => doc
empty
; () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return () }
}
solveCt :: Ct -> SolverStage Void
solveCt :: Ct -> SolverStage Void
solveCt (CNonCanonical CtEvidence
ev) = CtEvidence -> SolverStage Void
solveNC CtEvidence
ev
solveCt (CIrredCan (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev })) = CtEvidence -> SolverStage Void
solveNC CtEvidence
ev
solveCt (CEqCan (EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel
, eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
rhs }))
= CtEvidence -> EqRel -> TcType -> TcType -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel (CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs) TcType
rhs
solveCt (CQuantCan (QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev, qci_pend_sc :: QCInst -> Int
qci_pend_sc = Int
pend_sc }))
= do { ev <- CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev
; case classifyPredType (ctEvPred ev) of
ForAllPred [EvVar]
tvs [TcType]
th TcType
p -> TcS (StopOrContinue Void) -> SolverStage Void
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue Void) -> SolverStage Void)
-> TcS (StopOrContinue Void) -> SolverStage Void
forall a b. (a -> b) -> a -> b
$ CtEvidence
-> [EvVar]
-> [TcType]
-> TcType
-> Int
-> TcS (StopOrContinue Void)
solveForAll CtEvidence
ev [EvVar]
tvs [TcType]
th TcType
p Int
pend_sc
Pred
_ -> String -> SDoc -> SolverStage Void
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"SolveCt" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev) }
solveCt (CDictCan (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_pend_sc :: DictCt -> Int
di_pend_sc = Int
pend_sc }))
= do { ev <- CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev
; case classifyPredType (ctEvPred ev) of
ClassPred Class
cls [TcType]
tys
-> DictCt -> SolverStage Void
solveDict (DictCt { di_ev :: CtEvidence
di_ev = CtEvidence
ev, di_cls :: Class
di_cls = Class
cls
, di_tys :: [TcType]
di_tys = [TcType]
tys, di_pend_sc :: Int
di_pend_sc = Int
pend_sc })
Pred
_ -> String -> SDoc -> SolverStage Void
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"solveCt" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev) }
solveNC :: CtEvidence -> SolverStage Void
solveNC :: CtEvidence -> SolverStage Void
solveNC CtEvidence
ev
=
case TcType -> Pred
classifyPredType (CtEvidence -> TcType
ctEvPred CtEvidence
ev) of {
EqPred EqRel
eq_rel TcType
ty1 TcType
ty2 -> CtEvidence -> EqRel -> TcType -> TcType -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2 ;
Pred
_ ->
do { ev <- CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev
; case classifyPredType (ctEvPred ev) of
ClassPred Class
cls [TcType]
tys -> CtEvidence -> Class -> [TcType] -> SolverStage Void
solveDictNC CtEvidence
ev Class
cls [TcType]
tys
ForAllPred [EvVar]
tvs [TcType]
th TcType
p -> TcS (StopOrContinue Void) -> SolverStage Void
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue Void) -> SolverStage Void)
-> TcS (StopOrContinue Void) -> SolverStage Void
forall a b. (a -> b) -> a -> b
$ CtEvidence
-> [EvVar] -> [TcType] -> TcType -> TcS (StopOrContinue Void)
solveForAllNC CtEvidence
ev [EvVar]
tvs [TcType]
th TcType
p
IrredPred {} -> IrredCt -> SolverStage Void
solveIrred (IrredCt { ir_ev :: CtEvidence
ir_ev = CtEvidence
ev, ir_reason :: CtIrredReason
ir_reason = CtIrredReason
IrredShapeReason })
EqPred EqRel
eq_rel TcType
ty1 TcType
ty2 -> CtEvidence -> EqRel -> TcType -> TcType -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2
}}
solveForAllNC :: CtEvidence -> [TcTyVar] -> TcThetaType -> TcPredType
-> TcS (StopOrContinue Void)
solveForAllNC :: CtEvidence
-> [EvVar] -> [TcType] -> TcType -> TcS (StopOrContinue Void)
solveForAllNC CtEvidence
ev [EvVar]
tvs [TcType]
theta TcType
pred
| CtEvidence -> Bool
isGiven CtEvidence
ev
, Just (Class
cls, [TcType]
tys) <- Maybe (Class, [TcType])
cls_pred_tys_maybe
= do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys
; emitWork (listToBag sc_cts)
; solveForAll ev tvs theta pred doNotExpand }
| Bool
otherwise
= do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; let fuel | Just (Class
cls, [TcType]
_) <- Maybe (Class, [TcType])
cls_pred_tys_maybe
, Class -> Bool
classHasSCs Class
cls = DynFlags -> Int
qcsFuel DynFlags
dflags
| Bool
otherwise = Int
doNotExpand
; solveForAll ev tvs theta pred fuel }
where
cls_pred_tys_maybe :: Maybe (Class, [TcType])
cls_pred_tys_maybe = TcType -> Maybe (Class, [TcType])
getClassPredTys_maybe TcType
pred
solveForAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> ExpansionFuel
-> TcS (StopOrContinue Void)
solveForAll :: CtEvidence
-> [EvVar]
-> [TcType]
-> TcType
-> Int
-> TcS (StopOrContinue Void)
solveForAll ev :: CtEvidence
ev@(CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
[EvVar]
tvs [TcType]
theta TcType
pred Int
_fuel
=
RealSrcSpan
-> TcS (StopOrContinue Void) -> TcS (StopOrContinue Void)
forall a. RealSrcSpan -> TcS a -> TcS a
TcS.setSrcSpan (CtLocEnv -> RealSrcSpan
getCtLocEnvLoc (CtLocEnv -> RealSrcSpan) -> CtLocEnv -> RealSrcSpan
forall a b. (a -> b) -> a -> b
$ CtLoc -> CtLocEnv
ctLocEnv CtLoc
loc) (TcS (StopOrContinue Void) -> TcS (StopOrContinue Void))
-> TcS (StopOrContinue Void) -> TcS (StopOrContinue Void)
forall a b. (a -> b) -> a -> b
$
do { let empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
[TcType] -> VarSet
tyCoVarsOfTypes (TcType
predTcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
:[TcType]
theta) VarSet -> [EvVar] -> VarSet
`delVarSetList` [EvVar]
tvs
is_qc :: ClsInstOrQC
is_qc = CtOrigin -> ClsInstOrQC
IsQC (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc)
; rec { skol_info <- mkSkolemInfo skol_info_anon
; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
; let inst_pred = HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy Subst
subst TcType
pred
inst_theta = HasDebugCallStack => Subst -> [TcType] -> [TcType]
Subst -> [TcType] -> [TcType]
substTheta Subst
subst [TcType]
theta
skol_info_anon = ClsInstOrQC -> PatersonSize -> SkolemInfoAnon
InstSkol ClsInstOrQC
is_qc (TcType -> PatersonSize
get_size TcType
inst_pred) }
; given_ev_vars <- mapM newEvVar inst_theta
; (lvl, (w_id, wanteds))
<- pushLevelNoWorkList (ppr skol_info) $
do { let loc' = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc (ClsInstOrQC -> NakedScFlag -> CtOrigin
ScOrigin ClsInstOrQC
is_qc NakedScFlag
NakedSc)
; wanted_ev <- newWantedNC loc' rewriters inst_pred
; return ( ctEvEvId wanted_ev
, unitBag (mkNonCanonical wanted_ev)) }
; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id)
; ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds
; setWantedEvTerm dest EvCanonical $
EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
, et_binds = ev_binds, et_body = w_id }
; stopWith ev "Wanted forall-constraint" }
where
get_size :: TcType -> PatersonSize
get_size TcType
pred = case TcType -> Pred
classifyPredType TcType
pred of
ClassPred Class
cls [TcType]
tys -> Class -> [TcType] -> PatersonSize
pSizeClassPred Class
cls [TcType]
tys
Pred
_ -> TcType -> PatersonSize
pSizeType TcType
pred
solveForAll ev :: CtEvidence
ev@(CtGiven {}) [EvVar]
tvs [TcType]
_theta TcType
pred Int
fuel
= do { QCInst -> TcS ()
addInertForAll QCInst
qci
; CtEvidence -> String -> TcS (StopOrContinue Void)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Given forall-constraint" }
where
qci :: QCInst
qci = QCI { qci_ev :: CtEvidence
qci_ev = CtEvidence
ev, qci_tvs :: [EvVar]
qci_tvs = [EvVar]
tvs
, qci_pred :: TcType
qci_pred = TcType
pred, qci_pend_sc :: Int
qci_pend_sc = Int
fuel }
rewriteEvidence :: CtEvidence -> SolverStage CtEvidence
rewriteEvidence :: CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev
= TcS (StopOrContinue CtEvidence) -> SolverStage CtEvidence
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue CtEvidence) -> SolverStage CtEvidence)
-> TcS (StopOrContinue CtEvidence) -> SolverStage CtEvidence
forall a b. (a -> b) -> a -> b
$ do { String -> SDoc -> TcS ()
traceTcS String
"rewriteEvidence" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
; (redn, rewriters) <- CtEvidence -> TcType -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev (CtEvidence -> TcType
ctEvPred CtEvidence
ev)
; finish_rewrite ev redn rewriters }
finish_rewrite :: CtEvidence
-> Reduction
-> RewriterSet
-> TcS (StopOrContinue CtEvidence)
finish_rewrite :: CtEvidence
-> Reduction -> RewriterSet -> TcS (StopOrContinue CtEvidence)
finish_rewrite CtEvidence
old_ev (Reduction TcCoercion
co TcType
new_pred) RewriterSet
rewriters
| TcCoercion -> Bool
isReflCo TcCoercion
co
= Bool
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a. HasCallStack => Bool -> a -> a
assert (RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters) (TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence))
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a b. (a -> b) -> a -> b
$
CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith (HasDebugCallStack => CtEvidence -> TcType -> CtEvidence
CtEvidence -> TcType -> CtEvidence
setCtEvPredType CtEvidence
old_ev TcType
new_pred)
finish_rewrite ev :: CtEvidence
ev@(CtGiven { ctev_evar :: CtEvidence -> EvVar
ctev_evar = EvVar
old_evar, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
(Reduction TcCoercion
co TcType
new_pred) RewriterSet
rewriters
= Bool
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a. HasCallStack => Bool -> a -> a
assert (RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters) (TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence))
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a b. (a -> b) -> a -> b
$
do { new_ev <- CtLoc -> (TcType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (TcType
new_pred, EvTerm
new_tm)
; continueWith new_ev }
where
ev_rw_role :: Role
ev_rw_role = HasDebugCallStack => CtEvidence -> Role
CtEvidence -> Role
ctEvRewriteRole CtEvidence
ev
new_tm :: EvTerm
new_tm = Bool
-> (EvExpr -> TcCoercion -> EvTerm)
-> EvExpr
-> TcCoercion
-> EvTerm
forall a. HasCallStack => Bool -> a -> a
assert (TcCoercion -> Role
coercionRole TcCoercion
co Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
ev_rw_role)
EvExpr -> TcCoercion -> EvTerm
mkEvCast (EvVar -> EvExpr
evId EvVar
old_evar)
(Role -> Role -> TcCoercion -> TcCoercion
downgradeRole Role
Representational Role
ev_rw_role TcCoercion
co)
finish_rewrite ev :: CtEvidence
ev@(CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest
, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc
, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters })
(Reduction TcCoercion
co TcType
new_pred) RewriterSet
new_rewriters
= do { mb_new_ev <- CtLoc -> RewriterSet -> TcType -> TcS MaybeNew
newWanted CtLoc
loc RewriterSet
rewriters' TcType
new_pred
; let ev_rw_role = HasDebugCallStack => CtEvidence -> Role
CtEvidence -> Role
ctEvRewriteRole CtEvidence
ev
; massert (coercionRole co == ev_rw_role)
; setWantedEvTerm dest EvCanonical $
mkEvCast (getEvExpr mb_new_ev)
(downgradeRole Representational ev_rw_role (mkSymCo co))
; case mb_new_ev of
Fresh CtEvidence
new_ev -> CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith CtEvidence
new_ev
Cached EvExpr
_ -> CtEvidence -> String -> TcS (StopOrContinue CtEvidence)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Cached wanted" }
where
rewriters' :: RewriterSet
rewriters' = RewriterSet
rewriters RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
new_rewriters
runTcPluginsGiven :: TcS [Ct]
runTcPluginsGiven :: TcS [Ct]
runTcPluginsGiven
= do { solvers <- TcS [TcPluginSolver]
getTcPluginSolvers
; if null solvers then return [] else
do { givens <- getInertGivens
; if null givens then return [] else
do { traceTcS "runTcPluginsGiven {" (ppr givens)
; p <- runTcPluginSolvers solvers (givens,[])
; let (solved_givens, _) = pluginSolvedCts p
insols = (Ct -> IrredCt) -> [Ct] -> [IrredCt]
forall a b. (a -> b) -> [a] -> [b]
map (CtIrredReason -> Ct -> IrredCt
ctIrredCt CtIrredReason
PluginReason) (TcPluginProgress -> [Ct]
pluginBadCts TcPluginProgress
p)
; updInertCans (removeInertCts solved_givens .
updIrreds (addIrreds insols) )
; traceTcS "runTcPluginsGiven }" $
vcat [ text "solved_givens:" <+> ppr solved_givens
, text "insols:" <+> ppr insols
, text "new:" <+> ppr (pluginNewCts p) ]
; return (pluginNewCts p) } } }
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples1 })
| Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
simples1
= (Bool, WantedConstraints) -> TcS (Bool, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, WantedConstraints
wc)
| Bool
otherwise
= do { solvers <- TcS [TcPluginSolver]
getTcPluginSolvers
; if null solvers then return (False, wc) else
do { given <- getInertGivens
; wanted <- TcS.zonkSimples simples1
; traceTcS "Running plugins (" (vcat [ text "Given:" <+> ppr given
, text "Watned:" <+> ppr wanted ])
; p <- runTcPluginSolvers solvers (given, bagToList wanted)
; let (_, solved_wanted) = pluginSolvedCts p
(_, unsolved_wanted) = pluginInputCts p
new_wanted = TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p
insols = TcPluginProgress -> [Ct]
pluginBadCts TcPluginProgress
p
all_new_wanted = [Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
new_wanted Cts -> Cts -> Cts
`andCts`
[Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
unsolved_wanted Cts -> Cts -> Cts
`andCts`
[Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
insols
; mapM_ setEv solved_wanted
; traceTcS "Finished plugins }" (ppr new_wanted)
; return ( notNull (pluginNewCts p)
, wc { wc_simple = all_new_wanted } ) } }
where
setEv :: (EvTerm,Ct) -> TcS ()
setEv :: (EvTerm, Ct) -> TcS ()
setEv (EvTerm
ev,Ct
ct) = case Ct -> CtEvidence
ctEvidence Ct
ct of
CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } -> TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest CanonicalEvidence
EvCanonical EvTerm
ev
CtEvidence
_ -> String -> TcS ()
forall a. HasCallStack => String -> a
panic String
"runTcPluginsWanted.setEv: attempt to solve non-wanted!"
type SplitCts = ([Ct], [Ct])
type SolvedCts = ([Ct], [(EvTerm,Ct)])
data TcPluginProgress = TcPluginProgress
{ TcPluginProgress -> SplitCts
pluginInputCts :: SplitCts
, TcPluginProgress -> ([Ct], [(EvTerm, Ct)])
pluginSolvedCts :: SolvedCts
, TcPluginProgress -> [Ct]
pluginBadCts :: [Ct]
, TcPluginProgress -> [Ct]
pluginNewCts :: [Ct]
}
getTcPluginSolvers :: TcS [TcPluginSolver]
getTcPluginSolvers :: TcS [TcPluginSolver]
getTcPluginSolvers
= do { tcg_env <- TcS TcGblEnv
TcS.getGblEnv; return (tcg_tc_plugin_solvers tcg_env) }
runTcPluginSolvers :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers [TcPluginSolver]
solvers SplitCts
all_cts
= do { ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
; foldM (do_plugin ev_binds_var) initialProgress solvers }
where
do_plugin :: EvBindsVar -> TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
do_plugin :: EvBindsVar
-> TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
do_plugin EvBindsVar
ev_binds_var TcPluginProgress
p TcPluginSolver
solver = do
result <- TcPluginM TcPluginSolveResult -> TcS TcPluginSolveResult
forall a. TcPluginM a -> TcS a
runTcPluginTcS (([Ct] -> [Ct] -> TcPluginM TcPluginSolveResult)
-> SplitCts -> TcPluginM TcPluginSolveResult
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (TcPluginSolver
solver EvBindsVar
ev_binds_var) (TcPluginProgress -> SplitCts
pluginInputCts TcPluginProgress
p))
return $ progress p result
progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
progress TcPluginProgress
p
(TcPluginSolveResult
{ tcPluginInsolubleCts :: TcPluginSolveResult -> [Ct]
tcPluginInsolubleCts = [Ct]
bad_cts
, tcPluginSolvedCts :: TcPluginSolveResult -> [(EvTerm, Ct)]
tcPluginSolvedCts = [(EvTerm, Ct)]
solved_cts
, tcPluginNewCts :: TcPluginSolveResult -> [Ct]
tcPluginNewCts = [Ct]
new_cts
}
) =
TcPluginProgress
p { pluginInputCts = discard (bad_cts ++ map snd solved_cts) (pluginInputCts p)
, pluginSolvedCts = add solved_cts (pluginSolvedCts p)
, pluginNewCts = new_cts ++ pluginNewCts p
, pluginBadCts = bad_cts ++ pluginBadCts p
}
initialProgress :: TcPluginProgress
initialProgress = SplitCts
-> ([Ct], [(EvTerm, Ct)]) -> [Ct] -> [Ct] -> TcPluginProgress
TcPluginProgress SplitCts
all_cts ([], []) [] []
discard :: [Ct] -> SplitCts -> SplitCts
discard :: [Ct] -> SplitCts -> SplitCts
discard [Ct]
cts ([Ct]
xs, [Ct]
ys) =
([Ct]
xs [Ct] -> [Ct] -> [Ct]
`without` [Ct]
cts, [Ct]
ys [Ct] -> [Ct] -> [Ct]
`without` [Ct]
cts)
without :: [Ct] -> [Ct] -> [Ct]
without :: [Ct] -> [Ct] -> [Ct]
without = (Ct -> Ct -> Bool) -> [Ct] -> [Ct] -> [Ct]
forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
deleteFirstsBy Ct -> Ct -> Bool
eq_ct
eq_ct :: Ct -> Ct -> Bool
eq_ct :: Ct -> Ct -> Bool
eq_ct Ct
c Ct
c' = Ct -> CtFlavour
ctFlavour Ct
c CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
== Ct -> CtFlavour
ctFlavour Ct
c'
Bool -> Bool -> Bool
&& Ct -> TcType
ctPred Ct
c HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` Ct -> TcType
ctPred Ct
c'
add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
add :: [(EvTerm, Ct)] -> ([Ct], [(EvTerm, Ct)]) -> ([Ct], [(EvTerm, Ct)])
add [(EvTerm, Ct)]
xs ([Ct], [(EvTerm, Ct)])
scs = (([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)]))
-> ([Ct], [(EvTerm, Ct)])
-> [(EvTerm, Ct)]
-> ([Ct], [(EvTerm, Ct)])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)])
addOne ([Ct], [(EvTerm, Ct)])
scs [(EvTerm, Ct)]
xs
addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
addOne :: ([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)])
addOne ([Ct]
givens, [(EvTerm, Ct)]
wanteds) (EvTerm
ev,Ct
ct) = case Ct -> CtEvidence
ctEvidence Ct
ct of
CtGiven {} -> (Ct
ctCt -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
:[Ct]
givens, [(EvTerm, Ct)]
wanteds)
CtWanted {} -> ([Ct]
givens, (EvTerm
ev,Ct
ct)(EvTerm, Ct) -> [(EvTerm, Ct)] -> [(EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[(EvTerm, Ct)]
wanteds)