{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module GHC.Tc.Solver.Monad (
TcS, runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS,
emitImplicationTcS, emitTvImplicationTcS,
emitFunDepWanteds,
selectNextWorkItem,
getWorkList,
updWorkListTcS,
pushLevelNoWorkList,
runTcPluginTcS, recordUsedGREs,
matchGlobalInst, TcM.ClsInstResult(..),
QCInst(..),
StopOrContinue(..), continueWith, stopWith,
startAgainWith, SolverStage(Stage, runSolverStage), simpleStage,
stopWithStage, nopStage,
panicTcS, traceTcS, tryEarlyAbortTcS,
traceFireTcS, bumpStepCountTcS, csTraceTcS,
wrapErrTcS, wrapWarnTcS,
resetUnificationFlag, setUnificationFlag,
MaybeNew(..), freshGoals, isFresh, getEvExpr,
CanonicalEvidence(..),
newTcEvBinds, newNoTcEvBinds,
newWantedEq, emitNewWantedEq,
newWanted,
newWantedNC, newWantedEvVarNC,
newBoundEvVarId,
unifyTyVar, reportUnifications,
setEvBind, setWantedEq,
setWantedEvTerm, setEvBindIfWanted,
newEvVar, newGivenEvVar, emitNewGivens,
checkReductionDepth,
getSolvedDicts, setSolvedDicts,
getInstEnvs, getFamInstEnvs,
getTopEnv, getGblEnv, getLclEnv, setSrcSpan,
getTcEvBindsVar, getTcLevel,
getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
tcLookupClass, tcLookupId, tcLookupTyCon,
updInertSet, updInertCans,
getHasGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertGivens,
getInertInsols, getInnermostGivenEqLevel,
getInertSet, setInertSet,
getUnsolvedInerts,
removeInertCts, getPendingGivenScs,
insertFunEq, addInertForAll,
emitWorkNC, emitWork,
lookupInertDict,
kickOutAfterUnification, kickOutRewritable,
addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
getSafeOverlapFailures,
updSolvedDicts, lookupSolvedDict,
foldIrreds,
lookupFamAppInert, lookupFamAppCache, extendFamAppCache,
pprKicked,
instDFunType,
wrapUnifierTcS, unifyFunDeps, uPairsTcM, unifyForAllBody,
newFlexiTcSTy, instFlexiX,
cloneMetaTyVar,
tcInstSkolTyVarsX,
TcLevel,
isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar,
zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
zonkTyCoVarsAndFVList,
zonkSimples, zonkWC,
zonkTyCoVarKind,
newTcRef, readTcRef, writeTcRef, updTcRef,
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam, matchFamTcM,
checkWellStagedDFun,
pprEq,
checkTypeEq, checkTouchableTyVarEq
) where
import GHC.Prelude
import GHC.Driver.Env
import qualified GHC.Tc.Utils.Instantiate as TcM
import GHC.Core.InstEnv
import GHC.Tc.Instance.Family as FamInst
import GHC.Core.FamInstEnv
import qualified GHC.Tc.Utils.Monad as TcM
import qualified GHC.Tc.Utils.TcMType as TcM
import qualified GHC.Tc.Instance.Class as TcM( matchGlobalInst, ClsInstResult(..) )
import qualified GHC.Tc.Utils.Env as TcM
( checkWellStaged, tcGetDefaultTys
, tcLookupClass, tcLookupId, tcLookupTyCon
, topIdLvl )
import GHC.Tc.Zonk.Monad ( ZonkM )
import qualified GHC.Tc.Zonk.TcType as TcM
import qualified GHC.Tc.Zonk.Type as TcM
import GHC.Driver.DynFlags
import GHC.Tc.Instance.Class( safeOverlap, instanceReturnsDictCon )
import GHC.Tc.Instance.FunDeps( FunDepEqn(..) )
import GHC.Tc.Solver.Types
import GHC.Tc.Solver.InertSet
import GHC.Tc.Errors.Types
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Unify
import GHC.Tc.Types.Evidence
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.CtLoc
import GHC.Tc.Types.Constraint
import GHC.Builtin.Names ( unsatisfiableClassNameKey )
import GHC.Core.Type
import GHC.Core.TyCo.Rep as Rep
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom( TypeEqn )
import GHC.Core.Predicate
import GHC.Core.Reduction
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Types.Name
import GHC.Types.TyThing
import GHC.Types.Name.Reader
import GHC.Types.DefaultEnv ( DefaultEnv )
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Unique.Supply
import GHC.Types.Unique.Set( elementOfUniqSet )
import GHC.Unit.Module ( HasModule, getModule, extractModule )
import qualified GHC.Rename.Env as TcM
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Logger
import GHC.Utils.Misc (HasDebugCallStack)
import GHC.Data.Bag as Bag
import GHC.Data.Pair
import GHC.Utils.Monad
import GHC.Exts (oneShot)
import Control.Monad
import Data.IORef
import Data.List ( mapAccumL )
import Data.Foldable
import qualified Data.Semigroup as S
import GHC.Types.SrcLoc
import GHC.Rename.Env
#if defined(DEBUG)
import GHC.Types.Unique.Set (nonDetEltsUniqSet)
import GHC.Data.Graph.Directed
#endif
data StopOrContinue a
= StartAgain Ct
| ContinueWith !a
| Stop CtEvidence
SDoc
deriving ((forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b)
-> (forall a b. a -> StopOrContinue b -> StopOrContinue a)
-> Functor StopOrContinue
forall a b. a -> StopOrContinue b -> StopOrContinue a
forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
fmap :: forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
$c<$ :: forall a b. a -> StopOrContinue b -> StopOrContinue a
<$ :: forall a b. a -> StopOrContinue b -> StopOrContinue a
Functor)
instance Outputable a => Outputable (StopOrContinue a) where
ppr :: StopOrContinue a -> SDoc
ppr (Stop CtEvidence
ev SDoc
s) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Stop" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc
s SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ev:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
ppr (ContinueWith a
w) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ContinueWith" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
w
ppr (StartAgain Ct
w) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"StartAgain" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
w
newtype SolverStage a = Stage { forall a. SolverStage a -> TcS (StopOrContinue a)
runSolverStage :: TcS (StopOrContinue a) }
deriving( (forall a b. (a -> b) -> SolverStage a -> SolverStage b)
-> (forall a b. a -> SolverStage b -> SolverStage a)
-> Functor SolverStage
forall a b. a -> SolverStage b -> SolverStage a
forall a b. (a -> b) -> SolverStage a -> SolverStage b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SolverStage a -> SolverStage b
fmap :: forall a b. (a -> b) -> SolverStage a -> SolverStage b
$c<$ :: forall a b. a -> SolverStage b -> SolverStage a
<$ :: forall a b. a -> SolverStage b -> SolverStage a
Functor )
instance Applicative SolverStage where
pure :: forall a. a -> SolverStage a
pure a
x = TcS (StopOrContinue a) -> SolverStage a
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> StopOrContinue a
forall a. a -> StopOrContinue a
ContinueWith a
x))
<*> :: forall a b. SolverStage (a -> b) -> SolverStage a -> SolverStage b
(<*>) = SolverStage (a -> b) -> SolverStage a -> SolverStage b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad SolverStage where
return :: forall a. a -> SolverStage a
return = a -> SolverStage a
forall a. a -> SolverStage a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(Stage TcS (StopOrContinue a)
m) >>= :: forall a b. SolverStage a -> (a -> SolverStage b) -> SolverStage b
>>= a -> SolverStage b
k = TcS (StopOrContinue b) -> SolverStage b
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue b) -> SolverStage b)
-> TcS (StopOrContinue b) -> SolverStage b
forall a b. (a -> b) -> a -> b
$
do { soc <- TcS (StopOrContinue a)
m
; case soc of
StartAgain Ct
x -> StopOrContinue b -> TcS (StopOrContinue b)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> StopOrContinue b
forall a. Ct -> StopOrContinue a
StartAgain Ct
x)
Stop CtEvidence
ev SDoc
d -> StopOrContinue b -> TcS (StopOrContinue b)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue b
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev SDoc
d)
ContinueWith a
x -> SolverStage b -> TcS (StopOrContinue b)
forall a. SolverStage a -> TcS (StopOrContinue a)
runSolverStage (a -> SolverStage b
k a
x) }
nopStage :: a -> SolverStage a
nopStage :: forall a. a -> SolverStage a
nopStage a
res = TcS (StopOrContinue a) -> SolverStage a
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (a -> TcS (StopOrContinue a)
forall a. a -> TcS (StopOrContinue a)
continueWith a
res)
simpleStage :: TcS a -> SolverStage a
simpleStage :: forall a. TcS a -> SolverStage a
simpleStage TcS a
thing = TcS (StopOrContinue a) -> SolverStage a
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (do { res <- TcS a
thing; continueWith res })
startAgainWith :: Ct -> TcS (StopOrContinue a)
startAgainWith :: forall a. Ct -> TcS (StopOrContinue a)
startAgainWith Ct
ct = StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> StopOrContinue a
forall a. Ct -> StopOrContinue a
StartAgain Ct
ct)
continueWith :: a -> TcS (StopOrContinue a)
continueWith :: forall a. a -> TcS (StopOrContinue a)
continueWith a
ct = StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> StopOrContinue a
forall a. a -> StopOrContinue a
ContinueWith a
ct)
stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
stopWith :: forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
s = StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue a
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
s))
stopWithStage :: CtEvidence -> String -> SolverStage a
stopWithStage :: forall a. CtEvidence -> String -> SolverStage a
stopWithStage CtEvidence
ev String
s = TcS (StopOrContinue a) -> SolverStage a
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (CtEvidence -> String -> TcS (StopOrContinue a)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
s)
addInertForAll :: QCInst -> TcS ()
addInertForAll :: QCInst -> TcS ()
addInertForAll QCInst
new_qci
= do { ics <- TcS InertCans
getInertCans
; ics1 <- add_qci ics
; tclvl <- getTcLevel
; let pred = QCInst -> Type
qci_pred QCInst
new_qci
not_equality = Type -> Bool
isClassPred Type
pred Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isEqClassPred Type
pred)
ics2 | Bool
not_equality = InertCans
ics1
| Bool
otherwise = InertCans
ics1 { inert_given_eq_lvl = tclvl
, inert_given_eqs = True }
; setInertCans ics2 }
where
add_qci :: InertCans -> TcS InertCans
add_qci :: InertCans -> TcS InertCans
add_qci ics :: InertCans
ics@(IC { inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
qcis })
| (QCInst -> Bool) -> [QCInst] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any QCInst -> Bool
same_qci [QCInst]
qcis
= do { String -> SDoc -> TcS ()
traceTcS String
"skipping duplicate quantified instance" (QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr QCInst
new_qci)
; InertCans -> TcS InertCans
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"adding new inert quantified instance" (QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr QCInst
new_qci)
; InertCans -> TcS InertCans
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans
ics { inert_insts = new_qci : qcis }) }
same_qci :: QCInst -> Bool
same_qci QCInst
old_qci = HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType (CtEvidence -> Type
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
old_qci))
(CtEvidence -> Type
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
new_qci))
kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS ()
kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS ()
kickOutRewritable KickOutSpec
ko_spec CtFlavourRole
new_fr
= do { ics <- TcS InertCans
getInertCans
; let (kicked_out, ics') = kickOutRewritableLHS ko_spec new_fr ics
n_kicked = Cts -> Int
forall a. Bag a -> Int
lengthBag Cts
kicked_out
; setInertCans ics'
; unless (isEmptyBag kicked_out) $
do { emitWork kicked_out
; let kicked_given_ev_vars = (Ct -> VarSet -> VarSet) -> VarSet -> Cts -> 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 Ct -> VarSet -> VarSet
add_one VarSet
emptyVarSet Cts
kicked_out
add_one :: Ct -> VarSet -> VarSet
add_one Ct
ct VarSet
vs | CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
ev_var } <- Ct -> CtEvidence
ctEvidence Ct
ct
= VarSet
vs VarSet -> TcTyVar -> VarSet
`extendVarSet` TcTyVar
ev_var
| Bool
otherwise = VarSet
vs
; when (new_fr `eqCanRewriteFR` (Given, NomEq) &&
not (isEmptyVarSet kicked_given_ev_vars)) $
do { traceTcS "Given(s) have been kicked out; drop from famapp-cache"
(ppr kicked_given_ev_vars)
; dropFromFamAppCache kicked_given_ev_vars }
; csTraceTcS $
hang (text "Kick out")
2 (vcat [ text "n-kicked =" <+> int n_kicked
, text "kicked_out =" <+> ppr kicked_out
, text "Residual inerts =" <+> ppr ics' ]) } }
kickOutAfterUnification :: [TcTyVar] -> TcS ()
kickOutAfterUnification :: [TcTyVar] -> TcS ()
kickOutAfterUnification [TcTyVar]
tvs
| [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs
= () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { let tv_set :: VarSet
tv_set = [TcTyVar] -> VarSet
mkVarSet [TcTyVar]
tvs
; n_kicked <- KickOutSpec -> CtFlavourRole -> TcS ()
kickOutRewritable (VarSet -> KickOutSpec
KOAfterUnify VarSet
tv_set) (CtFlavour
Given, EqRel
NomEq)
; let min_tv_lvl = (TcLevel -> TcLevel -> TcLevel) -> [TcLevel] -> TcLevel
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 TcLevel -> TcLevel -> TcLevel
minTcLevel ((TcTyVar -> TcLevel) -> [TcTyVar] -> [TcLevel]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> TcLevel
tcTyVarLevel [TcTyVar]
tvs)
; ambient_lvl <- getTcLevel
; when (ambient_lvl `strictlyDeeperThan` min_tv_lvl) $
setUnificationFlag min_tv_lvl
; traceTcS "kickOutAfterUnification" (ppr tvs $$ text "n_kicked =" <+> ppr n_kicked)
; return n_kicked }
kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole
= do { ics <- TcS InertCans
getInertCans
; let (kicked_out, ics') = kick_out ics
n_kicked = Bag IrredCt -> Int
forall a. Bag a -> Int
lengthBag Bag IrredCt
kicked_out
; unless (n_kicked == 0) $
do { updWorkListTcS (extendWorkListCts (fmap CIrredCan kicked_out))
; csTraceTcS $
hang (text "Kick out, hole =" <+> ppr hole)
2 (vcat [ text "n-kicked =" <+> int n_kicked
, text "kicked_out =" <+> ppr kicked_out
, text "Residual inerts =" <+> ppr ics' ]) }
; setInertCans ics' }
where
kick_out :: InertCans -> (Bag IrredCt, InertCans)
kick_out :: InertCans -> (Bag IrredCt, InertCans)
kick_out ics :: InertCans
ics@(IC { inert_irreds :: InertCans -> Bag IrredCt
inert_irreds = Bag IrredCt
irreds })
=
(Bag IrredCt
irreds_to_kick, InertCans
ics { inert_irreds = irreds_to_keep })
where
(Bag IrredCt
irreds_to_kick, Bag IrredCt
irreds_to_keep) = (IrredCt -> Bool) -> Bag IrredCt -> (Bag IrredCt, Bag IrredCt)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag IrredCt -> Bool
kick_ct Bag IrredCt
irreds
kick_ct :: IrredCt -> Bool
kick_ct :: IrredCt -> Bool
kick_ct IrredCt
ct
| IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev, ir_reason :: IrredCt -> CtIrredReason
ir_reason = CtIrredReason
reason } <- IrredCt
ct
, CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet UniqSet CoercionHole
rewriters } <- CtEvidence
ev
, NonCanonicalReason CheckTyEqResult
ctyeq <- CtIrredReason
reason
, CheckTyEqResult
ctyeq CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasProblem` CheckTyEqProblem
cteCoercionHole
, CoercionHole
hole CoercionHole -> UniqSet CoercionHole -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
`elementOfUniqSet` UniqSet CoercionHole
rewriters
= Bool
True
| Bool
otherwise
= Bool
False
addInertSafehask :: InertCans -> DictCt -> InertCans
addInertSafehask :: InertCans -> DictCt -> InertCans
addInertSafehask InertCans
ics DictCt
item
= InertCans
ics { inert_safehask = addDict item (inert_dicts ics) }
insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
insertSafeOverlapFailureTcS InstanceWhat
what DictCt
item
| InstanceWhat -> Bool
safeOverlap InstanceWhat
what = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = (InertCans -> InertCans) -> TcS ()
updInertCans (\InertCans
ics -> InertCans -> DictCt -> InertCans
addInertSafehask InertCans
ics DictCt
item)
getSafeOverlapFailures :: TcS (Bag DictCt)
getSafeOverlapFailures :: TcS (Bag DictCt)
getSafeOverlapFailures
= do { IC { inert_safehask = safehask } <- TcS InertCans
getInertCans
; return $ foldDicts consBag safehask emptyBag }
updSolvedDicts :: InstanceWhat -> DictCt -> TcS ()
updSolvedDicts :: InstanceWhat -> DictCt -> TcS ()
updSolvedDicts InstanceWhat
what dict_ct :: DictCt
dict_ct@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev })
| CtEvidence -> Bool
isWanted CtEvidence
ev
, InstanceWhat -> Bool
instanceReturnsDictCon InstanceWhat
what
= do { String -> SDoc -> TcS ()
traceTcS String
"updSolvedDicts:" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_ct
; (InertSet -> InertSet) -> TcS ()
updInertSet ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
InertSet
ics { inert_solved_dicts = addSolvedDict dict_ct (inert_solved_dicts ics) } }
| Bool
otherwise
= () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
getSolvedDicts :: TcS (DictMap DictCt)
getSolvedDicts :: TcS (DictMap DictCt)
getSolvedDicts = do { ics <- TcS InertSet
getInertSet; return (inert_solved_dicts ics) }
setSolvedDicts :: DictMap DictCt -> TcS ()
setSolvedDicts :: DictMap DictCt -> TcS ()
setSolvedDicts DictMap DictCt
solved_dicts
= (InertSet -> InertSet) -> TcS ()
updInertSet ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
InertSet
ics { inert_solved_dicts = solved_dicts }
updInertSet :: (InertSet -> InertSet) -> TcS ()
updInertSet :: (InertSet -> InertSet) -> TcS ()
updInertSet InertSet -> InertSet
upd_fn
= do { is_var <- TcS (IORef InertSet)
getInertSetRef
; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
getInertCans :: TcS InertCans
getInertCans :: TcS InertCans
getInertCans = do { inerts <- TcS InertSet
getInertSet; return (inert_cans inerts) }
setInertCans :: InertCans -> TcS ()
setInertCans :: InertCans -> TcS ()
setInertCans InertCans
ics = (InertSet -> InertSet) -> TcS ()
updInertSet ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans = ics }
updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
updRetInertCans :: forall a. (InertCans -> (a, InertCans)) -> TcS a
updRetInertCans InertCans -> (a, InertCans)
upd_fn
= do { is_var <- TcS (IORef InertSet)
getInertSetRef
; wrapTcS (do { inerts <- TcM.readTcRef is_var
; let (res, cans') = upd_fn (inert_cans inerts)
; TcM.writeTcRef is_var (inerts { inert_cans = cans' })
; return res }) }
updInertCans :: (InertCans -> InertCans) -> TcS ()
updInertCans :: (InertCans -> InertCans) -> TcS ()
updInertCans InertCans -> InertCans
upd_fn
= (InertSet -> InertSet) -> TcS ()
updInertSet ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans = upd_fn (inert_cans inerts) }
updInertSafehask :: (DictMap DictCt -> DictMap DictCt) -> TcS ()
updInertSafehask :: (DictMap DictCt -> DictMap DictCt) -> TcS ()
updInertSafehask DictMap DictCt -> DictMap DictCt
upd_fn
= (InertCans -> InertCans) -> TcS ()
updInertCans ((InertCans -> InertCans) -> TcS ())
-> (InertCans -> InertCans) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_safehask = upd_fn (inert_safehask ics) }
getInertEqs :: TcS InertEqs
getInertEqs :: TcS InertEqs
getInertEqs = do { inert <- TcS InertCans
getInertCans; return (inert_eqs inert) }
getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel = do { inert <- TcS InertCans
getInertCans
; return (inert_given_eq_lvl inert) }
getInertInsols :: TcS Cts
getInertInsols :: TcS Cts
getInertInsols
= do { inert <- TcS InertCans
getInertCans
; let insols = (IrredCt -> Bool) -> Bag IrredCt -> Bag IrredCt
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag IrredCt -> Bool
insolubleIrredCt (InertCans -> Bag IrredCt
inert_irreds InertCans
inert)
unsats = DictMap DictCt -> Unique -> Bag DictCt
forall a. DictMap a -> Unique -> Bag a
findDictsByTyConKey (InertCans -> DictMap DictCt
inert_dicts InertCans
inert) Unique
unsatisfiableClassNameKey
; return $ fmap CDictCan unsats `unionBags` fmap CIrredCan insols }
getInertGivens :: TcS [Ct]
getInertGivens :: TcS [Ct]
getInertGivens
= do { inerts <- TcS InertCans
getInertCans
; let all_cts = (IrredCt -> [Ct] -> [Ct]) -> Bag IrredCt -> [Ct] -> [Ct]
forall b. (IrredCt -> b -> b) -> Bag IrredCt -> b -> b
foldIrreds ((:) (Ct -> [Ct] -> [Ct]) -> (IrredCt -> Ct) -> IrredCt -> [Ct] -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IrredCt -> Ct
CIrredCan) (InertCans -> Bag IrredCt
inert_irreds InertCans
inerts)
([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (DictCt -> [Ct] -> [Ct]) -> DictMap DictCt -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts ((:) (Ct -> [Ct] -> [Ct]) -> (DictCt -> Ct) -> DictCt -> [Ct] -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DictCt -> Ct
CDictCan) (InertCans -> DictMap DictCt
inert_dicts InertCans
inerts)
([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (EqCt -> [Ct] -> [Ct]) -> FunEqMap EqualCtList -> [Ct] -> [Ct]
forall b. (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
foldFunEqs ((:) (Ct -> [Ct] -> [Ct]) -> (EqCt -> Ct) -> EqCt -> [Ct] -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqCt -> Ct
CEqCan) (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
inerts)
([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (EqCt -> [Ct] -> [Ct]) -> InertEqs -> [Ct] -> [Ct]
forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs ((:) (Ct -> [Ct] -> [Ct]) -> (EqCt -> Ct) -> EqCt -> [Ct] -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqCt -> Ct
CEqCan) (InertCans -> InertEqs
inert_eqs InertCans
inerts)
([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ []
; return (filter isGivenCt all_cts) }
getPendingGivenScs :: TcS [Ct]
getPendingGivenScs :: TcS [Ct]
getPendingGivenScs = do { lvl <- TcS TcLevel
getTcLevel
; updRetInertCans (get_sc_pending lvl) }
get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending TcLevel
this_lvl ic :: InertCans
ic@(IC { inert_dicts :: InertCans -> DictMap DictCt
inert_dicts = DictMap DictCt
dicts, inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts })
= Bool -> SDoc -> ([Ct], InertCans) -> ([Ct], InertCans)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((Ct -> Bool) -> [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ct -> Bool
isGivenCt [Ct]
sc_pending) ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
sc_pending)
([Ct]
sc_pending, InertCans
ic { inert_dicts = dicts', inert_insts = insts' })
where
sc_pending :: [Ct]
sc_pending = [Ct]
sc_pend_insts [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ (DictCt -> Ct) -> [DictCt] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map DictCt -> Ct
CDictCan [DictCt]
sc_pend_dicts
sc_pend_dicts :: [DictCt]
sc_pend_dicts :: [DictCt]
sc_pend_dicts = (DictCt -> [DictCt] -> [DictCt])
-> DictMap DictCt -> [DictCt] -> [DictCt]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts DictCt -> [DictCt] -> [DictCt]
get_pending DictMap DictCt
dicts []
dicts' :: DictMap DictCt
dicts' = (DictCt -> DictMap DictCt -> DictMap DictCt)
-> DictMap DictCt -> [DictCt] -> DictMap DictCt
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr DictCt -> DictMap DictCt -> DictMap DictCt
exhaustAndAdd DictMap DictCt
dicts [DictCt]
sc_pend_dicts
([Ct]
sc_pend_insts, [QCInst]
insts') = ([Ct] -> QCInst -> ([Ct], QCInst))
-> [Ct] -> [QCInst] -> ([Ct], [QCInst])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL [Ct] -> QCInst -> ([Ct], QCInst)
get_pending_inst [] [QCInst]
insts
exhaustAndAdd :: DictCt -> DictMap DictCt -> DictMap DictCt
exhaustAndAdd :: DictCt -> DictMap DictCt -> DictMap DictCt
exhaustAndAdd DictCt
ct DictMap DictCt
dicts = DictCt -> DictMap DictCt -> DictMap DictCt
addDict (DictCt
ct {di_pend_sc = doNotExpand}) DictMap DictCt
dicts
get_pending :: DictCt -> [DictCt] -> [DictCt]
get_pending :: DictCt -> [DictCt] -> [DictCt]
get_pending DictCt
dict [DictCt]
dicts
| DictCt -> Bool
isPendingScDictCt DictCt
dict
, CtEvidence -> Bool
belongs_to_this_level (DictCt -> CtEvidence
dictCtEvidence DictCt
dict)
= DictCt
dict DictCt -> [DictCt] -> [DictCt]
forall a. a -> [a] -> [a]
: [DictCt]
dicts
| Bool
otherwise
= [DictCt]
dicts
get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
get_pending_inst [Ct]
cts qci :: QCInst
qci@(QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev })
| Just QCInst
qci' <- QCInst -> Maybe QCInst
pendingScInst_maybe QCInst
qci
, CtEvidence -> Bool
belongs_to_this_level CtEvidence
ev
= (QCInst -> Ct
CQuantCan QCInst
qci Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
cts, QCInst
qci')
| Bool
otherwise
= ([Ct]
cts, QCInst
qci)
belongs_to_this_level :: CtEvidence -> Bool
belongs_to_this_level CtEvidence
ev = CtLoc -> TcLevel
ctLocLevel (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
this_lvl
getUnsolvedInerts :: TcS ( Bag Implication
, Cts )
getUnsolvedInerts :: TcS (Bag Implication, Cts)
getUnsolvedInerts
= do { IC { inert_eqs = tv_eqs
, inert_funeqs = fun_eqs
, inert_irreds = irreds
, inert_dicts = idicts
} <- TcS InertCans
getInertCans
; let unsolved_tv_eqs = (EqCt -> Cts -> Cts) -> InertEqs -> Cts -> Cts
forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs ((EqCt -> Ct) -> EqCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved EqCt -> Ct
CEqCan) InertEqs
tv_eqs Cts
emptyCts
unsolved_fun_eqs = (EqCt -> Cts -> Cts) -> FunEqMap EqualCtList -> Cts -> Cts
forall b. (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
foldFunEqs ((EqCt -> Ct) -> EqCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved EqCt -> Ct
CEqCan) FunEqMap EqualCtList
fun_eqs Cts
emptyCts
unsolved_irreds = (IrredCt -> Cts -> Cts) -> Cts -> Bag IrredCt -> Cts
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((IrredCt -> Ct) -> IrredCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved IrredCt -> Ct
CIrredCan) Cts
emptyCts Bag IrredCt
irreds
unsolved_dicts = (DictCt -> Cts -> Cts) -> DictMap DictCt -> Cts -> Cts
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts ((DictCt -> Ct) -> DictCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved DictCt -> Ct
CDictCan) DictMap DictCt
idicts Cts
emptyCts
; implics <- getWorkListImplics
; traceTcS "getUnsolvedInerts" $
vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
, text "fun eqs =" <+> ppr unsolved_fun_eqs
, text "dicts =" <+> ppr unsolved_dicts
, text "irreds =" <+> ppr unsolved_irreds
, text "implics =" <+> ppr implics ]
; return ( implics, unsolved_tv_eqs `unionBags`
unsolved_fun_eqs `unionBags`
unsolved_irreds `unionBags`
unsolved_dicts ) }
where
add_if_unsolved :: (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved :: forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved a -> Ct
mk_ct a
thing Cts
cts
| Ct -> Bool
isWantedCt Ct
ct = Ct
ct Ct -> Cts -> Cts
`consCts` Cts
cts
| Bool
otherwise = Cts
cts
where
ct :: Ct
ct = a -> Ct
mk_ct a
thing
getHasGivenEqs :: TcLevel
-> TcS ( HasGivenEqs
, InertIrreds )
getHasGivenEqs :: TcLevel -> TcS (HasGivenEqs, Bag IrredCt)
getHasGivenEqs TcLevel
tclvl
= do { inerts@(IC { inert_irreds = irreds
, inert_given_eqs = given_eqs
, inert_given_eq_lvl = ge_lvl })
<- TcS InertCans
getInertCans
; let given_insols = (IrredCt -> Bool) -> Bag IrredCt -> Bag IrredCt
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag IrredCt -> Bool
insoluble_given_equality Bag IrredCt
irreds
has_ge | TcLevel
ge_lvl TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
tclvl = HasGivenEqs
MaybeGivenEqs
| Bool
given_eqs = HasGivenEqs
LocalGivenEqs
| Bool
otherwise = HasGivenEqs
NoGivenEqs
; traceTcS "getHasGivenEqs" $
vcat [ text "given_eqs:" <+> ppr given_eqs
, text "ge_lvl:" <+> ppr ge_lvl
, text "ambient level:" <+> ppr tclvl
, text "Inerts:" <+> ppr inerts
, text "Insols:" <+> ppr given_insols]
; return (has_ge, given_insols) }
where
insoluble_given_equality :: IrredCt -> Bool
insoluble_given_equality :: IrredCt -> Bool
insoluble_given_equality (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev, ir_reason :: IrredCt -> CtIrredReason
ir_reason = CtIrredReason
reason })
= CtIrredReason -> Bool
isInsolubleReason CtIrredReason
reason Bool -> Bool -> Bool
&& CtEvidence -> Bool
isGiven CtEvidence
ev
removeInertCts :: [Ct] -> InertCans -> InertCans
removeInertCts :: [Ct] -> InertCans -> InertCans
removeInertCts [Ct]
cts InertCans
icans = (InertCans -> Ct -> InertCans) -> InertCans -> [Ct] -> InertCans
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' InertCans -> Ct -> InertCans
removeInertCt InertCans
icans [Ct]
cts
removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt InertCans
is Ct
ct
= case Ct
ct of
CDictCan DictCt
dict_ct -> InertCans
is { inert_dicts = delDict dict_ct (inert_dicts is) }
CEqCan EqCt
eq_ct -> EqCt -> InertCans -> InertCans
delEq EqCt
eq_ct InertCans
is
CIrredCan IrredCt
ir_ct -> IrredCt -> InertCans -> InertCans
delIrred IrredCt
ir_ct InertCans
is
CQuantCan {} -> String -> InertCans
forall a. HasCallStack => String -> a
panic String
"removeInertCt: CQuantCan"
CNonCanonical {} -> String -> InertCans
forall a. HasCallStack => String -> a
panic String
"removeInertCt: CNonCanonical"
lookupFamAppInert :: (CtFlavourRole -> Bool)
-> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
lookupFamAppInert :: (CtFlavourRole -> Bool)
-> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
lookupFamAppInert CtFlavourRole -> Bool
rewrite_pred TyCon
fam_tc [Type]
tys
= do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- TcS InertSet
getInertSet
; return (lookup_inerts inert_funeqs) }
where
lookup_inerts :: FunEqMap EqualCtList -> Maybe (Reduction, CtFlavourRole)
lookup_inerts FunEqMap EqualCtList
inert_funeqs
| Just EqualCtList
ecl <- FunEqMap EqualCtList -> TyCon -> [Type] -> Maybe EqualCtList
forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap EqualCtList
inert_funeqs TyCon
fam_tc [Type]
tys
, Just (EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ctev, eq_rhs :: EqCt -> Type
eq_rhs = Type
rhs })
<- (EqCt -> Bool) -> EqualCtList -> Maybe EqCt
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (CtFlavourRole -> Bool
rewrite_pred (CtFlavourRole -> Bool) -> (EqCt -> CtFlavourRole) -> EqCt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqCt -> CtFlavourRole
eqCtFlavourRole) EqualCtList
ecl
= (Reduction, CtFlavourRole) -> Maybe (Reduction, CtFlavourRole)
forall a. a -> Maybe a
Just (Coercion -> Type -> Reduction
mkReduction (HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion CtEvidence
ctev) Type
rhs, HasDebugCallStack => CtEvidence -> CtFlavourRole
CtEvidence -> CtFlavourRole
ctEvFlavourRole CtEvidence
ctev)
| Bool
otherwise = Maybe (Reduction, CtFlavourRole)
forall a. Maybe a
Nothing
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts :: CtLoc -> Type -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc Type
pty
| ClassPred Class
cls [Type]
tys <- Type -> Pred
classifyPredType Type
pty
= do { inerts <- TcS InertSet
getInertSet
; let mb_solved = InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict InertSet
inerts CtLoc
loc Class
cls [Type]
tys
mb_inert = (DictCt -> CtEvidence) -> Maybe DictCt -> Maybe CtEvidence
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DictCt -> CtEvidence
dictCtEvidence (InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
lookupInertDict (InertSet -> InertCans
inert_cans InertSet
inerts) CtLoc
loc Class
cls [Type]
tys)
; return $ do
found_ev <- mb_solved `mplus` mb_inert
guard $ not (prohibitedSuperClassSolve (ctEvLoc found_ev) loc)
return found_ev }
| Bool
otherwise
= Maybe CtEvidence -> TcS (Maybe CtEvidence)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe CtEvidence
forall a. Maybe a
Nothing
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
lookupInertDict (IC { inert_dicts :: InertCans -> DictMap DictCt
inert_dicts = DictMap DictCt
dicts }) CtLoc
loc Class
cls [Type]
tys
= DictMap DictCt -> CtLoc -> Class -> [Type] -> Maybe DictCt
forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap DictCt
dicts CtLoc
loc Class
cls [Type]
tys
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict (IS { inert_solved_dicts :: InertSet -> DictMap DictCt
inert_solved_dicts = DictMap DictCt
solved }) CtLoc
loc Class
cls [Type]
tys
= (DictCt -> CtEvidence) -> Maybe DictCt -> Maybe CtEvidence
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DictCt -> CtEvidence
dictCtEvidence (DictMap DictCt -> CtLoc -> Class -> [Type] -> Maybe DictCt
forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap DictCt
solved CtLoc
loc Class
cls [Type]
tys)
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache TyCon
fam_tc [Type]
tys
= do { IS { inert_famapp_cache = famapp_cache } <- TcS InertSet
getInertSet
; case findFunEq famapp_cache fam_tc tys of
result :: Maybe Reduction
result@(Just Reduction
redn) ->
do { String -> SDoc -> TcS ()
traceTcS String
"famapp_cache hit" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys)
, Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn ])
; Maybe Reduction -> TcS (Maybe Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
result }
Maybe Reduction
Nothing -> Maybe Reduction -> TcS (Maybe Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing }
extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
extendFamAppCache TyCon
tc [Type]
xi_args stuff :: Reduction
stuff@(Reduction Coercion
_ Type
ty)
= do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; when (gopt Opt_FamAppCache dflags) $
do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args
, ppr ty ])
; updInertSet $ \ is :: InertSet
is@(IS { inert_famapp_cache :: InertSet -> FunEqMap Reduction
inert_famapp_cache = FunEqMap Reduction
fc }) ->
InertSet
is { inert_famapp_cache = insertFunEq fc tc xi_args stuff } } }
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache VarSet
varset
= (InertSet -> InertSet) -> TcS ()
updInertSet (\inerts :: InertSet
inerts@(IS { inert_famapp_cache :: InertSet -> FunEqMap Reduction
inert_famapp_cache = FunEqMap Reduction
famapp_cache }) ->
InertSet
inerts { inert_famapp_cache = filterTcAppMap check famapp_cache })
where
check :: Reduction -> Bool
check :: Reduction -> Bool
check Reduction
redn
= Bool -> Bool
not ((TcTyVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo (TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
varset) (Coercion -> Bool) -> Coercion -> Bool
forall a b. (a -> b) -> a -> b
$ Reduction -> Coercion
reductionCoercion Reduction
redn)
data TcSEnv
= TcSEnv {
TcSEnv -> EvBindsVar
tcs_ev_binds :: EvBindsVar,
TcSEnv -> IORef Int
tcs_unified :: IORef Int,
TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl :: IORef (Maybe TcLevel),
TcSEnv -> IORef Int
tcs_count :: IORef Int,
TcSEnv -> IORef InertSet
tcs_inerts :: IORef InertSet,
TcSEnv -> Bool
tcs_abort_on_insoluble :: Bool,
TcSEnv -> IORef WorkList
tcs_worklist :: IORef WorkList
}
newtype TcS a = TcS { forall a. TcS a -> TcSEnv -> TcM a
unTcS :: TcSEnv -> TcM a }
deriving ((forall a b. (a -> b) -> TcS a -> TcS b)
-> (forall a b. a -> TcS b -> TcS a) -> Functor TcS
forall a b. a -> TcS b -> TcS a
forall a b. (a -> b) -> TcS a -> TcS b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TcS a -> TcS b
fmap :: forall a b. (a -> b) -> TcS a -> TcS b
$c<$ :: forall a b. a -> TcS b -> TcS a
<$ :: forall a b. a -> TcS b -> TcS a
Functor)
instance MonadFix TcS where
mfix :: forall a. (a -> TcS a) -> TcS a
mfix a -> TcS a
k = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env -> (a -> TcM a) -> TcM a
forall a.
(a -> IOEnv (Env TcGblEnv TcLclEnv) a)
-> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (\a
x -> TcS a -> TcSEnv -> TcM a
forall a. TcS a -> TcSEnv -> TcM a
unTcS (a -> TcS a
k a
x) TcSEnv
env)
mkTcS :: (TcSEnv -> TcM a) -> TcS a
mkTcS :: forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS TcSEnv -> TcM a
f = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcSEnv -> TcM a
forall a b. (a -> b) -> a -> b
oneShot TcSEnv -> TcM a
f)
instance Applicative TcS where
pure :: forall a. a -> TcS a
pure a
x = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
_ -> a -> TcM a
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
<*> :: forall a b. TcS (a -> b) -> TcS a -> TcS b
(<*>) = TcS (a -> b) -> TcS a -> TcS b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad TcS where
TcS a
m >>= :: forall a b. TcS a -> (a -> TcS b) -> TcS b
>>= a -> TcS b
k = (TcSEnv -> TcM b) -> TcS b
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM b) -> TcS b) -> (TcSEnv -> TcM b) -> TcS b
forall a b. (a -> b) -> a -> b
$ \TcSEnv
ebs -> do
TcS a -> TcSEnv -> TcM a
forall a. TcS a -> TcSEnv -> TcM a
unTcS TcS a
m TcSEnv
ebs TcM a -> (a -> TcM b) -> TcM b
forall a b.
IOEnv (Env TcGblEnv TcLclEnv) a
-> (a -> IOEnv (Env TcGblEnv TcLclEnv) b)
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a
r -> TcS b -> TcSEnv -> TcM b
forall a. TcS a -> TcSEnv -> TcM a
unTcS (a -> TcS b
k a
r) TcSEnv
ebs)
instance MonadIO TcS where
liftIO :: forall a. IO a -> TcS a
liftIO IO a
act = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
_env -> IO a -> TcM a
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO a
act
instance MonadFail TcS where
fail :: forall a. String -> TcS a
fail String
err = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
_ -> String -> TcM a
forall a. String -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
instance MonadUnique TcS where
getUniqueSupplyM :: TcS UniqSupply
getUniqueSupplyM = TcM UniqSupply -> TcS UniqSupply
forall a. TcM a -> TcS a
wrapTcS TcM UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
instance HasModule TcS where
getModule :: TcS Module
getModule = TcM Module -> TcS Module
forall a. TcM a -> TcS a
wrapTcS TcM Module
forall (m :: * -> *). HasModule m => m Module
getModule
instance MonadThings TcS where
lookupThing :: Name -> TcS TyThing
lookupThing Name
n = TcM TyThing -> TcS TyThing
forall a. TcM a -> TcS a
wrapTcS (Name -> TcM TyThing
forall (m :: * -> *). MonadThings m => Name -> m TyThing
lookupThing Name
n)
wrapTcS :: TcM a -> TcS a
wrapTcS :: forall a. TcM a -> TcS a
wrapTcS TcM a
action = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
_env -> TcM a
action
liftZonkTcS :: ZonkM a -> TcS a
liftZonkTcS :: forall a. ZonkM a -> TcS a
liftZonkTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcM a -> TcS a) -> (ZonkM a -> TcM a) -> ZonkM a -> TcS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ZonkM a -> TcM a
forall a. ZonkM a -> TcM a
TcM.liftZonkM
wrap2TcS :: (TcM a -> TcM a) -> TcS a -> TcS a
wrap2TcS :: forall a. (TcM a -> TcM a) -> TcS a -> TcS a
wrap2TcS TcM a -> TcM a
fn (TcS TcSEnv -> TcM a
thing) = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env -> TcM a -> TcM a
fn (TcSEnv -> TcM a
thing TcSEnv
env)
wrapErrTcS :: TcM a -> TcS a
wrapErrTcS :: forall a. TcM a -> TcS a
wrapErrTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS
wrapWarnTcS :: TcM a -> TcS a
wrapWarnTcS :: forall a. TcM a -> TcS a
wrapWarnTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS
panicTcS :: SDoc -> TcS a
failTcS :: TcRnMessage -> TcS a
warnTcS, addErrTcS :: TcRnMessage -> TcS ()
failTcS :: forall a. TcRnMessage -> TcS a
failTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcM a -> TcS a) -> (TcRnMessage -> TcM a) -> TcRnMessage -> TcS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcRnMessage -> TcM a
forall a. TcRnMessage -> TcRn a
TcM.failWith
warnTcS :: TcRnMessage -> TcS ()
warnTcS TcRnMessage
msg = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcRnMessage -> TcM ()
TcM.addDiagnostic TcRnMessage
msg)
addErrTcS :: TcRnMessage -> TcS ()
addErrTcS = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ())
-> (TcRnMessage -> TcM ()) -> TcRnMessage -> TcS ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcRnMessage -> TcM ()
TcM.addErr
panicTcS :: forall a. SDoc -> TcS a
panicTcS SDoc
doc = String -> SDoc -> TcS a
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"GHC.Tc.Solver.Monad" SDoc
doc
tryEarlyAbortTcS :: TcS ()
tryEarlyAbortTcS :: TcS ()
tryEarlyAbortTcS
= (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS (\TcSEnv
env -> Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TcSEnv -> Bool
tcs_abort_on_insoluble TcSEnv
env) TcM ()
forall env a. IOEnv env a
TcM.failM)
ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS ()
ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS ()
ctLocWarnTcS CtLoc
loc TcRnMessage
msg = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcM () -> TcM ()
forall a. CtLoc -> TcM a -> TcM a
TcM.setCtLocM CtLoc
loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ TcRnMessage -> TcM ()
TcM.addDiagnostic TcRnMessage
msg
traceTcS :: String -> SDoc -> TcS ()
traceTcS :: String -> SDoc -> TcS ()
traceTcS String
herald SDoc
doc = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (String -> SDoc -> TcM ()
TcM.traceTc String
herald SDoc
doc)
{-# INLINE traceTcS #-}
runTcPluginTcS :: TcPluginM a -> TcS a
runTcPluginTcS :: forall a. TcPluginM a -> TcS a
runTcPluginTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcM a -> TcS a) -> (TcPluginM a -> TcM a) -> TcPluginM a -> TcS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM a -> TcM a
forall a. TcPluginM a -> TcM a
runTcPluginM
instance HasDynFlags TcS where
getDynFlags :: TcS DynFlags
getDynFlags = TcM DynFlags -> TcS DynFlags
forall a. TcM a -> TcS a
wrapTcS TcM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS = TcM GlobalRdrEnv -> TcS GlobalRdrEnv
forall a. TcM a -> TcS a
wrapTcS TcM GlobalRdrEnv
TcM.getGlobalRdrEnv
bumpStepCountTcS :: TcS ()
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env ->
do { let ref :: IORef Int
ref = TcSEnv -> IORef Int
tcs_count TcSEnv
env
; n <- IORef Int -> IOEnv (Env TcGblEnv TcLclEnv) Int
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef Int
ref
; TcM.writeTcRef ref (n+1) }
csTraceTcS :: SDoc -> TcS ()
csTraceTcS :: SDoc -> TcS ()
csTraceTcS SDoc
doc
= TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ TcM SDoc -> TcM ()
csTraceTcM (SDoc -> TcM SDoc
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return SDoc
doc)
{-# INLINE csTraceTcS #-}
traceFireTcS :: CtEvidence -> SDoc -> TcS ()
traceFireTcS :: CtEvidence -> SDoc -> TcS ()
traceFireTcS CtEvidence
ev SDoc
doc
= (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env -> TcM SDoc -> TcM ()
csTraceTcM (TcM SDoc -> TcM ()) -> TcM SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { n <- IORef Int -> IOEnv (Env TcGblEnv TcLclEnv) Int
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef (TcSEnv -> IORef Int
tcs_count TcSEnv
env)
; tclvl <- TcM.getTcLevel
; return (hang (text "Step" <+> int n
<> brackets (text "l:" <> ppr tclvl <> comma <>
text "d:" <> ppr (ctLocDepth (ctEvLoc ev)))
<+> doc <> colon)
4 (ppr ev)) }
{-# INLINE traceFireTcS #-}
csTraceTcM :: TcM SDoc -> TcM ()
csTraceTcM :: TcM SDoc -> TcM ()
csTraceTcM TcM SDoc
mk_doc
= do { logger <- IOEnv (Env TcGblEnv TcLclEnv) Logger
forall (m :: * -> *). HasLogger m => m Logger
getLogger
; when ( logHasDumpFlag logger Opt_D_dump_cs_trace
|| logHasDumpFlag logger Opt_D_dump_tc_trace)
( do { msg <- mk_doc
; TcM.dumpTcRn False
Opt_D_dump_cs_trace
"" FormatText
msg }) }
{-# INLINE csTraceTcM #-}
runTcS :: TcS a
-> TcM (a, EvBindMap)
runTcS :: forall a. TcS a -> TcM (a, EvBindMap)
runTcS TcS a
tcs
= do { ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
; res <- runTcSWithEvBinds ev_binds_var tcs
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
; return (res, ev_binds) }
runTcSEarlyAbort :: TcS a -> TcM a
runTcSEarlyAbort :: forall a. TcS a -> TcM a
runTcSEarlyAbort TcS a
tcs
= do { ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
; runTcSWithEvBinds' True True ev_binds_var tcs }
runTcSEqualities :: TcS a -> TcM a
runTcSEqualities :: forall a. TcS a -> TcM a
runTcSEqualities TcS a
thing_inside
= do { ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
; runTcSWithEvBinds ev_binds_var thing_inside }
runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
runTcSInerts :: forall a. InertSet -> TcS a -> TcM (a, InertSet)
runTcSInerts InertSet
inerts TcS a
tcs = do
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
runTcSWithEvBinds' False False ev_binds_var $ do
setInertSet inerts
a <- tcs
new_inerts <- getInertSet
return (a, new_inerts)
runTcSWithEvBinds :: EvBindsVar
-> TcS a
-> TcM a
runTcSWithEvBinds :: forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds = Bool -> Bool -> EvBindsVar -> TcS a -> TcM a
forall a. Bool -> Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
True Bool
False
runTcSWithEvBinds' :: Bool
-> Bool
-> EvBindsVar
-> TcS a
-> TcM a
runTcSWithEvBinds' :: forall a. Bool -> Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
restore_cycles Bool
abort_on_insoluble EvBindsVar
ev_binds_var TcS a
tcs
= do { unified_var <- Int -> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int)
forall (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
TcM.newTcRef Int
0
; step_count <- TcM.newTcRef 0
; inert_var <- TcM.newTcRef emptyInert
; wl_var <- TcM.newTcRef emptyWorkList
; unif_lvl_var <- TcM.newTcRef Nothing
; let env = TcSEnv { tcs_ev_binds :: EvBindsVar
tcs_ev_binds = EvBindsVar
ev_binds_var
, tcs_unified :: IORef Int
tcs_unified = IORef Int
unified_var
, tcs_unif_lvl :: IORef (Maybe TcLevel)
tcs_unif_lvl = IORef (Maybe TcLevel)
unif_lvl_var
, tcs_count :: IORef Int
tcs_count = IORef Int
step_count
, tcs_inerts :: IORef InertSet
tcs_inerts = IORef InertSet
inert_var
, tcs_abort_on_insoluble :: Bool
tcs_abort_on_insoluble = Bool
abort_on_insoluble
, tcs_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
wl_var }
; res <- unTcS tcs env
; count <- TcM.readTcRef step_count
; when (count > 0) $
csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
; when restore_cycles $
do { inert_set <- TcM.readTcRef inert_var
; restoreTyVarCycles inert_set }
#if defined(DEBUG)
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
; checkForCyclicBinds ev_binds
#endif
; return res }
#if defined(DEBUG)
checkForCyclicBinds :: EvBindMap -> TcM ()
checkForCyclicBinds ev_binds_map
| null cycles
= return ()
| null coercion_cycles
= TcM.traceTc "Cycle in evidence binds" $ ppr cycles
| otherwise
= pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
where
ev_binds = evBindMapBinds ev_binds_map
cycles :: [[EvBind]]
cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
coercion_cycles = [c | c <- cycles, any is_co_bind c]
is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
edges :: [ Node EvVar EvBind ]
edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (evVarsOfTerm rhs))
| bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs}) <- bagToList ev_binds ]
#endif
setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
setEvBindsTcS :: forall a. EvBindsVar -> TcS a -> TcS a
setEvBindsTcS EvBindsVar
ref (TcS TcSEnv -> TcM a
thing_inside)
= (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env -> TcSEnv -> TcM a
thing_inside (TcSEnv
env { tcs_ev_binds = ref })
nestImplicTcS :: EvBindsVar
-> TcLevel -> TcS a
-> TcS a
nestImplicTcS :: forall a. EvBindsVar -> TcLevel -> TcS a -> TcS a
nestImplicTcS EvBindsVar
ref TcLevel
inner_tclvl (TcS TcSEnv -> TcM a
thing_inside)
= (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ TcSEnv { tcs_unified :: TcSEnv -> IORef Int
tcs_unified = IORef Int
unified_var
, tcs_inerts :: TcSEnv -> IORef InertSet
tcs_inerts = IORef InertSet
old_inert_var
, tcs_count :: TcSEnv -> IORef Int
tcs_count = IORef Int
count
, tcs_unif_lvl :: TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl = IORef (Maybe TcLevel)
unif_lvl
, tcs_abort_on_insoluble :: TcSEnv -> Bool
tcs_abort_on_insoluble = Bool
abort_on_insoluble
} ->
do { inerts <- IORef InertSet -> IOEnv (Env TcGblEnv TcLclEnv) InertSet
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef InertSet
old_inert_var
; let nest_inert = InertSet
inerts { inert_cycle_breakers = pushCycleBreakerVarStack
(inert_cycle_breakers inerts)
, inert_cans = (inert_cans inerts)
{ inert_given_eqs = False } }
; new_inert_var <- TcM.newTcRef nest_inert
; new_wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = TcSEnv { tcs_count :: IORef Int
tcs_count = IORef Int
count
, tcs_unif_lvl :: IORef (Maybe TcLevel)
tcs_unif_lvl = IORef (Maybe TcLevel)
unif_lvl
, tcs_ev_binds :: EvBindsVar
tcs_ev_binds = EvBindsVar
ref
, tcs_unified :: IORef Int
tcs_unified = IORef Int
unified_var
, tcs_inerts :: IORef InertSet
tcs_inerts = IORef InertSet
new_inert_var
, tcs_abort_on_insoluble :: Bool
tcs_abort_on_insoluble = Bool
abort_on_insoluble
, tcs_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
new_wl_var }
; res <- TcM.setTcLevel inner_tclvl $
thing_inside nest_env
; out_inert_set <- TcM.readTcRef new_inert_var
; restoreTyVarCycles out_inert_set
#if defined(DEBUG)
; ev_binds <- TcM.getTcEvBindsMap ref
; checkForCyclicBinds ev_binds
#endif
; return res }
nestTcS :: TcS a -> TcS a
nestTcS :: forall a. TcS a -> TcS a
nestTcS (TcS TcSEnv -> TcM a
thing_inside)
= (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ env :: TcSEnv
env@(TcSEnv { tcs_inerts :: TcSEnv -> IORef InertSet
tcs_inerts = IORef InertSet
inerts_var }) ->
do { inerts <- IORef InertSet -> IOEnv (Env TcGblEnv TcLclEnv) InertSet
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef InertSet
inerts_var
; new_inert_var <- TcM.newTcRef inerts
; new_wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = TcSEnv
env { tcs_inerts = new_inert_var
, tcs_worklist = new_wl_var }
; res <- thing_inside nest_env
; new_inerts <- TcM.readTcRef new_inert_var
; let old_ic = InertSet -> InertCans
inert_cans InertSet
inerts
new_ic = InertSet -> InertCans
inert_cans InertSet
new_inerts
nxt_ic = InertCans
old_ic { inert_safehask = inert_safehask new_ic }
; TcM.writeTcRef inerts_var
(inerts { inert_solved_dicts = inert_solved_dicts new_inerts
, inert_cans = nxt_ic })
; return res }
emitImplicationTcS :: TcLevel -> SkolemInfoAnon
-> [TcTyVar]
-> [EvVar]
-> Cts
-> TcS TcEvBinds
emitImplicationTcS :: TcLevel
-> SkolemInfoAnon -> [TcTyVar] -> [TcTyVar] -> Cts -> TcS TcEvBinds
emitImplicationTcS TcLevel
new_tclvl SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
givens Cts
wanteds
= do { let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple = wanteds }
; imp <- TcM Implication -> TcS Implication
forall a. TcM a -> TcS a
wrapTcS (TcM Implication -> TcS Implication)
-> TcM Implication -> TcS Implication
forall a b. (a -> b) -> a -> b
$
do { ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
; imp <- TcM.newImplication
; return (imp { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_given = givens
, ic_wanted = wc
, ic_binds = ev_binds_var
, ic_info = skol_info }) }
; emitImplication imp
; return (TcEvBinds (ic_binds imp)) }
emitTvImplicationTcS :: TcLevel -> SkolemInfoAnon
-> [TcTyVar]
-> Cts
-> TcS ()
emitTvImplicationTcS :: TcLevel -> SkolemInfoAnon -> [TcTyVar] -> Cts -> TcS ()
emitTvImplicationTcS TcLevel
new_tclvl SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs Cts
wanteds
= do { let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple = wanteds }
; imp <- TcM Implication -> TcS Implication
forall a. TcM a -> TcS a
wrapTcS (TcM Implication -> TcS Implication)
-> TcM Implication -> TcS Implication
forall a b. (a -> b) -> a -> b
$
do { ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
; imp <- TcM.newImplication
; return (imp { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_wanted = wc
, ic_binds = ev_binds_var
, ic_info = skol_info }) }
; emitImplication imp }
getUnifiedRef :: TcS (IORef Int)
getUnifiedRef :: TcS (IORef Int)
getUnifiedRef = (TcSEnv -> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int))
-> TcS (IORef Int)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (IORef Int -> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef Int -> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int))
-> (TcSEnv -> IORef Int)
-> TcSEnv
-> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef Int
tcs_unified)
getInertSetRef :: TcS (IORef InertSet)
getInertSetRef :: TcS (IORef InertSet)
getInertSetRef = (TcSEnv -> IOEnv (Env TcGblEnv TcLclEnv) (IORef InertSet))
-> TcS (IORef InertSet)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (IORef InertSet -> IOEnv (Env TcGblEnv TcLclEnv) (IORef InertSet)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef InertSet -> IOEnv (Env TcGblEnv TcLclEnv) (IORef InertSet))
-> (TcSEnv -> IORef InertSet)
-> TcSEnv
-> IOEnv (Env TcGblEnv TcLclEnv) (IORef InertSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef InertSet
tcs_inerts)
getInertSet :: TcS InertSet
getInertSet :: TcS InertSet
getInertSet = TcS (IORef InertSet)
getInertSetRef TcS (IORef InertSet)
-> (IORef InertSet -> TcS InertSet) -> TcS InertSet
forall a b. TcS a -> (a -> TcS b) -> TcS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IORef InertSet -> TcS InertSet
forall a. TcRef a -> TcS a
readTcRef
setInertSet :: InertSet -> TcS ()
setInertSet :: InertSet -> TcS ()
setInertSet InertSet
is = do { r <- TcS (IORef InertSet)
getInertSetRef; writeTcRef r is }
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef = (TcSEnv -> IOEnv (Env TcGblEnv TcLclEnv) (IORef WorkList))
-> TcS (IORef WorkList)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (IORef WorkList -> IOEnv (Env TcGblEnv TcLclEnv) (IORef WorkList)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef WorkList -> IOEnv (Env TcGblEnv TcLclEnv) (IORef WorkList))
-> (TcSEnv -> IORef WorkList)
-> TcSEnv
-> IOEnv (Env TcGblEnv TcLclEnv) (IORef WorkList)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef WorkList
tcs_worklist)
getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics
= do { wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; wl_curr <- readTcRef wl_var
; return (wl_implics wl_curr) }
pushLevelNoWorkList :: SDoc -> TcS a -> TcS (TcLevel, a)
#if defined(DEBUG)
pushLevelNoWorkList err_doc (TcS thing_inside)
= TcS (\env -> TcM.pushTcLevelM $
thing_inside (env { tcs_worklist = wl_panic })
)
where
wl_panic = pprPanic "GHC.Tc.Solver.Monad.buildImplication" err_doc
#else
pushLevelNoWorkList :: forall a. SDoc -> TcS a -> TcS (TcLevel, a)
pushLevelNoWorkList SDoc
_ (TcS TcSEnv -> TcM a
thing_inside)
= (TcSEnv -> TcM (TcLevel, a)) -> TcS (TcLevel, a)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (\TcSEnv
env -> TcM a -> TcM (TcLevel, a)
forall a. TcM a -> TcM (TcLevel, a)
TcM.pushTcLevelM (TcSEnv -> TcM a
thing_inside TcSEnv
env))
#endif
updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS WorkList -> WorkList
f
= do { wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; updTcRef wl_var f }
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence]
evs
| [CtEvidence] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CtEvidence]
evs
= () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= Cts -> TcS ()
emitWork ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag ((CtEvidence -> Ct) -> [CtEvidence] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
evs))
emitWork :: Cts -> TcS ()
emitWork :: Cts -> TcS ()
emitWork Cts
cts
| Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
cts
= () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"Emitting fresh work" (Cts -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag Cts
cts)
; cts <- TcM Cts -> TcS Cts
forall a. TcM a -> TcS a
wrapTcS (TcM Cts -> TcS Cts) -> TcM Cts -> TcS Cts
forall a b. (a -> b) -> a -> b
$ (Ct -> IOEnv (Env TcGblEnv TcLclEnv) Ct) -> Cts -> TcM Cts
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Ct -> IOEnv (Env TcGblEnv TcLclEnv) Ct
TcM.zonkCtRewriterSet Cts
cts
; updWorkListTcS (extendWorkListCts cts) }
emitImplication :: Implication -> TcS ()
emitImplication :: Implication -> TcS ()
emitImplication Implication
implic
= (WorkList -> WorkList) -> TcS ()
updWorkListTcS (Implication -> WorkList -> WorkList
extendWorkListImplic Implication
implic)
newTcRef :: a -> TcS (TcRef a)
newTcRef :: forall a. a -> TcS (TcRef a)
newTcRef a
x = TcM (TcRef a) -> TcS (TcRef a)
forall a. TcM a -> TcS a
wrapTcS (a -> TcM (TcRef a)
forall (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
TcM.newTcRef a
x)
readTcRef :: TcRef a -> TcS a
readTcRef :: forall a. TcRef a -> TcS a
readTcRef TcRef a
ref = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcRef a -> TcM a
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef TcRef a
ref)
writeTcRef :: TcRef a -> a -> TcS ()
writeTcRef :: forall a. TcRef a -> a -> TcS ()
writeTcRef TcRef a
ref a
val = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcRef a -> a -> TcM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
TcM.writeTcRef TcRef a
ref a
val)
updTcRef :: TcRef a -> (a->a) -> TcS ()
updTcRef :: forall a. TcRef a -> (a -> a) -> TcS ()
updTcRef TcRef a
ref a -> a
upd_fn = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcRef a -> (a -> a) -> TcM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> (a -> a) -> m ()
TcM.updTcRef TcRef a
ref a -> a
upd_fn)
getTcEvBindsVar :: TcS EvBindsVar
getTcEvBindsVar :: TcS EvBindsVar
getTcEvBindsVar = (TcSEnv -> TcM EvBindsVar) -> TcS EvBindsVar
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (EvBindsVar -> TcM EvBindsVar
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvBindsVar -> TcM EvBindsVar)
-> (TcSEnv -> EvBindsVar) -> TcSEnv -> TcM EvBindsVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> EvBindsVar
tcs_ev_binds)
getTcLevel :: TcS TcLevel
getTcLevel :: TcS TcLevel
getTcLevel = TcM TcLevel -> TcS TcLevel
forall a. TcM a -> TcS a
wrapTcS TcM TcLevel
TcM.getTcLevel
getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
getTcEvTyCoVars :: EvBindsVar -> TcS VarSet
getTcEvTyCoVars EvBindsVar
ev_binds_var
= TcM VarSet -> TcS VarSet
forall a. TcM a -> TcS a
wrapTcS (TcM VarSet -> TcS VarSet) -> TcM VarSet -> TcS VarSet
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> TcM VarSet
TcM.getTcEvTyCoVars EvBindsVar
ev_binds_var
getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
getTcEvBindsMap EvBindsVar
ev_binds_var
= TcM EvBindMap -> TcS EvBindMap
forall a. TcM a -> TcS a
wrapTcS (TcM EvBindMap -> TcS EvBindMap) -> TcM EvBindMap -> TcS EvBindMap
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> TcM EvBindMap
TcM.getTcEvBindsMap EvBindsVar
ev_binds_var
setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
setTcEvBindsMap EvBindsVar
ev_binds_var EvBindMap
binds
= TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> EvBindMap -> TcM ()
TcM.setTcEvBindsMap EvBindsVar
ev_binds_var EvBindMap
binds
unifyTyVar :: TcTyVar -> TcType -> TcS ()
unifyTyVar :: TcTyVar -> Type -> TcS ()
unifyTyVar TcTyVar
tv Type
ty
= Bool -> SDoc -> TcS () -> TcS ()
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcTyVar -> Bool
isMetaTyVar TcTyVar
tv) (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
(TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env ->
do { String -> SDoc -> TcM ()
TcM.traceTc String
"unifyTyVar" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
; ZonkM () -> TcM ()
forall a. ZonkM a -> TcM a
TcM.liftZonkM (ZonkM () -> TcM ()) -> ZonkM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => TcTyVar -> Type -> ZonkM ()
TcTyVar -> Type -> ZonkM ()
TcM.writeMetaTyVar TcTyVar
tv Type
ty
; IORef Int -> (Int -> Int) -> TcM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> (a -> a) -> m ()
TcM.updTcRef (TcSEnv -> IORef Int
tcs_unified TcSEnv
env) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) }
reportUnifications :: TcS a -> TcS (Int, a)
reportUnifications :: forall a. TcS a -> TcS (Int, a)
reportUnifications (TcS TcSEnv -> TcM a
thing_inside)
= (TcSEnv -> TcM (Int, a)) -> TcS (Int, a)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM (Int, a)) -> TcS (Int, a))
-> (TcSEnv -> TcM (Int, a)) -> TcS (Int, a)
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env ->
do { inner_unified <- Int -> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int)
forall (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
TcM.newTcRef Int
0
; res <- thing_inside (env { tcs_unified = inner_unified })
; n_unifs <- TcM.readTcRef inner_unified
; TcM.updTcRef (tcs_unified env) (+ n_unifs)
; return (n_unifs, res) }
getDefaultInfo :: TcS (DefaultEnv, Bool)
getDefaultInfo :: TcS (DefaultEnv, Bool)
getDefaultInfo = TcM (DefaultEnv, Bool) -> TcS (DefaultEnv, Bool)
forall a. TcM a -> TcS a
wrapTcS TcM (DefaultEnv, Bool)
TcM.tcGetDefaultTys
getWorkList :: TcS WorkList
getWorkList :: TcS WorkList
getWorkList = do { wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; wrapTcS (TcM.readTcRef wl_var) }
selectNextWorkItem :: TcS (Maybe Ct)
selectNextWorkItem :: TcS (Maybe Ct)
selectNextWorkItem
= do { wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; wl <- readTcRef wl_var
; case selectWorkItem wl of {
Maybe (Ct, WorkList)
Nothing -> Maybe Ct -> TcS (Maybe Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Ct
forall a. Maybe a
Nothing ;
Just (Ct
ct, WorkList
new_wl) ->
do {
; IORef WorkList -> WorkList -> TcS ()
forall a. TcRef a -> a -> TcS ()
writeTcRef IORef WorkList
wl_var WorkList
new_wl
; Maybe Ct -> TcS (Maybe Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> Maybe Ct
forall a. a -> Maybe a
Just Ct
ct) } } }
getInstEnvs :: TcS InstEnvs
getInstEnvs :: TcS InstEnvs
getInstEnvs = TcM InstEnvs -> TcS InstEnvs
forall a. TcM a -> TcS a
wrapTcS (TcM InstEnvs -> TcS InstEnvs) -> TcM InstEnvs -> TcS InstEnvs
forall a b. (a -> b) -> a -> b
$ TcM InstEnvs
TcM.tcGetInstEnvs
getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs = TcM (FamInstEnv, FamInstEnv) -> TcS (FamInstEnv, FamInstEnv)
forall a. TcM a -> TcS a
wrapTcS (TcM (FamInstEnv, FamInstEnv) -> TcS (FamInstEnv, FamInstEnv))
-> TcM (FamInstEnv, FamInstEnv) -> TcS (FamInstEnv, FamInstEnv)
forall a b. (a -> b) -> a -> b
$ TcM (FamInstEnv, FamInstEnv)
FamInst.tcGetFamInstEnvs
getTopEnv :: TcS HscEnv
getTopEnv :: TcS HscEnv
getTopEnv = TcM HscEnv -> TcS HscEnv
forall a. TcM a -> TcS a
wrapTcS (TcM HscEnv -> TcS HscEnv) -> TcM HscEnv -> TcS HscEnv
forall a b. (a -> b) -> a -> b
$ TcM HscEnv
forall gbl lcl. TcRnIf gbl lcl HscEnv
TcM.getTopEnv
getGblEnv :: TcS TcGblEnv
getGblEnv :: TcS TcGblEnv
getGblEnv = TcM TcGblEnv -> TcS TcGblEnv
forall a. TcM a -> TcS a
wrapTcS (TcM TcGblEnv -> TcS TcGblEnv) -> TcM TcGblEnv -> TcS TcGblEnv
forall a b. (a -> b) -> a -> b
$ TcM TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
TcM.getGblEnv
getLclEnv :: TcS TcLclEnv
getLclEnv :: TcS TcLclEnv
getLclEnv = TcM TcLclEnv -> TcS TcLclEnv
forall a. TcM a -> TcS a
wrapTcS (TcM TcLclEnv -> TcS TcLclEnv) -> TcM TcLclEnv -> TcS TcLclEnv
forall a b. (a -> b) -> a -> b
$ TcM TcLclEnv
forall gbl lcl. TcRnIf gbl lcl lcl
TcM.getLclEnv
setSrcSpan :: RealSrcSpan -> TcS a -> TcS a
setSrcSpan :: forall a. RealSrcSpan -> TcS a -> TcS a
setSrcSpan RealSrcSpan
ss = (TcM a -> TcM a) -> TcS a -> TcS a
forall a. (TcM a -> TcM a) -> TcS a -> TcS a
wrap2TcS (SrcSpan -> TcM a -> TcM a
forall a. SrcSpan -> TcRn a -> TcRn a
TcM.setSrcSpan (RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan RealSrcSpan
ss Maybe BufSpan
forall a. Monoid a => a
mempty))
tcLookupClass :: Name -> TcS Class
tcLookupClass :: Name -> TcS Class
tcLookupClass Name
c = TcM Class -> TcS Class
forall a. TcM a -> TcS a
wrapTcS (TcM Class -> TcS Class) -> TcM Class -> TcS Class
forall a b. (a -> b) -> a -> b
$ Name -> TcM Class
TcM.tcLookupClass Name
c
tcLookupId :: Name -> TcS Id
tcLookupId :: Name -> TcS TcTyVar
tcLookupId Name
n = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (TcM TcTyVar -> TcS TcTyVar) -> TcM TcTyVar -> TcS TcTyVar
forall a b. (a -> b) -> a -> b
$ Name -> TcM TcTyVar
TcM.tcLookupId Name
n
tcLookupTyCon :: Name -> TcS TyCon
tcLookupTyCon :: Name -> TcS TyCon
tcLookupTyCon Name
n = TcM TyCon -> TcS TyCon
forall a. TcM a -> TcS a
wrapTcS (TcM TyCon -> TcS TyCon) -> TcM TyCon -> TcS TyCon
forall a b. (a -> b) -> a -> b
$ Name -> TcM TyCon
TcM.tcLookupTyCon Name
n
recordUsedGREs :: Bag GlobalRdrElt -> TcS ()
recordUsedGREs :: Bag GlobalRdrElt -> TcS ()
recordUsedGREs Bag GlobalRdrElt
gres
= do { TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ DeprecationWarnings -> [GlobalRdrElt] -> TcM ()
TcM.addUsedGREs DeprecationWarnings
NoDeprecationWarnings [GlobalRdrElt]
gre_list
; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ (GlobalRdrElt -> TcM ()) -> [GlobalRdrElt] -> TcM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (Name -> TcM ()
TcM.keepAlive (Name -> TcM ())
-> (GlobalRdrElt -> Name) -> GlobalRdrElt -> TcM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRdrElt -> Name
forall info. GlobalRdrEltX info -> Name
greName) [GlobalRdrElt]
gre_list }
where
gre_list :: [GlobalRdrElt]
gre_list = Bag GlobalRdrElt -> [GlobalRdrElt]
forall a. Bag a -> [a]
bagToList Bag GlobalRdrElt
gres
checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
checkWellStagedDFun :: CtLoc -> InstanceWhat -> Type -> TcS ()
checkWellStagedDFun CtLoc
loc InstanceWhat
what Type
pred
= do
mbind_lvl <- InstanceWhat -> TcS (Maybe Int)
checkWellStagedInstanceWhat InstanceWhat
what
case mbind_lvl of
Just Int
bind_lvl | Int
bind_lvl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
impLevel ->
TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcM () -> TcM ()
forall a. CtLoc -> TcM a -> TcM a
TcM.setCtLocM CtLoc
loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ do
{ use_stage <- TcM ThStage
TcM.getStage
; TcM.checkWellStaged (StageCheckInstance what pred) bind_lvl (thLevel use_stage) }
Maybe Int
_ ->
() -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkWellStagedInstanceWhat :: InstanceWhat -> TcS (Maybe ThLevel)
checkWellStagedInstanceWhat :: InstanceWhat -> TcS (Maybe Int)
checkWellStagedInstanceWhat InstanceWhat
what
| TopLevInstance { iw_dfun_id :: InstanceWhat -> TcTyVar
iw_dfun_id = TcTyVar
dfun_id } <- InstanceWhat
what
= Maybe Int -> TcS (Maybe Int)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> TcS (Maybe Int)) -> Maybe Int -> TcS (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just (TcTyVar -> Int
TcM.topIdLvl TcTyVar
dfun_id)
| BuiltinTypeableInstance TyCon
tc <- InstanceWhat
what
= do
cur_mod <- TcGblEnv -> Module
forall t. ContainsModule t => t -> Module
extractModule (TcGblEnv -> Module) -> TcS TcGblEnv -> TcS Module
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcS TcGblEnv
getGblEnv
return $ Just (if nameIsLocalOrFrom cur_mod (tyConName tc)
then outerLevel
else impLevel)
| Bool
otherwise = Maybe Int -> TcS (Maybe Int)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
pprEq :: TcType -> TcType -> SDoc
pprEq :: Type -> Type -> SDoc
pprEq Type
ty1 Type
ty2 = Type -> SDoc
pprParendType Type
ty1 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'~' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
pprParendType Type
ty2
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe TcTyVar
tv = TcM (Maybe Type) -> TcS (Maybe Type)
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM (Maybe Type)
TcM.isFilledMetaTyVar_maybe TcTyVar
tv)
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar TcTyVar
tv = TcM Bool -> TcS Bool
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM Bool
TcM.isFilledMetaTyVar TcTyVar
tv)
isUnfilledMetaTyVar :: TcTyVar -> TcS Bool
isUnfilledMetaTyVar :: TcTyVar -> TcS Bool
isUnfilledMetaTyVar TcTyVar
tv = TcM Bool -> TcS Bool
forall a. TcM a -> TcS a
wrapTcS (TcM Bool -> TcS Bool) -> TcM Bool -> TcS Bool
forall a b. (a -> b) -> a -> b
$ TcTyVar -> TcM Bool
TcM.isUnfilledMetaTyVar TcTyVar
tv
zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
zonkTyCoVarsAndFV :: VarSet -> TcS VarSet
zonkTyCoVarsAndFV VarSet
tvs = ZonkM VarSet -> TcS VarSet
forall a. ZonkM a -> TcS a
liftZonkTcS (VarSet -> ZonkM VarSet
TcM.zonkTyCoVarsAndFV VarSet
tvs)
zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
zonkTyCoVarsAndFVList :: [TcTyVar] -> TcS [TcTyVar]
zonkTyCoVarsAndFVList [TcTyVar]
tvs = ZonkM [TcTyVar] -> TcS [TcTyVar]
forall a. ZonkM a -> TcS a
liftZonkTcS ([TcTyVar] -> ZonkM [TcTyVar]
TcM.zonkTyCoVarsAndFVList [TcTyVar]
tvs)
zonkCo :: Coercion -> TcS Coercion
zonkCo :: Coercion -> TcS Coercion
zonkCo = TcM Coercion -> TcS Coercion
forall a. TcM a -> TcS a
wrapTcS (TcM Coercion -> TcS Coercion)
-> (Coercion -> TcM Coercion) -> Coercion -> TcS Coercion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ZonkM Coercion -> TcM Coercion)
-> (Coercion -> ZonkM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> (Coercion -> a) -> Coercion -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ZonkM Coercion -> TcM Coercion
forall a. ZonkM a -> TcM a
TcM.liftZonkM Coercion -> ZonkM Coercion
TcM.zonkCo
zonkTcType :: TcType -> TcS TcType
zonkTcType :: Type -> TcS Type
zonkTcType Type
ty = ZonkM Type -> TcS Type
forall a. ZonkM a -> TcS a
liftZonkTcS (Type -> ZonkM Type
TcM.zonkTcType Type
ty)
zonkTcTypes :: [TcType] -> TcS [TcType]
zonkTcTypes :: [Type] -> TcS [Type]
zonkTcTypes [Type]
tys = ZonkM [Type] -> TcS [Type]
forall a. ZonkM a -> TcS a
liftZonkTcS ([Type] -> ZonkM [Type]
TcM.zonkTcTypes [Type]
tys)
zonkTcTyVar :: TcTyVar -> TcS TcType
zonkTcTyVar :: TcTyVar -> TcS Type
zonkTcTyVar TcTyVar
tv = ZonkM Type -> TcS Type
forall a. ZonkM a -> TcS a
liftZonkTcS (TcTyVar -> ZonkM Type
TcM.zonkTcTyVar TcTyVar
tv)
zonkSimples :: Cts -> TcS Cts
zonkSimples :: Cts -> TcS Cts
zonkSimples Cts
cts = ZonkM Cts -> TcS Cts
forall a. ZonkM a -> TcS a
liftZonkTcS (Cts -> ZonkM Cts
TcM.zonkSimples Cts
cts)
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC WantedConstraints
wc = ZonkM WantedConstraints -> TcS WantedConstraints
forall a. ZonkM a -> TcS a
liftZonkTcS (WantedConstraints -> ZonkM WantedConstraints
TcM.zonkWC WantedConstraints
wc)
zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
zonkTyCoVarKind :: TcTyVar -> TcS TcTyVar
zonkTyCoVarKind TcTyVar
tv = ZonkM TcTyVar -> TcS TcTyVar
forall a. ZonkM a -> TcS a
liftZonkTcS (TcTyVar -> ZonkM TcTyVar
TcM.zonkTyCoVarKind TcTyVar
tv)
pprKicked :: Int -> SDoc
pprKicked :: Int -> SDoc
pprKicked Int
0 = SDoc
forall doc. IsOutput doc => doc
empty
pprKicked Int
n = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
n SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"kicked out")
resetUnificationFlag :: TcS Bool
resetUnificationFlag :: TcS Bool
resetUnificationFlag
= (TcSEnv -> TcM Bool) -> TcS Bool
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM Bool) -> TcS Bool)
-> (TcSEnv -> TcM Bool) -> TcS Bool
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env ->
do { let ref :: IORef (Maybe TcLevel)
ref = TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl TcSEnv
env
; ambient_lvl <- TcM TcLevel
TcM.getTcLevel
; mb_lvl <- TcM.readTcRef ref
; TcM.traceTc "resetUnificationFlag" $
vcat [ text "ambient:" <+> ppr ambient_lvl
, text "unif_lvl:" <+> ppr mb_lvl ]
; case mb_lvl of
Maybe TcLevel
Nothing -> Bool -> TcM Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just TcLevel
unif_lvl | TcLevel
ambient_lvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
unif_lvl
-> Bool -> TcM Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise
-> do { IORef (Maybe TcLevel) -> Maybe TcLevel -> TcM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
TcM.writeTcRef IORef (Maybe TcLevel)
ref Maybe TcLevel
forall a. Maybe a
Nothing
; Bool -> TcM Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True } }
setUnificationFlag :: TcLevel -> TcS ()
setUnificationFlag :: TcLevel -> TcS ()
setUnificationFlag TcLevel
lvl
= (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env ->
do { let ref :: IORef (Maybe TcLevel)
ref = TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl TcSEnv
env
; mb_lvl <- IORef (Maybe TcLevel)
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TcLevel)
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef (Maybe TcLevel)
ref
; case mb_lvl of
Just TcLevel
unif_lvl | TcLevel
lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcLevel
unif_lvl
-> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe TcLevel
_ -> IORef (Maybe TcLevel) -> Maybe TcLevel -> TcM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
TcM.writeTcRef IORef (Maybe TcLevel)
ref (TcLevel -> Maybe TcLevel
forall a. a -> Maybe a
Just TcLevel
lvl) }
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
instDFunType :: TcTyVar -> [Maybe Type] -> TcS ([Type], [Type])
instDFunType TcTyVar
dfun_id [Maybe Type]
inst_tys
= TcM ([Type], [Type]) -> TcS ([Type], [Type])
forall a. TcM a -> TcS a
wrapTcS (TcM ([Type], [Type]) -> TcS ([Type], [Type]))
-> TcM ([Type], [Type]) -> TcS ([Type], [Type])
forall a b. (a -> b) -> a -> b
$ TcTyVar -> [Maybe Type] -> TcM ([Type], [Type])
TcM.instDFunType TcTyVar
dfun_id [Maybe Type]
inst_tys
newFlexiTcSTy :: Kind -> TcS TcType
newFlexiTcSTy :: Type -> TcS Type
newFlexiTcSTy Type
knd = TcM Type -> TcS Type
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM Type
TcM.newFlexiTyVarTy Type
knd)
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar TcTyVar
tv = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM TcTyVar
TcM.cloneMetaTyVar TcTyVar
tv)
instFlexiX :: Subst -> [TKVar] -> TcS Subst
instFlexiX :: Subst -> [TcTyVar] -> TcS Subst
instFlexiX Subst
subst [TcTyVar]
tvs = TcM Subst -> TcS Subst
forall a. TcM a -> TcS a
wrapTcS (Subst -> [TcTyVar] -> TcM Subst
instFlexiXTcM Subst
subst [TcTyVar]
tvs)
instFlexiXTcM :: Subst -> [TKVar] -> TcM Subst
instFlexiXTcM :: Subst -> [TcTyVar] -> TcM Subst
instFlexiXTcM Subst
subst []
= Subst -> TcM Subst
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
subst
instFlexiXTcM Subst
subst (TcTyVar
tv:[TcTyVar]
tvs)
= do { uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
TcM.newUnique
; details <- TcM.newMetaDetails TauTv
; let name = Name -> Unique -> Name
setNameUnique (TcTyVar -> Name
tyVarName TcTyVar
tv) Unique
uniq
kind = Subst -> Type -> Type
substTyUnchecked Subst
subst (TcTyVar -> Type
tyVarKind TcTyVar
tv)
tv' = Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
name Type
kind TcTyVarDetails
details
subst' = Subst -> TcTyVar -> TcTyVar -> Subst
extendTvSubstWithClone Subst
subst TcTyVar
tv TcTyVar
tv'
; instFlexiXTcM subst' tvs }
matchGlobalInst :: DynFlags
-> Bool
-> Class -> [Type] -> CtLoc -> TcS TcM.ClsInstResult
matchGlobalInst :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Bool
short_cut Class
cls [Type]
tys CtLoc
loc
= TcM ClsInstResult -> TcS ClsInstResult
forall a. TcM a -> TcS a
wrapTcS (TcM ClsInstResult -> TcS ClsInstResult)
-> TcM ClsInstResult -> TcS ClsInstResult
forall a b. (a -> b) -> a -> b
$ DynFlags
-> Bool -> Class -> [Type] -> Maybe CtLoc -> TcM ClsInstResult
TcM.matchGlobalInst DynFlags
dflags Bool
short_cut Class
cls [Type]
tys (CtLoc -> Maybe CtLoc
forall a. a -> Maybe a
Just CtLoc
loc)
tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TcTyVar])
tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TcTyVar] -> TcS (Subst, [TcTyVar])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
subst [TcTyVar]
tvs = TcM (Subst, [TcTyVar]) -> TcS (Subst, [TcTyVar])
forall a. TcM a -> TcS a
wrapTcS (TcM (Subst, [TcTyVar]) -> TcS (Subst, [TcTyVar]))
-> TcM (Subst, [TcTyVar]) -> TcS (Subst, [TcTyVar])
forall a b. (a -> b) -> a -> b
$ SkolemInfo -> Subst -> [TcTyVar] -> TcM (Subst, [TcTyVar])
TcM.tcInstSkolTyVarsX SkolemInfo
skol_info Subst
subst [TcTyVar]
tvs
data MaybeNew = Fresh CtEvidence | Cached EvExpr
isFresh :: MaybeNew -> Bool
isFresh :: MaybeNew -> Bool
isFresh (Fresh {}) = Bool
True
isFresh (Cached {}) = Bool
False
freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals [MaybeNew]
mns = [ CtEvidence
ctev | Fresh CtEvidence
ctev <- [MaybeNew]
mns ]
getEvExpr :: MaybeNew -> EvExpr
getEvExpr :: MaybeNew -> EvExpr
getEvExpr (Fresh CtEvidence
ctev) = HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev
getEvExpr (Cached EvExpr
evt) = EvExpr
evt
setEvBind :: EvBind -> TcS ()
setEvBind :: EvBind -> TcS ()
setEvBind EvBind
ev_bind
= do { evb <- TcS EvBindsVar
getTcEvBindsVar
; wrapTcS $ TcM.addTcEvBind evb ev_bind }
useVars :: CoVarSet -> TcS ()
useVars :: VarSet -> TcS ()
useVars VarSet
co_vars
= do { ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
; let ref = EvBindsVar -> IORef VarSet
ebv_tcvs EvBindsVar
ev_binds_var
; wrapTcS $
do { tcvs <- TcM.readTcRef ref
; let tcvs' = VarSet
tcvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
co_vars
; TcM.writeTcRef ref tcvs' } }
setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS ()
setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS ()
setWantedEq (HoleDest CoercionHole
hole) Coercion
co
= do { VarSet -> TcS ()
useVars (Coercion -> VarSet
coVarsOfCo Coercion
co)
; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole Coercion
co }
setWantedEq (EvVarDest TcTyVar
ev) Coercion
_ = String -> SDoc -> TcS ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setWantedEq: EvVarDest" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
ev)
setWantedEvTerm :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedEvTerm :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedEvTerm (HoleDest CoercionHole
hole) CanonicalEvidence
_canonical EvTerm
tm
| Just Coercion
co <- EvTerm -> Maybe Coercion
evTermCoercion_maybe EvTerm
tm
= do { VarSet -> TcS ()
useVars (Coercion -> VarSet
coVarsOfCo Coercion
co)
; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole Coercion
co }
| Bool
otherwise
=
do { let co_var :: TcTyVar
co_var = CoercionHole -> TcTyVar
coHoleCoVar CoercionHole
hole
; EvBind -> TcS ()
setEvBind (TcTyVar -> CanonicalEvidence -> EvTerm -> EvBind
mkWantedEvBind TcTyVar
co_var CanonicalEvidence
EvCanonical EvTerm
tm)
; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole (TcTyVar -> Coercion
mkCoVarCo TcTyVar
co_var) }
setWantedEvTerm (EvVarDest TcTyVar
ev_id) CanonicalEvidence
canonical EvTerm
tm
= EvBind -> TcS ()
setEvBind (TcTyVar -> CanonicalEvidence -> EvTerm -> EvBind
mkWantedEvBind TcTyVar
ev_id CanonicalEvidence
canonical EvTerm
tm)
fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole Coercion
co
= do { TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CoercionHole -> Coercion -> TcM ()
TcM.fillCoercionHole CoercionHole
hole Coercion
co
; CoercionHole -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole }
setEvBindIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev CanonicalEvidence
canonical EvTerm
tm
= case CtEvidence
ev of
CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } -> TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest CanonicalEvidence
canonical EvTerm
tm
CtEvidence
_ -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds = TcM EvBindsVar -> TcS EvBindsVar
forall a. TcM a -> TcS a
wrapTcS TcM EvBindsVar
TcM.newTcEvBinds
newNoTcEvBinds :: TcS EvBindsVar
newNoTcEvBinds :: TcS EvBindsVar
newNoTcEvBinds = TcM EvBindsVar -> TcS EvBindsVar
forall a. TcM a -> TcS a
wrapTcS TcM EvBindsVar
TcM.newNoTcEvBinds
newEvVar :: TcPredType -> TcS EvVar
newEvVar :: Type -> TcS TcTyVar
newEvVar Type
pred = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TcTyVar
forall gbl lcl. Type -> TcRnIf gbl lcl TcTyVar
TcM.newEvVar Type
pred)
newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar :: CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (Type
pred, EvTerm
rhs)
= do { new_ev <- Type -> EvTerm -> TcS TcTyVar
newBoundEvVarId Type
pred EvTerm
rhs
; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
newBoundEvVarId :: Type -> EvTerm -> TcS TcTyVar
newBoundEvVarId Type
pred EvTerm
rhs
= do { new_ev <- Type -> TcS TcTyVar
newEvVar Type
pred
; setEvBind (mkGivenEvBind new_ev rhs)
; return new_ev }
emitNewGivens :: CtLoc -> [(Role,TcCoercion)] -> TcS ()
emitNewGivens :: CtLoc -> [(Role, Coercion)] -> TcS ()
emitNewGivens CtLoc
loc [(Role, Coercion)]
pts
= do { String -> SDoc -> TcS ()
traceTcS String
"emitNewGivens" ([(Role, Coercion)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Role, Coercion)]
pts)
; evs <- ((Type, EvTerm) -> TcS CtEvidence)
-> [(Type, EvTerm)] -> TcS [CtEvidence]
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 (CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc) ([(Type, EvTerm)] -> TcS [CtEvidence])
-> [(Type, EvTerm)] -> TcS [CtEvidence]
forall a b. (a -> b) -> a -> b
$
[ (Role -> Type -> Type -> Type
mkEqPredRole Role
role Type
ty1 Type
ty2, Coercion -> EvTerm
evCoercion Coercion
co)
| (Role
role, Coercion
co) <- [(Role, Coercion)]
pts
, let Pair Type
ty1 Type
ty2 = HasDebugCallStack => Coercion -> TypeEqn
Coercion -> TypeEqn
coercionKind Coercion
co
, Bool -> Bool
not (Type
ty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2) ]
; emitWorkNC evs }
emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion
emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> Type -> Type -> TcS Coercion
emitNewWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
= do { (ev, co) <- CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
; updWorkListTcS (extendWorkListEq rewriters (mkNonCanonical ev))
; return co }
newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType
-> TcS (CtEvidence, Coercion)
newWantedEq :: CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
= do { hole <- TcM CoercionHole -> TcS CoercionHole
forall a. TcM a -> TcS a
wrapTcS (TcM CoercionHole -> TcS CoercionHole)
-> TcM CoercionHole -> TcS CoercionHole
forall a b. (a -> b) -> a -> b
$ CtLoc -> Type -> TcM CoercionHole
TcM.newCoercionHole CtLoc
loc Type
pty
; return ( CtWanted { ctev_pred = pty
, ctev_dest = HoleDest hole
, ctev_loc = loc
, ctev_rewriters = rewriters }
, mkHoleCo hole ) }
where
pty :: Type
pty = Role -> Type -> Type -> Type
mkEqPredRole Role
role Type
ty1 Type
ty2
newWantedEvVarNC :: CtLoc -> RewriterSet
-> TcPredType -> TcS CtEvidence
newWantedEvVarNC :: CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
rewriters Type
pty
= Bool -> SDoc -> TcS CtEvidence -> TcS CtEvidence
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (Type -> Bool
isEqPred Type
pty)) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pty) (TcS CtEvidence -> TcS CtEvidence)
-> TcS CtEvidence -> TcS CtEvidence
forall a b. (a -> b) -> a -> b
$
do { new_ev <- Type -> TcS TcTyVar
newEvVar Type
pty
; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
pprCtLoc loc)
; return (CtWanted { ctev_pred = pty
, ctev_dest = EvVarDest new_ev
, ctev_loc = loc
, ctev_rewriters = rewriters })}
newWantedEvVar :: CtLoc -> RewriterSet
-> TcPredType -> TcS MaybeNew
newWantedEvVar :: CtLoc -> RewriterSet -> Type -> TcS MaybeNew
newWantedEvVar CtLoc
loc RewriterSet
rewriters Type
pty
= Bool -> SDoc -> TcS MaybeNew -> TcS MaybeNew
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (Type -> Bool
isEqPred Type
pty))
([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"newWantedEvVar: HoleDestPred"
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pty:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pty ]) (TcS MaybeNew -> TcS MaybeNew) -> TcS MaybeNew -> TcS MaybeNew
forall a b. (a -> b) -> a -> b
$
do { mb_ct <- CtLoc -> Type -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc Type
pty
; case mb_ct of
Just CtEvidence
ctev
-> do { String -> SDoc -> TcS ()
traceTcS String
"newWantedEvVar/cache hit" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev
; MaybeNew -> TcS MaybeNew
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeNew -> TcS MaybeNew) -> MaybeNew -> TcS MaybeNew
forall a b. (a -> b) -> a -> b
$ EvExpr -> MaybeNew
Cached (HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev) }
Maybe CtEvidence
_ -> do { ctev <- CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
rewriters Type
pty
; return (Fresh ctev) } }
newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew
newWanted :: CtLoc -> RewriterSet -> Type -> TcS MaybeNew
newWanted CtLoc
loc RewriterSet
rewriters Type
pty
| Just (Role
role, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pty
= CtEvidence -> MaybeNew
Fresh (CtEvidence -> MaybeNew)
-> ((CtEvidence, Coercion) -> CtEvidence)
-> (CtEvidence, Coercion)
-> MaybeNew
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CtEvidence, Coercion) -> CtEvidence
forall a b. (a, b) -> a
fst ((CtEvidence, Coercion) -> MaybeNew)
-> TcS (CtEvidence, Coercion) -> TcS MaybeNew
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
| Bool
otherwise
= CtLoc -> RewriterSet -> Type -> TcS MaybeNew
newWantedEvVar CtLoc
loc RewriterSet
rewriters Type
pty
newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS CtEvidence
newWantedNC :: CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedNC CtLoc
loc RewriterSet
rewriters Type
pty
| Just (Role
role, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pty
= (CtEvidence, Coercion) -> CtEvidence
forall a b. (a, b) -> a
fst ((CtEvidence, Coercion) -> CtEvidence)
-> TcS (CtEvidence, Coercion) -> TcS CtEvidence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
| Bool
otherwise
= CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
rewriters Type
pty
checkReductionDepth :: CtLoc -> TcType
-> TcS ()
checkReductionDepth :: CtLoc -> Type -> TcS ()
checkReductionDepth CtLoc
loc Type
ty
= do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; when (subGoalDepthExceeded (reductionDepth dflags) (ctLocDepth loc)) $
wrapErrTcS $ solverDepthError loc ty }
matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN)
matchFam :: TyCon -> [Type] -> TcS (Maybe Reduction)
matchFam TyCon
tycon [Type]
args = TcM (Maybe Reduction) -> TcS (Maybe Reduction)
forall a. TcM a -> TcS a
wrapTcS (TcM (Maybe Reduction) -> TcS (Maybe Reduction))
-> TcM (Maybe Reduction) -> TcS (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> TcM (Maybe Reduction)
matchFamTcM TyCon
tycon [Type]
args
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe ReductionN)
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe Reduction)
matchFamTcM TyCon
tycon [Type]
args
= do { fam_envs <- TcM (FamInstEnv, FamInstEnv)
FamInst.tcGetFamInstEnvs
; let match_fam_result
= (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe Reduction
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
fam_envs Role
Nominal TyCon
tycon [Type]
args
; TcM.traceTc "matchFamTcM" $
vcat [ text "Matching:" <+> ppr (mkTyConApp tycon args)
, ppr_res match_fam_result ]
; return match_fam_result }
where
ppr_res :: Maybe Reduction -> SDoc
ppr_res Maybe Reduction
Nothing = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Match failed"
ppr_res (Just (Reduction Coercion
co Type
ty))
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Match succeeded:")
Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Rewrites to:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Coercion:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co ])
solverDepthError :: CtLoc -> TcType -> TcM a
solverDepthError :: forall a. CtLoc -> Type -> TcM a
solverDepthError CtLoc
loc Type
ty
= CtLoc -> TcM a -> TcM a
forall a. CtLoc -> TcM a -> TcM a
TcM.setCtLocM CtLoc
loc (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
do { (ty, env0) <- ZonkM (Type, TidyEnv) -> TcM (Type, TidyEnv)
forall a. ZonkM a -> TcM a
TcM.liftZonkM (ZonkM (Type, TidyEnv) -> TcM (Type, TidyEnv))
-> ZonkM (Type, TidyEnv) -> TcM (Type, TidyEnv)
forall a b. (a -> b) -> a -> b
$
do { ty <- Type -> ZonkM Type
TcM.zonkTcType Type
ty
; env0 <- TcM.tcInitTidyEnv
; return (ty, env0) }
; let (tidy_env, tidy_ty) = tidyOpenTypeX env0 ty
msg = Type -> SubGoalDepth -> TcRnMessage
TcRnSolverDepthError Type
tidy_ty SubGoalDepth
depth
; TcM.failWithTcM (tidy_env, msg) }
where
depth :: SubGoalDepth
depth = CtLoc -> SubGoalDepth
ctLocDepth CtLoc
loc
emitFunDepWanteds :: CtEvidence
-> [FunDepEqn (CtLoc, RewriterSet)]
-> TcS Bool
emitFunDepWanteds :: CtEvidence -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool
emitFunDepWanteds CtEvidence
_ [] = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
emitFunDepWanteds CtEvidence
ev [FunDepEqn (CtLoc, RewriterSet)]
fd_eqns
= CtEvidence -> Role -> (UnifyEnv -> TcM ()) -> TcS Bool
unifyFunDeps CtEvidence
ev Role
Nominal UnifyEnv -> TcM ()
do_fundeps
where
do_fundeps :: UnifyEnv -> TcM ()
do_fundeps :: UnifyEnv -> TcM ()
do_fundeps UnifyEnv
env = (FunDepEqn (CtLoc, RewriterSet) -> TcM ())
-> [FunDepEqn (CtLoc, RewriterSet)] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM ()
do_one UnifyEnv
env) [FunDepEqn (CtLoc, RewriterSet)]
fd_eqns
do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM ()
do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM ()
do_one UnifyEnv
uenv (FDEqn { fd_qtvs :: forall loc. FunDepEqn loc -> [TcTyVar]
fd_qtvs = [TcTyVar]
tvs, fd_eqs :: forall loc. FunDepEqn loc -> [TypeEqn]
fd_eqs = [TypeEqn]
eqs, fd_loc :: forall loc. FunDepEqn loc -> loc
fd_loc = (CtLoc
loc, RewriterSet
rewriters) })
= do { eqs' <- [TcTyVar] -> [TypeEqn] -> TcM [TypeEqn]
instantiate_eqs [TcTyVar]
tvs ([TypeEqn] -> [TypeEqn]
forall a. [a] -> [a]
reverse [TypeEqn]
eqs)
; uPairsTcM env_one eqs' }
where
env_one :: UnifyEnv
env_one = UnifyEnv
uenv { u_rewriters = u_rewriters uenv S.<> rewriters
, u_loc = loc }
instantiate_eqs :: [TyVar] -> [TypeEqn] -> TcM [TypeEqn]
instantiate_eqs :: [TcTyVar] -> [TypeEqn] -> TcM [TypeEqn]
instantiate_eqs [TcTyVar]
tvs [TypeEqn]
eqs
| [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs
= [TypeEqn] -> TcM [TypeEqn]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
eqs
| Bool
otherwise
= do { String -> SDoc -> TcM ()
TcM.traceTc String
"emitFunDepWanteds 2" ([TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TypeEqn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TypeEqn]
eqs)
; subst <- Subst -> [TcTyVar] -> TcM Subst
instFlexiXTcM Subst
emptySubst [TcTyVar]
tvs
; return [ Pair (substTyUnchecked subst' ty1) ty2
| Pair ty1 ty2 <- eqs
, let subst' = Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (Type -> VarSet
tyCoVarsOfType Type
ty1) ]
}
uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM ()
uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM ()
uPairsTcM UnifyEnv
uenv [TypeEqn]
eqns = (TypeEqn -> TcM Coercion) -> [TypeEqn] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Pair Type
ty1 Type
ty2) -> UnifyEnv -> Type -> Type -> TcM Coercion
uType UnifyEnv
uenv Type
ty1 Type
ty2) [TypeEqn]
eqns
unifyFunDeps :: CtEvidence -> Role
-> (UnifyEnv -> TcM ())
-> TcS Bool
unifyFunDeps :: CtEvidence -> Role -> (UnifyEnv -> TcM ()) -> TcS Bool
unifyFunDeps CtEvidence
ev Role
role UnifyEnv -> TcM ()
do_unifications
= do { (_, _, unified) <- CtEvidence
-> Role -> (UnifyEnv -> TcM ()) -> TcS ((), Cts, [TcTyVar])
forall a.
CtEvidence
-> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [TcTyVar])
wrapUnifierTcS CtEvidence
ev Role
role UnifyEnv -> TcM ()
do_unifications
; return (any (`elemVarSet` fvs) unified) }
where
fvs :: VarSet
fvs = Type -> VarSet
tyCoVarsOfType (CtEvidence -> Type
ctEvPred CtEvidence
ev)
unifyForAllBody :: CtEvidence -> Role -> (UnifyEnv -> TcM a)
-> TcS (a, Cts)
unifyForAllBody :: forall a. CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts)
unifyForAllBody CtEvidence
ev Role
role UnifyEnv -> TcM a
unify_body
= do { (res, cts, unified, _rewriters) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
forall a.
CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
wrapUnifierX CtEvidence
ev Role
role UnifyEnv -> TcM a
unify_body
; _ <- kickOutAfterUnification unified
; return (res, cts) }
wrapUnifierTcS :: CtEvidence -> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Bag Ct, [TcTyVar])
wrapUnifierTcS :: forall a.
CtEvidence
-> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [TcTyVar])
wrapUnifierTcS CtEvidence
ev Role
role UnifyEnv -> TcM a
do_unifications
= do { (res, cts, unified, rewriters) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
forall a.
CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
wrapUnifierX CtEvidence
ev Role
role UnifyEnv -> TcM a
do_unifications
; unless (isEmptyBag cts) $
updWorkListTcS (extendWorkListEqs rewriters cts)
; _ <- kickOutAfterUnification unified
; return (res, cts, unified) }
wrapUnifierX :: CtEvidence -> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Bag Ct, [TcTyVar], RewriterSet)
wrapUnifierX :: forall a.
CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
wrapUnifierX CtEvidence
ev Role
role UnifyEnv -> TcM a
do_unifications
= do { unif_count_ref <- TcS (IORef Int)
getUnifiedRef
; wrapTcS $
do { defer_ref <- TcM.newTcRef emptyBag
; unified_ref <- TcM.newTcRef []
; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev)
; let env = UE { u_role :: Role
u_role = Role
role
, u_rewriters :: RewriterSet
u_rewriters = RewriterSet
rewriters
, u_loc :: CtLoc
u_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
, u_defer :: TcRef Cts
u_defer = TcRef Cts
defer_ref
, u_unified :: Maybe (TcRef [TcTyVar])
u_unified = TcRef [TcTyVar] -> Maybe (TcRef [TcTyVar])
forall a. a -> Maybe a
Just TcRef [TcTyVar]
unified_ref}
; res <- do_unifications env
; cts <- TcM.readTcRef defer_ref
; unified <- TcM.readTcRef unified_ref
; unless (null unified) $
TcM.updTcRef unif_count_ref (+ (length unified))
; return (res, cts, unified, rewriters) } }
checkTouchableTyVarEq
:: CtEvidence
-> TcTyVar
-> TcType
-> TcS (PuResult () Reduction)
checkTouchableTyVarEq :: CtEvidence -> TcTyVar -> Type -> TcS (PuResult () Reduction)
checkTouchableTyVarEq CtEvidence
ev TcTyVar
lhs_tv Type
rhs
| UnifyCheckCaller -> TcTyVar -> Type -> Bool
simpleUnifyCheck UnifyCheckCaller
UC_Solver TcTyVar
lhs_tv Type
rhs
= do { String -> SDoc -> TcS ()
traceTcS String
"checkTouchableTyVarEq: simple-check wins" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs)
; PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> PuResult () Reduction
forall a. a -> PuResult () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Role -> Type -> Reduction
mkReflRedn Role
Nominal Type
rhs)) }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"checkTouchableTyVarEq {" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs)
; check_result <- TcM (PuResult Ct Reduction) -> TcS (PuResult Ct Reduction)
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM (PuResult Ct Reduction)
check_rhs Type
rhs)
; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result)
; case check_result of
PuFail CheckTyEqResult
reason -> PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqResult -> PuResult () Reduction
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
reason)
PuOK Cts
cts Reduction
redn -> do { Cts -> TcS ()
emitWork Cts
cts
; PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> PuResult () Reduction
forall a. a -> PuResult () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Reduction
redn) } }
where
(MetaInfo
lhs_tv_info, TcLevel
lhs_tv_lvl) = case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
lhs_tv of
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info, mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
lvl } -> (MetaInfo
info,TcLevel
lvl)
TcTyVarDetails
_ -> String -> SDoc -> (MetaInfo, TcLevel)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"checkTouchableTyVarEq" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv)
is_concrete_lhs_tv :: Bool
is_concrete_lhs_tv = MetaInfo -> Bool
isConcreteInfo MetaInfo
lhs_tv_info
check_rhs :: Type -> TcM (PuResult Ct Reduction)
check_rhs Type
rhs
| Just (TyFamLHS TyCon
tc [Type]
tys) <- Type -> Maybe CanEqLHS
canTyFamEqLHS_maybe Type
rhs
= if Bool
is_concrete_lhs_tv
then CheckTyEqResult -> TcM (PuResult Ct Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteConcrete)
else TyEqFlags Ct -> TyCon -> [Type] -> TcM (PuResult Ct Reduction)
forall a.
TyEqFlags a -> TyCon -> [Type] -> TcM (PuResult a Reduction)
recurseIntoTyConApp TyEqFlags Ct
arg_flags TyCon
tc [Type]
tys
| Bool
otherwise
= TyEqFlags Ct -> Type -> TcM (PuResult Ct Reduction)
forall a. TyEqFlags a -> Type -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags Ct
flags Type
rhs
flags :: TyEqFlags Ct
flags = TEF { tef_foralls :: Bool
tef_foralls = Bool
False
, tef_fam_app :: TyEqFamApp Ct
tef_fam_app = CtEvidence
-> EqRel -> (Type -> TcM (PuResult Ct Reduction)) -> TyEqFamApp Ct
forall a. CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
mkTEFA_Break CtEvidence
ev EqRel
NomEq Type -> TcM (PuResult Ct Reduction)
break_wanted
, tef_unifying :: AreUnifying
tef_unifying = MetaInfo -> TcLevel -> LevelCheck -> AreUnifying
Unifying MetaInfo
lhs_tv_info TcLevel
lhs_tv_lvl (Bool -> LevelCheck
LC_Promote Bool
False)
, tef_lhs :: CanEqLHS
tef_lhs = TcTyVar -> CanEqLHS
TyVarLHS TcTyVar
lhs_tv
, tef_occurs :: CheckTyEqProblem
tef_occurs = CheckTyEqProblem
cteInsolubleOccurs }
arg_flags :: TyEqFlags Ct
arg_flags = TyEqFlags Ct -> TyEqFlags Ct
forall a. TyEqFlags a -> TyEqFlags a
famAppArgFlags TyEqFlags Ct
flags
break_wanted :: FamAppBreaker Ct
break_wanted :: Type -> TcM (PuResult Ct Reduction)
break_wanted Type
fam_app
= do { let fam_app_kind :: Type
fam_app_kind = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
fam_app
; reason <- CheckTyEqProblem
-> TcTyVar -> TcLevel -> VarSet -> TcM CheckTyEqResult
checkPromoteFreeVars CheckTyEqProblem
cteInsolubleOccurs
TcTyVar
lhs_tv TcLevel
lhs_tv_lvl (Type -> VarSet
tyCoVarsOfType Type
fam_app_kind)
; if not (cterHasNoProblem reason)
then failCheckWith reason
else
do { new_tv_ty <-
case lhs_tv_info of
ConcreteTv ConcreteTvOrigin
conc_info ->
ConcreteTvOrigin -> TcLevel -> Type -> TcM Type
TcM.newConcreteTyVarTyAtLevel ConcreteTvOrigin
conc_info TcLevel
lhs_tv_lvl Type
fam_app_kind
MetaInfo
_ -> TcLevel -> Type -> TcM Type
TcM.newMetaTyVarTyAtLevel TcLevel
lhs_tv_lvl Type
fam_app_kind
; let pty = Type -> Type -> Type
mkNomEqPred Type
fam_app Type
new_tv_ty
; hole <- TcM.newVanillaCoercionHole pty
; let new_ev = CtWanted { ctev_pred :: Type
ctev_pred = Type
pty
, ctev_dest :: TcEvDest
ctev_dest = CoercionHole -> TcEvDest
HoleDest CoercionHole
hole
, ctev_loc :: CtLoc
ctev_loc = CtLoc
cb_loc
, ctev_rewriters :: RewriterSet
ctev_rewriters = CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev }
; return (PuOK (singleCt (mkNonCanonical new_ev))
(mkReduction (HoleCo hole) new_tv_ty)) } }
cb_loc :: CtLoc
cb_loc = CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) CtOrigin -> CtOrigin
CycleBreakerOrigin
checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
-> TcS (PuResult () Reduction)
checkTypeEq :: CtEvidence
-> EqRel -> CanEqLHS -> Type -> TcS (PuResult () Reduction)
checkTypeEq CtEvidence
ev EqRel
eq_rel CanEqLHS
lhs Type
rhs
| CtEvidence -> Bool
isGiven CtEvidence
ev
= do { String -> SDoc -> TcS ()
traceTcS String
"checkTypeEq {" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"lhs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rhs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs ])
; check_result <- TcM (PuResult (TcTyVar, Type) Reduction)
-> TcS (PuResult (TcTyVar, Type) Reduction)
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM (PuResult (TcTyVar, Type) Reduction)
check_given_rhs Type
rhs)
; traceTcS "checkTypeEq }" (ppr check_result)
; case check_result of
PuFail CheckTyEqResult
reason -> PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqResult -> PuResult () Reduction
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
reason)
PuOK Bag (TcTyVar, Type)
prs Reduction
redn -> do { new_givens <- ((TcTyVar, Type) -> TcS Ct) -> Bag (TcTyVar, Type) -> TcS Cts
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM (TcTyVar, Type) -> TcS Ct
mk_new_given Bag (TcTyVar, Type)
prs
; emitWork new_givens
; updInertSet (addCycleBreakerBindings prs)
; return (pure redn) } }
| Bool
otherwise
= do { check_result <- TcM (PuResult Ct Reduction) -> TcS (PuResult Ct Reduction)
forall a. TcM a -> TcS a
wrapTcS (TyEqFlags Ct -> Type -> TcM (PuResult Ct Reduction)
forall a. TyEqFlags a -> Type -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags Ct
wanted_flags Type
rhs)
; case check_result of
PuFail CheckTyEqResult
reason -> PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqResult -> PuResult () Reduction
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
reason)
PuOK Cts
cts Reduction
redn -> do { Cts -> TcS ()
emitWork Cts
cts
; PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> PuResult () Reduction
forall a. a -> PuResult () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Reduction
redn) } }
where
check_given_rhs :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
check_given_rhs :: Type -> TcM (PuResult (TcTyVar, Type) Reduction)
check_given_rhs Type
rhs
| Just (TyFamLHS TyCon
tc [Type]
tys) <- Type -> Maybe CanEqLHS
canTyFamEqLHS_maybe Type
rhs
= TyEqFlags (TcTyVar, Type)
-> TyCon -> [Type] -> TcM (PuResult (TcTyVar, Type) Reduction)
forall a.
TyEqFlags a -> TyCon -> [Type] -> TcM (PuResult a Reduction)
recurseIntoTyConApp TyEqFlags (TcTyVar, Type)
arg_flags TyCon
tc [Type]
tys
| Bool
otherwise
= TyEqFlags (TcTyVar, Type)
-> Type -> TcM (PuResult (TcTyVar, Type) Reduction)
forall a. TyEqFlags a -> Type -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags (TcTyVar, Type)
given_flags Type
rhs
arg_flags :: TyEqFlags (TcTyVar, Type)
arg_flags = TyEqFlags (TcTyVar, Type) -> TyEqFlags (TcTyVar, Type)
forall a. TyEqFlags a -> TyEqFlags a
famAppArgFlags TyEqFlags (TcTyVar, Type)
given_flags
given_flags :: TyEqFlags (TcTyVar,TcType)
given_flags :: TyEqFlags (TcTyVar, Type)
given_flags = TEF { tef_lhs :: CanEqLHS
tef_lhs = CanEqLHS
lhs
, tef_foralls :: Bool
tef_foralls = Bool
False
, tef_unifying :: AreUnifying
tef_unifying = AreUnifying
NotUnifying
, tef_fam_app :: TyEqFamApp (TcTyVar, Type)
tef_fam_app = CtEvidence
-> EqRel
-> (Type -> TcM (PuResult (TcTyVar, Type) Reduction))
-> TyEqFamApp (TcTyVar, Type)
forall a. CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
mkTEFA_Break CtEvidence
ev EqRel
eq_rel Type -> TcM (PuResult (TcTyVar, Type) Reduction)
break_given
, tef_occurs :: CheckTyEqProblem
tef_occurs = CheckTyEqProblem
occ_prob }
wanted_flags :: TyEqFlags Ct
wanted_flags = TEF { tef_lhs :: CanEqLHS
tef_lhs = CanEqLHS
lhs
, tef_foralls :: Bool
tef_foralls = Bool
False
, tef_unifying :: AreUnifying
tef_unifying = AreUnifying
NotUnifying
, tef_fam_app :: TyEqFamApp Ct
tef_fam_app = TyEqFamApp Ct
forall a. TyEqFamApp a
TEFA_Recurse
, tef_occurs :: CheckTyEqProblem
tef_occurs = CheckTyEqProblem
occ_prob }
occ_prob :: CheckTyEqProblem
occ_prob = case EqRel
eq_rel of
EqRel
NomEq -> CheckTyEqProblem
cteInsolubleOccurs
EqRel
ReprEq -> CheckTyEqProblem
cteSolubleOccurs
break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
break_given :: Type -> TcM (PuResult (TcTyVar, Type) Reduction)
break_given Type
fam_app
= do { new_tv <- Type -> TcM TcTyVar
TcM.newCycleBreakerTyVar (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
fam_app)
; return (PuOK (unitBag (new_tv, fam_app))
(mkReflRedn Nominal (mkTyVarTy new_tv))) }
mk_new_given :: (TcTyVar, TcType) -> TcS Ct
mk_new_given :: (TcTyVar, Type) -> TcS Ct
mk_new_given (TcTyVar
new_tv, Type
fam_app)
= CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> TcS CtEvidence -> TcS Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
cb_loc (Type
given_pred, EvTerm
given_term)
where
new_ty :: Type
new_ty = TcTyVar -> Type
mkTyVarTy TcTyVar
new_tv
given_pred :: Type
given_pred = Type -> Type -> Type
mkNomEqPred Type
fam_app Type
new_ty
given_term :: EvTerm
given_term = Coercion -> EvTerm
evCoercion (Coercion -> EvTerm) -> Coercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ Type -> Coercion
mkNomReflCo Type
new_ty
cb_loc :: CtLoc
cb_loc = CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) CtOrigin -> CtOrigin
CycleBreakerOrigin
mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
mkTEFA_Break :: forall a. CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
mkTEFA_Break CtEvidence
ev EqRel
eq_rel FamAppBreaker a
breaker
| EqRel
NomEq <- EqRel
eq_rel
, Bool -> Bool
not Bool
cycle_breaker_origin
= FamAppBreaker a -> TyEqFamApp a
forall a. FamAppBreaker a -> TyEqFamApp a
TEFA_Break FamAppBreaker a
breaker
| Bool
otherwise
= TyEqFamApp a
forall a. TyEqFamApp a
TEFA_Recurse
where
cycle_breaker_origin :: Bool
cycle_breaker_origin = case CtLoc -> CtOrigin
ctLocOrigin (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) of
CycleBreakerOrigin {} -> Bool
True
CtOrigin
_ -> Bool
False
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles InertSet
is
= ZonkM () -> TcM ()
forall a. ZonkM a -> TcM a
TcM.liftZonkM
(ZonkM () -> TcM ()) -> ZonkM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ CycleBreakerVarStack -> (TcTyVar -> Type -> ZonkM ()) -> ZonkM ()
forall (m :: * -> *).
Monad m =>
CycleBreakerVarStack -> (TcTyVar -> Type -> m ()) -> m ()
forAllCycleBreakerBindings_ (InertSet -> CycleBreakerVarStack
inert_cycle_breakers InertSet
is) HasDebugCallStack => TcTyVar -> Type -> ZonkM ()
TcTyVar -> Type -> ZonkM ()
TcM.writeMetaTyVar
{-# SPECIALISE forAllCycleBreakerBindings_ ::
CycleBreakerVarStack -> (TcTyVar -> TcType -> ZonkM ()) -> ZonkM () #-}