{-# 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,
selectNextWorkItem,
getWorkList,
updWorkListTcS,
pushLevelNoWorkList,
runTcPluginTcS, recordUsedGREs,
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, 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.Driver.Session
import GHC.Tc.Instance.Class( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
import GHC.Tc.Utils.TcType
import GHC.Tc.Solver.Types
import GHC.Tc.Solver.InertSet
import GHC.Tc.Types.Evidence
import GHC.Tc.Errors.Types
import GHC.Core.Type
import qualified GHC.Core.TyCo.Rep as Rep
import GHC.Core.Coercion
import GHC.Core.Reduction
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Types.Error ( mkPlainError, noHints )
import GHC.Types.Name
import GHC.Types.TyThing
import GHC.Types.Name.Reader
import GHC.Unit.Module ( HasModule, getModule, extractModule )
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 )
import Data.Foldable
#if defined(DEBUG)
import GHC.Data.Graph.Directed
#endif
addInertForAll :: QCInst -> TcS ()
addInertForAll :: QCInst -> TcS ()
addInertForAll QCInst
new_qci
= do { InertCans
ics <- TcS InertCans
getInertCans
; InertCans
ics1 <- InertCans -> TcS InertCans
add_qci InertCans
ics
; TcLevel
tclvl <- TcS TcLevel
getTcLevel
; let pred :: Type
pred = QCInst -> Type
qci_pred QCInst
new_qci
not_equality :: Bool
not_equality = Type -> Bool
isClassPred Type
pred Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isEqPred Type
pred)
ics2 :: InertCans
ics2 | Bool
not_equality = InertCans
ics1
| Bool
otherwise = InertCans
ics1 { inert_given_eq_lvl = tclvl
, inert_given_eqs = True }
; InertCans -> TcS ()
setInertCans InertCans
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 = (() :: Constraint) => 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))
addInertCan :: Ct -> TcS ()
addInertCan :: Ct -> TcS ()
addInertCan Ct
ct =
do { String -> SDoc -> TcS ()
traceTcS String
"addInertCan {" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Trying to insert new inert item:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct
; (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS (\TcSEnv{tcs_abort_on_insoluble :: TcSEnv -> Bool
tcs_abort_on_insoluble=Bool
abort_flag} ->
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
abort_flag Bool -> Bool -> Bool
&& Ct -> Bool
insolubleEqCt Ct
ct) TcM ()
forall env a. IOEnv env a
TcM.failM)
; InertCans
ics <- TcS InertCans
getInertCans
; InertCans
ics <- InertCans -> Ct -> TcS InertCans
maybeKickOut InertCans
ics Ct
ct
; TcLevel
tclvl <- TcS TcLevel
getTcLevel
; InertCans -> TcS ()
setInertCans (TcLevel -> InertCans -> Ct -> InertCans
addInertItem TcLevel
tclvl InertCans
ics Ct
ct)
; String -> SDoc -> TcS ()
traceTcS String
"addInertCan }" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ SDoc
forall doc. IsOutput doc => doc
empty }
maybeKickOut :: InertCans -> Ct -> TcS InertCans
maybeKickOut :: InertCans -> Ct -> TcS InertCans
maybeKickOut InertCans
ics Ct
ct
| CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel } <- Ct
ct
= do { (Int
_, InertCans
ics') <- CtFlavourRole -> CanEqLHS -> InertCans -> TcS (Int, InertCans)
kickOutRewritable (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel) CanEqLHS
lhs InertCans
ics
; InertCans -> TcS InertCans
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics' }
| Ct -> Bool
isGivenCt Ct
ct
, CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type
ip_name_strty, Type
_ip_ty] } <- Ct
ct
, Class -> Bool
isIPClass Class
cls
, Just FastString
ip_name <- Type -> Maybe FastString
isStrLitTy Type
ip_name_strty
= let dict_map :: DictMap Ct
dict_map = InertCans -> DictMap Ct
inert_dicts InertCans
ics
dict_map' :: DictMap Ct
dict_map' = (Ct -> Bool) -> DictMap Ct -> DictMap Ct
filterDicts Ct -> Bool
doesn't_match_ip_name DictMap Ct
dict_map
doesn't_match_ip_name :: Ct -> Bool
doesn't_match_ip_name :: Ct -> Bool
doesn't_match_ip_name Ct
ct
| Just (FastString
inert_ip_name, Type
_inert_ip_ty) <- Type -> Maybe (FastString, Type)
isIPPred_maybe (Ct -> Type
ctPred Ct
ct)
= FastString
inert_ip_name FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
/= FastString
ip_name
| Bool
otherwise
= Bool
True
in
InertCans -> TcS InertCans
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans
ics { inert_dicts = dict_map' })
| Bool
otherwise
= InertCans -> TcS InertCans
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics
kickOutRewritable :: CtFlavourRole
-> CanEqLHS
-> InertCans
-> TcS (Int, InertCans)
kickOutRewritable :: CtFlavourRole -> CanEqLHS -> InertCans -> TcS (Int, InertCans)
kickOutRewritable CtFlavourRole
new_fr CanEqLHS
new_lhs InertCans
ics
= do { let (WorkList
kicked_out, InertCans
ics') = CtFlavourRole -> CanEqLHS -> InertCans -> (WorkList, InertCans)
kickOutRewritableLHS CtFlavourRole
new_fr CanEqLHS
new_lhs InertCans
ics
n_kicked :: Int
n_kicked = WorkList -> Int
workListSize WorkList
kicked_out
; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n_kicked Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
do { (WorkList -> WorkList) -> TcS ()
updWorkListTcS (WorkList -> WorkList -> WorkList
appendWorkList WorkList
kicked_out)
; let kicked_given_ev_vars :: [TyVar]
kicked_given_ev_vars =
[ TyVar
ev_var | Ct
ct <- WorkList -> [Ct]
wl_eqs WorkList
kicked_out
, CtGiven { ctev_evar :: CtEvidence -> TyVar
ctev_evar = TyVar
ev_var } <- [Ct -> CtEvidence
ctEvidence Ct
ct] ]
; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CtFlavourRole
new_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` (CtFlavour
Given, EqRel
NomEq) Bool -> Bool -> Bool
&&
Bool -> Bool
not ([TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
kicked_given_ev_vars)) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcS ()
traceTcS String
"Given(s) have been kicked out; drop from famapp-cache"
([TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
kicked_given_ev_vars)
; VarSet -> TcS ()
dropFromFamAppCache ([TyVar] -> VarSet
mkVarSet [TyVar]
kicked_given_ev_vars) }
; SDoc -> TcS ()
csTraceTcS (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Kick out, lhs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
new_lhs)
Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"n-kicked =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
n_kicked
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"kicked_out =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WorkList -> SDoc
forall a. Outputable a => a -> SDoc
ppr WorkList
kicked_out
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Residual inerts =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ics' ]) }
; (Int, InertCans) -> TcS (Int, InertCans)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n_kicked, InertCans
ics') }
kickOutAfterUnification :: TcTyVar -> TcS Int
kickOutAfterUnification :: TyVar -> TcS Int
kickOutAfterUnification TyVar
new_tv
= do { InertCans
ics <- TcS InertCans
getInertCans
; (Int
n_kicked, InertCans
ics2) <- CtFlavourRole -> CanEqLHS -> InertCans -> TcS (Int, InertCans)
kickOutRewritable (CtFlavour
Given,EqRel
NomEq)
(TyVar -> CanEqLHS
TyVarLHS TyVar
new_tv) InertCans
ics
; InertCans -> TcS ()
setInertCans InertCans
ics2
; Int -> TcS Int
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n_kicked }
kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole
= do { InertCans
ics <- TcS InertCans
getInertCans
; let (WorkList
kicked_out, InertCans
ics') = InertCans -> (WorkList, InertCans)
kick_out InertCans
ics
n_kicked :: Int
n_kicked = WorkList -> Int
workListSize WorkList
kicked_out
; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n_kicked Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
do { (WorkList -> WorkList) -> TcS ()
updWorkListTcS (WorkList -> WorkList -> WorkList
appendWorkList WorkList
kicked_out)
; SDoc -> TcS ()
csTraceTcS (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Kick out, hole =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
hole)
Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"n-kicked =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
n_kicked
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"kicked_out =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WorkList -> SDoc
forall a. Outputable a => a -> SDoc
ppr WorkList
kicked_out
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Residual inerts =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ics' ]) }
; InertCans -> TcS ()
setInertCans InertCans
ics' }
where
kick_out :: InertCans -> (WorkList, InertCans)
kick_out :: InertCans -> (WorkList, InertCans)
kick_out ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs, inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
funeqs })
= (WorkList
kicked_out, InertCans
ics { inert_eqs = eqs_to_keep, inert_funeqs = funeqs_to_keep })
where
([Ct]
eqs_to_kick, InertEqs
eqs_to_keep) = (Ct -> Bool) -> InertEqs -> ([Ct], InertEqs)
partitionInertEqs Ct -> Bool
kick_ct InertEqs
eqs
([Ct]
funeqs_to_kick, FunEqMap [Ct]
funeqs_to_keep) = (Ct -> Bool) -> FunEqMap [Ct] -> ([Ct], FunEqMap [Ct])
partitionFunEqs Ct -> Bool
kick_ct FunEqMap [Ct]
funeqs
kicked_out :: WorkList
kicked_out = [Ct] -> WorkList -> WorkList
extendWorkListCts ([Ct]
eqs_to_kick [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
funeqs_to_kick) WorkList
emptyWorkList
kick_ct :: Ct -> Bool
kick_ct :: Ct -> Bool
kick_ct (CEqCan { cc_rhs :: Ct -> Type
cc_rhs = Type
rhs, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev })
= CtEvidence -> Bool
isWanted CtEvidence
ctev Bool -> Bool -> Bool
&&
Type
rhs Type -> CoercionHole -> Bool
`hasThisCoercionHoleTy` CoercionHole
hole
kick_ct Ct
other = String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"kick_ct (coercion hole)" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
other)
addInertSafehask :: InertCans -> Ct -> InertCans
addInertSafehask :: InertCans -> Ct -> InertCans
addInertSafehask InertCans
ics item :: Ct
item@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys })
= InertCans
ics { inert_safehask = addDict (inert_dicts ics) cls tys item }
addInertSafehask InertCans
_ Ct
item
= String -> SDoc -> InertCans
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"addInertSafehask: can't happen! Inserting " (SDoc -> InertCans) -> SDoc -> InertCans
forall a b. (a -> b) -> a -> b
$ Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
item
insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
insertSafeOverlapFailureTcS InstanceWhat
what Ct
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 -> Ct -> InertCans
addInertSafehask InertCans
ics Ct
item)
getSafeOverlapFailures :: TcS Cts
getSafeOverlapFailures :: TcS Cts
getSafeOverlapFailures
= do { IC { inert_safehask :: InertCans -> DictMap Ct
inert_safehask = DictMap Ct
safehask } <- TcS InertCans
getInertCans
; Cts -> TcS Cts
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cts -> TcS Cts) -> Cts -> TcS Cts
forall a b. (a -> b) -> a -> b
$ (Ct -> Cts -> Cts) -> DictMap Ct -> Cts -> Cts
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts Ct -> Cts -> Cts
consCts DictMap Ct
safehask Cts
emptyCts }
addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
addSolvedDict InstanceWhat
what CtEvidence
item Class
cls [Type]
tys
| CtEvidence -> Bool
isWanted CtEvidence
item
, InstanceWhat -> Bool
instanceReturnsDictCon InstanceWhat
what
= do { String -> SDoc -> TcS ()
traceTcS String
"updSolvedSetTcs:" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
item
; (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
InertSet
ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
| Bool
otherwise
= () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts = do { InertSet
ics <- TcS InertSet
getTcSInerts; DictMap CtEvidence -> TcS (DictMap CtEvidence)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (InertSet -> DictMap CtEvidence
inert_solved_dicts InertSet
ics) }
setSolvedDicts :: DictMap CtEvidence -> TcS ()
setSolvedDicts :: DictMap CtEvidence -> TcS ()
setSolvedDicts DictMap CtEvidence
solved_dicts
= (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
InertSet
ics { inert_solved_dicts = solved_dicts }
updInertTcS :: (InertSet -> InertSet) -> TcS ()
updInertTcS :: (InertSet -> InertSet) -> TcS ()
updInertTcS InertSet -> InertSet
upd_fn
= do { IORef InertSet
is_var <- TcS (IORef InertSet)
getTcSInertsRef
; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (do { InertSet
curr_inert <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
is_var
; IORef InertSet -> InertSet -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef InertSet
is_var (InertSet -> InertSet
upd_fn InertSet
curr_inert) }) }
getInertCans :: TcS InertCans
getInertCans :: TcS InertCans
getInertCans = do { InertSet
inerts <- TcS InertSet
getTcSInerts; InertCans -> TcS InertCans
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (InertSet -> InertCans
inert_cans InertSet
inerts) }
setInertCans :: InertCans -> TcS ()
setInertCans :: InertCans -> TcS ()
setInertCans InertCans
ics = (InertSet -> InertSet) -> TcS ()
updInertTcS ((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 { IORef InertSet
is_var <- TcS (IORef InertSet)
getTcSInertsRef
; TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (do { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
is_var
; let (a
res, InertCans
cans') = InertCans -> (a, InertCans)
upd_fn (InertSet -> InertCans
inert_cans InertSet
inerts)
; IORef InertSet -> InertSet -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef InertSet
is_var (InertSet
inerts { inert_cans = cans' })
; a -> TcM a
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res }) }
updInertCans :: (InertCans -> InertCans) -> TcS ()
updInertCans :: (InertCans -> InertCans) -> TcS ()
updInertCans InertCans -> InertCans
upd_fn
= (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans = upd_fn (inert_cans inerts) }
updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertDicts DictMap Ct -> DictMap Ct
upd_fn
= (InertCans -> InertCans) -> TcS ()
updInertCans ((InertCans -> InertCans) -> TcS ())
-> (InertCans -> InertCans) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_dicts = upd_fn (inert_dicts ics) }
updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertSafehask DictMap Ct -> DictMap Ct
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) }
updInertIrreds :: (Cts -> Cts) -> TcS ()
updInertIrreds :: (Cts -> Cts) -> TcS ()
updInertIrreds Cts -> Cts
upd_fn
= (InertCans -> InertCans) -> TcS ()
updInertCans ((InertCans -> InertCans) -> TcS ())
-> (InertCans -> InertCans) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_irreds = upd_fn (inert_irreds ics) }
getInertEqs :: TcS InertEqs
getInertEqs :: TcS InertEqs
getInertEqs = do { InertCans
inert <- TcS InertCans
getInertCans; InertEqs -> TcS InertEqs
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans -> InertEqs
inert_eqs InertCans
inert) }
getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel = do { InertCans
inert <- TcS InertCans
getInertCans
; TcLevel -> TcS TcLevel
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans -> TcLevel
inert_given_eq_lvl InertCans
inert) }
getInertInsols :: TcS Cts
getInertInsols :: TcS Cts
getInertInsols = do { InertCans
inert <- TcS InertCans
getInertCans
; Cts -> TcS Cts
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cts -> TcS Cts) -> Cts -> TcS Cts
forall a b. (a -> b) -> a -> b
$ (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
insolubleCt (InertCans -> Cts
inert_irreds InertCans
inert) }
getInertGivens :: TcS [Ct]
getInertGivens :: TcS [Ct]
getInertGivens
= do { InertCans
inerts <- TcS InertCans
getInertCans
; let all_cts :: [Ct]
all_cts = (Ct -> [Ct] -> [Ct]) -> Cts -> [Ct] -> [Ct]
forall b. (Ct -> b -> b) -> Cts -> b -> b
foldIrreds (:) (InertCans -> Cts
inert_irreds InertCans
inerts)
([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (Ct -> [Ct] -> [Ct]) -> DictMap Ct -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts (:) (InertCans -> DictMap Ct
inert_dicts InertCans
inerts)
([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ ([Ct] -> [Ct] -> [Ct]) -> FunEqMap [Ct] -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldFunEqs [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
(++) (InertCans -> FunEqMap [Ct]
inert_funeqs InertCans
inerts)
([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ ([Ct] -> [Ct] -> [Ct]) -> [Ct] -> InertEqs -> [Ct]
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
(++) [] (InertCans -> InertEqs
inert_eqs InertCans
inerts)
; [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter Ct -> Bool
isGivenCt [Ct]
all_cts) }
getPendingGivenScs :: TcS [Ct]
getPendingGivenScs :: TcS [Ct]
getPendingGivenScs = do { TcLevel
lvl <- TcS TcLevel
getTcLevel
; (InertCans -> ([Ct], InertCans)) -> TcS [Ct]
forall a. (InertCans -> (a, InertCans)) -> TcS a
updRetInertCans (TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending TcLevel
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 Ct
inert_dicts = DictMap Ct
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]
++ [Ct]
sc_pend_dicts
sc_pend_dicts :: [Ct]
sc_pend_dicts = (Ct -> [Ct] -> [Ct]) -> DictMap Ct -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts Ct -> [Ct] -> [Ct]
get_pending DictMap Ct
dicts []
dicts' :: DictMap Ct
dicts' = (Ct -> DictMap Ct -> DictMap Ct)
-> DictMap Ct -> [Ct] -> DictMap Ct
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> DictMap Ct -> DictMap Ct
add DictMap Ct
dicts [Ct]
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
get_pending :: Ct -> [Ct] -> [Ct]
get_pending :: Ct -> [Ct] -> [Ct]
get_pending Ct
dict [Ct]
dicts
| Just Ct
dict' <- Ct -> Maybe Ct
pendingScDict_maybe Ct
dict
, CtEvidence -> Bool
belongs_to_this_level (Ct -> CtEvidence
ctEvidence Ct
dict)
= Ct
dict' Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
dicts
| Bool
otherwise
= [Ct]
dicts
add :: Ct -> DictMap Ct -> DictMap Ct
add :: Ct -> DictMap Ct -> DictMap Ct
add ct :: Ct
ct@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys }) DictMap Ct
dicts
= DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
forall a. DictMap a -> Class -> [Type] -> a -> DictMap a
addDict DictMap Ct
dicts Class
cls [Type]
tys Ct
ct
add Ct
ct DictMap Ct
_ = String -> SDoc -> DictMap Ct
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getPendingScDicts" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
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
forall a. Eq a => a -> a -> Bool
== TcLevel
this_lvl
getUnsolvedInerts :: TcS ( Bag Implication
, Cts )
getUnsolvedInerts :: TcS (Bag Implication, Cts)
getUnsolvedInerts
= do { IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
tv_eqs
, inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
fun_eqs
, inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds
, inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
idicts
} <- TcS InertCans
getInertCans
; let unsolved_tv_eqs :: Cts
unsolved_tv_eqs = (Ct -> Cts -> Cts) -> InertEqs -> Cts -> Cts
forall b. (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs Ct -> Cts -> Cts
add_if_unsolved InertEqs
tv_eqs Cts
emptyCts
unsolved_fun_eqs :: Cts
unsolved_fun_eqs = ([Ct] -> Cts -> Cts) -> FunEqMap [Ct] -> Cts -> Cts
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldFunEqs [Ct] -> Cts -> Cts
add_if_unsolveds FunEqMap [Ct]
fun_eqs Cts
emptyCts
unsolved_irreds :: Cts
unsolved_irreds = (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
Bag.filterBag Ct -> Bool
isWantedCt Cts
irreds
unsolved_dicts :: Cts
unsolved_dicts = (Ct -> Cts -> Cts) -> DictMap Ct -> Cts -> Cts
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts Ct -> Cts -> Cts
add_if_unsolved DictMap Ct
idicts Cts
emptyCts
unsolved_others :: Cts
unsolved_others = [Cts] -> Cts
forall a. [Bag a] -> Bag a
unionManyBags [ Cts
unsolved_irreds
, Cts
unsolved_dicts ]
; Bag Implication
implics <- TcS (Bag Implication)
getWorkListImplics
; String -> SDoc -> TcS ()
traceTcS String
"getUnsolvedInerts" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" tv eqs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
unsolved_tv_eqs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"fun eqs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
unsolved_fun_eqs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"others =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
unsolved_others
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"implics =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag Implication
implics ]
; (Bag Implication, Cts) -> TcS (Bag Implication, Cts)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ( Bag Implication
implics, Cts
unsolved_tv_eqs Cts -> Cts -> Cts
forall a. Bag a -> Bag a -> Bag a
`unionBags`
Cts
unsolved_fun_eqs Cts -> Cts -> Cts
forall a. Bag a -> Bag a -> Bag a
`unionBags`
Cts
unsolved_others) }
where
add_if_unsolved :: Ct -> Cts -> Cts
add_if_unsolved :: Ct -> Cts -> Cts
add_if_unsolved Ct
ct Cts
cts | Ct -> Bool
isWantedCt Ct
ct = Ct
ct Ct -> Cts -> Cts
`consCts` Cts
cts
| Bool
otherwise = Cts
cts
add_if_unsolveds :: EqualCtList -> Cts -> Cts
add_if_unsolveds :: [Ct] -> Cts -> Cts
add_if_unsolveds [Ct]
new_cts Cts
old_cts = (Ct -> Cts -> Cts) -> Cts -> [Ct] -> Cts
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> Cts -> Cts
add_if_unsolved Cts
old_cts [Ct]
new_cts
getHasGivenEqs :: TcLevel
-> TcS ( HasGivenEqs
, Cts )
getHasGivenEqs :: TcLevel -> TcS (HasGivenEqs, Cts)
getHasGivenEqs TcLevel
tclvl
= do { inerts :: InertCans
inerts@(IC { inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds
, inert_given_eqs :: InertCans -> Bool
inert_given_eqs = Bool
given_eqs
, inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl })
<- TcS InertCans
getInertCans
; let given_insols :: Cts
given_insols = (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
insoluble_given_equality Cts
irreds
has_ge :: HasGivenEqs
has_ge | TcLevel
ge_lvl TcLevel -> TcLevel -> Bool
forall a. Eq a => a -> a -> Bool
== TcLevel
tclvl = HasGivenEqs
MaybeGivenEqs
| Bool
given_eqs = HasGivenEqs
LocalGivenEqs
| Bool
otherwise = HasGivenEqs
NoGivenEqs
; String -> SDoc -> TcS ()
traceTcS String
"getHasGivenEqs" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"given_eqs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
given_eqs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ge_lvl:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
ge_lvl
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ambient level:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Inerts:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
inerts
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Insols:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
given_insols]
; (HasGivenEqs, Cts) -> TcS (HasGivenEqs, Cts)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (HasGivenEqs
has_ge, Cts
given_insols) }
where
insoluble_given_equality :: Ct -> Bool
insoluble_given_equality Ct
ct
= Ct -> Bool
insolubleEqCt Ct
ct Bool -> Bool -> Bool
&& Ct -> Bool
isGivenCt Ct
ct
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 { cc_class :: Ct -> Class
cc_class = Class
cl, cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys } ->
InertCans
is { inert_dicts = delDict (inert_dicts is) cl tys }
CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs, cc_rhs :: Ct -> Type
cc_rhs = Type
rhs } -> InertCans -> CanEqLHS -> Type -> InertCans
delEq InertCans
is CanEqLHS
lhs Type
rhs
CIrredCan {} -> InertCans
is { inert_irreds = filterBag (not . eqCt ct) $ inert_irreds 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"
eqCt :: Ct -> Ct -> Bool
eqCt :: Ct -> Ct -> Bool
eqCt Ct
c Ct
c' = (() :: Constraint) => Ct -> TyVar
Ct -> TyVar
ctEvId Ct
c TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== (() :: Constraint) => Ct -> TyVar
Ct -> TyVar
ctEvId Ct
c'
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 :: InertSet -> InertCans
inert_cans = IC { inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
inert_funeqs } } <- TcS InertSet
getTcSInerts
; Maybe (Reduction, CtFlavourRole)
-> TcS (Maybe (Reduction, CtFlavourRole))
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunEqMap [Ct] -> Maybe (Reduction, CtFlavourRole)
lookup_inerts FunEqMap [Ct]
inert_funeqs) }
where
lookup_inerts :: FunEqMap [Ct] -> Maybe (Reduction, CtFlavourRole)
lookup_inerts FunEqMap [Ct]
inert_funeqs
| Just [Ct]
ecl <- FunEqMap [Ct] -> TyCon -> [Type] -> Maybe [Ct]
forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap [Ct]
inert_funeqs TyCon
fam_tc [Type]
tys
, Just (CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev, cc_rhs :: Ct -> Type
cc_rhs = Type
rhs })
<- (Ct -> Bool) -> [Ct] -> Maybe Ct
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (CtFlavourRole -> Bool
rewrite_pred (CtFlavourRole -> Bool) -> (Ct -> CtFlavourRole) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtFlavourRole
ctFlavourRole) [Ct]
ecl
= (Reduction, CtFlavourRole) -> Maybe (Reduction, CtFlavourRole)
forall a. a -> Maybe a
Just (Coercion -> Type -> Reduction
mkReduction ((() :: Constraint) => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion CtEvidence
ctev) Type
rhs, 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 { InertSet
inerts <- TcS InertSet
getTcSInerts
; let mb_solved :: Maybe CtEvidence
mb_solved = InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict InertSet
inerts CtLoc
loc Class
cls [Type]
tys
mb_inert :: Maybe CtEvidence
mb_inert = (Ct -> CtEvidence) -> Maybe Ct -> Maybe CtEvidence
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ct -> CtEvidence
ctEvidence (InertCans -> CtLoc -> Class -> [Type] -> Maybe Ct
lookupInertDict (InertSet -> InertCans
inert_cans InertSet
inerts) CtLoc
loc Class
cls [Type]
tys)
; Maybe CtEvidence -> TcS (Maybe CtEvidence)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe CtEvidence -> TcS (Maybe CtEvidence))
-> Maybe CtEvidence -> TcS (Maybe CtEvidence)
forall a b. (a -> b) -> a -> b
$ do
CtEvidence
found_ev <- Maybe CtEvidence
mb_solved Maybe CtEvidence -> Maybe CtEvidence -> Maybe CtEvidence
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe CtEvidence
mb_inert
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve (CtEvidence -> CtLoc
ctEvLoc CtEvidence
found_ev) CtLoc
loc)
CtEvidence -> Maybe CtEvidence
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return CtEvidence
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 Ct
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe Ct
lookupInertDict (IC { inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dicts }) CtLoc
loc Class
cls [Type]
tys
= case DictMap Ct -> CtLoc -> Class -> [Type] -> Maybe Ct
forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap Ct
dicts CtLoc
loc Class
cls [Type]
tys of
Just Ct
ct -> Ct -> Maybe Ct
forall a. a -> Maybe a
Just Ct
ct
Maybe Ct
_ -> Maybe Ct
forall a. Maybe a
Nothing
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict (IS { inert_solved_dicts :: InertSet -> DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved }) CtLoc
loc Class
cls [Type]
tys
= case DictMap CtEvidence -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap CtEvidence
solved CtLoc
loc Class
cls [Type]
tys of
Just CtEvidence
ev -> CtEvidence -> Maybe CtEvidence
forall a. a -> Maybe a
Just CtEvidence
ev
Maybe CtEvidence
_ -> Maybe CtEvidence
forall a. Maybe a
Nothing
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache TyCon
fam_tc [Type]
tys
= do { IS { inert_famapp_cache :: InertSet -> FunEqMap Reduction
inert_famapp_cache = FunEqMap Reduction
famapp_cache } <- TcS InertSet
getTcSInerts
; case FunEqMap Reduction -> TyCon -> [Type] -> Maybe Reduction
forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap Reduction
famapp_cache TyCon
fam_tc [Type]
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 { DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_FamAppCache DynFlags
dflags) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcS ()
traceTcS String
"extendFamAppCache" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
xi_args
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty ])
; (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ 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
= do { inerts :: InertSet
inerts@(IS { inert_famapp_cache :: InertSet -> FunEqMap Reduction
inert_famapp_cache = FunEqMap Reduction
famapp_cache }) <- TcS InertSet
getTcSInerts
; let filtered :: FunEqMap Reduction
filtered = (Reduction -> Bool) -> FunEqMap Reduction -> FunEqMap Reduction
forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap Reduction -> Bool
check FunEqMap Reduction
famapp_cache
; InertSet -> TcS ()
setTcSInerts (InertSet -> TcS ()) -> InertSet -> TcS ()
forall a b. (a -> b) -> a -> b
$ InertSet
inerts { inert_famapp_cache = filtered } }
where
check :: Reduction -> Bool
check :: Reduction -> Bool
check Reduction
redn
= Bool -> Bool
not ((TyVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo (TyVar -> VarSet -> Bool
`elemVarSet` VarSet
varset) (Coercion -> Bool) -> Coercion -> Bool
forall a b. (a -> b) -> a -> b
$ Reduction -> Coercion
reductionCoercion Reduction
redn)
foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
foldIrreds :: forall b. (Ct -> b -> b) -> Cts -> b -> b
foldIrreds Ct -> b -> b
k Cts
irreds b
z = (Ct -> b -> b) -> b -> Cts -> b
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 -> b -> b
k b
z Cts
irreds
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
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.Canonical" SDoc
doc
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
; Int
n <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
ref
; IORef Int -> Int -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef Int
ref (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
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 { Int
n <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef (TcSEnv -> IORef Int
tcs_count TcSEnv
env)
; TcLevel
tclvl <- TcM TcLevel
TcM.getTcLevel
; SDoc -> TcM SDoc
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Step" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
n
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
brackets (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"l:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<>
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"d:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SubGoalDepth -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> SubGoalDepth
ctLocDepth (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev)))
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
doc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
colon)
Int
4 (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)) }
{-# INLINE traceFireTcS #-}
csTraceTcM :: TcM SDoc -> TcM ()
csTraceTcM :: TcM SDoc -> TcM ()
csTraceTcM TcM SDoc
mk_doc
= do { Logger
logger <- IOEnv (Env TcGblEnv TcLclEnv) Logger
forall (m :: * -> *). HasLogger m => m Logger
getLogger
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Logger -> DumpFlag -> Bool
logHasDumpFlag Logger
logger DumpFlag
Opt_D_dump_cs_trace
Bool -> Bool -> Bool
|| Logger -> DumpFlag -> Bool
logHasDumpFlag Logger
logger DumpFlag
Opt_D_dump_tc_trace)
( do { SDoc
msg <- TcM SDoc
mk_doc
; Bool -> DumpFlag -> String -> DumpFormat -> SDoc -> TcM ()
TcM.dumpTcRn Bool
False
DumpFlag
Opt_D_dump_cs_trace
String
"" DumpFormat
FormatText
SDoc
msg }) }
{-# INLINE csTraceTcM #-}
runTcS :: TcS a
-> TcM (a, EvBindMap)
runTcS :: forall a. TcS a -> TcM (a, EvBindMap)
runTcS TcS a
tcs
= do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
; a
res <- EvBindsVar -> TcS a -> TcM a
forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
ev_binds_var TcS a
tcs
; EvBindMap
ev_binds <- EvBindsVar -> TcM EvBindMap
TcM.getTcEvBindsMap EvBindsVar
ev_binds_var
; (a, EvBindMap) -> TcM (a, EvBindMap)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, EvBindMap
ev_binds) }
runTcSEarlyAbort :: TcS a -> TcM a
runTcSEarlyAbort :: forall a. TcS a -> TcM a
runTcSEarlyAbort TcS a
tcs
= do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
; Bool -> Bool -> EvBindsVar -> TcS a -> TcM a
forall a. Bool -> Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
True Bool
True EvBindsVar
ev_binds_var TcS a
tcs }
runTcSEqualities :: TcS a -> TcM a
runTcSEqualities :: forall a. TcS a -> TcM a
runTcSEqualities TcS a
thing_inside
= do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
; EvBindsVar -> TcS a -> TcM a
forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
ev_binds_var TcS a
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
EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
Bool
-> Bool -> EvBindsVar -> TcS (a, InertSet) -> TcM (a, InertSet)
forall a. Bool -> Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
False Bool
False EvBindsVar
ev_binds_var (TcS (a, InertSet) -> TcM (a, InertSet))
-> TcS (a, InertSet) -> TcM (a, InertSet)
forall a b. (a -> b) -> a -> b
$ do
InertSet -> TcS ()
setTcSInerts InertSet
inerts
a
a <- TcS a
tcs
InertSet
new_inerts <- TcS InertSet
getTcSInerts
(a, InertSet) -> TcS (a, InertSet)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, InertSet
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 { IORef Int
unified_var <- Int -> TcRnIf TcGblEnv TcLclEnv (IORef Int)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
; IORef Int
step_count <- Int -> TcRnIf TcGblEnv TcLclEnv (IORef Int)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
; IORef InertSet
inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
emptyInert
; IORef WorkList
wl_var <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
; IORef (Maybe TcLevel)
unif_lvl_var <- Maybe TcLevel -> TcRnIf TcGblEnv TcLclEnv (IORef (Maybe TcLevel))
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Maybe TcLevel
forall a. Maybe a
Nothing
; let env :: TcSEnv
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 }
; a
res <- TcS a -> TcSEnv -> TcM a
forall a. TcS a -> TcSEnv -> TcM a
unTcS TcS a
tcs TcSEnv
env
; Int
count <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
step_count
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
count Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
TcM SDoc -> TcM ()
csTraceTcM (TcM SDoc -> TcM ()) -> TcM SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$ SDoc -> TcM SDoc
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Constraint solver steps =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
count)
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
restore_cycles (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { InertSet
inert_set <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
inert_var
; InertSet -> TcM ()
restoreTyVarCycles InertSet
inert_set }
#if defined(DEBUG)
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
; checkForCyclicBinds ev_binds
#endif
; a -> TcM a
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
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 :: 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 { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
old_inert_var
; let nest_inert :: InertSet
nest_inert = InertSet
inerts { inert_cycle_breakers = pushCycleBreakerVarStack
(inert_cycle_breakers inerts)
, inert_cans = (inert_cans inerts)
{ inert_given_eqs = False } }
; IORef InertSet
new_inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
nest_inert
; IORef WorkList
new_wl_var <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
; let nest_env :: TcSEnv
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 }
; a
res <- TcLevel -> TcM a -> TcM a
forall a. TcLevel -> TcM a -> TcM a
TcM.setTcLevel TcLevel
inner_tclvl (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
TcSEnv -> TcM a
thing_inside TcSEnv
nest_env
; InertSet
out_inert_set <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
new_inert_var
; InertSet -> TcM ()
restoreTyVarCycles InertSet
out_inert_set
#if defined(DEBUG)
; ev_binds <- TcM.getTcEvBindsMap ref
; checkForCyclicBinds ev_binds
#endif
; a -> TcM a
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
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 { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
inerts_var
; IORef InertSet
new_inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
inerts
; IORef WorkList
new_wl_var <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
; let nest_env :: TcSEnv
nest_env = TcSEnv
env { tcs_inerts = new_inert_var
, tcs_worklist = new_wl_var }
; a
res <- TcSEnv -> TcM a
thing_inside TcSEnv
nest_env
; InertSet
new_inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
new_inert_var
; let old_ic :: InertCans
old_ic = InertSet -> InertCans
inert_cans InertSet
inerts
new_ic :: InertCans
new_ic = InertSet -> InertCans
inert_cans InertSet
new_inerts
nxt_ic :: InertCans
nxt_ic = InertCans
old_ic { inert_safehask = inert_safehask new_ic }
; IORef InertSet -> InertSet -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef InertSet
inerts_var
(InertSet
inerts { inert_solved_dicts = inert_solved_dicts new_inerts
, inert_cans = nxt_ic })
; a -> TcM a
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res }
emitImplicationTcS :: TcLevel -> SkolemInfoAnon
-> [TcTyVar]
-> [EvVar]
-> Cts
-> TcS TcEvBinds
emitImplicationTcS :: TcLevel
-> SkolemInfoAnon -> [TyVar] -> [TyVar] -> Cts -> TcS TcEvBinds
emitImplicationTcS TcLevel
new_tclvl SkolemInfoAnon
skol_info [TyVar]
skol_tvs [TyVar]
givens Cts
wanteds
= do { let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple = wanteds }
; Implication
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 { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
; Implication
imp <- TcM Implication
TcM.newImplication
; Implication -> TcM Implication
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
imp { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_given = givens
, ic_wanted = wc
, ic_binds = ev_binds_var
, ic_info = skol_info }) }
; Implication -> TcS ()
emitImplication Implication
imp
; TcEvBinds -> TcS TcEvBinds
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvBindsVar -> TcEvBinds
TcEvBinds (Implication -> EvBindsVar
ic_binds Implication
imp)) }
emitTvImplicationTcS :: TcLevel -> SkolemInfoAnon
-> [TcTyVar]
-> Cts
-> TcS ()
emitTvImplicationTcS :: TcLevel -> SkolemInfoAnon -> [TyVar] -> Cts -> TcS ()
emitTvImplicationTcS TcLevel
new_tclvl SkolemInfoAnon
skol_info [TyVar]
skol_tvs Cts
wanteds
= do { let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple = wanteds }
; Implication
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 { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
; Implication
imp <- TcM Implication
TcM.newImplication
; Implication -> TcM Implication
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
imp { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_wanted = wc
, ic_binds = ev_binds_var
, ic_info = skol_info }) }
; Implication -> TcS ()
emitImplication Implication
imp }
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef = (TcSEnv -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet))
-> TcS (IORef InertSet)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (IORef InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet))
-> (TcSEnv -> IORef InertSet)
-> TcSEnv
-> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef InertSet
tcs_inerts)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef = (TcSEnv -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList))
-> TcS (IORef WorkList)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (IORef WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList))
-> (TcSEnv -> IORef WorkList)
-> TcSEnv
-> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef WorkList
tcs_worklist)
getTcSInerts :: TcS InertSet
getTcSInerts :: TcS InertSet
getTcSInerts = TcS (IORef InertSet)
getTcSInertsRef 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
setTcSInerts :: InertSet -> TcS ()
setTcSInerts :: InertSet -> TcS ()
setTcSInerts InertSet
ics = do { IORef InertSet
r <- TcS (IORef InertSet)
getTcSInertsRef; IORef InertSet -> InertSet -> TcS ()
forall a. TcRef a -> a -> TcS ()
writeTcRef IORef InertSet
r InertSet
ics }
getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics
= do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; WorkList
wl_curr <- IORef WorkList -> TcS WorkList
forall a. TcRef a -> TcS a
readTcRef IORef WorkList
wl_var
; Bag Implication -> TcS (Bag Implication)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (WorkList -> Bag Implication
wl_implics WorkList
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 { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; IORef WorkList -> (WorkList -> WorkList) -> TcS ()
forall a. TcRef a -> (a -> a) -> TcS ()
updTcRef IORef WorkList
wl_var WorkList -> WorkList
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
= [Ct] -> TcS ()
emitWork ((CtEvidence -> Ct) -> [CtEvidence] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
evs)
emitWork :: [Ct] -> TcS ()
emitWork :: [Ct] -> TcS ()
emitWork [] = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
emitWork [Ct]
cts
= do { String -> SDoc -> TcS ()
traceTcS String
"Emitting fresh work" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
cts))
; (WorkList -> WorkList) -> TcS ()
updWorkListTcS ([Ct] -> WorkList -> WorkList
extendWorkListCts [Ct]
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 a gbl lcl. a -> TcRnIf gbl lcl (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 a gbl lcl. TcRef a -> TcRnIf gbl lcl 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 a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
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 a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
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 :: TyVar -> Type -> TcS ()
unifyTyVar TyVar
tv Type
ty
= Bool -> SDoc -> TcS () -> TcS ()
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyVar -> Bool
isMetaTyVar TyVar
tv) (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
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" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
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)
; (() :: Constraint) => TyVar -> Type -> TcM ()
TyVar -> Type -> TcM ()
TcM.writeMetaTyVar TyVar
tv Type
ty
; IORef Int -> (Int -> Int) -> TcM ()
forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
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 { IORef Int
inner_unified <- Int -> TcRnIf TcGblEnv TcLclEnv (IORef Int)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
; a
res <- TcSEnv -> TcM a
thing_inside (TcSEnv
env { tcs_unified = inner_unified })
; Int
n_unifs <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
inner_unified
; IORef Int -> (Int -> Int) -> TcM ()
forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
TcM.updTcRef (TcSEnv -> IORef Int
tcs_unified TcSEnv
env) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n_unifs)
; (Int, a) -> TcM (Int, a)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n_unifs, a
res) }
data TouchabilityTestResult
= TouchableSameLevel
| TouchableOuterLevel [TcTyVar]
TcLevel
| Untouchable
instance Outputable TouchabilityTestResult where
ppr :: TouchabilityTestResult -> SDoc
ppr TouchabilityTestResult
TouchableSameLevel = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TouchableSameLevel"
ppr (TouchableOuterLevel [TyVar]
tvs TcLevel
lvl) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TouchableOuterLevel" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
lvl SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs)
ppr TouchabilityTestResult
Untouchable = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Untouchable"
touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS (TouchabilityTestResult, TcType)
touchabilityTest :: CtFlavour -> TyVar -> Type -> TcS (TouchabilityTestResult, Type)
touchabilityTest CtFlavour
flav TyVar
tv1 Type
rhs
| CtFlavour
flav CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
/= CtFlavour
Given
, MetaTv { mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
tv_lvl, mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info } <- TyVar -> TcTyVarDetails
tcTyVarDetails TyVar
tv1
= do { Maybe Type
continue_solving <- TcM (Maybe Type) -> TcS (Maybe Type)
forall a. TcM a -> TcS a
wrapTcS (TcM (Maybe Type) -> TcS (Maybe Type))
-> TcM (Maybe Type) -> TcS (Maybe Type)
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Type -> TcM (Maybe Type)
startSolvingByUnification MetaInfo
info Type
rhs
; case Maybe Type
continue_solving of
{ Maybe Type
Nothing -> (TouchabilityTestResult, Type)
-> TcS (TouchabilityTestResult, Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TouchabilityTestResult
Untouchable, Type
rhs)
; Just Type
rhs ->
do { let ([TyVar]
free_metas, [TyVar]
free_skols) = (TyVar -> Bool) -> [TyVar] -> ([TyVar], [TyVar])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition TyVar -> Bool
isPromotableMetaTyVar ([TyVar] -> ([TyVar], [TyVar])) -> [TyVar] -> ([TyVar], [TyVar])
forall a b. (a -> b) -> a -> b
$
VarSet -> [TyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet (VarSet -> [TyVar]) -> VarSet -> [TyVar]
forall a b. (a -> b) -> a -> b
$
Type -> VarSet
tyCoVarsOfType Type
rhs
; TcLevel
ambient_lvl <- TcS TcLevel
getTcLevel
; TcLevel
given_eq_lvl <- TcS TcLevel
getInnermostGivenEqLevel
; if | TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
ambient_lvl
-> (TouchabilityTestResult, Type)
-> TcS (TouchabilityTestResult, Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TouchabilityTestResult
TouchableSameLevel, Type
rhs)
| TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcLevel
given_eq_lvl
, (TyVar -> Bool) -> [TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcLevel -> TyVar -> Bool
does_not_escape TcLevel
tv_lvl) [TyVar]
free_skols
-> (TouchabilityTestResult, Type)
-> TcS (TouchabilityTestResult, Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVar] -> TcLevel -> TouchabilityTestResult
TouchableOuterLevel [TyVar]
free_metas TcLevel
tv_lvl, Type
rhs)
| Bool
otherwise
-> (TouchabilityTestResult, Type)
-> TcS (TouchabilityTestResult, Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TouchabilityTestResult
Untouchable, Type
rhs) } } }
| Bool
otherwise
= (TouchabilityTestResult, Type)
-> TcS (TouchabilityTestResult, Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TouchabilityTestResult
Untouchable, Type
rhs)
where
does_not_escape :: TcLevel -> TyVar -> Bool
does_not_escape TcLevel
tv_lvl TyVar
fv
| TyVar -> Bool
isTyVar TyVar
fv = TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TyVar -> TcLevel
tcTyVarLevel TyVar
fv
| Bool
otherwise = Bool
True
getDefaultInfo :: TcS ([Type], (Bool, Bool))
getDefaultInfo :: TcS ([Type], (Bool, Bool))
getDefaultInfo = TcM ([Type], (Bool, Bool)) -> TcS ([Type], (Bool, Bool))
forall a. TcM a -> TcS a
wrapTcS TcM ([Type], (Bool, Bool))
TcM.tcGetDefaultTys
getWorkList :: TcS WorkList
getWorkList :: TcS WorkList
getWorkList = do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; TcM WorkList -> TcS WorkList
forall a. TcM a -> TcS a
wrapTcS (IORef WorkList -> TcM WorkList
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef WorkList
wl_var) }
selectNextWorkItem :: TcS (Maybe Ct)
selectNextWorkItem :: TcS (Maybe Ct)
selectNextWorkItem
= do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; WorkList
wl <- IORef WorkList -> TcS WorkList
forall a. TcRef a -> TcS a
readTcRef IORef WorkList
wl_var
; case WorkList -> Maybe (Ct, WorkList)
selectWorkItem WorkList
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
setLclEnv :: TcLclEnv -> TcS a -> TcS a
setLclEnv :: forall a. TcLclEnv -> TcS a -> TcS a
setLclEnv TcLclEnv
env = (TcM a -> TcM a) -> TcS a -> TcS a
forall a. (TcM a -> TcM a) -> TcS a -> TcS a
wrap2TcS (TcLclEnv -> TcM a -> TcM a
forall lcl' gbl a lcl.
lcl' -> TcRnIf gbl lcl' a -> TcRnIf gbl lcl a
TcM.setLclEnv TcLclEnv
env)
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 TyVar
tcLookupId Name
n = TcM TyVar -> TcS TyVar
forall a. TcM a -> TcS a
wrapTcS (TcM TyVar -> TcS TyVar) -> TcM TyVar -> TcS TyVar
forall a b. (a -> b) -> a -> b
$ Name -> TcM TyVar
TcM.tcLookupId 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
$ [GlobalRdrElt] -> TcM ()
TcM.addUsedGREs [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
greMangledName) [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
Maybe Int
mbind_lvl <- InstanceWhat -> TcS (Maybe Int)
checkWellStagedInstanceWhat InstanceWhat
what
case Maybe Int
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
{ ThStage
use_stage <- TcM ThStage
TcM.getStage
; SDoc -> Int -> Int -> TcM ()
TcM.checkWellStaged SDoc
pp_thing Int
bind_lvl (ThStage -> Int
thLevel ThStage
use_stage) }
Maybe Int
_ ->
() -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
pp_thing :: SDoc
pp_thing = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"instance for" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
checkWellStagedInstanceWhat :: InstanceWhat -> TcS (Maybe ThLevel)
checkWellStagedInstanceWhat :: InstanceWhat -> TcS (Maybe Int)
checkWellStagedInstanceWhat InstanceWhat
what
| TopLevInstance { iw_dfun_id :: InstanceWhat -> TyVar
iw_dfun_id = TyVar
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 (TyVar -> Int
TcM.topIdLvl TyVar
dfun_id)
| BuiltinTypeableInstance TyCon
tc <- InstanceWhat
what
= do
Module
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
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 (if Module -> Name -> Bool
nameIsLocalOrFrom Module
cur_mod (TyCon -> Name
tyConName TyCon
tc)
then Int
outerLevel
else Int
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 :: TyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe TyVar
tv = TcM (Maybe Type) -> TcS (Maybe Type)
forall a. TcM a -> TcS a
wrapTcS (TyVar -> TcM (Maybe Type)
TcM.isFilledMetaTyVar_maybe TyVar
tv)
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar :: TyVar -> TcS Bool
isFilledMetaTyVar TyVar
tv = TcM Bool -> TcS Bool
forall a. TcM a -> TcS a
wrapTcS (TyVar -> TcM Bool
TcM.isFilledMetaTyVar TyVar
tv)
zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
zonkTyCoVarsAndFV :: VarSet -> TcS VarSet
zonkTyCoVarsAndFV VarSet
tvs = TcM VarSet -> TcS VarSet
forall a. TcM a -> TcS a
wrapTcS (VarSet -> TcM VarSet
TcM.zonkTyCoVarsAndFV VarSet
tvs)
zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
zonkTyCoVarsAndFVList :: [TyVar] -> TcS [TyVar]
zonkTyCoVarsAndFVList [TyVar]
tvs = TcM [TyVar] -> TcS [TyVar]
forall a. TcM a -> TcS a
wrapTcS ([TyVar] -> TcM [TyVar]
TcM.zonkTyCoVarsAndFVList [TyVar]
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
. Coercion -> TcM Coercion
TcM.zonkCo
zonkTcType :: TcType -> TcS TcType
zonkTcType :: Type -> TcS Type
zonkTcType Type
ty = TcM Type -> TcS Type
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM Type
TcM.zonkTcType Type
ty)
zonkTcTypes :: [TcType] -> TcS [TcType]
zonkTcTypes :: [Type] -> TcS [Type]
zonkTcTypes [Type]
tys = TcM [Type] -> TcS [Type]
forall a. TcM a -> TcS a
wrapTcS ([Type] -> TcM [Type]
TcM.zonkTcTypes [Type]
tys)
zonkTcTyVar :: TcTyVar -> TcS TcType
zonkTcTyVar :: TyVar -> TcS Type
zonkTcTyVar TyVar
tv = TcM Type -> TcS Type
forall a. TcM a -> TcS a
wrapTcS (TyVar -> TcM Type
TcM.zonkTcTyVar TyVar
tv)
zonkSimples :: Cts -> TcS Cts
zonkSimples :: Cts -> TcS Cts
zonkSimples Cts
cts = TcM Cts -> TcS Cts
forall a. TcM a -> TcS a
wrapTcS (Cts -> TcM Cts
TcM.zonkSimples Cts
cts)
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC WantedConstraints
wc = TcM WantedConstraints -> TcS WantedConstraints
forall a. TcM a -> TcS a
wrapTcS (WantedConstraints -> TcM WantedConstraints
TcM.zonkWC WantedConstraints
wc)
zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
zonkTyCoVarKind :: TyVar -> TcS TyVar
zonkTyCoVarKind TyVar
tv = TcM TyVar -> TcS TyVar
forall a. TcM a -> TcS a
wrapTcS (TyVar -> TcM TyVar
TcM.zonkTyCoVarKind TyVar
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
; TcLevel
ambient_lvl <- TcM TcLevel
TcM.getTcLevel
; Maybe TcLevel
mb_lvl <- IORef (Maybe TcLevel) -> TcRnIf TcGblEnv TcLclEnv (Maybe TcLevel)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef (Maybe TcLevel)
ref
; String -> SDoc -> TcM ()
TcM.traceTc String
"resetUnificationFlag" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ambient:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
ambient_lvl
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"unif_lvl:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Maybe TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe TcLevel
mb_lvl ]
; case Maybe TcLevel
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 a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
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
; Maybe TcLevel
mb_lvl <- IORef (Maybe TcLevel) -> TcRnIf TcGblEnv TcLclEnv (Maybe TcLevel)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef (Maybe TcLevel)
ref
; case Maybe TcLevel
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 a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef (Maybe TcLevel)
ref (TcLevel -> Maybe TcLevel
forall a. a -> Maybe a
Just TcLevel
lvl) }
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
instDFunType :: TyVar -> [Maybe Type] -> TcS ([Type], [Type])
instDFunType TyVar
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
$ TyVar -> [Maybe Type] -> TcM ([Type], [Type])
TcM.instDFunType TyVar
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 :: TyVar -> TcS TyVar
cloneMetaTyVar TyVar
tv = TcM TyVar -> TcS TyVar
forall a. TcM a -> TcS a
wrapTcS (TyVar -> TcM TyVar
TcM.cloneMetaTyVar TyVar
tv)
instFlexiX :: Subst -> [TKVar] -> TcS Subst
instFlexiX :: Subst -> [TyVar] -> TcS Subst
instFlexiX Subst
subst [TyVar]
tvs
= TcM Subst -> TcS Subst
forall a. TcM a -> TcS a
wrapTcS ((Subst -> TyVar -> TcM Subst) -> Subst -> [TyVar] -> TcM Subst
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Subst -> TyVar -> TcM Subst
instFlexiHelper Subst
subst [TyVar]
tvs)
instFlexiHelper :: Subst -> TKVar -> TcM Subst
instFlexiHelper :: Subst -> TyVar -> TcM Subst
instFlexiHelper Subst
subst TyVar
tv
= do { Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
TcM.newUnique
; TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
TcM.newMetaDetails MetaInfo
TauTv
; let name :: Name
name = Name -> Unique -> Name
setNameUnique (TyVar -> Name
tyVarName TyVar
tv) Unique
uniq
kind :: Type
kind = Subst -> Type -> Type
substTyUnchecked Subst
subst (TyVar -> Type
tyVarKind TyVar
tv)
tv' :: TyVar
tv' = Name -> Type -> TcTyVarDetails -> TyVar
mkTcTyVar Name
name Type
kind TcTyVarDetails
details
subst' :: Subst
subst' = Subst -> TyVar -> TyVar -> Subst
extendTvSubstWithClone Subst
subst TyVar
tv TyVar
tv'
; String -> SDoc -> TcM ()
TcM.traceTc String
"instFlexi" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv')
; Subst -> TcM Subst
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> TyVar -> Type -> Subst
extendTvSubst Subst
subst' TyVar
tv (TyVar -> Type
mkTyVarTy TyVar
tv')) }
matchGlobalInst :: DynFlags
-> Bool
-> Class -> [Type] -> TcS TcM.ClsInstResult
matchGlobalInst :: DynFlags -> Bool -> Class -> [Type] -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Bool
short_cut Class
cls [Type]
tys
= TcM ClsInstResult -> TcS ClsInstResult
forall a. TcM a -> TcS a
wrapTcS (DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
TcM.matchGlobalInst DynFlags
dflags Bool
short_cut Class
cls [Type]
tys)
tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TcTyVar])
tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TyVar])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
subst [TyVar]
tvs = TcM (Subst, [TyVar]) -> TcS (Subst, [TyVar])
forall a. TcM a -> TcS a
wrapTcS (TcM (Subst, [TyVar]) -> TcS (Subst, [TyVar]))
-> TcM (Subst, [TyVar]) -> TcS (Subst, [TyVar])
forall a b. (a -> b) -> a -> b
$ SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TyVar])
TcM.tcInstSkolTyVarsX SkolemInfo
skol_info Subst
subst [TyVar]
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) = (() :: Constraint) => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev
getEvExpr (Cached EvExpr
evt) = EvExpr
evt
setEvBind :: EvBind -> TcS ()
setEvBind :: EvBind -> TcS ()
setEvBind EvBind
ev_bind
= do { EvBindsVar
evb <- TcS EvBindsVar
getTcEvBindsVar
; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> EvBind -> TcM ()
TcM.addTcEvBind EvBindsVar
evb EvBind
ev_bind }
useVars :: CoVarSet -> TcS ()
useVars :: VarSet -> TcS ()
useVars VarSet
co_vars
= do { EvBindsVar
ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
; let ref :: IORef VarSet
ref = EvBindsVar -> IORef VarSet
ebv_tcvs EvBindsVar
ev_binds_var
; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$
do { VarSet
tcvs <- IORef VarSet -> TcM VarSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef VarSet
ref
; let tcvs' :: VarSet
tcvs' = VarSet
tcvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
co_vars
; IORef VarSet -> VarSet -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef VarSet
ref VarSet
tcvs' } }
setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS ()
setWantedEq :: (() :: Constraint) => 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 TyVar
ev) Coercion
_ = String -> SDoc -> TcS ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setWantedEq: EvVarDest" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
ev)
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm (HoleDest CoercionHole
hole) 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 :: TyVar
co_var = CoercionHole -> TyVar
coHoleCoVar CoercionHole
hole
; EvBind -> TcS ()
setEvBind (TyVar -> EvTerm -> EvBind
mkWantedEvBind TyVar
co_var EvTerm
tm)
; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole (TyVar -> Coercion
mkCoVarCo TyVar
co_var) }
setWantedEvTerm (EvVarDest TyVar
ev_id) EvTerm
tm
= EvBind -> TcS ()
setEvBind (TyVar -> EvTerm -> EvBind
mkWantedEvBind TyVar
ev_id 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 -> EvTerm -> TcS ()
setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev EvTerm
tm
= case CtEvidence
ev of
CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } -> TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest 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 TyVar
newEvVar Type
pred = TcM TyVar -> TcS TyVar
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TyVar
forall gbl lcl. Type -> TcRnIf gbl lcl TyVar
TcM.newEvVar Type
pred)
newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar :: CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (Type
pred, EvTerm
rhs)
= do { TyVar
new_ev <- Type -> EvTerm -> TcS TyVar
newBoundEvVarId Type
pred EvTerm
rhs
; CtEvidence -> TcS CtEvidence
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtGiven { ctev_pred :: Type
ctev_pred = Type
pred, ctev_evar :: TyVar
ctev_evar = TyVar
new_ev, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }) }
newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
newBoundEvVarId :: Type -> EvTerm -> TcS TyVar
newBoundEvVarId Type
pred EvTerm
rhs
= do { TyVar
new_ev <- Type -> TcS TyVar
newEvVar Type
pred
; EvBind -> TcS ()
setEvBind (TyVar -> EvTerm -> EvBind
mkGivenEvBind TyVar
new_ev EvTerm
rhs)
; TyVar -> TcS TyVar
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return TyVar
new_ev }
newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars :: CtLoc -> [(Type, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars CtLoc
loc [(Type, EvTerm)]
pts = ((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)]
pts
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 { (CtEvidence
ev, Coercion
co) <- CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
; (WorkList -> WorkList) -> TcS ()
updWorkListTcS (Ct -> WorkList -> WorkList
extendWorkListEq (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev))
; Coercion -> TcS Coercion
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
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 { CoercionHole
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
$ Type -> TcM CoercionHole
TcM.newCoercionHole Type
pty
; String -> SDoc -> TcS ()
traceTcS String
"Emitting new coercion hole" (CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
hole SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pty)
; (CtEvidence, Coercion) -> TcS (CtEvidence, Coercion)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ( CtWanted { ctev_pred :: Type
ctev_pred = Type
pty
, ctev_dest :: TcEvDest
ctev_dest = CoercionHole -> TcEvDest
HoleDest CoercionHole
hole
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc
, ctev_rewriters :: RewriterSet
ctev_rewriters = RewriterSet
rewriters }
, CoercionHole -> Coercion
mkHoleCo CoercionHole
hole ) }
where
pty :: Type
pty = Role -> Type -> Type -> Type
mkPrimEqPredRole 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
= do { TyVar
new_ev <- Type -> TcS TyVar
newEvVar Type
pty
; String -> SDoc -> TcS ()
traceTcS String
"Emitting new wanted" (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
new_ev SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
CtLoc -> SDoc
pprCtLoc CtLoc
loc)
; CtEvidence -> TcS CtEvidence
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtWanted { ctev_pred :: Type
ctev_pred = Type
pty
, ctev_dest :: TcEvDest
ctev_dest = TyVar -> TcEvDest
EvVarDest TyVar
new_ev
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc
, ctev_rewriters :: RewriterSet
ctev_rewriters = RewriterSet
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
isEqPrimPred 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 { Maybe CtEvidence
mb_ct <- CtLoc -> Type -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc Type
pty
; case Maybe CtEvidence
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 ((() :: Constraint) => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev) }
Maybe CtEvidence
_ -> do { CtEvidence
ctev <- CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
rewriters Type
pty
; MaybeNew -> TcS MaybeNew
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> MaybeNew
Fresh CtEvidence
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 { DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DynFlags -> SubGoalDepth -> Bool
subGoalDepthExceeded DynFlags
dflags (CtLoc -> SubGoalDepth
ctLocDepth CtLoc
loc)) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapErrTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> Type -> TcM ()
forall a. CtLoc -> Type -> TcM a
solverDepthError CtLoc
loc Type
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 { (FamInstEnv, FamInstEnv)
fam_envs <- TcM (FamInstEnv, FamInstEnv)
FamInst.tcGetFamInstEnvs
; let match_fam_result :: Maybe Reduction
match_fam_result
= (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe Reduction
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
fam_envs Role
Nominal TyCon
tycon [Type]
args
; String -> SDoc -> TcM ()
TcM.traceTc String
"matchFamTcM" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Matching:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
tycon [Type]
args)
, Maybe Reduction -> SDoc
ppr_res Maybe Reduction
match_fam_result ]
; Maybe Reduction -> TcM (Maybe Reduction)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
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 { Type
ty <- Type -> TcM Type
TcM.zonkTcType Type
ty
; TidyEnv
env0 <- TcM TidyEnv
TcM.tcInitTidyEnv
; let tidy_env :: TidyEnv
tidy_env = TidyEnv -> [TyVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env0 (Type -> [TyVar]
tyCoVarsOfTypeList Type
ty)
tidy_ty :: Type
tidy_ty = TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env Type
ty
msg :: TcRnMessage
msg = DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [GhcHint]
noHints (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Reduction stack overflow; size =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SubGoalDepth -> SDoc
forall a. Outputable a => a -> SDoc
ppr SubGoalDepth
depth
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"When simplifying the following type:")
Int
2 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
tidy_ty)
, SDoc
note ]
; (TidyEnv, TcRnMessage) -> TcM a
forall a. (TidyEnv, TcRnMessage) -> TcM a
TcM.failWithTcM (TidyEnv
tidy_env, TcRnMessage
msg) }
where
depth :: SubGoalDepth
depth = CtLoc -> SubGoalDepth
ctLocDepth CtLoc
loc
note :: SDoc
note = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat
[ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Use -freduction-depth=0 to disable this check"
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(any upper bound you could choose might fail unpredictably with"
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" minor updates to GHC, so disabling the check is recommended if"
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" you're sure that type checking should terminate)" ]
breakTyEqCycle_maybe :: CtEvidence
-> CheckTyEqResult
-> CanEqLHS
-> TcType
-> TcS (Maybe ReductionN)
breakTyEqCycle_maybe :: CtEvidence
-> CheckTyEqResult -> CanEqLHS -> Type -> TcS (Maybe Reduction)
breakTyEqCycle_maybe (CtLoc -> CtOrigin
ctLocOrigin (CtLoc -> CtOrigin)
-> (CtEvidence -> CtLoc) -> CtEvidence -> CtOrigin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> CtLoc
ctEvLoc -> CycleBreakerOrigin CtOrigin
_) CheckTyEqResult
_ CanEqLHS
_ Type
_
= 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
breakTyEqCycle_maybe CtEvidence
ev CheckTyEqResult
cte_result CanEqLHS
lhs Type
rhs
| EqRel
NomEq <- EqRel
eq_rel
, CheckTyEqResult
cte_result CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasOnlyProblem` CheckTyEqProblem
cteSolubleOccurs
= do { Maybe Type
should_break <- TcS (Maybe Type)
final_check
; (Type -> TcS Reduction) -> Maybe Type -> TcS (Maybe Reduction)
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) -> Maybe a -> m (Maybe b)
mapM Type -> TcS Reduction
go Maybe Type
should_break }
where
flavour :: CtFlavour
flavour = CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev
eq_rel :: EqRel
eq_rel = CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev
final_check :: TcS (Maybe Type)
final_check = case CtFlavour
flavour of
CtFlavour
Given -> Maybe Type -> TcS (Maybe Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> TcS (Maybe Type)) -> Maybe Type -> TcS (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
rhs
CtFlavour
Wanted
| TyVarLHS TyVar
lhs_tv <- CanEqLHS
lhs ->
do { (TouchabilityTestResult
result, Type
rhs) <- CtFlavour -> TyVar -> Type -> TcS (TouchabilityTestResult, Type)
touchabilityTest CtFlavour
Wanted TyVar
lhs_tv Type
rhs
; Maybe Type -> TcS (Maybe Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> TcS (Maybe Type)) -> Maybe Type -> TcS (Maybe Type)
forall a b. (a -> b) -> a -> b
$ case TouchabilityTestResult
result of
TouchabilityTestResult
Untouchable -> Maybe Type
forall a. Maybe a
Nothing
TouchabilityTestResult
_ -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
rhs }
| Bool
otherwise -> Maybe Type -> TcS (Maybe Type)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
go :: TcType -> TcS ReductionN
go :: Type -> TcS Reduction
go Type
ty | Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty = Type -> TcS Reduction
go Type
ty'
go (Rep.TyConApp TyCon
tc [Type]
tys)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
= do { let ([Type]
fun_args, [Type]
extra_args) = Int -> [Type] -> ([Type], [Type])
forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) [Type]
tys
fun_app :: Type
fun_app = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
fun_args
fun_app_kind :: Type
fun_app_kind = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
fun_app
; Reduction
fun_redn <- Type -> Type -> TcS Reduction
emit_work Type
fun_app_kind Type
fun_app
; Reductions
arg_redns <- [Reduction] -> Reductions
unzipRedns ([Reduction] -> Reductions) -> TcS [Reduction] -> TcS Reductions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> TcS Reduction) -> [Type] -> TcS [Reduction]
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 Type -> TcS Reduction
go [Type]
extra_args
; Reduction -> TcS Reduction
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> TcS Reduction) -> Reduction -> TcS Reduction
forall a b. (a -> b) -> a -> b
$ Reduction -> Reductions -> Reduction
mkAppRedns Reduction
fun_redn Reductions
arg_redns }
| Bool
otherwise
= do { Reductions
arg_redns <- [Reduction] -> Reductions
unzipRedns ([Reduction] -> Reductions) -> TcS [Reduction] -> TcS Reductions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> TcS Reduction) -> [Type] -> TcS [Reduction]
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 Type -> TcS Reduction
go [Type]
tys
; Reduction -> TcS Reduction
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> TcS Reduction) -> Reduction -> TcS Reduction
forall a b. (a -> b) -> a -> b
$ Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
Nominal TyCon
tc Reductions
arg_redns }
go (Rep.AppTy Type
ty1 Type
ty2)
= Reduction -> Reduction -> Reduction
mkAppRedn (Reduction -> Reduction -> Reduction)
-> TcS Reduction -> TcS (Reduction -> Reduction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TcS Reduction
go Type
ty1 TcS (Reduction -> Reduction) -> TcS Reduction -> TcS Reduction
forall a b. TcS (a -> b) -> TcS a -> TcS b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> TcS Reduction
go Type
ty2
go (Rep.FunTy FunTyFlag
vis Type
w Type
arg Type
res)
= Role
-> FunTyFlag -> Reduction -> Reduction -> Reduction -> Reduction
mkFunRedn Role
Nominal FunTyFlag
vis (Reduction -> Reduction -> Reduction -> Reduction)
-> TcS Reduction -> TcS (Reduction -> Reduction -> Reduction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TcS Reduction
go Type
w TcS (Reduction -> Reduction -> Reduction)
-> TcS Reduction -> TcS (Reduction -> Reduction)
forall a b. TcS (a -> b) -> TcS a -> TcS b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> TcS Reduction
go Type
arg TcS (Reduction -> Reduction) -> TcS Reduction -> TcS Reduction
forall a b. TcS (a -> b) -> TcS a -> TcS b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> TcS Reduction
go Type
res
go (Rep.CastTy Type
ty Coercion
cast_co)
= Role -> Type -> Coercion -> Reduction -> Reduction
mkCastRedn1 Role
Nominal Type
ty Coercion
cast_co (Reduction -> Reduction) -> TcS Reduction -> TcS Reduction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TcS Reduction
go Type
ty
go ty :: Type
ty@(Rep.TyVarTy {}) = Type -> TcS Reduction
forall {m :: * -> *}. Monad m => Type -> m Reduction
skip Type
ty
go ty :: Type
ty@(Rep.LitTy {}) = Type -> TcS Reduction
forall {m :: * -> *}. Monad m => Type -> m Reduction
skip Type
ty
go ty :: Type
ty@(Rep.ForAllTy {}) = Type -> TcS Reduction
forall {m :: * -> *}. Monad m => Type -> m Reduction
skip Type
ty
go ty :: Type
ty@(Rep.CoercionTy {}) = Type -> TcS Reduction
forall {m :: * -> *}. Monad m => Type -> m Reduction
skip Type
ty
skip :: Type -> m Reduction
skip Type
ty = Reduction -> m Reduction
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> m Reduction) -> Reduction -> m Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
Nominal Type
ty
emit_work :: TcKind
-> TcType
-> TcS ReductionN
emit_work :: Type -> Type -> TcS Reduction
emit_work Type
fun_app_kind Type
fun_app = case CtFlavour
flavour of
CtFlavour
Given ->
do { TyVar
new_tv <- TcM TyVar -> TcS TyVar
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TyVar
TcM.newCycleBreakerTyVar Type
fun_app_kind)
; let new_ty :: Type
new_ty = TyVar -> Type
mkTyVarTy TyVar
new_tv
given_pred :: Type
given_pred = Type -> Type -> Type -> Type -> Type
mkHeteroPrimEqPred Type
fun_app_kind Type
fun_app_kind
Type
fun_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
; CtEvidence
new_given <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
new_loc (Type
given_pred, EvTerm
given_term)
; String -> SDoc -> TcS ()
traceTcS String
"breakTyEqCycle replacing type family in Given" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
new_given)
; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence
new_given]
; (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \InertSet
is ->
InertSet
is { inert_cycle_breakers = insertCycleBreakerBinding new_tv fun_app
(inert_cycle_breakers is) }
; Reduction -> TcS Reduction
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> TcS Reduction) -> Reduction -> TcS Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
Nominal Type
new_ty }
CtFlavour
Wanted ->
do { TyVar
new_tv <- TcM TyVar -> TcS TyVar
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TyVar
TcM.newFlexiTyVar Type
fun_app_kind)
; let new_ty :: Type
new_ty = TyVar -> Type
mkTyVarTy TyVar
new_tv
; Coercion
co <- CtLoc -> RewriterSet -> Role -> Type -> Type -> TcS Coercion
emitNewWantedEq CtLoc
new_loc (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev) Role
Nominal Type
new_ty Type
fun_app
; Reduction -> TcS Reduction
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> TcS Reduction) -> Reduction -> TcS Reduction
forall a b. (a -> b) -> a -> b
$ Coercion -> Type -> Reduction
mkReduction (Coercion -> Coercion
mkSymCo Coercion
co) Type
new_ty }
new_loc :: CtLoc
new_loc = CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) CtOrigin -> CtOrigin
CycleBreakerOrigin
breakTyEqCycle_maybe CtEvidence
_ CheckTyEqResult
_ CanEqLHS
_ Type
_ = 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
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles InertSet
is
= CycleBreakerVarStack -> (TyVar -> Type -> TcM ()) -> TcM ()
forall (m :: * -> *).
Monad m =>
CycleBreakerVarStack -> (TyVar -> Type -> m ()) -> m ()
forAllCycleBreakerBindings_ (InertSet -> CycleBreakerVarStack
inert_cycle_breakers InertSet
is) (() :: Constraint) => TyVar -> Type -> TcM ()
TyVar -> Type -> TcM ()
TcM.writeMetaTyVar
{-# SPECIALISE forAllCycleBreakerBindings_ ::
CycleBreakerVarStack -> (TcTyVar -> TcType -> TcM ()) -> TcM () #-}
rewriterView :: TcType -> Maybe TcType
rewriterView :: Type -> Maybe Type
rewriterView ty :: Type
ty@(Rep.TyConApp TyCon
tc [Type]
_)
| TyCon -> Bool
isForgetfulSynTyCon TyCon
tc Bool -> Bool -> Bool
|| (TyCon -> Bool
isTypeSynonymTyCon TyCon
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isFamFreeTyCon TyCon
tc))
= Type -> Maybe Type
coreView Type
ty
rewriterView Type
_other = Maybe Type
forall a. Maybe a
Nothing