module GHC.Tc.Solver.Monad (
TcS, runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
failTcS, warnTcS, addErrTcS, wrapTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS,
emitImplicationTcS, emitTvImplicationTcS,
selectNextWorkItem,
getWorkList,
updWorkListTcS,
pushLevelNoWorkList,
runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive,
matchGlobalInst, TcM.ClsInstResult(..),
QCInst(..),
panicTcS, traceTcS,
traceFireTcS, bumpStepCountTcS, csTraceTcS,
wrapErrTcS, wrapWarnTcS,
resetUnificationFlag, setUnificationFlag,
MaybeNew(..), freshGoals, isFresh, getEvExpr,
newTcEvBinds, newNoTcEvBinds,
newWantedEq, emitNewWantedEq,
newWanted,
newWantedNC, newWantedEvVarNC,
newBoundEvVarId,
unifyTyVar, reportUnifications, touchabilityTest, TouchabilityTestResult(..),
setEvBind, setWantedEq,
setWantedEvTerm, setEvBindIfWanted,
newEvVar, newGivenEvVar, newGivenEvVars,
checkReductionDepth,
getSolvedDicts, setSolvedDicts,
getInstEnvs, getFamInstEnvs,
getTopEnv, getGblEnv, getLclEnv, setLclEnv,
getTcEvBindsVar, getTcLevel,
getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
tcLookupClass, tcLookupId,
updInertTcS, updInertCans, updInertDicts, updInertIrreds,
getHasGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertGivens,
getInertInsols, getInnermostGivenEqLevel,
getTcSInerts, setTcSInerts,
getUnsolvedInerts,
removeInertCts, getPendingGivenScs,
addInertCan, insertFunEq, addInertForAll,
emitWorkNC, emitWork,
lookupInertDict,
kickOutAfterUnification,
addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
getSafeOverlapFailures,
addSolvedDict, lookupSolvedDict,
foldIrreds,
lookupFamAppInert, lookupFamAppCache, extendFamAppCache,
pprKicked,
instDFunType,
newFlexiTcSTy, instFlexi, instFlexiX,
cloneMetaTyVar,
tcInstSkolTyVarsX,
TcLevel,
isFilledMetaTyVar_maybe, isFilledMetaTyVar,
zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
zonkTyCoVarsAndFVList,
zonkSimples, zonkWC,
zonkTyCoVarKind,
newTcRef, readTcRef, writeTcRef, updTcRef,
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam, matchFamTcM,
checkWellStagedDFun,
pprEq,
breakTyEqCycle_maybe, rewriterView
) 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, topIdLvl
, tcInitTidyEnv )
import GHC.Tc.Instance.Class( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
import GHC.Tc.Utils.TcType
import GHC.Driver.Session
import GHC.Core.Type
import qualified GHC.Core.TyCo.Rep as Rep
import GHC.Core.Coercion
import GHC.Core.Reduction
import GHC.Tc.Solver.Types
import GHC.Tc.Solver.InertSet
import GHC.Tc.Types.Evidence
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Tc.Errors.Types
import GHC.Types.Error ( mkPlainError, noHints )
import GHC.Types.Name
import GHC.Types.TyThing
import GHC.Unit.Module ( HasModule, getModule, extractModule )
import GHC.Types.Name.Reader ( GlobalRdrEnv, GlobalRdrElt )
import qualified GHC.Rename.Env as TcM
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
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.Types.Unique.Supply
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.Unify
import GHC.Core.Predicate
import GHC.Types.Unique.Set (nonDetEltsUniqSet)
import Control.Monad
import GHC.Utils.Monad
import Data.IORef
import GHC.Exts (oneShot)
import Data.List ( mapAccumL, partition, find )
#if defined(DEBUG)
import GHC.Data.Graph.Directed
#endif
addInertForAll :: QCInst -> TcS ()
addInertForAll new_qci
= do { ics <- getInertCans
; ics1 <- add_qci ics
; tclvl <- getTcLevel
; let pred = qci_pred new_qci
not_equality = isClassPred pred && not (isEqPred pred)
ics2 | not_equality = ics1
| otherwise = ics1 { inert_given_eq_lvl = tclvl
, inert_given_eqs = True }
; setInertCans ics2 }
where
add_qci :: InertCans -> TcS InertCans
add_qci ics@(IC { inert_insts = qcis })
| any same_qci qcis
= do { traceTcS "skipping duplicate quantified instance" (ppr new_qci)
; return ics }
| otherwise
= do { traceTcS "adding new inert quantified instance" (ppr new_qci)
; return (ics { inert_insts = new_qci : qcis }) }
same_qci old_qci = tcEqType (ctEvPred (qci_ev old_qci))
(ctEvPred (qci_ev new_qci))
addInertCan :: Ct -> TcS ()
addInertCan ct =
do { traceTcS "addInertCan {" $
text "Trying to insert new inert item:" <+> ppr ct
; mkTcS (\TcSEnv{tcs_abort_on_insoluble=abort_flag} ->
when (abort_flag && insolubleEqCt ct) TcM.failM)
; ics <- getInertCans
; ics <- maybeKickOut ics ct
; tclvl <- getTcLevel
; setInertCans (addInertItem tclvl ics ct)
; traceTcS "addInertCan }" $ empty }
maybeKickOut :: InertCans -> Ct -> TcS InertCans
maybeKickOut ics ct
| CEqCan { cc_lhs = lhs, cc_ev = ev, cc_eq_rel = eq_rel } <- ct
= do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics
; return ics' }
| isGivenCt ct
, CDictCan { cc_class = cls, cc_tyargs = [ip_name_strty, _ip_ty] } <- ct
, isIPClass cls
, Just ip_name <- isStrLitTy ip_name_strty
= let dict_map = inert_dicts ics
dict_map' = filterDicts doesn't_match_ip_name dict_map
doesn't_match_ip_name :: Ct -> Bool
doesn't_match_ip_name ct
| Just (inert_ip_name, _inert_ip_ty) <- isIPPred_maybe (ctPred ct)
= inert_ip_name /= ip_name
| otherwise
= True
in
return (ics { inert_dicts = dict_map' })
| otherwise
= return ics
kickOutRewritable :: CtFlavourRole
-> CanEqLHS
-> InertCans
-> TcS (Int, InertCans)
kickOutRewritable new_fr new_lhs ics
= do { let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics
n_kicked = workListSize kicked_out
; unless (n_kicked == 0) $
do { updWorkListTcS (appendWorkList kicked_out)
; let kicked_given_ev_vars =
[ ev_var | ct <- wl_eqs kicked_out
, CtGiven { ctev_evar = ev_var } <- [ctEvidence ct] ]
; when (new_fr `eqCanRewriteFR` (Given, NomEq) &&
not (null kicked_given_ev_vars)) $
do { traceTcS "Given(s) have been kicked out; drop from famapp-cache"
(ppr kicked_given_ev_vars)
; dropFromFamAppCache (mkVarSet kicked_given_ev_vars) }
; csTraceTcS $
hang (text "Kick out, lhs =" <+> ppr new_lhs)
2 (vcat [ text "n-kicked =" <+> int n_kicked
, text "kicked_out =" <+> ppr kicked_out
, text "Residual inerts =" <+> ppr ics' ]) }
; return (n_kicked, ics') }
kickOutAfterUnification :: TcTyVar -> TcS Int
kickOutAfterUnification new_tv
= do { ics <- getInertCans
; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq)
(TyVarLHS new_tv) ics
; setInertCans ics2
; return n_kicked }
kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
kickOutAfterFillingCoercionHole hole
= do { ics <- getInertCans
; let (kicked_out, ics') = kick_out ics
n_kicked = workListSize kicked_out
; unless (n_kicked == 0) $
do { updWorkListTcS (appendWorkList 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 -> (WorkList, InertCans)
kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs })
= (kicked_out, ics { inert_eqs = eqs_to_keep, inert_funeqs = funeqs_to_keep })
where
(eqs_to_kick, eqs_to_keep) = partitionInertEqs kick_ct eqs
(funeqs_to_kick, funeqs_to_keep) = partitionFunEqs kick_ct funeqs
kicked_out = extendWorkListCts (eqs_to_kick ++ funeqs_to_kick) emptyWorkList
kick_ct :: Ct -> Bool
kick_ct (CEqCan { cc_rhs = rhs, cc_ev = ctev })
= isWanted ctev &&
rhs `hasThisCoercionHoleTy` hole
kick_ct other = pprPanic "kick_ct (coercion hole)" (ppr other)
addInertSafehask :: InertCans -> Ct -> InertCans
addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
= ics { inert_safehask = addDict (inert_dicts ics) cls tys item }
addInertSafehask _ item
= pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
insertSafeOverlapFailureTcS what item
| safeOverlap what = return ()
| otherwise = updInertCans (\ics -> addInertSafehask ics item)
getSafeOverlapFailures :: TcS Cts
getSafeOverlapFailures
= do { IC { inert_safehask = safehask } <- getInertCans
; return $ foldDicts consCts safehask emptyCts }
addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
addSolvedDict what item cls tys
| isWanted item
, instanceReturnsDictCon what
= do { traceTcS "updSolvedSetTcs:" $ ppr item
; updInertTcS $ \ ics ->
ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
| otherwise
= return ()
getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts = do { ics <- getTcSInerts; return (inert_solved_dicts ics) }
setSolvedDicts :: DictMap CtEvidence -> TcS ()
setSolvedDicts solved_dicts
= updInertTcS $ \ ics ->
ics { inert_solved_dicts = solved_dicts }
updInertTcS :: (InertSet -> InertSet) -> TcS ()
updInertTcS upd_fn
= do { is_var <- getTcSInertsRef
; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
getInertCans :: TcS InertCans
getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
setInertCans :: InertCans -> TcS ()
setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
updRetInertCans upd_fn
= do { is_var <- getTcSInertsRef
; 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 upd_fn
= updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertDicts upd_fn
= updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertSafehask upd_fn
= updInertCans $ \ ics -> ics { inert_safehask = upd_fn (inert_safehask ics) }
updInertIrreds :: (Cts -> Cts) -> TcS ()
updInertIrreds upd_fn
= updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
getInertEqs :: TcS InertEqs
getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel = do { inert <- getInertCans
; return (inert_given_eq_lvl inert) }
getInertInsols :: TcS Cts
getInertInsols = do { inert <- getInertCans
; return $ filterBag insolubleCt (inert_irreds inert) }
getInertGivens :: TcS [Ct]
getInertGivens
= do { inerts <- getInertCans
; let all_cts = foldIrreds (:) (inert_irreds inerts)
$ foldDicts (:) (inert_dicts inerts)
$ foldFunEqs (++) (inert_funeqs inerts)
$ foldDVarEnv (++) [] (inert_eqs inerts)
; return (filter isGivenCt all_cts) }
getPendingGivenScs :: TcS [Ct]
getPendingGivenScs = do { lvl <- getTcLevel
; updRetInertCans (get_sc_pending lvl) }
get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
= assertPpr (all isGivenCt sc_pending) (ppr sc_pending)
(sc_pending, ic { inert_dicts = dicts', inert_insts = insts' })
where
sc_pending = sc_pend_insts ++ sc_pend_dicts
sc_pend_dicts = foldDicts get_pending dicts []
dicts' = foldr add dicts sc_pend_dicts
(sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
get_pending :: Ct -> [Ct] -> [Ct]
get_pending dict dicts
| Just dict' <- pendingScDict_maybe dict
, belongs_to_this_level (ctEvidence dict)
= dict' : dicts
| otherwise
= dicts
add :: Ct -> DictMap Ct -> DictMap Ct
add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
= addDict dicts cls tys ct
add ct _ = pprPanic "getPendingScDicts" (ppr ct)
get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
get_pending_inst cts qci@(QCI { qci_ev = ev })
| Just qci' <- pendingScInst_maybe qci
, belongs_to_this_level ev
= (CQuantCan qci' : cts, qci')
| otherwise
= (cts, qci)
belongs_to_this_level ev = ctLocLevel (ctEvLoc ev) == this_lvl
getUnsolvedInerts :: TcS ( Bag Implication
, Cts )
getUnsolvedInerts
= do { IC { inert_eqs = tv_eqs
, inert_funeqs = fun_eqs
, inert_irreds = irreds
, inert_dicts = idicts
} <- getInertCans
; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts
unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts
unsolved_irreds = Bag.filterBag isWantedCt irreds
unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
unsolved_others = unionManyBags [ unsolved_irreds
, unsolved_dicts ]
; implics <- getWorkListImplics
; traceTcS "getUnsolvedInerts" $
vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
, text "fun eqs =" <+> ppr unsolved_fun_eqs
, text "others =" <+> ppr unsolved_others
, text "implics =" <+> ppr implics ]
; return ( implics, unsolved_tv_eqs `unionBags`
unsolved_fun_eqs `unionBags`
unsolved_others) }
where
add_if_unsolved :: Ct -> Cts -> Cts
add_if_unsolved ct cts | isWantedCt ct = ct `consCts` cts
| otherwise = cts
add_if_unsolveds :: EqualCtList -> Cts -> Cts
add_if_unsolveds new_cts old_cts = foldr add_if_unsolved old_cts new_cts
getHasGivenEqs :: TcLevel
-> TcS ( HasGivenEqs
, Cts )
getHasGivenEqs tclvl
= do { inerts@(IC { inert_irreds = irreds
, inert_given_eqs = given_eqs
, inert_given_eq_lvl = ge_lvl })
<- getInertCans
; let given_insols = filterBag insoluble_given_equality irreds
has_ge | ge_lvl == tclvl = MaybeGivenEqs
| given_eqs = LocalGivenEqs
| otherwise = 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 ct
= insolubleEqCt ct && isGivenCt ct
removeInertCts :: [Ct] -> InertCans -> InertCans
removeInertCts cts icans = foldl' removeInertCt icans cts
removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt is ct =
case ct of
CDictCan { cc_class = cl, cc_tyargs = tys } ->
is { inert_dicts = delDict (inert_dicts is) cl tys }
CEqCan { cc_lhs = lhs, cc_rhs = rhs } -> delEq is lhs rhs
CIrredCan {} -> is { inert_irreds = filterBag (not . eqCt ct) $ inert_irreds is }
CQuantCan {} -> panic "removeInertCt: CQuantCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
eqCt :: Ct -> Ct -> Bool
eqCt c c' = ctEvId c == ctEvId c'
lookupFamAppInert :: (CtFlavourRole -> Bool)
-> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
lookupFamAppInert rewrite_pred fam_tc tys
= do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
; return (lookup_inerts inert_funeqs) }
where
lookup_inerts inert_funeqs
| Just ecl <- findFunEq inert_funeqs fam_tc tys
, Just (CEqCan { cc_ev = ctev, cc_rhs = rhs })
<- find (rewrite_pred . ctFlavourRole) ecl
= Just (mkReduction (ctEvCoercion ctev) rhs, ctEvFlavourRole ctev)
| otherwise = Nothing
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts loc pty
| ClassPred cls tys <- classifyPredType pty
= do { inerts <- getTcSInerts
; return (lookupSolvedDict inerts loc cls tys `mplus`
fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)) }
| otherwise
= return Nothing
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe Ct
lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
= case findDict dicts loc cls tys of
Just ct -> Just ct
_ -> Nothing
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
= case findDict solved loc cls tys of
Just ev -> Just ev
_ -> Nothing
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache fam_tc tys
= do { IS { inert_famapp_cache = famapp_cache } <- getTcSInerts
; case findFunEq famapp_cache fam_tc tys of
result@(Just redn) ->
do { traceTcS "famapp_cache hit" (vcat [ ppr (mkTyConApp fam_tc tys)
, ppr redn ])
; return result }
Nothing -> return Nothing }
extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
extendFamAppCache tc xi_args stuff@(Reduction _ ty)
= do { dflags <- getDynFlags
; when (gopt Opt_FamAppCache dflags) $
do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args
, ppr ty ])
; updInertTcS $ \ is@(IS { inert_famapp_cache = fc }) ->
is { inert_famapp_cache = insertFunEq fc tc xi_args stuff } } }
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache varset
= do { inerts@(IS { inert_famapp_cache = famapp_cache }) <- getTcSInerts
; let filtered = filterTcAppMap check famapp_cache
; setTcSInerts $ inerts { inert_famapp_cache = filtered } }
where
check :: Reduction -> Bool
check redn
= not (anyFreeVarsOfCo (`elemVarSet` varset) $ reductionCoercion redn)
foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
foldIrreds k irreds z = foldr k z irreds
data TcSEnv
= TcSEnv {
tcs_ev_binds :: EvBindsVar,
tcs_unified :: IORef Int,
tcs_unif_lvl :: IORef (Maybe TcLevel),
tcs_count :: IORef Int,
tcs_inerts :: IORef InertSet,
tcs_abort_on_insoluble :: Bool,
tcs_worklist :: IORef WorkList
}
newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } deriving (Functor)
mkTcS :: (TcSEnv -> TcM a) -> TcS a
mkTcS f = TcS (oneShot f)
instance Applicative TcS where
pure x = mkTcS $ \_ -> return x
(<*>) = ap
instance Monad TcS where
m >>= k = mkTcS $ \ebs -> do
unTcS m ebs >>= (\r -> unTcS (k r) ebs)
instance MonadIO TcS where
liftIO act = TcS $ \_env -> liftIO act
instance MonadFail TcS where
fail err = mkTcS $ \_ -> fail err
instance MonadUnique TcS where
getUniqueSupplyM = wrapTcS getUniqueSupplyM
instance HasModule TcS where
getModule = wrapTcS getModule
instance MonadThings TcS where
lookupThing n = wrapTcS (lookupThing n)
wrapTcS :: TcM a -> TcS a
wrapTcS action = mkTcS $ \_env -> action
wrap2TcS :: (TcM a -> TcM a) -> TcS a -> TcS a
wrap2TcS fn (TcS thing) = mkTcS $ \env -> fn (thing env)
wrapErrTcS :: TcM a -> TcS a
wrapErrTcS = wrapTcS
wrapWarnTcS :: TcM a -> TcS a
wrapWarnTcS = wrapTcS
panicTcS :: SDoc -> TcS a
failTcS :: TcRnMessage -> TcS a
warnTcS, addErrTcS :: TcRnMessage -> TcS ()
failTcS = wrapTcS . TcM.failWith
warnTcS msg = wrapTcS (TcM.addDiagnostic msg)
addErrTcS = wrapTcS . TcM.addErr
panicTcS doc = pprPanic "GHC.Tc.Solver.Canonical" doc
traceTcS :: String -> SDoc -> TcS ()
traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
runTcPluginTcS :: TcPluginM a -> TcS a
runTcPluginTcS = wrapTcS . runTcPluginM
instance HasDynFlags TcS where
getDynFlags = wrapTcS getDynFlags
getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = mkTcS $ \env ->
do { let ref = tcs_count env
; n <- TcM.readTcRef ref
; TcM.writeTcRef ref (n+1) }
csTraceTcS :: SDoc -> TcS ()
csTraceTcS doc
= wrapTcS $ csTraceTcM (return doc)
traceFireTcS :: CtEvidence -> SDoc -> TcS ()
traceFireTcS ev doc
= mkTcS $ \env -> csTraceTcM $
do { n <- TcM.readTcRef (tcs_count 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)) }
csTraceTcM :: TcM SDoc -> TcM ()
csTraceTcM mk_doc
= do { 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 }) }
runTcS :: TcS a
-> TcM (a, EvBindMap)
runTcS tcs
= do { ev_binds_var <- 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 tcs
= do { ev_binds_var <- TcM.newTcEvBinds
; runTcSWithEvBinds' True True ev_binds_var tcs }
runTcSEqualities :: TcS a -> TcM a
runTcSEqualities thing_inside
= do { ev_binds_var <- TcM.newNoTcEvBinds
; runTcSWithEvBinds ev_binds_var thing_inside }
runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
runTcSInerts inerts tcs = do
ev_binds_var <- TcM.newTcEvBinds
runTcSWithEvBinds' False False ev_binds_var $ do
setTcSInerts inerts
a <- tcs
new_inerts <- getTcSInerts
return (a, new_inerts)
runTcSWithEvBinds :: EvBindsVar
-> TcS a
-> TcM a
runTcSWithEvBinds = runTcSWithEvBinds' True False
runTcSWithEvBinds' :: Bool
-> Bool
-> EvBindsVar
-> TcS a
-> TcM a
runTcSWithEvBinds' restore_cycles abort_on_insoluble ev_binds_var tcs
= do { unified_var <- TcM.newTcRef 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 = ev_binds_var
, tcs_unified = unified_var
, tcs_unif_lvl = unif_lvl_var
, tcs_count = step_count
, tcs_inerts = inert_var
, tcs_abort_on_insoluble = abort_on_insoluble
, tcs_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 }) = isEqPrimPred (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 ref (TcS thing_inside)
= TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
nestImplicTcS :: EvBindsVar
-> TcLevel -> TcS a
-> TcS a
nestImplicTcS ref inner_tclvl (TcS thing_inside)
= TcS $ \ TcSEnv { tcs_unified = unified_var
, tcs_inerts = old_inert_var
, tcs_count = count
, tcs_unif_lvl = unif_lvl
, tcs_abort_on_insoluble = abort_on_insoluble
} ->
do { inerts <- TcM.readTcRef old_inert_var
; let nest_inert = 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 = count
, tcs_unif_lvl = unif_lvl
, tcs_ev_binds = ref
, tcs_unified = unified_var
, tcs_inerts = new_inert_var
, tcs_abort_on_insoluble = abort_on_insoluble
, tcs_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 (TcS thing_inside)
= TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
do { inerts <- TcM.readTcRef inerts_var
; new_inert_var <- TcM.newTcRef inerts
; new_wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = 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 = inert_cans inerts
new_ic = inert_cans new_inerts
nxt_ic = 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 new_tclvl skol_info skol_tvs givens wanteds
= do { let wc = emptyWC { wc_simple = wanteds }
; imp <- wrapTcS $
do { ev_binds_var <- 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 new_tclvl skol_info skol_tvs wanteds
= do { let wc = emptyWC { wc_simple = wanteds }
; imp <- wrapTcS $
do { ev_binds_var <- 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 }
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef = TcS (return . tcs_inerts)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef = TcS (return . tcs_worklist)
getTcSInerts :: TcS InertSet
getTcSInerts = getTcSInertsRef >>= readTcRef
setTcSInerts :: InertSet -> TcS ()
setTcSInerts ics = do { r <- getTcSInertsRef; writeTcRef r ics }
getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics
= do { wl_var <- 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 _ (TcS thing_inside)
= TcS (\env -> TcM.pushTcLevelM (thing_inside env))
#endif
updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS f
= do { wl_var <- getTcSWorkListRef
; updTcRef wl_var f }
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC evs
| null evs
= return ()
| otherwise
= emitWork (map mkNonCanonical evs)
emitWork :: [Ct] -> TcS ()
emitWork [] = return ()
emitWork cts
= do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
; updWorkListTcS (extendWorkListCts cts) }
emitImplication :: Implication -> TcS ()
emitImplication implic
= updWorkListTcS (extendWorkListImplic implic)
newTcRef :: a -> TcS (TcRef a)
newTcRef x = wrapTcS (TcM.newTcRef x)
readTcRef :: TcRef a -> TcS a
readTcRef ref = wrapTcS (TcM.readTcRef ref)
writeTcRef :: TcRef a -> a -> TcS ()
writeTcRef ref val = wrapTcS (TcM.writeTcRef ref val)
updTcRef :: TcRef a -> (a->a) -> TcS ()
updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
getTcEvBindsVar :: TcS EvBindsVar
getTcEvBindsVar = TcS (return . tcs_ev_binds)
getTcLevel :: TcS TcLevel
getTcLevel = wrapTcS TcM.getTcLevel
getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
getTcEvTyCoVars ev_binds_var
= wrapTcS $ TcM.getTcEvTyCoVars ev_binds_var
getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
getTcEvBindsMap ev_binds_var
= wrapTcS $ TcM.getTcEvBindsMap ev_binds_var
setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
setTcEvBindsMap ev_binds_var binds
= wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds
unifyTyVar :: TcTyVar -> TcType -> TcS ()
unifyTyVar tv ty
= assertPpr (isMetaTyVar tv) (ppr tv) $
TcS $ \ env ->
do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty)
; TcM.writeMetaTyVar tv ty
; TcM.updTcRef (tcs_unified env) (+1) }
reportUnifications :: TcS a -> TcS (Int, a)
reportUnifications (TcS thing_inside)
= TcS $ \ env ->
do { inner_unified <- TcM.newTcRef 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) }
data TouchabilityTestResult
= TouchableSameLevel
| TouchableOuterLevel [TcTyVar]
TcLevel
| Untouchable
instance Outputable TouchabilityTestResult where
ppr TouchableSameLevel = text "TouchableSameLevel"
ppr (TouchableOuterLevel tvs lvl) = text "TouchableOuterLevel" <> parens (ppr lvl <+> ppr tvs)
ppr Untouchable = text "Untouchable"
touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS TouchabilityTestResult
touchabilityTest flav tv1 rhs
| flav /= Given
, MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1
= do { can_continue_solving <- wrapTcS $ startSolvingByUnification info rhs
; if not can_continue_solving
then return Untouchable
else
do { ambient_lvl <- getTcLevel
; given_eq_lvl <- getInnermostGivenEqLevel
; if | tv_lvl `sameDepthAs` ambient_lvl
-> return TouchableSameLevel
| tv_lvl `deeperThanOrSame` given_eq_lvl
, all (does_not_escape tv_lvl) free_skols
-> return (TouchableOuterLevel free_metas tv_lvl)
| otherwise
-> return Untouchable } }
| otherwise
= return Untouchable
where
(free_metas, free_skols) = partition isPromotableMetaTyVar $
nonDetEltsUniqSet $
tyCoVarsOfType rhs
does_not_escape tv_lvl fv
| isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv
| otherwise = True
getDefaultInfo :: TcS ([Type], (Bool, Bool))
getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
getWorkList :: TcS WorkList
getWorkList = do { wl_var <- getTcSWorkListRef
; wrapTcS (TcM.readTcRef wl_var) }
selectNextWorkItem :: TcS (Maybe Ct)
selectNextWorkItem
= do { wl_var <- getTcSWorkListRef
; wl <- readTcRef wl_var
; case selectWorkItem wl of {
Nothing -> return Nothing ;
Just (ct, new_wl) ->
do {
; writeTcRef wl_var new_wl
; return (Just ct) } } }
getInstEnvs :: TcS InstEnvs
getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
getTopEnv :: TcS HscEnv
getTopEnv = wrapTcS $ TcM.getTopEnv
getGblEnv :: TcS TcGblEnv
getGblEnv = wrapTcS $ TcM.getGblEnv
getLclEnv :: TcS TcLclEnv
getLclEnv = wrapTcS $ TcM.getLclEnv
setLclEnv :: TcLclEnv -> TcS a -> TcS a
setLclEnv env = wrap2TcS (TcM.setLclEnv env)
tcLookupClass :: Name -> TcS Class
tcLookupClass c = wrapTcS $ TcM.tcLookupClass c
tcLookupId :: Name -> TcS Id
tcLookupId n = wrapTcS $ TcM.tcLookupId n
addUsedGREs :: [GlobalRdrElt] -> TcS ()
addUsedGREs gres = wrapTcS $ TcM.addUsedGREs gres
addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre
keepAlive :: Name -> TcS ()
keepAlive = wrapTcS . TcM.keepAlive
checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
checkWellStagedDFun loc what pred
= do
mbind_lvl <- checkWellStagedInstanceWhat what
case mbind_lvl of
Just bind_lvl | bind_lvl > impLevel ->
wrapTcS $ TcM.setCtLocM loc $ do
{ use_stage <- TcM.getStage
; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
_ ->
return ()
where
pp_thing = text "instance for" <+> quotes (ppr pred)
checkWellStagedInstanceWhat :: InstanceWhat -> TcS (Maybe ThLevel)
checkWellStagedInstanceWhat what
| TopLevInstance { iw_dfun_id = dfun_id } <- what
= return $ Just (TcM.topIdLvl dfun_id)
| BuiltinTypeableInstance tc <- what
= do
cur_mod <- extractModule <$> getGblEnv
return $ Just (if nameIsLocalOrFrom cur_mod (tyConName tc)
then outerLevel
else impLevel)
| otherwise = return Nothing
pprEq :: TcType -> TcType -> SDoc
pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe tv = wrapTcS (TcM.isFilledMetaTyVar_maybe tv)
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
zonkTyCoVarsAndFV tvs = wrapTcS (TcM.zonkTyCoVarsAndFV tvs)
zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
zonkTyCoVarsAndFVList tvs = wrapTcS (TcM.zonkTyCoVarsAndFVList tvs)
zonkCo :: Coercion -> TcS Coercion
zonkCo = wrapTcS . TcM.zonkCo
zonkTcType :: TcType -> TcS TcType
zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
zonkTcTypes :: [TcType] -> TcS [TcType]
zonkTcTypes tys = wrapTcS (TcM.zonkTcTypes tys)
zonkTcTyVar :: TcTyVar -> TcS TcType
zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
zonkSimples :: Cts -> TcS Cts
zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC wc = wrapTcS (TcM.zonkWC wc)
zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv)
pprKicked :: Int -> SDoc
pprKicked 0 = empty
pprKicked n = parens (int n <+> text "kicked out")
resetUnificationFlag :: TcS Bool
resetUnificationFlag
= TcS $ \env ->
do { let ref = tcs_unif_lvl env
; ambient_lvl <- 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
Nothing -> return False
Just unif_lvl | ambient_lvl `strictlyDeeperThan` unif_lvl
-> return False
| otherwise
-> do { TcM.writeTcRef ref Nothing
; return True } }
setUnificationFlag :: TcLevel -> TcS ()
setUnificationFlag lvl
= TcS $ \env ->
do { let ref = tcs_unif_lvl env
; mb_lvl <- TcM.readTcRef ref
; case mb_lvl of
Just unif_lvl | lvl `deeperThanOrSame` unif_lvl
-> return ()
_ -> TcM.writeTcRef ref (Just lvl) }
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
instDFunType dfun_id inst_tys
= wrapTcS $ TcM.instDFunType dfun_id inst_tys
newFlexiTcSTy :: Kind -> TcS TcType
newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
instFlexi :: [TKVar] -> TcS TCvSubst
instFlexi = instFlexiX emptyTCvSubst
instFlexiX :: TCvSubst -> [TKVar] -> TcS TCvSubst
instFlexiX subst tvs
= wrapTcS (foldlM instFlexiHelper subst tvs)
instFlexiHelper :: TCvSubst -> TKVar -> TcM TCvSubst
instFlexiHelper subst tv
= do { uniq <- TcM.newUnique
; details <- TcM.newMetaDetails TauTv
; let name = setNameUnique (tyVarName tv) uniq
kind = substTyUnchecked subst (tyVarKind tv)
ty' = mkTyVarTy (mkTcTyVar name kind details)
; TcM.traceTc "instFlexi" (ppr ty')
; return (extendTvSubst subst tv ty') }
matchGlobalInst :: DynFlags
-> Bool
-> Class -> [Type] -> TcS TcM.ClsInstResult
matchGlobalInst dflags short_cut cls tys
= wrapTcS (TcM.matchGlobalInst dflags short_cut cls tys)
tcInstSkolTyVarsX :: SkolemInfo -> TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX skol_info subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX skol_info subst tvs
data MaybeNew = Fresh CtEvidence | Cached EvExpr
isFresh :: MaybeNew -> Bool
isFresh (Fresh {}) = True
isFresh (Cached {}) = False
freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals mns = [ ctev | Fresh ctev <- mns ]
getEvExpr :: MaybeNew -> EvExpr
getEvExpr (Fresh ctev) = ctEvExpr ctev
getEvExpr (Cached evt) = evt
setEvBind :: EvBind -> TcS ()
setEvBind ev_bind
= do { evb <- getTcEvBindsVar
; wrapTcS $ TcM.addTcEvBind evb ev_bind }
useVars :: CoVarSet -> TcS ()
useVars co_vars
= do { ev_binds_var <- getTcEvBindsVar
; let ref = ebv_tcvs ev_binds_var
; wrapTcS $
do { tcvs <- TcM.readTcRef ref
; let tcvs' = tcvs `unionVarSet` co_vars
; TcM.writeTcRef ref tcvs' } }
setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS ()
setWantedEq (HoleDest hole) co
= do { useVars (coVarsOfCo co)
; fillCoercionHole hole co }
setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq: EvVarDest" (ppr ev)
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm (HoleDest hole) tm
| Just co <- evTermCoercion_maybe tm
= do { useVars (coVarsOfCo co)
; fillCoercionHole hole co }
| otherwise
=
do { let co_var = coHoleCoVar hole
; setEvBind (mkWantedEvBind co_var tm)
; fillCoercionHole hole (mkTcCoVarCo co_var) }
setWantedEvTerm (EvVarDest ev_id) tm
= setEvBind (mkWantedEvBind ev_id tm)
fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
fillCoercionHole hole co
= do { wrapTcS $ TcM.fillCoercionHole hole co
; kickOutAfterFillingCoercionHole hole }
setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted ev tm
= case ev of
CtWanted { ctev_dest = dest } -> setWantedEvTerm dest tm
_ -> return ()
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds = wrapTcS TcM.newTcEvBinds
newNoTcEvBinds :: TcS EvBindsVar
newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds
newEvVar :: TcPredType -> TcS EvVar
newEvVar pred = wrapTcS (TcM.newEvVar pred)
newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar loc (pred, rhs)
= do { new_ev <- newBoundEvVarId pred rhs
; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
newBoundEvVarId pred rhs
= do { new_ev <- newEvVar pred
; setEvBind (mkGivenEvBind new_ev rhs)
; return new_ev }
newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion
emitNewWantedEq loc rewriters role ty1 ty2
= do { (ev, co) <- newWantedEq loc rewriters role ty1 ty2
; updWorkListTcS (extendWorkListEq (mkNonCanonical ev))
; return co }
newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType
-> TcS (CtEvidence, Coercion)
newWantedEq loc rewriters role ty1 ty2
= do { hole <- wrapTcS $ TcM.newCoercionHole pty
; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
; return ( CtWanted { ctev_pred = pty
, ctev_dest = HoleDest hole
, ctev_loc = loc
, ctev_rewriters = rewriters }
, mkHoleCo hole ) }
where
pty = mkPrimEqPredRole role ty1 ty2
newWantedEvVarNC :: CtLoc -> RewriterSet
-> TcPredType -> TcS CtEvidence
newWantedEvVarNC loc rewriters pty
= do { new_ev <- newEvVar 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 loc rewriters pty
= assertPpr (not (isEqPrimPred pty))
(vcat [ text "newWantedEvVar: HoleDestPred"
, text "pty:" <+> ppr pty ]) $
do { mb_ct <- lookupInInerts loc pty
; case mb_ct of
Just ctev
-> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
; return $ Cached (ctEvExpr ctev) }
_ -> do { ctev <- newWantedEvVarNC loc rewriters pty
; return (Fresh ctev) } }
newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew
newWanted loc rewriters pty
| Just (role, ty1, ty2) <- getEqPredTys_maybe pty
= Fresh . fst <$> newWantedEq loc rewriters role ty1 ty2
| otherwise
= newWantedEvVar loc rewriters pty
newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS CtEvidence
newWantedNC loc rewriters pty
| Just (role, ty1, ty2) <- getEqPredTys_maybe pty
= fst <$> newWantedEq loc rewriters role ty1 ty2
| otherwise
= newWantedEvVarNC loc rewriters pty
checkReductionDepth :: CtLoc -> TcType
-> TcS ()
checkReductionDepth loc ty
= do { dflags <- getDynFlags
; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $
wrapErrTcS $ solverDepthError loc ty }
matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN)
matchFam tycon args = wrapTcS $ matchFamTcM tycon args
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe ReductionN)
matchFamTcM tycon args
= do { fam_envs <- FamInst.tcGetFamInstEnvs
; let match_fam_result
= reduceTyFamApp_maybe fam_envs Nominal tycon args
; TcM.traceTc "matchFamTcM" $
vcat [ text "Matching:" <+> ppr (mkTyConApp tycon args)
, ppr_res match_fam_result ]
; return match_fam_result }
where
ppr_res Nothing = text "Match failed"
ppr_res (Just (Reduction co ty))
= hang (text "Match succeeded:")
2 (vcat [ text "Rewrites to:" <+> ppr ty
, text "Coercion:" <+> ppr co ])
solverDepthError :: CtLoc -> TcType -> TcM a
solverDepthError loc ty
= TcM.setCtLocM loc $
do { ty <- TcM.zonkTcType ty
; env0 <- TcM.tcInitTidyEnv
; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)
tidy_ty = tidyType tidy_env ty
msg = TcRnUnknownMessage $ mkPlainError noHints $
vcat [ text "Reduction stack overflow; size =" <+> ppr depth
, hang (text "When simplifying the following type:")
2 (ppr tidy_ty)
, note ]
; TcM.failWithTcM (tidy_env, msg) }
where
depth = ctLocDepth loc
note = vcat
[ text "Use -freduction-depth=0 to disable this check"
, text "(any upper bound you could choose might fail unpredictably with"
, text " minor updates to GHC, so disabling the check is recommended if"
, text " you're sure that type checking should terminate)" ]
breakTyEqCycle_maybe :: CtEvidence
-> CheckTyEqResult
-> CanEqLHS
-> TcType
-> TcS (Maybe ReductionN)
breakTyEqCycle_maybe (ctLocOrigin . ctEvLoc -> CycleBreakerOrigin _) _ _ _
= return Nothing
breakTyEqCycle_maybe ev cte_result lhs rhs
| NomEq <- eq_rel
, cte_result `cterHasOnlyProblem` cteSolubleOccurs
= do { should_break <- final_check
; if should_break then do { redn <- go rhs
; return (Just redn) }
else return Nothing }
where
flavour = ctEvFlavour ev
eq_rel = ctEvEqRel ev
final_check = case flavour of
Given -> return True
Wanted
| TyVarLHS lhs_tv <- lhs ->
do { result <- touchabilityTest Wanted lhs_tv rhs
; return $ case result of
Untouchable -> False
_ -> True }
| otherwise -> return False
go :: TcType -> TcS ReductionN
go ty | Just ty' <- rewriterView ty = go ty'
go (Rep.TyConApp tc tys)
| isTypeFamilyTyCon tc
= do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
fun_app = mkTyConApp tc fun_args
fun_app_kind = tcTypeKind fun_app
; fun_redn <- emit_work fun_app_kind fun_app
; arg_redns <- unzipRedns <$> mapM go extra_args
; return $ mkAppRedns fun_redn arg_redns }
| otherwise
= do { arg_redns <- unzipRedns <$> mapM go tys
; return $ mkTyConAppRedn Nominal tc arg_redns }
go (Rep.AppTy ty1 ty2)
= mkAppRedn <$> go ty1 <*> go ty2
go (Rep.FunTy vis w arg res)
= mkFunRedn Nominal vis <$> go w <*> go arg <*> go res
go (Rep.CastTy ty cast_co)
= mkCastRedn1 Nominal ty cast_co <$> go ty
go ty@(Rep.TyVarTy {}) = skip ty
go ty@(Rep.LitTy {}) = skip ty
go ty@(Rep.ForAllTy {}) = skip ty
go ty@(Rep.CoercionTy {}) = skip ty
skip ty = return $ mkReflRedn Nominal ty
emit_work :: TcKind
-> TcType
-> TcS ReductionN
emit_work fun_app_kind fun_app = case flavour of
Given ->
do { new_tv <- wrapTcS (TcM.newCycleBreakerTyVar fun_app_kind)
; let new_ty = mkTyVarTy new_tv
given_pred = mkHeteroPrimEqPred fun_app_kind fun_app_kind
fun_app new_ty
given_term = evCoercion $ mkNomReflCo new_ty
; new_given <- newGivenEvVar new_loc (given_pred, given_term)
; traceTcS "breakTyEqCycle replacing type family in Given" (ppr new_given)
; emitWorkNC [new_given]
; updInertTcS $ \is ->
is { inert_cycle_breakers = insertCycleBreakerBinding new_tv fun_app
(inert_cycle_breakers is) }
; return $ mkReflRedn Nominal new_ty }
Wanted ->
do { new_tv <- wrapTcS (TcM.newFlexiTyVar fun_app_kind)
; let new_ty = mkTyVarTy new_tv
; co <- emitNewWantedEq new_loc (ctEvRewriters ev) Nominal new_ty fun_app
; return $ mkReduction (mkSymCo co) new_ty }
new_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
breakTyEqCycle_maybe _ _ _ _ = return Nothing
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles is
= forAllCycleBreakerBindings_ (inert_cycle_breakers is) TcM.writeMetaTyVar
rewriterView :: TcType -> Maybe TcType
rewriterView ty@(Rep.TyConApp tc _)
| isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc))
= tcView ty
rewriterView _other = Nothing