{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies, ScopedTypeVariables, TypeApplications,
DerivingStrategies, GeneralizedNewtypeDeriving, ScopedTypeVariables, MultiWayIf, ViewPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Solver.Monad (
WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListEq,
appendWorkList,
selectNextWorkItem,
workListSize,
getWorkList, updWorkListTcS, pushLevelNoWorkList,
TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, runTcSInerts,
failTcS, warnTcS, addErrTcS, wrapTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS,
emitImplicationTcS, emitTvImplicationTcS,
runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive,
matchGlobalInst, TcM.ClsInstResult(..),
QCInst(..),
panicTcS, traceTcS,
traceFireTcS, bumpStepCountTcS, csTraceTcS,
wrapErrTcS, wrapWarnTcS,
resetUnificationFlag, setUnificationFlag,
MaybeNew(..), freshGoals, isFresh, getEvExpr,
newTcEvBinds, newNoTcEvBinds,
newWantedEq, newWantedEq_SI, emitNewWantedEq,
newWanted, newWanted_SI, newWantedEvVar,
newWantedNC, newWantedEvVarNC,
newDerivedNC,
newBoundEvVarId,
unifyTyVar, reportUnifications, touchabilityTest, TouchabilityTestResult(..),
setEvBind, setWantedEq,
setWantedEvTerm, setEvBindIfWanted,
newEvVar, newGivenEvVar, newGivenEvVars,
emitNewDeriveds, emitNewDerivedEq,
checkReductionDepth,
getSolvedDicts, setSolvedDicts,
getInstEnvs, getFamInstEnvs,
getTopEnv, getGblEnv, getLclEnv,
getTcEvBindsVar, getTcLevel,
getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
tcLookupClass, tcLookupId,
InertSet(..), InertCans(..), emptyInert,
updInertTcS, updInertCans, updInertDicts, updInertIrreds,
getHasGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertGivens,
getInertInsols, getInnermostGivenEqLevel,
getTcSInerts, setTcSInerts,
matchableGivens, prohibitedSuperClassSolve, mightEqualLater,
getUnsolvedInerts,
removeInertCts, getPendingGivenScs,
addInertCan, insertFunEq, addInertForAll,
emitWorkNC, emitWork,
isImprovable,
kickOutAfterUnification,
addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
getSafeOverlapFailures,
DictMap, emptyDictMap, lookupInertDict, findDictsByClass, addDict,
addDictsByClass, delDict, foldDicts, filterDicts, findDict,
EqualCtList(..), findTyEqs, foldTyEqs,
findEq,
addSolvedDict, lookupSolvedDict,
foldIrreds,
lookupFamAppInert, lookupFamAppCache, extendFamAppCache,
pprKicked,
findFunEq, findFunEqsByTyCon,
instDFunType,
newFlexiTcSTy, instFlexi, instFlexiX,
cloneMetaTyVar,
tcInstSkolTyVarsX,
TcLevel,
isFilledMetaTyVar_maybe, isFilledMetaTyVar,
zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
zonkTyCoVarsAndFVList,
zonkSimples, zonkWC,
zonkTyCoVarKind,
newTcRef, readTcRef, writeTcRef, updTcRef,
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam, matchFamTcM,
checkWellStagedDFun,
pprEq,
breakTyEqCycle_maybe, rewriterView
) where
#include "HsVersions.h"
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 )
import GHC.Tc.Instance.Class( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Unify ( canSolveByUnification )
import GHC.Driver.Session
import GHC.Core.Type
import qualified GHC.Core.TyCo.Rep as Rep
import GHC.Core.Coercion
import GHC.Core.Unify
import GHC.Tc.Types.Evidence
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Tc.Errors ( solverDepthErrorTcS )
import GHC.Types.Name
import GHC.Types.TyThing
import GHC.Unit.Module ( HasModule, getModule )
import GHC.Types.Name.Reader ( GlobalRdrEnv, GlobalRdrElt )
import qualified GHC.Rename.Env as TcM
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Logger
import GHC.Data.Bag as Bag
import GHC.Types.Unique.Supply
import GHC.Utils.Misc
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Types.Unique.Set
import GHC.Core.TyCon.Env
import GHC.Data.Maybe
import GHC.Core.Map.Type
import GHC.Data.TrieMap
import Control.Monad
import GHC.Utils.Monad
import Data.IORef
import GHC.Exts (oneShot)
import Data.List ( partition, mapAccumL )
import Data.List.NonEmpty ( NonEmpty(..), cons, toList, nonEmpty )
import qualified Data.List.NonEmpty as NE
import Control.Arrow ( first )
#if defined(DEBUG)
import GHC.Data.Graph.Directed
#endif
data WorkList
= WL { WorkList -> [Ct]
wl_eqs :: [Ct]
, WorkList -> [Ct]
wl_rest :: [Ct]
, WorkList -> Bag Implication
wl_implics :: Bag Implication
}
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
(WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs1, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest1
, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics1 })
(WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs2, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest2
, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics2 })
= WL { wl_eqs :: [Ct]
wl_eqs = [Ct]
eqs1 forall a. [a] -> [a] -> [a]
++ [Ct]
eqs2
, wl_rest :: [Ct]
wl_rest = [Ct]
rest1 forall a. [a] -> [a] -> [a]
++ [Ct]
rest2
, wl_implics :: Bag Implication
wl_implics = Bag Implication
implics1 forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Implication
implics2 }
workListSize :: WorkList -> Int
workListSize :: WorkList -> Int
workListSize (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
eqs forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
rest
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl = WorkList
wl { wl_eqs :: [Ct]
wl_eqs = Ct
ct forall a. a -> [a] -> [a]
: WorkList -> [Ct]
wl_eqs WorkList
wl }
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl = WorkList
wl { wl_rest :: [Ct]
wl_rest = Ct
ct forall a. a -> [a] -> [a]
: WorkList -> [Ct]
wl_rest WorkList
wl }
extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds [CtEvidence]
evs WorkList
wl
= [Ct] -> WorkList -> WorkList
extendWorkListCts (forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
evs) WorkList
wl
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic Implication
implic WorkList
wl = WorkList
wl { wl_implics :: Bag Implication
wl_implics = Implication
implic forall a. a -> Bag a -> Bag a
`consBag` WorkList -> Bag Implication
wl_implics WorkList
wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt Ct
ct WorkList
wl
= case Type -> Pred
classifyPredType (Ct -> Type
ctPred Ct
ct) of
EqPred {}
-> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl
ClassPred Class
cls [Type]
_
| Class -> Bool
isEqPredClass Class
cls
-> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl
Pred
_ -> Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl
extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts [Ct]
cts WorkList
wl = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt WorkList
wl [Ct]
cts
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
= forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest Bool -> Bool -> Bool
&& forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics
emptyWorkList :: WorkList
emptyWorkList :: WorkList
emptyWorkList = WL { wl_eqs :: [Ct]
wl_eqs = [], wl_rest :: [Ct]
wl_rest = [], wl_implics :: Bag Implication
wl_implics = forall a. Bag a
emptyBag }
selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
selectWorkItem wl :: WorkList
wl@(WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
| Ct
ct:[Ct]
cts <- [Ct]
eqs = forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_eqs :: [Ct]
wl_eqs = [Ct]
cts })
| Ct
ct:[Ct]
cts <- [Ct]
rest = forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_rest :: [Ct]
wl_rest = [Ct]
cts })
| Bool
otherwise = forall a. Maybe a
Nothing
getWorkList :: TcS WorkList
getWorkList :: TcS WorkList
getWorkList = do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
; forall a. TcM a -> TcS a
wrapTcS (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 <- forall a. TcRef a -> TcS a
readTcRef IORef WorkList
wl_var
; case WorkList -> Maybe (Ct, WorkList)
selectWorkItem WorkList
wl of {
Maybe (Ct, WorkList)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing ;
Just (Ct
ct, WorkList
new_wl) ->
do {
; forall a. TcRef a -> a -> TcS ()
writeTcRef IORef WorkList
wl_var WorkList
new_wl
; forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Ct
ct) } } }
instance Outputable WorkList where
ppr :: WorkList -> SDoc
ppr (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
= String -> SDoc
text String
"WL" SDoc -> SDoc -> SDoc
<+> (SDoc -> SDoc
braces forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Eqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [Ct]
eqs)
, Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Non-eqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [Ct]
rest)
, Bool -> SDoc -> SDoc
ppUnless (forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics) forall a b. (a -> b) -> a -> b
$
SDoc -> SDoc -> SDoc
ifPprDebug (String -> SDoc
text String
"Implics =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr (forall a. Bag a -> [a]
bagToList Bag Implication
implics)))
(String -> SDoc
text String
"(Implics omitted)")
])
type CycleBreakerVarStack = NonEmpty [(TcTyVar, TcType)]
data InertSet
= IS { InertSet -> InertCans
inert_cans :: InertCans
, InertSet -> CycleBreakerVarStack
inert_cycle_breakers :: CycleBreakerVarStack
, InertSet -> FunEqMap (Coercion, Type)
inert_famapp_cache :: FunEqMap (TcCoercion, TcType)
, InertSet -> DictMap CtEvidence
inert_solved_dicts :: DictMap CtEvidence
}
instance Outputable InertSet where
ppr :: InertSet -> SDoc
ppr (IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
ics
, inert_solved_dicts :: InertSet -> DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved_dicts })
= [SDoc] -> SDoc
vcat [ forall a. Outputable a => a -> SDoc
ppr InertCans
ics
, Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CtEvidence]
dicts) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Solved dicts =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
dicts) ]
where
dicts :: [CtEvidence]
dicts = forall a. Bag a -> [a]
bagToList (forall a. DictMap a -> Bag a
dictsToBag DictMap CtEvidence
solved_dicts)
emptyInertCans :: InertCans
emptyInertCans :: InertCans
emptyInertCans
= IC { inert_eqs :: InertEqs
inert_eqs = forall a. DVarEnv a
emptyDVarEnv
, inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
topTcLevel
, inert_given_eqs :: Bool
inert_given_eqs = Bool
False
, inert_dicts :: DictMap Ct
inert_dicts = forall a. DictMap a
emptyDicts
, inert_safehask :: DictMap Ct
inert_safehask = forall a. DictMap a
emptyDicts
, inert_funeqs :: FunEqMap EqualCtList
inert_funeqs = forall a. DictMap a
emptyFunEqs
, inert_insts :: [QCInst]
inert_insts = []
, inert_irreds :: Bag Ct
inert_irreds = Bag Ct
emptyCts
, inert_blocked :: Bag Ct
inert_blocked = Bag Ct
emptyCts }
emptyInert :: InertSet
emptyInert :: InertSet
emptyInert
= IS { inert_cans :: InertCans
inert_cans = InertCans
emptyInertCans
, inert_cycle_breakers :: CycleBreakerVarStack
inert_cycle_breakers = [] forall a. a -> [a] -> NonEmpty a
:| []
, inert_famapp_cache :: FunEqMap (Coercion, Type)
inert_famapp_cache = forall a. DictMap a
emptyFunEqs
, inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = forall a. DictMap a
emptyDictMap }
data InertCans
= IC { InertCans -> InertEqs
inert_eqs :: InertEqs
, InertCans -> FunEqMap EqualCtList
inert_funeqs :: FunEqMap EqualCtList
, InertCans -> DictMap Ct
inert_dicts :: DictMap Ct
, InertCans -> [QCInst]
inert_insts :: [QCInst]
, InertCans -> DictMap Ct
inert_safehask :: DictMap Ct
, InertCans -> Bag Ct
inert_irreds :: Cts
, InertCans -> Bag Ct
inert_blocked :: Cts
, InertCans -> TcLevel
inert_given_eq_lvl :: TcLevel
, InertCans -> Bool
inert_given_eqs :: Bool
}
type InertEqs = DTyVarEnv EqualCtList
newtype EqualCtList = EqualCtList (NonEmpty Ct)
deriving newtype EqualCtList -> SDoc
forall a. (a -> SDoc) -> Outputable a
ppr :: EqualCtList -> SDoc
$cppr :: EqualCtList -> SDoc
Outputable
unitEqualCtList :: Ct -> EqualCtList
unitEqualCtList :: Ct -> EqualCtList
unitEqualCtList Ct
ct = NonEmpty Ct -> EqualCtList
EqualCtList (Ct
ct forall a. a -> [a] -> NonEmpty a
:| [])
addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
addToEqualCtList Ct
ct (EqualCtList NonEmpty Ct
old_eqs)
| Ct -> Bool
isWantedCt Ct
ct
, Ct
eq1 :| [Ct]
eqs <- NonEmpty Ct
old_eqs
= NonEmpty Ct -> EqualCtList
EqualCtList (Ct
eq1 forall a. a -> [a] -> NonEmpty a
:| Ct
ct forall a. a -> [a] -> [a]
: [Ct]
eqs)
| Bool
otherwise
= NonEmpty Ct -> EqualCtList
EqualCtList (Ct
ct forall a. a -> NonEmpty a -> NonEmpty a
`cons` NonEmpty Ct
old_eqs)
filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
filterEqualCtList Ct -> Bool
pred (EqualCtList NonEmpty Ct
cts)
= forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty Ct -> EqualCtList
EqualCtList (forall a. [a] -> Maybe (NonEmpty a)
nonEmpty forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> NonEmpty a -> [a]
NE.filter Ct -> Bool
pred NonEmpty Ct
cts)
equalCtListToList :: EqualCtList -> [Ct]
equalCtListToList :: EqualCtList -> [Ct]
equalCtListToList (EqualCtList NonEmpty Ct
cts) = forall a. NonEmpty a -> [a]
toList NonEmpty Ct
cts
listToEqualCtList :: [Ct] -> Maybe EqualCtList
listToEqualCtList :: [Ct] -> Maybe EqualCtList
listToEqualCtList [Ct]
cts = NonEmpty Ct -> EqualCtList
EqualCtList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Ct]
cts
instance Outputable InertCans where
ppr :: InertCans -> SDoc
ppr (IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs
, inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
funeqs
, inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dicts
, inert_safehask :: InertCans -> DictMap Ct
inert_safehask = DictMap Ct
safehask
, inert_irreds :: InertCans -> Bag Ct
inert_irreds = Bag Ct
irreds
, inert_blocked :: InertCans -> Bag Ct
inert_blocked = Bag Ct
blocked
, inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl
, inert_given_eqs :: InertCans -> Bool
inert_given_eqs = Bool
given_eqs
, inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts })
= SDoc -> SDoc
braces forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ Bool -> SDoc -> SDoc
ppUnless (forall a. DVarEnv a -> Bool
isEmptyDVarEnv InertEqs
eqs) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Equalities:"
SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts (forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv EqualCtList -> Bag Ct -> Bag Ct
folder Bag Ct
emptyCts InertEqs
eqs)
, Bool -> SDoc -> SDoc
ppUnless (forall a. TcAppMap a -> Bool
isEmptyTcAppMap FunEqMap EqualCtList
funeqs) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Type-function equalities =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts (forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs EqualCtList -> Bag Ct -> Bag Ct
folder FunEqMap EqualCtList
funeqs Bag Ct
emptyCts)
, Bool -> SDoc -> SDoc
ppUnless (forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap Ct
dicts) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Dictionaries =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts (forall a. DictMap a -> Bag a
dictsToBag DictMap Ct
dicts)
, Bool -> SDoc -> SDoc
ppUnless (forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap Ct
safehask) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Safe Haskell unsafe overlap =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts (forall a. DictMap a -> Bag a
dictsToBag DictMap Ct
safehask)
, Bool -> SDoc -> SDoc
ppUnless (Bag Ct -> Bool
isEmptyCts Bag Ct
irreds) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Irreds =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts Bag Ct
irreds
, Bool -> SDoc -> SDoc
ppUnless (Bag Ct -> Bool
isEmptyCts Bag Ct
blocked) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Blocked =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts Bag Ct
blocked
, Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QCInst]
insts) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Given instances =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [QCInst]
insts)
, String -> SDoc
text String
"Innermost given equalities =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcLevel
ge_lvl
, String -> SDoc
text String
"Given eqs at this level =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Bool
given_eqs
]
where
folder :: EqualCtList -> Bag Ct -> Bag Ct
folder (EqualCtList NonEmpty Ct
eqs) Bag Ct
rest = forall a. NonEmpty a -> Bag a
nonEmptyToBag NonEmpty Ct
eqs Bag Ct -> Bag Ct -> Bag Ct
`andCts` Bag Ct
rest
maybeEmitShadow :: InertCans -> Ct -> TcS Ct
maybeEmitShadow :: InertCans -> Ct -> TcS Ct
maybeEmitShadow InertCans
ics Ct
ct
| let ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct
, CtWanted { ctev_pred :: CtEvidence -> Type
ctev_pred = Type
pred, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc
, ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WDeriv } <- CtEvidence
ev
, InertEqs -> FunEqMap EqualCtList -> Ct -> Bool
shouldSplitWD (InertCans -> InertEqs
inert_eqs InertCans
ics) (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
ics) Ct
ct
= do { String -> SDoc -> TcS ()
traceTcS String
"Emit derived shadow" (forall a. Outputable a => a -> SDoc
ppr Ct
ct)
; let derived_ev :: CtEvidence
derived_ev = CtDerived { ctev_pred :: Type
ctev_pred = Type
pred
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }
shadow_ct :: Ct
shadow_ct = Ct
ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
derived_ev }
; [Ct] -> TcS ()
emitWork [Ct
shadow_ct]
; let ev' :: CtEvidence
ev' = CtEvidence
ev { ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
WOnly }
ct' :: Ct
ct' = Ct
ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev' }
; forall (m :: * -> *) a. Monad m => a -> m a
return Ct
ct' }
| Bool
otherwise
= forall (m :: * -> *) a. Monad m => a -> m a
return Ct
ct
shouldSplitWD :: InertEqs -> FunEqMap EqualCtList -> Ct -> Bool
shouldSplitWD :: InertEqs -> FunEqMap EqualCtList -> Ct -> Bool
shouldSplitWD InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs (CDictCan { cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys })
= InertEqs -> FunEqMap EqualCtList -> [Type] -> Bool
should_split_match_args InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs [Type]
tys
shouldSplitWD InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS TcTyVar
tv, cc_rhs :: Ct -> Type
cc_rhs = Type
ty
, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
= TcTyVar
tv forall a. TcTyVar -> DVarEnv a -> Bool
`elemDVarEnv` InertEqs
inert_eqs
Bool -> Bool -> Bool
|| EqRel
-> (EqRel -> TcTyVar -> Bool)
-> (EqRel -> TyCon -> [Type] -> Bool)
-> Type
-> Bool
anyRewritableCanEqLHS EqRel
eq_rel (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs) (FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs) Type
ty
shouldSplitWD InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs (CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
= EqRel
-> (EqRel -> TcTyVar -> Bool)
-> (EqRel -> TyCon -> [Type] -> Bool)
-> Type
-> Bool
anyRewritableCanEqLHS EqRel
eq_rel (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs) (FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs)
(CtEvidence -> Type
ctEvPred CtEvidence
ev)
shouldSplitWD InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs (CIrredCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
= EqRel
-> (EqRel -> TcTyVar -> Bool)
-> (EqRel -> TyCon -> [Type] -> Bool)
-> Type
-> Bool
anyRewritableCanEqLHS (CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev) (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs)
(FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs) (CtEvidence -> Type
ctEvPred CtEvidence
ev)
shouldSplitWD InertEqs
_ FunEqMap EqualCtList
_ Ct
_ = Bool
False
should_split_match_args :: InertEqs -> FunEqMap EqualCtList -> [TcType] -> Bool
should_split_match_args :: InertEqs -> FunEqMap EqualCtList -> [Type] -> Bool
should_split_match_args InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs [Type]
tys
= forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (EqRel
-> (EqRel -> TcTyVar -> Bool)
-> (EqRel -> TyCon -> [Type] -> Bool)
-> Type
-> Bool
anyRewritableCanEqLHS EqRel
NomEq (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs) (FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs)) [Type]
tys
canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool
canRewriteTv :: InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs EqRel
eq_rel TcTyVar
tv
| Just (EqualCtList (Ct
ct :| [Ct]
_)) <- forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv InertEqs
inert_eqs TcTyVar
tv
, CEqCan { cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel1 } <- Ct
ct
= EqRel
eq_rel1 EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
eq_rel
| Bool
otherwise
= Bool
False
canRewriteTyFam :: FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
canRewriteTyFam :: FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs EqRel
eq_rel TyCon
tf [Type]
args
| Just (EqualCtList (Ct
ct :| [Ct]
_)) <- forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap EqualCtList
fun_eqs TyCon
tf [Type]
args
, CEqCan { cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel1 } <- Ct
ct
= EqRel
eq_rel1 EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
eq_rel
| Bool
otherwise
= Bool
False
isImprovable :: CtEvidence -> Bool
isImprovable :: CtEvidence -> Bool
isImprovable (CtWanted { ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WOnly }) = Bool
False
isImprovable CtEvidence
_ = Bool
True
addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq InertEqs
old_eqs TcTyVar
tv Ct
ct
= forall a. (a -> a -> a) -> DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv_C EqualCtList -> EqualCtList -> EqualCtList
add_eq InertEqs
old_eqs TcTyVar
tv (Ct -> EqualCtList
unitEqualCtList Ct
ct)
where
add_eq :: EqualCtList -> EqualCtList -> EqualCtList
add_eq EqualCtList
old_eqs EqualCtList
_ = Ct -> EqualCtList -> EqualCtList
addToEqualCtList Ct
ct EqualCtList
old_eqs
addCanFunEq :: FunEqMap EqualCtList -> TyCon -> [TcType] -> Ct
-> FunEqMap EqualCtList
addCanFunEq :: FunEqMap EqualCtList
-> TyCon -> [Type] -> Ct -> FunEqMap EqualCtList
addCanFunEq FunEqMap EqualCtList
old_eqs TyCon
fun_tc [Type]
fun_args Ct
ct
= forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp FunEqMap EqualCtList
old_eqs TyCon
fun_tc [Type]
fun_args Maybe EqualCtList -> Maybe EqualCtList
upd
where
upd :: Maybe EqualCtList -> Maybe EqualCtList
upd (Just EqualCtList
old_equal_ct_list) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Ct -> EqualCtList -> EqualCtList
addToEqualCtList Ct
ct EqualCtList
old_equal_ct_list
upd Maybe EqualCtList
Nothing = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Ct -> EqualCtList
unitEqualCtList Ct
ct
foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs :: forall b. (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs Ct -> b -> b
k InertEqs
eqs b
z
= forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv (\(EqualCtList NonEmpty Ct
cts) b
z -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> b -> b
k b
z NonEmpty Ct
cts) b
z InertEqs
eqs
findTyEqs :: InertCans -> TyVar -> [Ct]
findTyEqs :: InertCans -> TcTyVar -> [Ct]
findTyEqs InertCans
icans TcTyVar
tv = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] forall a. a -> a
id (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap @Maybe EqualCtList -> [Ct]
equalCtListToList forall a b. (a -> b) -> a -> b
$
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv (InertCans -> InertEqs
inert_eqs InertCans
icans) TcTyVar
tv)
delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
delEq :: InertCans -> CanEqLHS -> Type -> InertCans
delEq InertCans
ic CanEqLHS
lhs Type
rhs = case CanEqLHS
lhs of
TyVarLHS TcTyVar
tv
-> InertCans
ic { inert_eqs :: InertEqs
inert_eqs = forall a. (Maybe a -> Maybe a) -> DVarEnv a -> TcTyVar -> DVarEnv a
alterDVarEnv Maybe EqualCtList -> Maybe EqualCtList
upd (InertCans -> InertEqs
inert_eqs InertCans
ic) TcTyVar
tv }
TyFamLHS TyCon
tf [Type]
args
-> InertCans
ic { inert_funeqs :: FunEqMap EqualCtList
inert_funeqs = forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
ic) TyCon
tf [Type]
args Maybe EqualCtList -> Maybe EqualCtList
upd }
where
isThisOne :: Ct -> Bool
isThisOne :: Ct -> Bool
isThisOne (CEqCan { cc_rhs :: Ct -> Type
cc_rhs = Type
t1 }) = Type -> Type -> Bool
tcEqTypeNoKindCheck Type
rhs Type
t1
isThisOne Ct
other = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"delEq" (forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr InertCans
ic SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr Ct
other)
upd :: Maybe EqualCtList -> Maybe EqualCtList
upd :: Maybe EqualCtList -> Maybe EqualCtList
upd (Just EqualCtList
eq_ct_list) = (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
filterEqualCtList (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Bool
isThisOne) EqualCtList
eq_ct_list
upd Maybe EqualCtList
Nothing = forall a. Maybe a
Nothing
findEq :: InertCans -> CanEqLHS -> [Ct]
findEq :: InertCans -> CanEqLHS -> [Ct]
findEq InertCans
icans (TyVarLHS TcTyVar
tv) = InertCans -> TcTyVar -> [Ct]
findTyEqs InertCans
icans TcTyVar
tv
findEq InertCans
icans (TyFamLHS TyCon
fun_tc [Type]
fun_args)
= forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] forall a. a -> a
id (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap @Maybe EqualCtList -> [Ct]
equalCtListToList forall a b. (a -> b) -> a -> b
$
forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
icans) TyCon
fun_tc [Type]
fun_args)
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 :: TcLevel
inert_given_eq_lvl = TcLevel
tclvl
, inert_given_eqs :: Bool
inert_given_eqs = Bool
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 })
| 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" (forall a. Outputable a => a -> SDoc
ppr QCInst
new_qci)
; forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"adding new inert quantified instance" (forall a. Outputable a => a -> SDoc
ppr QCInst
new_qci)
; forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans
ics { inert_insts :: [QCInst]
inert_insts = QCInst
new_qci forall a. a -> [a] -> [a]
: [QCInst]
qcis }) }
same_qci :: QCInst -> Bool
same_qci QCInst
old_qci = HasDebugCallStack => 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 {" forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Trying to insert new inert item:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Ct
ct
; InertCans
ics <- TcS InertCans
getInertCans
; Ct
ct <- InertCans -> Ct -> TcS Ct
maybeEmitShadow InertCans
ics Ct
ct
; InertCans
ics <- InertCans -> Ct -> TcS InertCans
maybeKickOut InertCans
ics Ct
ct
; TcLevel
tclvl <- TcS TcLevel
getTcLevel
; InertCans -> TcS ()
setInertCans (TcLevel -> InertCans -> Ct -> InertCans
add_item TcLevel
tclvl InertCans
ics Ct
ct)
; String -> SDoc -> TcS ()
traceTcS String
"addInertCan }" forall a b. (a -> b) -> a -> b
$ SDoc
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
; forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics' }
| Bool
otherwise
= forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics
add_item :: TcLevel -> InertCans -> Ct -> InertCans
add_item :: TcLevel -> InertCans -> Ct -> InertCans
add_item TcLevel
tc_lvl
ics :: InertCans
ics@(IC { inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
funeqs, inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs })
item :: Ct
item@(CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs })
= TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item forall a b. (a -> b) -> a -> b
$
case CanEqLHS
lhs of
TyFamLHS TyCon
tc [Type]
tys -> InertCans
ics { inert_funeqs :: FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
-> TyCon -> [Type] -> Ct -> FunEqMap EqualCtList
addCanFunEq FunEqMap EqualCtList
funeqs TyCon
tc [Type]
tys Ct
item }
TyVarLHS TcTyVar
tv -> InertCans
ics { inert_eqs :: InertEqs
inert_eqs = InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq InertEqs
eqs TcTyVar
tv Ct
item }
add_item TcLevel
tc_lvl ics :: InertCans
ics@(IC { inert_blocked :: InertCans -> Bag Ct
inert_blocked = Bag Ct
blocked })
item :: Ct
item@(CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = HoleBlockerReason {}})
= TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item forall a b. (a -> b) -> a -> b
$
InertCans
ics { inert_blocked :: Bag Ct
inert_blocked = Bag Ct
blocked forall a. Bag a -> a -> Bag a
`snocBag` Ct
item }
add_item TcLevel
tc_lvl ics :: InertCans
ics@(IC { inert_irreds :: InertCans -> Bag Ct
inert_irreds = Bag Ct
irreds }) item :: Ct
item@(CIrredCan {})
= TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item forall a b. (a -> b) -> a -> b
$
InertCans
ics { inert_irreds :: Bag Ct
inert_irreds = Bag Ct
irreds forall a. Bag a -> a -> Bag a
`Bag.snocBag` Ct
item }
add_item TcLevel
_ 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_dicts :: DictMap Ct
inert_dicts = DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
addDictCt (InertCans -> DictMap Ct
inert_dicts InertCans
ics) Class
cls [Type]
tys Ct
item }
add_item TcLevel
_ InertCans
_ Ct
item
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"upd_inert set: can't happen! Inserting " forall a b. (a -> b) -> a -> b
$
forall a. Outputable a => a -> SDoc
ppr Ct
item
updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tclvl Ct
ct inerts :: InertCans
inerts@(IC { inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl })
| Bool -> Bool
not (Ct -> Bool
isGivenCt Ct
ct) = InertCans
inerts
| Ct -> Bool
not_equality Ct
ct = InertCans
inerts
| Bool
otherwise = InertCans
inerts { inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl'
, inert_given_eqs :: Bool
inert_given_eqs = Bool
True }
where
ge_lvl' :: TcLevel
ge_lvl' | TcLevel -> CtEvidence -> Bool
mentionsOuterVar TcLevel
tclvl (Ct -> CtEvidence
ctEvidence Ct
ct)
= TcLevel
tclvl
| Bool
otherwise
= TcLevel
ge_lvl
not_equality :: Ct -> Bool
not_equality :: Ct -> Bool
not_equality (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS TcTyVar
tv }) = Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv)
not_equality (CDictCan {}) = Bool
True
not_equality Ct
_ = Bool
False
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)
kick_out_rewritable CtFlavourRole
new_fr CanEqLHS
new_lhs InertCans
ics
n_kicked :: Int
n_kicked = WorkList -> Int
workListSize WorkList
kicked_out
; forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n_kicked forall a. Eq a => a -> a -> Bool
== Int
0) forall a b. (a -> b) -> a -> b
$
do { (WorkList -> WorkList) -> TcS ()
updWorkListTcS (WorkList -> WorkList -> WorkList
appendWorkList WorkList
kicked_out)
; let kicked_given_ev_vars :: [TcTyVar]
kicked_given_ev_vars =
[ TcTyVar
ev_var | Ct
ct <- WorkList -> [Ct]
wl_eqs WorkList
kicked_out
, CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
ev_var } <- [Ct -> CtEvidence
ctEvidence Ct
ct] ]
; 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
kicked_given_ev_vars)) forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcS ()
traceTcS String
"Given(s) have been kicked out; drop from famapp-cache"
(forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
kicked_given_ev_vars)
; VarSet -> TcS ()
dropFromFamAppCache ([TcTyVar] -> VarSet
mkVarSet [TcTyVar]
kicked_given_ev_vars) }
; SDoc -> TcS ()
csTraceTcS forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Kick out, lhs =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr CanEqLHS
new_lhs)
Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"n-kicked =" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n_kicked
, String -> SDoc
text String
"kicked_out =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr WorkList
kicked_out
, String -> SDoc
text String
"Residual inerts =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr InertCans
ics' ]) }
; forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n_kicked, InertCans
ics') }
kick_out_rewritable :: CtFlavourRole
-> CanEqLHS
-> InertCans
-> (WorkList, InertCans)
kick_out_rewritable :: CtFlavourRole -> CanEqLHS -> InertCans -> (WorkList, InertCans)
kick_out_rewritable CtFlavourRole
new_fr CanEqLHS
new_lhs
ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
tv_eqs
, inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dictmap
, inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
funeqmap
, inert_irreds :: InertCans -> Bag Ct
inert_irreds = Bag Ct
irreds
, inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
old_insts })
| Bool -> Bool
not (CtFlavourRole
new_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
new_fr)
= (WorkList
emptyWorkList, InertCans
ics)
| Bool
otherwise
= (WorkList
kicked_out, InertCans
inert_cans_in)
where
inert_cans_in :: InertCans
inert_cans_in = InertCans
ics { inert_eqs :: InertEqs
inert_eqs = InertEqs
tv_eqs_in
, inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct
dicts_in
, inert_funeqs :: FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
feqs_in
, inert_irreds :: Bag Ct
inert_irreds = Bag Ct
irs_in
, inert_insts :: [QCInst]
inert_insts = [QCInst]
insts_in }
kicked_out :: WorkList
kicked_out :: WorkList
kicked_out = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt
(WorkList
emptyWorkList { wl_eqs :: [Ct]
wl_eqs = [Ct]
tv_eqs_out forall a. [a] -> [a] -> [a]
++ [Ct]
feqs_out })
((Bag Ct
dicts_out Bag Ct -> Bag Ct -> Bag Ct
`andCts` Bag Ct
irs_out)
Bag Ct -> [Ct] -> Bag Ct
`extendCtsList` [Ct]
insts_out)
([Ct]
tv_eqs_out, InertEqs
tv_eqs_in) = forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv (forall container.
(container -> CanEqLHS -> EqualCtList -> container)
-> EqualCtList -> ([Ct], container) -> ([Ct], container)
kick_out_eqs InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
extend_tv_eqs)
([], forall a. DVarEnv a
emptyDVarEnv) InertEqs
tv_eqs
([Ct]
feqs_out, FunEqMap EqualCtList
feqs_in) = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs (forall container.
(container -> CanEqLHS -> EqualCtList -> container)
-> EqualCtList -> ([Ct], container) -> ([Ct], container)
kick_out_eqs FunEqMap EqualCtList
-> CanEqLHS -> EqualCtList -> FunEqMap EqualCtList
extend_fun_eqs)
FunEqMap EqualCtList
funeqmap ([], forall a. DictMap a
emptyFunEqs)
(Bag Ct
dicts_out, DictMap Ct
dicts_in) = (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
partitionDicts Ct -> Bool
kick_out_ct DictMap Ct
dictmap
(Bag Ct
irs_out, Bag Ct
irs_in) = forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag Ct -> Bool
kick_out_ct Bag Ct
irreds
insts_out :: [Ct]
insts_in :: [QCInst]
([Ct]
insts_out, [QCInst]
insts_in)
| CtFlavourRole -> Bool
fr_may_rewrite (CtFlavour
Given, EqRel
NomEq)
= forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith QCInst -> Either Ct QCInst
kick_out_qci [QCInst]
old_insts
| Bool
otherwise
= ([], [QCInst]
old_insts)
kick_out_qci :: QCInst -> Either Ct QCInst
kick_out_qci QCInst
qci
| let ev :: CtEvidence
ev = QCInst -> CtEvidence
qci_ev QCInst
qci
, EqRel -> Type -> Bool
fr_can_rewrite_ty EqRel
NomEq (CtEvidence -> Type
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
qci))
= forall a b. a -> Either a b
Left (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev)
| Bool
otherwise
= forall a b. b -> Either a b
Right QCInst
qci
(CtFlavour
_, EqRel
new_role) = CtFlavourRole
new_fr
fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty :: TcTyVar -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv EqRel
role Type
ty
= Bool -> EqRel -> (EqRel -> TcTyVar -> Bool) -> Type -> Bool
anyRewritableTyVar Bool
True EqRel
role EqRel -> TcTyVar -> Bool
can_rewrite Type
ty
where
can_rewrite :: EqRel -> TyVar -> Bool
can_rewrite :: EqRel -> TcTyVar -> Bool
can_rewrite EqRel
old_role TcTyVar
tv = EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&& TcTyVar
tv forall a. Eq a => a -> a -> Bool
== TcTyVar
new_tv
fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty :: TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [Type]
new_tf_args EqRel
role Type
ty
= EqRel -> (EqRel -> TyCon -> [Type] -> Bool) -> Type -> Bool
anyRewritableTyFamApp EqRel
role EqRel -> TyCon -> [Type] -> Bool
can_rewrite Type
ty
where
can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool
can_rewrite :: EqRel -> TyCon -> [Type] -> Bool
can_rewrite EqRel
old_role TyCon
old_tf [Type]
old_tf_args
= EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&&
TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps TyCon
new_tf [Type]
new_tf_args TyCon
old_tf [Type]
old_tf_args
{-# INLINE fr_can_rewrite_ty #-}
fr_can_rewrite_ty :: EqRel -> Type -> Bool
fr_can_rewrite_ty :: EqRel -> Type -> Bool
fr_can_rewrite_ty = case CanEqLHS
new_lhs of
TyVarLHS TcTyVar
new_tv -> TcTyVar -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv
TyFamLHS TyCon
new_tf [Type]
new_tf_args -> TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [Type]
new_tf_args
fr_may_rewrite :: CtFlavourRole -> Bool
fr_may_rewrite :: CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs = CtFlavourRole
new_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
fs
{-# INLINE kick_out_ct #-}
kick_out_ct :: Ct -> Bool
kick_out_ct :: Ct -> Bool
kick_out_ct = case CanEqLHS
new_lhs of
TyVarLHS TcTyVar
new_tv -> \Ct
ct -> let fs :: CtFlavourRole
fs@(CtFlavour
_,EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct in
CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
Bool -> Bool -> Bool
&& TcTyVar -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv EqRel
role (Ct -> Type
ctPred Ct
ct)
TyFamLHS TyCon
new_tf [Type]
new_tf_args
-> \Ct
ct -> let fs :: CtFlavourRole
fs@(CtFlavour
_, EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct in
CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
Bool -> Bool -> Bool
&& TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [Type]
new_tf_args EqRel
role (Ct -> Type
ctPred Ct
ct)
extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
extend_tv_eqs InertEqs
eqs (TyVarLHS TcTyVar
tv) EqualCtList
cts = forall a. DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv InertEqs
eqs TcTyVar
tv EqualCtList
cts
extend_tv_eqs InertEqs
eqs CanEqLHS
other EqualCtList
_cts = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extend_tv_eqs" (forall a. Outputable a => a -> SDoc
ppr InertEqs
eqs SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr CanEqLHS
other)
extend_fun_eqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList
-> FunEqMap EqualCtList
extend_fun_eqs :: FunEqMap EqualCtList
-> CanEqLHS -> EqualCtList -> FunEqMap EqualCtList
extend_fun_eqs FunEqMap EqualCtList
eqs (TyFamLHS TyCon
fam_tc [Type]
fam_args) EqualCtList
cts
= forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp FunEqMap EqualCtList
eqs TyCon
fam_tc [Type]
fam_args EqualCtList
cts
extend_fun_eqs FunEqMap EqualCtList
eqs CanEqLHS
other EqualCtList
_cts = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extend_fun_eqs" (forall a. Outputable a => a -> SDoc
ppr FunEqMap EqualCtList
eqs SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr CanEqLHS
other)
kick_out_eqs :: (container -> CanEqLHS -> EqualCtList -> container)
-> EqualCtList -> ([Ct], container)
-> ([Ct], container)
kick_out_eqs :: forall container.
(container -> CanEqLHS -> EqualCtList -> container)
-> EqualCtList -> ([Ct], container) -> ([Ct], container)
kick_out_eqs container -> CanEqLHS -> EqualCtList -> container
extend EqualCtList
eqs ([Ct]
acc_out, container
acc_in)
= ([Ct]
eqs_out forall a. [a] -> [a] -> [a]
`chkAppend` [Ct]
acc_out, case [Ct] -> Maybe EqualCtList
listToEqualCtList [Ct]
eqs_in of
Maybe EqualCtList
Nothing -> container
acc_in
Just eqs_in_ecl :: EqualCtList
eqs_in_ecl@(EqualCtList (Ct
eq1 :| [Ct]
_))
-> container -> CanEqLHS -> EqualCtList -> container
extend container
acc_in (Ct -> CanEqLHS
cc_lhs Ct
eq1) EqualCtList
eqs_in_ecl)
where
([Ct]
eqs_out, [Ct]
eqs_in) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Ct -> Bool
kick_out_eq (EqualCtList -> [Ct]
equalCtListToList EqualCtList
eqs)
kick_out_eq :: Ct -> Bool
kick_out_eq (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs, cc_rhs :: Ct -> Type
cc_rhs = Type
rhs_ty
, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
| Bool -> Bool
not (CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs)
= Bool
False
| TyVarLHS TcTyVar
_ <- CanEqLHS
lhs
, CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
new_fr
= Bool
False
| EqRel -> Type -> Bool
fr_can_rewrite_ty EqRel
eq_rel (CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs)
= Bool
True
| Bool
kick_out_for_inertness = Bool
True
| Bool
kick_out_for_completeness = Bool
True
| Bool
otherwise = Bool
False
where
fs :: CtFlavourRole
fs = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)
kick_out_for_inertness :: Bool
kick_out_for_inertness
= (CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
fs)
Bool -> Bool -> Bool
&& EqRel -> Type -> Bool
fr_can_rewrite_ty EqRel
eq_rel Type
rhs_ty
kick_out_for_completeness :: Bool
kick_out_for_completeness
= case EqRel
eq_rel of
EqRel
NomEq -> Type
rhs_ty Type -> Type -> Bool
`eqType` CanEqLHS -> Type
canEqLHSType CanEqLHS
new_lhs
EqRel
ReprEq -> CanEqLHS -> Type -> Bool
is_can_eq_lhs_head CanEqLHS
new_lhs Type
rhs_ty
kick_out_eq Ct
ct = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"keep_eq" (forall a. Outputable a => a -> SDoc
ppr Ct
ct)
is_can_eq_lhs_head :: CanEqLHS -> Type -> Bool
is_can_eq_lhs_head (TyVarLHS TcTyVar
tv) = Type -> Bool
go
where
go :: Type -> Bool
go (Rep.TyVarTy TcTyVar
tv') = TcTyVar
tv forall a. Eq a => a -> a -> Bool
== TcTyVar
tv'
go (Rep.AppTy Type
fun Type
_) = Type -> Bool
go Type
fun
go (Rep.CastTy Type
ty Coercion
_) = Type -> Bool
go Type
ty
go (Rep.TyConApp {}) = Bool
False
go (Rep.LitTy {}) = Bool
False
go (Rep.ForAllTy {}) = Bool
False
go (Rep.FunTy {}) = Bool
False
go (Rep.CoercionTy {}) = Bool
False
is_can_eq_lhs_head (TyFamLHS TyCon
fun_tc [Type]
fun_args) = Type -> Bool
go
where
go :: Type -> Bool
go (Rep.TyVarTy {}) = Bool
False
go (Rep.AppTy {}) = Bool
False
go (Rep.CastTy Type
ty Coercion
_) = Type -> Bool
go Type
ty
go (Rep.TyConApp TyCon
tc [Type]
args) = TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps TyCon
fun_tc [Type]
fun_args TyCon
tc [Type]
args
go (Rep.LitTy {}) = Bool
False
go (Rep.ForAllTy {}) = Bool
False
go (Rep.FunTy {}) = Bool
False
go (Rep.CoercionTy {}) = Bool
False
kickOutAfterUnification :: TcTyVar -> TcS Int
kickOutAfterUnification :: TcTyVar -> TcS Int
kickOutAfterUnification TcTyVar
new_tv
= do { InertCans
ics <- TcS InertCans
getInertCans
; (Int
n_kicked, InertCans
ics2) <- CtFlavourRole -> CanEqLHS -> InertCans -> TcS (Int, InertCans)
kickOutRewritable (CtFlavour
Given,EqRel
NomEq)
(TcTyVar -> CanEqLHS
TyVarLHS TcTyVar
new_tv) InertCans
ics
; InertCans -> TcS ()
setInertCans InertCans
ics2
; forall (m :: * -> *) a. Monad m => a -> m a
return Int
n_kicked }
kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS ()
kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole Coercion
filled_co
= 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
; forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n_kicked forall a. Eq a => a -> a -> Bool
== Int
0) forall a b. (a -> b) -> a -> b
$
do { (WorkList -> WorkList) -> TcS ()
updWorkListTcS (WorkList -> WorkList -> WorkList
appendWorkList WorkList
kicked_out)
; SDoc -> TcS ()
csTraceTcS forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Kick out, hole =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr CoercionHole
hole)
Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"n-kicked =" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n_kicked
, String -> SDoc
text String
"kicked_out =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr WorkList
kicked_out
, String -> SDoc
text String
"Residual inerts =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr InertCans
ics' ]) }
; InertCans -> TcS ()
setInertCans InertCans
ics' }
where
holes_of_co :: UniqSet CoercionHole
holes_of_co = Coercion -> UniqSet CoercionHole
coercionHolesOfCo Coercion
filled_co
kick_out :: InertCans -> (WorkList, InertCans)
kick_out :: InertCans -> (WorkList, InertCans)
kick_out ics :: InertCans
ics@(IC { inert_blocked :: InertCans -> Bag Ct
inert_blocked = Bag Ct
blocked })
= let (Bag Ct
to_kick, Bag Ct
to_keep) = forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c)
partitionBagWith Ct -> Either Ct Ct
kick_ct Bag Ct
blocked
kicked_out :: WorkList
kicked_out = [Ct] -> WorkList -> WorkList
extendWorkListCts (forall a. Bag a -> [a]
bagToList Bag Ct
to_kick) WorkList
emptyWorkList
ics' :: InertCans
ics' = InertCans
ics { inert_blocked :: Bag Ct
inert_blocked = Bag Ct
to_keep }
in
(WorkList
kicked_out, InertCans
ics')
kick_ct :: Ct -> Either Ct Ct
kick_ct :: Ct -> Either Ct Ct
kick_ct ct :: Ct
ct@(CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = HoleBlockerReason UniqSet CoercionHole
holes })
| CoercionHole
hole forall a. Uniquable a => a -> UniqSet a -> Bool
`elementOfUniqSet` UniqSet CoercionHole
holes
= let new_holes :: UniqSet CoercionHole
new_holes = UniqSet CoercionHole
holes forall a. Uniquable a => UniqSet a -> a -> UniqSet a
`delOneFromUniqSet` CoercionHole
hole
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` UniqSet CoercionHole
holes_of_co
updated_ct :: Ct
updated_ct = Ct
ct { cc_reason :: CtIrredReason
cc_reason = UniqSet CoercionHole -> CtIrredReason
HoleBlockerReason UniqSet CoercionHole
new_holes }
in
if forall a. UniqSet a -> Bool
isEmptyUniqSet UniqSet CoercionHole
new_holes
then forall a b. a -> Either a b
Left Ct
updated_ct
else forall a b. b -> Either a b
Right Ct
updated_ct
| Bool
otherwise
= forall a b. b -> Either a b
Right Ct
ct
kick_ct Ct
other = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"kickOutAfterFillingCoercionHole" (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 :: DictMap Ct
inert_safehask = DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
addDictCt (InertCans -> DictMap Ct
inert_dicts InertCans
ics) Class
cls [Type]
tys Ct
item }
addInertSafehask InertCans
_ Ct
item
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"addInertSafehask: can't happen! Inserting " forall a b. (a -> b) -> a -> b
$ 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 = 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 (Bag Ct)
getSafeOverlapFailures
= do { IC { inert_safehask :: InertCans -> DictMap Ct
inert_safehask = DictMap Ct
safehask } <- TcS InertCans
getInertCans
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldDicts Ct -> Bag Ct -> Bag Ct
consCts DictMap Ct
safehask Bag Ct
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:" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr CtEvidence
item
; (InertSet -> InertSet) -> TcS ()
updInertTcS forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
InertSet
ics { inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = forall a. DictMap a -> Class -> [Type] -> a -> DictMap a
addDict (InertSet -> DictMap CtEvidence
inert_solved_dicts InertSet
ics) Class
cls [Type]
tys CtEvidence
item } }
| Bool
otherwise
= forall (m :: * -> *) a. Monad m => a -> m a
return ()
getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts = do { InertSet
ics <- TcS InertSet
getTcSInerts; 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 forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
InertSet
ics { inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved_dicts }
updInertTcS :: (InertSet -> InertSet) -> TcS ()
updInertTcS :: (InertSet -> InertSet) -> TcS ()
updInertTcS InertSet -> InertSet
upd_fn
= do { IORef InertSet
is_var <- TcS (IORef InertSet)
getTcSInertsRef
; forall a. TcM a -> TcS a
wrapTcS (do { InertSet
curr_inert <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
is_var
; 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; 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 forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans :: InertCans
inert_cans = InertCans
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
; forall a. TcM a -> TcS a
wrapTcS (do { InertSet
inerts <- 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)
; forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef InertSet
is_var (InertSet
inerts { inert_cans :: InertCans
inert_cans = InertCans
cans' })
; 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 forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans :: InertCans
inert_cans = InertCans -> InertCans
upd_fn (InertSet -> InertCans
inert_cans InertSet
inerts) }
updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertDicts DictMap Ct -> DictMap Ct
upd_fn
= (InertCans -> InertCans) -> TcS ()
updInertCans forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct -> DictMap Ct
upd_fn (InertCans -> DictMap Ct
inert_dicts InertCans
ics) }
updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertSafehask DictMap Ct -> DictMap Ct
upd_fn
= (InertCans -> InertCans) -> TcS ()
updInertCans forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_safehask :: DictMap Ct
inert_safehask = DictMap Ct -> DictMap Ct
upd_fn (InertCans -> DictMap Ct
inert_safehask InertCans
ics) }
updInertIrreds :: (Cts -> Cts) -> TcS ()
updInertIrreds :: (Bag Ct -> Bag Ct) -> TcS ()
updInertIrreds Bag Ct -> Bag Ct
upd_fn
= (InertCans -> InertCans) -> TcS ()
updInertCans forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_irreds :: Bag Ct
inert_irreds = Bag Ct -> Bag Ct
upd_fn (InertCans -> Bag Ct
inert_irreds InertCans
ics) }
getInertEqs :: TcS (DTyVarEnv EqualCtList)
getInertEqs :: TcS InertEqs
getInertEqs = do { InertCans
inert <- TcS InertCans
getInertCans; 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
; forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans -> TcLevel
inert_given_eq_lvl InertCans
inert) }
getInertInsols :: TcS Cts
getInertInsols :: TcS (Bag Ct)
getInertInsols = do { InertCans
inert <- TcS InertCans
getInertCans
; forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
insolubleEqCt (InertCans -> Bag Ct
inert_irreds InertCans
inert)) }
getInertGivens :: TcS [Ct]
getInertGivens :: TcS [Ct]
getInertGivens
= do { InertCans
inerts <- TcS InertCans
getInertCans
; let all_cts :: [Ct]
all_cts = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldDicts (:) (InertCans -> DictMap Ct
inert_dicts InertCans
inerts)
forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs (\EqualCtList
ecl [Ct]
out -> EqualCtList -> [Ct]
equalCtListToList EqualCtList
ecl forall a. [a] -> [a] -> [a]
++ [Ct]
out)
(InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
inerts)
forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap EqualCtList -> [Ct]
equalCtListToList (forall a. DVarEnv a -> [a]
dVarEnvElts (InertCans -> InertEqs
inert_eqs InertCans
inerts))
; forall (m :: * -> *) a. Monad m => a -> m a
return (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
; 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 })
= ASSERT2( all isGivenCt sc_pending, ppr sc_pending )
([Ct]
sc_pending, InertCans
ic { inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct
dicts', inert_insts :: [QCInst]
inert_insts = [QCInst]
insts' })
where
sc_pending :: [Ct]
sc_pending = [Ct]
sc_pend_insts forall a. [a] -> [a] -> [a]
++ [Ct]
sc_pend_dicts
sc_pend_dicts :: [Ct]
sc_pend_dicts = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldDicts Ct -> [Ct] -> [Ct]
get_pending DictMap Ct
dicts []
dicts' :: DictMap Ct
dicts' = 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') = 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
isPendingScDict Ct
dict
, CtEvidence -> Bool
belongs_to_this_level (Ct -> CtEvidence
ctEvidence Ct
dict)
= Ct
dict' 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
addDictCt DictMap Ct
dicts Class
cls [Type]
tys Ct
ct
add Ct
ct DictMap Ct
_ = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getPendingScDicts" (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
isPendingScInst QCInst
qci
, CtEvidence -> Bool
belongs_to_this_level CtEvidence
ev
= (QCInst -> Ct
CQuantCan QCInst
qci' 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) forall a. Eq a => a -> a -> Bool
== TcLevel
this_lvl
getUnsolvedInerts :: TcS ( Bag Implication
, Cts )
getUnsolvedInerts :: TcS (Bag Implication, Bag Ct)
getUnsolvedInerts
= do { IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
tv_eqs
, inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
fun_eqs
, inert_irreds :: InertCans -> Bag Ct
inert_irreds = Bag Ct
irreds
, inert_blocked :: InertCans -> Bag Ct
inert_blocked = Bag Ct
blocked
, inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
idicts
} <- TcS InertCans
getInertCans
; let unsolved_tv_eqs :: Bag Ct
unsolved_tv_eqs = forall b. (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs Ct -> Bag Ct -> Bag Ct
add_if_unsolved InertEqs
tv_eqs Bag Ct
emptyCts
unsolved_fun_eqs :: Bag Ct
unsolved_fun_eqs = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs EqualCtList -> Bag Ct -> Bag Ct
add_if_unsolveds FunEqMap EqualCtList
fun_eqs Bag Ct
emptyCts
unsolved_irreds :: Bag Ct
unsolved_irreds = forall a. (a -> Bool) -> Bag a -> Bag a
Bag.filterBag Ct -> Bool
is_unsolved Bag Ct
irreds
unsolved_blocked :: Bag Ct
unsolved_blocked = Bag Ct
blocked
unsolved_dicts :: Bag Ct
unsolved_dicts = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldDicts Ct -> Bag Ct -> Bag Ct
add_if_unsolved DictMap Ct
idicts Bag Ct
emptyCts
unsolved_others :: Bag Ct
unsolved_others = forall a. [Bag a] -> Bag a
unionManyBags [ Bag Ct
unsolved_irreds
, Bag Ct
unsolved_dicts
, Bag Ct
unsolved_blocked ]
; Bag Implication
implics <- TcS (Bag Implication)
getWorkListImplics
; String -> SDoc -> TcS ()
traceTcS String
"getUnsolvedInerts" forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
" tv eqs =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Bag Ct
unsolved_tv_eqs
, String -> SDoc
text String
"fun eqs =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Bag Ct
unsolved_fun_eqs
, String -> SDoc
text String
"others =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Bag Ct
unsolved_others
, String -> SDoc
text String
"implics =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Bag Implication
implics ]
; forall (m :: * -> *) a. Monad m => a -> m a
return ( Bag Implication
implics, Bag Ct
unsolved_tv_eqs forall a. Bag a -> Bag a -> Bag a
`unionBags`
Bag Ct
unsolved_fun_eqs forall a. Bag a -> Bag a -> Bag a
`unionBags`
Bag Ct
unsolved_others) }
where
add_if_unsolved :: Ct -> Cts -> Cts
add_if_unsolved :: Ct -> Bag Ct -> Bag Ct
add_if_unsolved Ct
ct Bag Ct
cts | Ct -> Bool
is_unsolved Ct
ct = Ct
ct Ct -> Bag Ct -> Bag Ct
`consCts` Bag Ct
cts
| Bool
otherwise = Bag Ct
cts
add_if_unsolveds :: EqualCtList -> Cts -> Cts
add_if_unsolveds :: EqualCtList -> Bag Ct -> Bag Ct
add_if_unsolveds EqualCtList
new_cts Bag Ct
old_cts = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> Bag Ct -> Bag Ct
add_if_unsolved Bag Ct
old_cts
(EqualCtList -> [Ct]
equalCtListToList EqualCtList
new_cts)
is_unsolved :: Ct -> Bool
is_unsolved Ct
ct = Bool -> Bool
not (Ct -> Bool
isGivenCt Ct
ct)
getHasGivenEqs :: TcLevel
-> TcS ( HasGivenEqs
, Cts )
getHasGivenEqs :: TcLevel -> TcS (HasGivenEqs, Bag Ct)
getHasGivenEqs TcLevel
tclvl
= do { inerts :: InertCans
inerts@(IC { inert_irreds :: InertCans -> Bag Ct
inert_irreds = Bag Ct
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 insols :: Bag Ct
insols = forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
insolubleEqCt Bag Ct
irreds
has_ge :: HasGivenEqs
has_ge | TcLevel
ge_lvl 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" forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"given_eqs:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Bool
given_eqs
, String -> SDoc
text String
"ge_lvl:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcLevel
ge_lvl
, String -> SDoc
text String
"ambient level:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl
, String -> SDoc
text String
"Inerts:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr InertCans
inerts
, String -> SDoc
text String
"Insols:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Bag Ct
insols]
; forall (m :: * -> *) a. Monad m => a -> m a
return (HasGivenEqs
has_ge, Bag Ct
insols) }
mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar TcLevel
tclvl CtEvidence
ev
= (TcTyVar -> Bool) -> Type -> Bool
anyFreeVarsOfType (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl) forall a b. (a -> b) -> a -> b
$
CtEvidence -> Type
ctEvPred CtEvidence
ev
isOuterTyVar :: TcLevel -> TyCoVar -> Bool
isOuterTyVar :: TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv
| TcTyVar -> Bool
isTyVar TcTyVar
tv = ASSERT2( not (isTouchableMetaTyVar tclvl tv), ppr tv <+> ppr tclvl )
TcLevel
tclvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv
| Bool
otherwise = Bool
False
matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
matchableGivens :: CtLoc -> Type -> InertSet -> Bag Ct
matchableGivens CtLoc
loc_w Type
pred_w inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans })
= forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
matchable_given Bag Ct
all_relevant_givens
where
all_relevant_givens :: Cts
all_relevant_givens :: Bag Ct
all_relevant_givens
| Just (Class
clas, [Type]
_) <- Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred_w
= forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> DictMap Ct
inert_dicts InertCans
inert_cans) Class
clas
forall a. Bag a -> Bag a -> Bag a
`unionBags` InertCans -> Bag Ct
inert_irreds InertCans
inert_cans
| Bool
otherwise
= InertCans -> Bag Ct
inert_irreds InertCans
inert_cans
matchable_given :: Ct -> Bool
matchable_given :: Ct -> Bool
matchable_given Ct
ct
| CtGiven { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_g, ctev_pred :: CtEvidence -> Type
ctev_pred = Type
pred_g } <- Ct -> CtEvidence
ctEvidence Ct
ct
= InertSet -> Type -> CtLoc -> Type -> CtLoc -> Bool
mightEqualLater InertSet
inerts Type
pred_g CtLoc
loc_g Type
pred_w CtLoc
loc_w
| Bool
otherwise
= Bool
False
mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
mightEqualLater :: InertSet -> Type -> CtLoc -> Type -> CtLoc -> Bool
mightEqualLater InertSet
inert_set Type
given_pred CtLoc
given_loc Type
wanted_pred CtLoc
wanted_loc
| CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc
= Bool
False
| Bool
otherwise
= case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
bind_fun [Type
flattened_given] [Type
flattened_wanted] of
UnifyResult
SurelyApart -> Bool
False
MaybeApart MaybeApartReason
MARInfinite TCvSubst
_ -> Bool
False
UnifyResult
_ -> Bool
True
where
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
tyCoVarsOfTypes [Type
given_pred, Type
wanted_pred]
([Type
flattened_given, Type
flattened_wanted], TyVarEnv (TyCon, [Type])
var_mapping)
= InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX InScopeSet
in_scope [Type
given_pred, Type
wanted_pred]
bind_fun :: BindFun
bind_fun :: BindFun
bind_fun TcTyVar
tv Type
rhs_ty
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
, TcTyVar -> MetaInfo -> Type -> Bool
can_unify TcTyVar
tv (TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv) Type
rhs_ty
= BindFlag
BindMe
| Just (TyCon
_fam_tc, [Type]
fam_args) <- forall a. VarEnv a -> TcTyVar -> Maybe a
lookupVarEnv TyVarEnv (TyCon, [Type])
var_mapping TcTyVar
tv
, (TcTyVar -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes TcTyVar -> Bool
mentions_meta_ty_var [Type]
fam_args
= BindFlag
BindMe
| Bool
otherwise
= BindFlag
Apart
mentions_meta_ty_var :: TyVar -> Bool
mentions_meta_ty_var :: TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
tv
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= case TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv of
MetaInfo
CycleBreakerTv
-> (TcTyVar -> Bool) -> Type -> Bool
anyFreeVarsOfType TcTyVar -> Bool
mentions_meta_ty_var
(TcTyVar -> InertSet -> Type
lookupCycleBreakerVar TcTyVar
tv InertSet
inert_set)
MetaInfo
_ -> Bool
True
| Bool
otherwise
= Bool
False
can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
can_unify TcTyVar
_lhs_tv MetaInfo
TyVarTv Type
rhs_ty
| Just TcTyVar
rhs_tv <- Type -> Maybe TcTyVar
tcGetTyVar_maybe Type
rhs_ty
= case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
rhs_tv of
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
TyVarTv } -> Bool
True
MetaTv {} -> Bool
False
SkolemTv {} -> Bool
True
TcTyVarDetails
RuntimeUnk -> Bool
True
| Bool
otherwise
= Bool
False
can_unify TcTyVar
lhs_tv MetaInfo
_other Type
_rhs_ty = TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
lhs_tv
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
from_loc CtLoc
solve_loc
| InstSCOrigin Int
_ TypeSize
given_size <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
from_loc
, ScOrigin TypeSize
wanted_size <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
solve_loc
= TypeSize
given_size forall a. Ord a => a -> a -> Bool
>= TypeSize
wanted_size
| Bool
otherwise
= Bool
False
lookupCycleBreakerVar :: TcTyVar
-> InertSet
-> TcType
lookupCycleBreakerVar :: TcTyVar -> InertSet -> Type
lookupCycleBreakerVar TcTyVar
cbv (IS { inert_cycle_breakers :: InertSet -> CycleBreakerVarStack
inert_cycle_breakers = CycleBreakerVarStack
cbvs_stack })
| Just Type
tyfam_app <- ASSERT( (isCycleBreakerTyVar cbv) )
forall (f :: * -> *) a. Foldable f => f (Maybe a) -> Maybe a
firstJusts (forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TcTyVar
cbv) CycleBreakerVarStack
cbvs_stack)
= Type
tyfam_app
| Bool
otherwise
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"lookupCycleBreakerVar found an unbound cycle breaker" (forall a. Outputable a => a -> SDoc
ppr TcTyVar
cbv SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr CycleBreakerVarStack
cbvs_stack)
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack = ([] forall a. a -> NonEmpty a -> NonEmpty a
NE.<|)
insertCycleBreakerBinding :: TcTyVar
-> TcType
-> CycleBreakerVarStack -> CycleBreakerVarStack
insertCycleBreakerBinding :: TcTyVar -> Type -> CycleBreakerVarStack -> CycleBreakerVarStack
insertCycleBreakerBinding TcTyVar
cbv Type
expansion ([(TcTyVar, Type)]
top_env :| [[(TcTyVar, Type)]]
rest_envs)
= ASSERT( (isCycleBreakerTyVar cbv) )
((TcTyVar
cbv, Type
expansion) forall a. a -> [a] -> [a]
: [(TcTyVar, Type)]
top_env) forall a. a -> [a] -> NonEmpty a
:| [[(TcTyVar, Type)]]
rest_envs
forAllCycleBreakerBindings_ :: Monad m
=> CycleBreakerVarStack
-> (TcTyVar -> TcType -> m ()) -> m ()
forAllCycleBreakerBindings_ :: forall (m :: * -> *).
Monad m =>
CycleBreakerVarStack -> (TcTyVar -> Type -> m ()) -> m ()
forAllCycleBreakerBindings_ ([(TcTyVar, Type)]
top_env :| [[(TcTyVar, Type)]]
_rest_envs) TcTyVar -> Type -> m ()
action
= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(TcTyVar, Type)]
top_env (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TcTyVar -> Type -> m ()
action)
{-# INLINABLE forAllCycleBreakerBindings_ #-}
removeInertCts :: [Ct] -> InertCans -> InertCans
removeInertCts :: [Ct] -> InertCans -> InertCans
removeInertCts [Ct]
cts InertCans
icans = 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 :: DictMap Ct
inert_dicts = forall a. DictMap a -> Class -> [Type] -> DictMap a
delDict (InertCans -> DictMap Ct
inert_dicts InertCans
is) Class
cl [Type]
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
CQuantCan {} -> forall a. String -> a
panic String
"removeInertCt: CQuantCan"
CIrredCan {} -> forall a. String -> a
panic String
"removeInertCt: CIrredEvCan"
CNonCanonical {} -> forall a. String -> a
panic String
"removeInertCt: CNonCanonical"
lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavourRole))
lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type, CtFlavourRole))
lookupFamAppInert TyCon
fam_tc [Type]
tys
= do { IS { inert_cans :: InertSet -> InertCans
inert_cans = IC { inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
inert_funeqs } } <- TcS InertSet
getTcSInerts
; forall (m :: * -> *) a. Monad m => a -> m a
return (FunEqMap EqualCtList -> Maybe (Coercion, Type, CtFlavourRole)
lookup_inerts FunEqMap EqualCtList
inert_funeqs) }
where
lookup_inerts :: FunEqMap EqualCtList -> Maybe (Coercion, Type, CtFlavourRole)
lookup_inerts FunEqMap EqualCtList
inert_funeqs
| Just (EqualCtList (CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev, cc_rhs :: Ct -> Type
cc_rhs = Type
rhs } :| [Ct]
_))
<- forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap EqualCtList
inert_funeqs TyCon
fam_tc [Type]
tys
= forall a. a -> Maybe a
Just (HasDebugCallStack => CtEvidence -> Coercion
ctEvCoercion CtEvidence
ctev, Type
rhs, CtEvidence -> CtFlavourRole
ctEvFlavourRole CtEvidence
ctev)
| Bool
otherwise = 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
; forall (m :: * -> *) a. Monad m => a -> m a
return (InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict InertSet
inerts CtLoc
loc Class
cls [Type]
tys forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
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)) }
| Bool
otherwise
= forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap Ct
dicts CtLoc
loc Class
cls [Type]
tys of
Just Ct
ct -> forall a. a -> Maybe a
Just Ct
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 forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap CtEvidence
solved CtLoc
loc Class
cls [Type]
tys of
Just CtEvidence
ev -> forall a. a -> Maybe a
Just CtEvidence
ev
Maybe CtEvidence
_ -> forall a. Maybe a
Nothing
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
lookupFamAppCache TyCon
fam_tc [Type]
tys
= do { IS { inert_famapp_cache :: InertSet -> FunEqMap (Coercion, Type)
inert_famapp_cache = FunEqMap (Coercion, Type)
famapp_cache } <- TcS InertSet
getTcSInerts
; case forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap (Coercion, Type)
famapp_cache TyCon
fam_tc [Type]
tys of
result :: Maybe (Coercion, Type)
result@(Just (Coercion
co, Type
ty)) ->
do { String -> SDoc -> TcS ()
traceTcS String
"famapp_cache hit" ([SDoc] -> SDoc
vcat [ forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys)
, forall a. Outputable a => a -> SDoc
ppr Type
ty
, forall a. Outputable a => a -> SDoc
ppr Coercion
co ])
; forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Coercion, Type)
result }
Maybe (Coercion, Type)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing }
extendFamAppCache :: TyCon -> [Type] -> (TcCoercion, TcType) -> TcS ()
extendFamAppCache :: TyCon -> [Type] -> (Coercion, Type) -> TcS ()
extendFamAppCache TyCon
tc [Type]
xi_args stuff :: (Coercion, Type)
stuff@(Coercion
_, Type
ty)
= do { DynFlags
dflags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_FamAppCache DynFlags
dflags) forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcS ()
traceTcS String
"extendFamAppCache" ([SDoc] -> SDoc
vcat [ forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [Type]
xi_args
, forall a. Outputable a => a -> SDoc
ppr Type
ty ])
; (InertSet -> InertSet) -> TcS ()
updInertTcS forall a b. (a -> b) -> a -> b
$ \ is :: InertSet
is@(IS { inert_famapp_cache :: InertSet -> FunEqMap (Coercion, Type)
inert_famapp_cache = FunEqMap (Coercion, Type)
fc }) ->
InertSet
is { inert_famapp_cache :: FunEqMap (Coercion, Type)
inert_famapp_cache = forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertFunEq FunEqMap (Coercion, Type)
fc TyCon
tc [Type]
xi_args (Coercion, Type)
stuff } } }
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache VarSet
varset
= do { inerts :: InertSet
inerts@(IS { inert_famapp_cache :: InertSet -> FunEqMap (Coercion, Type)
inert_famapp_cache = FunEqMap (Coercion, Type)
famapp_cache }) <- TcS InertSet
getTcSInerts
; let filtered :: FunEqMap (Coercion, Type)
filtered = forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap (Coercion, Type) -> Bool
check FunEqMap (Coercion, Type)
famapp_cache
; InertSet -> TcS ()
setTcSInerts forall a b. (a -> b) -> a -> b
$ InertSet
inerts { inert_famapp_cache :: FunEqMap (Coercion, Type)
inert_famapp_cache = FunEqMap (Coercion, Type)
filtered } }
where
check :: (TcCoercion, TcType) -> Bool
check :: (Coercion, Type) -> Bool
check (Coercion
co, Type
_) = Bool -> Bool
not ((TcTyVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo (TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
varset) Coercion
co)
foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
foldIrreds :: forall b. (Ct -> b -> b) -> Bag Ct -> b -> b
foldIrreds Ct -> b -> b
k Bag Ct
irreds b
z = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> b -> b
k b
z Bag Ct
irreds
type TcAppMap a = DTyConEnv (ListMap LooseTypeMap a)
isEmptyTcAppMap :: TcAppMap a -> Bool
isEmptyTcAppMap :: forall a. TcAppMap a -> Bool
isEmptyTcAppMap TcAppMap a
m = forall a. DTyConEnv a -> Bool
isEmptyDTyConEnv TcAppMap a
m
emptyTcAppMap :: TcAppMap a
emptyTcAppMap :: forall a. DictMap a
emptyTcAppMap = forall a. DTyConEnv a
emptyDTyConEnv
findTcApp :: TcAppMap a -> TyCon -> [Type] -> Maybe a
findTcApp :: forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findTcApp TcAppMap a
m TyCon
tc [Type]
tys = do { ListMap LooseTypeMap a
tys_map <- forall a. DTyConEnv a -> TyCon -> Maybe a
lookupDTyConEnv TcAppMap a
m TyCon
tc
; forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM [Type]
tys ListMap LooseTypeMap a
tys_map }
delTcApp :: TcAppMap a -> TyCon -> [Type] -> TcAppMap a
delTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> TcAppMap a
delTcApp TcAppMap a
m TyCon
tc [Type]
tys = forall a. (a -> a) -> DTyConEnv a -> TyCon -> DTyConEnv a
adjustDTyConEnv (forall (m :: * -> *) a. TrieMap m => Key m -> m a -> m a
deleteTM [Type]
tys) TcAppMap a
m TyCon
tc
insertTcApp :: TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp TcAppMap a
m TyCon
tc [Type]
tys a
ct = forall a.
(Maybe a -> Maybe a) -> DTyConEnv a -> TyCon -> DTyConEnv a
alterDTyConEnv Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm TcAppMap a
m TyCon
tc
where
alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm Maybe (ListMap LooseTypeMap a)
mb_tm = forall a. a -> Maybe a
Just (forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
insertTM [Type]
tys a
ct (Maybe (ListMap LooseTypeMap a)
mb_tm forall a. Maybe a -> a -> a
`orElse` forall (m :: * -> *) a. TrieMap m => m a
emptyTM))
alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp TcAppMap a
m TyCon
tc [Type]
tys XT a
upd = forall a.
(Maybe a -> Maybe a) -> DTyConEnv a -> TyCon -> DTyConEnv a
alterDTyConEnv Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm TcAppMap a
m TyCon
tc
where
alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm Maybe (ListMap LooseTypeMap a)
m_elt = forall a. a -> Maybe a
Just (forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM [Type]
tys XT a
upd (Maybe (ListMap LooseTypeMap a)
m_elt forall a. Maybe a -> a -> a
`orElse` forall (m :: * -> *) a. TrieMap m => m a
emptyTM))
filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap a -> Bool
f TcAppMap a
m = forall a b. (a -> Maybe b) -> DTyConEnv a -> DTyConEnv b
mapMaybeDTyConEnv ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
one_tycon TcAppMap a
m
where
one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
one_tycon ListMap LooseTypeMap a
tm
| forall (m :: * -> *) a. TrieMap m => m a -> Bool
isEmptyTM ListMap LooseTypeMap a
filtered_tm = forall a. Maybe a
Nothing
| Bool
otherwise = forall a. a -> Maybe a
Just ListMap LooseTypeMap a
filtered_tm
where
filtered_tm :: ListMap LooseTypeMap a
filtered_tm = forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f ListMap LooseTypeMap a
tm
tcAppMapToBag :: TcAppMap a -> Bag a
tcAppMapToBag :: forall a. DictMap a -> Bag a
tcAppMapToBag TcAppMap a
m = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldTcAppMap forall a. a -> Bag a -> Bag a
consBag TcAppMap a
m forall a. Bag a
emptyBag
foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap :: forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldTcAppMap a -> b -> b
k TcAppMap a
m b
z = forall elt a. (elt -> a -> a) -> a -> DTyConEnv elt -> a
foldDTyConEnv (forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k) b
z TcAppMap a
m
type DictMap a = TcAppMap a
emptyDictMap :: DictMap a
emptyDictMap :: forall a. DictMap a
emptyDictMap = forall a. DictMap a
emptyTcAppMap
findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict :: forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap a
m CtLoc
loc Class
cls [Type]
tys
| Class -> [Type] -> Bool
hasIPSuperClasses Class
cls [Type]
tys
= forall a. Maybe a
Nothing
| Just {} <- Class -> [Type] -> Maybe FastString
isCallStackPred Class
cls [Type]
tys
, OccurrenceOf {} <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
= forall a. Maybe a
Nothing
| Bool
otherwise
= forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findTcApp DictMap a
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys
findDictsByClass :: DictMap a -> Class -> Bag a
findDictsByClass :: forall a. DictMap a -> Class -> Bag a
findDictsByClass DictMap a
m Class
cls
| Just ListMap LooseTypeMap a
tm <- forall a. DTyConEnv a -> TyCon -> Maybe a
lookupDTyConEnv DictMap a
m (Class -> TyCon
classTyCon Class
cls) = forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM forall a. a -> Bag a -> Bag a
consBag ListMap LooseTypeMap a
tm forall a. Bag a
emptyBag
| Bool
otherwise = forall a. Bag a
emptyBag
delDict :: DictMap a -> Class -> [Type] -> DictMap a
delDict :: forall a. DictMap a -> Class -> [Type] -> DictMap a
delDict DictMap a
m Class
cls [Type]
tys = forall a. TcAppMap a -> TyCon -> [Type] -> TcAppMap a
delTcApp DictMap a
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys
addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
addDict :: forall a. DictMap a -> Class -> [Type] -> a -> DictMap a
addDict DictMap a
m Class
cls [Type]
tys a
item = forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp DictMap a
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys a
item
addDictCt :: DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
addDictCt :: DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
addDictCt DictMap Ct
m Class
cls [Type]
tys Ct
new_ct = forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp DictMap Ct
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys Maybe Ct -> Maybe Ct
xt_ct
where
new_ct_ev :: CtEvidence
new_ct_ev = Ct -> CtEvidence
ctEvidence Ct
new_ct
xt_ct :: Maybe Ct -> Maybe Ct
xt_ct :: Maybe Ct -> Maybe Ct
xt_ct (Just Ct
old_ct)
| CtWanted { ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WOnly } <- CtEvidence
old_ct_ev
, CtDerived {} <- CtEvidence
new_ct_ev
= forall a. a -> Maybe a
Just (Ct
old_ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
old_ct_ev { ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
WDeriv }})
| CtDerived {} <- CtEvidence
old_ct_ev
, CtWanted { ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WOnly } <- CtEvidence
new_ct_ev
= forall a. a -> Maybe a
Just (Ct
new_ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
new_ct_ev { ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
WDeriv }})
where
old_ct_ev :: CtEvidence
old_ct_ev = Ct -> CtEvidence
ctEvidence Ct
old_ct
xt_ct Maybe Ct
_ = forall a. a -> Maybe a
Just Ct
new_ct
addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
addDictsByClass DictMap Ct
m Class
cls Bag Ct
items
= forall a. DTyConEnv a -> TyCon -> a -> DTyConEnv a
extendDTyConEnv DictMap Ct
m (Class -> TyCon
classTyCon Class
cls) (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {m :: * -> *}.
(Key m ~ [Type], TrieMap m) =>
Ct -> m Ct -> m Ct
add forall (m :: * -> *) a. TrieMap m => m a
emptyTM Bag Ct
items)
where
add :: Ct -> m Ct -> m Ct
add ct :: Ct
ct@(CDictCan { cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys }) m Ct
tm = forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
insertTM [Type]
tys Ct
ct m Ct
tm
add Ct
ct m Ct
_ = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"addDictsByClass" (forall a. Outputable a => a -> SDoc
ppr Ct
ct)
filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
filterDicts Ct -> Bool
f DictMap Ct
m = forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap Ct -> Bool
f DictMap Ct
m
partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
partitionDicts Ct -> Bool
f DictMap Ct
m = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldTcAppMap Ct -> (Bag Ct, DictMap Ct) -> (Bag Ct, DictMap Ct)
k DictMap Ct
m (forall a. Bag a
emptyBag, forall a. DictMap a
emptyDicts)
where
k :: Ct -> (Bag Ct, DictMap Ct) -> (Bag Ct, DictMap Ct)
k Ct
ct (Bag Ct
yeses, DictMap Ct
noes) | Ct -> Bool
f Ct
ct = (Ct
ct forall a. a -> Bag a -> Bag a
`consBag` Bag Ct
yeses, DictMap Ct
noes)
| Bool
otherwise = (Bag Ct
yeses, Ct -> DictMap Ct -> DictMap Ct
add Ct
ct DictMap Ct
noes)
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
m
= forall a. DictMap a -> Class -> [Type] -> a -> DictMap a
addDict DictMap Ct
m Class
cls [Type]
tys Ct
ct
add Ct
ct DictMap Ct
_ = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"partitionDicts" (forall a. Outputable a => a -> SDoc
ppr Ct
ct)
dictsToBag :: DictMap a -> Bag a
dictsToBag :: forall a. DictMap a -> Bag a
dictsToBag = forall a. DictMap a -> Bag a
tcAppMapToBag
foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
foldDicts :: forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldDicts = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldTcAppMap
emptyDicts :: DictMap a
emptyDicts :: forall a. DictMap a
emptyDicts = forall a. DictMap a
emptyTcAppMap
type FunEqMap a = TcAppMap a
emptyFunEqs :: TcAppMap a
emptyFunEqs :: forall a. DictMap a
emptyFunEqs = forall a. DictMap a
emptyTcAppMap
findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq :: forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap a
m TyCon
tc [Type]
tys = forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findTcApp FunEqMap a
m TyCon
tc [Type]
tys
findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
findFunEqsByTyCon :: forall a. FunEqMap a -> TyCon -> [a]
findFunEqsByTyCon FunEqMap a
m TyCon
tc
| Just ListMap LooseTypeMap a
tm <- forall a. DTyConEnv a -> TyCon -> Maybe a
lookupDTyConEnv FunEqMap a
m TyCon
tc = forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (:) ListMap LooseTypeMap a
tm []
| Bool
otherwise = []
foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs :: forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldTcAppMap
insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
insertFunEq :: forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertFunEq FunEqMap a
m TyCon
tc [Type]
tys a
val = forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp FunEqMap a
m TyCon
tc [Type]
tys a
val
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 -> 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 -> 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
<$ :: forall a b. a -> TcS b -> TcS a
$c<$ :: forall a b. a -> TcS b -> TcS a
fmap :: forall a b. (a -> b) -> TcS a -> TcS b
$cfmap :: forall a b. (a -> b) -> TcS a -> TcS b
Functor)
mkTcS :: (TcSEnv -> TcM a) -> TcS a
mkTcS :: forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS TcSEnv -> TcM a
f = forall a. (TcSEnv -> TcM a) -> TcS a
TcS (oneShot :: 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 = forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS forall a b. (a -> b) -> a -> b
$ \TcSEnv
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return a
x
<*> :: forall a 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 = forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS forall a b. (a -> b) -> a -> b
$ \TcSEnv
ebs -> do
forall a. TcS a -> TcSEnv -> TcM a
unTcS TcS a
m TcSEnv
ebs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a
r -> forall a. TcS a -> TcSEnv -> TcM a
unTcS (a -> TcS b
k a
r) TcSEnv
ebs)
instance MonadFail TcS where
fail :: forall a. String -> TcS a
fail String
err = forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS forall a b. (a -> b) -> a -> b
$ \TcSEnv
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
instance MonadUnique TcS where
getUniqueSupplyM :: TcS UniqSupply
getUniqueSupplyM = forall a. TcM a -> TcS a
wrapTcS forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
instance HasModule TcS where
getModule :: TcS Module
getModule = forall a. TcM a -> TcS a
wrapTcS forall (m :: * -> *). HasModule m => m Module
getModule
instance MonadThings TcS where
lookupThing :: Name -> TcS TyThing
lookupThing Name
n = forall a. TcM a -> TcS a
wrapTcS (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 = forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS forall a b. (a -> b) -> a -> b
$ \TcSEnv
_env -> TcM a
action
wrapErrTcS :: TcM a -> TcS a
wrapErrTcS :: forall a. TcM a -> TcS a
wrapErrTcS = forall a. TcM a -> TcS a
wrapTcS
wrapWarnTcS :: TcM a -> TcS a
wrapWarnTcS :: forall a. TcM a -> TcS a
wrapWarnTcS = forall a. TcM a -> TcS a
wrapTcS
failTcS, panicTcS :: SDoc -> TcS a
warnTcS :: WarningFlag -> SDoc -> TcS ()
addErrTcS :: SDoc -> TcS ()
failTcS :: forall a. SDoc -> TcS a
failTcS = forall a. TcM a -> TcS a
wrapTcS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SDoc -> TcRn a
TcM.failWith
warnTcS :: WarningFlag -> SDoc -> TcS ()
warnTcS WarningFlag
flag = forall a. TcM a -> TcS a
wrapTcS forall b c a. (b -> c) -> (a -> b) -> a -> c
. WarnReason -> SDoc -> TcM ()
TcM.addWarn (WarningFlag -> WarnReason
Reason WarningFlag
flag)
addErrTcS :: SDoc -> TcS ()
addErrTcS = forall a. TcM a -> TcS a
wrapTcS forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> TcM ()
TcM.addErr
panicTcS :: forall a. SDoc -> TcS a
panicTcS SDoc
doc = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"GHC.Tc.Solver.Canonical" SDoc
doc
traceTcS :: String -> SDoc -> TcS ()
traceTcS :: String -> SDoc -> TcS ()
traceTcS String
herald SDoc
doc = 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 TcPluginM a
m = forall a. TcM a -> TcS a
wrapTcS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TcPluginM a -> EvBindsVar -> TcM a
runTcPluginM TcPluginM a
m forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TcS EvBindsVar
getTcEvBindsVar
instance HasDynFlags TcS where
getDynFlags :: TcS DynFlags
getDynFlags = forall a. TcM a -> TcS a
wrapTcS forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS = forall a. TcM a -> TcS a
wrapTcS TcRn GlobalRdrEnv
TcM.getGlobalRdrEnv
bumpStepCountTcS :: TcS ()
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS forall a b. (a -> b) -> a -> b
$ \TcSEnv
env ->
do { let ref :: IORef Int
ref = TcSEnv -> IORef Int
tcs_count TcSEnv
env
; Int
n <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
ref
; forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef Int
ref (Int
nforall a. Num a => a -> a -> a
+Int
1) }
csTraceTcS :: SDoc -> TcS ()
csTraceTcS :: SDoc -> TcS ()
csTraceTcS SDoc
doc
= forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ TcM SDoc -> TcM ()
csTraceTcM (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
= forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS forall a b. (a -> b) -> a -> b
$ \TcSEnv
env -> TcM SDoc -> TcM ()
csTraceTcM forall a b. (a -> b) -> a -> b
$
do { Int
n <- 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
; forall (m :: * -> *) a. Monad m => a -> m a
return (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Step" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n
SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
brackets (String -> SDoc
text String
"l:" SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl SDoc -> SDoc -> SDoc
<> SDoc
comma SDoc -> SDoc -> SDoc
<>
String -> SDoc
text String
"d:" SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr (CtLoc -> SubGoalDepth
ctLocDepth (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev)))
SDoc -> SDoc -> SDoc
<+> SDoc
doc SDoc -> SDoc -> SDoc
<> SDoc
colon)
Int
4 (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 { DynFlags
dflags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( DumpFlag -> DynFlags -> Bool
dopt DumpFlag
Opt_D_dump_cs_trace DynFlags
dflags
Bool -> Bool -> Bool
|| DumpFlag -> DynFlags -> Bool
dopt DumpFlag
Opt_D_dump_tc_trace DynFlags
dflags )
( 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 <- 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
; forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, EvBindMap
ev_binds) }
runTcSDeriveds :: TcS a -> TcM a
runTcSDeriveds :: forall a. TcS a -> TcM a
runTcSDeriveds TcS a
tcs
= do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
; forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds 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
; 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
forall a. Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
False EvBindsVar
ev_binds_var forall a b. (a -> b) -> a -> b
$ do
InertSet -> TcS ()
setTcSInerts InertSet
inerts
a
a <- TcS a
tcs
InertSet
new_inerts <- TcS InertSet
getTcSInerts
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 = forall a. Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
True
runTcSWithEvBinds' :: Bool
-> EvBindsVar
-> TcS a
-> TcM a
runTcSWithEvBinds' :: forall a. Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
restore_cycles EvBindsVar
ev_binds_var TcS a
tcs
= do { IORef Int
unified_var <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
; IORef Int
step_count <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
; IORef InertSet
inert_var <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
emptyInert
; IORef WorkList
wl_var <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
; IORef (Maybe TcLevel)
unif_lvl_var <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef 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_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
wl_var }
; a
res <- forall a. TcS a -> TcSEnv -> TcM a
unTcS TcS a
tcs TcSEnv
env
; Int
count <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
step_count
; forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
count forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
TcM SDoc -> TcM ()
csTraceTcM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (String -> SDoc
text String
"Constraint solver steps =" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
count)
; forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
restore_cycles forall a b. (a -> b) -> a -> b
$
do { InertSet
inert_set <- 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
; 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)
= forall a. (TcSEnv -> TcM a) -> TcS a
TcS forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env -> TcSEnv -> TcM a
thing_inside (TcSEnv
env { tcs_ev_binds :: EvBindsVar
tcs_ev_binds = EvBindsVar
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)
= forall a. (TcSEnv -> TcM a) -> TcS a
TcS 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
} ->
do { InertSet
inerts <- 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 :: CycleBreakerVarStack
inert_cycle_breakers = CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack
(InertSet -> CycleBreakerVarStack
inert_cycle_breakers InertSet
inerts)
, inert_cans :: InertCans
inert_cans = (InertSet -> InertCans
inert_cans InertSet
inerts)
{ inert_given_eqs :: Bool
inert_given_eqs = Bool
False } }
; IORef InertSet
new_inert_var <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
nest_inert
; IORef WorkList
new_wl_var <- 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_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
new_wl_var }
; a
res <- forall a. TcLevel -> TcM a -> TcM a
TcM.setTcLevel TcLevel
inner_tclvl forall a b. (a -> b) -> a -> b
$
TcSEnv -> TcM a
thing_inside TcSEnv
nest_env
; InertSet
out_inert_set <- 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
; 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)
= forall a. (TcSEnv -> TcM a) -> TcS a
TcS 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 <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
inerts_var
; IORef InertSet
new_inert_var <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
inerts
; IORef WorkList
new_wl_var <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
; let nest_env :: TcSEnv
nest_env = TcSEnv
env { tcs_inerts :: IORef InertSet
tcs_inerts = IORef InertSet
new_inert_var
, tcs_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
new_wl_var }
; a
res <- TcSEnv -> TcM a
thing_inside TcSEnv
nest_env
; InertSet
new_inerts <- 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 :: DictMap Ct
inert_safehask = InertCans -> DictMap Ct
inert_safehask InertCans
new_ic }
; forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef InertSet
inerts_var
(InertSet
inerts { inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = InertSet -> DictMap CtEvidence
inert_solved_dicts InertSet
new_inerts
, inert_cans :: InertCans
inert_cans = InertCans
nxt_ic })
; forall (m :: * -> *) a. Monad m => a -> m a
return a
res }
emitImplicationTcS :: TcLevel -> SkolemInfo
-> [TcTyVar]
-> [EvVar]
-> Cts
-> TcS TcEvBinds
emitImplicationTcS :: TcLevel
-> SkolemInfo -> [TcTyVar] -> [TcTyVar] -> Bag Ct -> TcS TcEvBinds
emitImplicationTcS TcLevel
new_tclvl SkolemInfo
skol_info [TcTyVar]
skol_tvs [TcTyVar]
givens Bag Ct
wanteds
= do { let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple :: Bag Ct
wc_simple = Bag Ct
wanteds }
; Implication
imp <- forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$
do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
; Implication
imp <- TcM Implication
TcM.newImplication
; forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
imp { ic_tclvl :: TcLevel
ic_tclvl = TcLevel
new_tclvl
, ic_skols :: [TcTyVar]
ic_skols = [TcTyVar]
skol_tvs
, ic_given :: [TcTyVar]
ic_given = [TcTyVar]
givens
, ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wc
, ic_binds :: EvBindsVar
ic_binds = EvBindsVar
ev_binds_var
, ic_info :: SkolemInfo
ic_info = SkolemInfo
skol_info }) }
; Implication -> TcS ()
emitImplication Implication
imp
; forall (m :: * -> *) a. Monad m => a -> m a
return (EvBindsVar -> TcEvBinds
TcEvBinds (Implication -> EvBindsVar
ic_binds Implication
imp)) }
emitTvImplicationTcS :: TcLevel -> SkolemInfo
-> [TcTyVar]
-> Cts
-> TcS ()
emitTvImplicationTcS :: TcLevel -> SkolemInfo -> [TcTyVar] -> Bag Ct -> TcS ()
emitTvImplicationTcS TcLevel
new_tclvl SkolemInfo
skol_info [TcTyVar]
skol_tvs Bag Ct
wanteds
= do { let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple :: Bag Ct
wc_simple = Bag Ct
wanteds }
; Implication
imp <- forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$
do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
; Implication
imp <- TcM Implication
TcM.newImplication
; forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
imp { ic_tclvl :: TcLevel
ic_tclvl = TcLevel
new_tclvl
, ic_skols :: [TcTyVar]
ic_skols = [TcTyVar]
skol_tvs
, ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wc
, ic_binds :: EvBindsVar
ic_binds = EvBindsVar
ev_binds_var
, ic_info :: SkolemInfo
ic_info = SkolemInfo
skol_info }) }
; Implication -> TcS ()
emitImplication Implication
imp }
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef = forall a. (TcSEnv -> TcM a) -> TcS a
TcS (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef InertSet
tcs_inerts)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef = forall a. (TcSEnv -> TcM a) -> TcS a
TcS (forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. TcRef a -> TcS a
readTcRef
setTcSInerts :: InertSet -> TcS ()
setTcSInerts :: InertSet -> TcS ()
setTcSInerts InertSet
ics = do { IORef InertSet
r <- TcS (IORef InertSet)
getTcSInertsRef; 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 <- forall a. TcRef a -> TcS a
readTcRef IORef WorkList
wl_var
; 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)
= forall a. (TcSEnv -> TcM a) -> TcS a
TcS (\TcSEnv
env -> 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
; forall a. TcRef a -> (a -> a) -> TcS ()
updTcRef IORef WorkList
wl_var WorkList -> WorkList
f }
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence]
evs
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CtEvidence]
evs
= forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= [Ct] -> TcS ()
emitWork (forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
evs)
emitWork :: [Ct] -> TcS ()
emitWork :: [Ct] -> TcS ()
emitWork [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
emitWork [Ct]
cts
= do { String -> SDoc -> TcS ()
traceTcS String
"Emitting fresh work" ([SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map 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 = forall a. TcM a -> TcS a
wrapTcS (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 = forall a. TcM a -> TcS a
wrapTcS (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 = forall a. TcM a -> TcS a
wrapTcS (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 = forall a. TcM a -> TcS a
wrapTcS (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 = forall a. (TcSEnv -> TcM a) -> TcS a
TcS (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> EvBindsVar
tcs_ev_binds)
getTcLevel :: TcS TcLevel
getTcLevel :: TcS TcLevel
getTcLevel = forall a. TcM a -> TcS a
wrapTcS TcM TcLevel
TcM.getTcLevel
getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
getTcEvTyCoVars :: EvBindsVar -> TcS VarSet
getTcEvTyCoVars EvBindsVar
ev_binds_var
= forall a. TcM a -> TcS a
wrapTcS 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
= forall a. TcM a -> TcS a
wrapTcS 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
= forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ EvBindsVar -> EvBindMap -> TcM ()
TcM.setTcEvBindsMap EvBindsVar
ev_binds_var EvBindMap
binds
unifyTyVar :: TcTyVar -> TcType -> TcS ()
unifyTyVar :: TcTyVar -> Type -> TcS ()
unifyTyVar TcTyVar
tv Type
ty
= ASSERT2( isMetaTyVar tv, ppr tv )
forall a. (TcSEnv -> TcM a) -> TcS a
TcS forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env ->
do { String -> SDoc -> TcM ()
TcM.traceTc String
"unifyTyVar" (forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
ty)
; TcTyVar -> Type -> TcM ()
TcM.writeMetaTyVar TcTyVar
tv Type
ty
; forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
TcM.updTcRef (TcSEnv -> IORef Int
tcs_unified TcSEnv
env) (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)
= forall a. (TcSEnv -> TcM a) -> TcS a
TcS forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env ->
do { IORef Int
inner_unified <- 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 :: IORef Int
tcs_unified = IORef Int
inner_unified })
; Int
n_unifs <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
inner_unified
; forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
TcM.updTcRef (TcSEnv -> IORef Int
tcs_unified TcSEnv
env) (forall a. Num a => a -> a -> a
+ Int
n_unifs)
; 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
text String
"TouchableSameLevel"
ppr (TouchableOuterLevel [TcTyVar]
tvs TcLevel
lvl) = String -> SDoc
text String
"TouchableOuterLevel" SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
parens (forall a. Outputable a => a -> SDoc
ppr TcLevel
lvl SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
tvs)
ppr TouchabilityTestResult
Untouchable = String -> SDoc
text String
"Untouchable"
touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS TouchabilityTestResult
touchabilityTest :: CtFlavour -> TcTyVar -> Type -> TcS TouchabilityTestResult
touchabilityTest CtFlavour
flav TcTyVar
tv1 Type
rhs
| CtFlavour
flav 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 } <- TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv1
, MetaInfo -> Type -> Bool
canSolveByUnification MetaInfo
info Type
rhs
= do { TcLevel
ambient_lvl <- TcS TcLevel
getTcLevel
; TcLevel
given_eq_lvl <- TcS TcLevel
getInnermostGivenEqLevel
; if | TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
ambient_lvl
-> forall (m :: * -> *) a. Monad m => a -> m a
return TouchabilityTestResult
TouchableSameLevel
| TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcLevel
given_eq_lvl
, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcLevel -> TcTyVar -> Bool
does_not_escape TcLevel
tv_lvl) [TcTyVar]
free_skols
-> forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar] -> TcLevel -> TouchabilityTestResult
TouchableOuterLevel [TcTyVar]
free_metas TcLevel
tv_lvl)
| Bool
otherwise
-> forall (m :: * -> *) a. Monad m => a -> m a
return TouchabilityTestResult
Untouchable }
| Bool
otherwise
= forall (m :: * -> *) a. Monad m => a -> m a
return TouchabilityTestResult
Untouchable
where
([TcTyVar]
free_metas, [TcTyVar]
free_skols) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition TcTyVar -> Bool
isPromotableMetaTyVar forall a b. (a -> b) -> a -> b
$
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet forall a b. (a -> b) -> a -> b
$
Type -> VarSet
tyCoVarsOfType Type
rhs
does_not_escape :: TcLevel -> TcTyVar -> Bool
does_not_escape TcLevel
tv_lvl TcTyVar
fv
| TcTyVar -> Bool
isTyVar TcTyVar
fv = TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
fv
| Bool
otherwise = Bool
True
getDefaultInfo :: TcS ([Type], (Bool, Bool))
getDefaultInfo :: TcS ([Type], (Bool, Bool))
getDefaultInfo = forall a. TcM a -> TcS a
wrapTcS TcM ([Type], (Bool, Bool))
TcM.tcGetDefaultTys
getInstEnvs :: TcS InstEnvs
getInstEnvs :: TcS InstEnvs
getInstEnvs = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ TcM InstEnvs
TcM.tcGetInstEnvs
getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ TcM (FamInstEnv, FamInstEnv)
FamInst.tcGetFamInstEnvs
getTopEnv :: TcS HscEnv
getTopEnv :: TcS HscEnv
getTopEnv = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ forall gbl lcl. TcRnIf gbl lcl HscEnv
TcM.getTopEnv
getGblEnv :: TcS TcGblEnv
getGblEnv :: TcS TcGblEnv
getGblEnv = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ forall gbl lcl. TcRnIf gbl lcl gbl
TcM.getGblEnv
getLclEnv :: TcS TcLclEnv
getLclEnv :: TcS TcLclEnv
getLclEnv = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ forall gbl lcl. TcRnIf gbl lcl lcl
TcM.getLclEnv
tcLookupClass :: Name -> TcS Class
tcLookupClass :: Name -> TcS Class
tcLookupClass Name
c = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ Name -> TcM Class
TcM.tcLookupClass Name
c
tcLookupId :: Name -> TcS Id
tcLookupId :: Name -> TcS TcTyVar
tcLookupId Name
n = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ Name -> TcM TcTyVar
TcM.tcLookupId Name
n
addUsedGREs :: [GlobalRdrElt] -> TcS ()
addUsedGREs :: [GlobalRdrElt] -> TcS ()
addUsedGREs [GlobalRdrElt]
gres = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ [GlobalRdrElt] -> TcM ()
TcM.addUsedGREs [GlobalRdrElt]
gres
addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
addUsedGRE Bool
warn_if_deprec GlobalRdrElt
gre = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ Bool -> GlobalRdrElt -> TcM ()
TcM.addUsedGRE Bool
warn_if_deprec GlobalRdrElt
gre
keepAlive :: Name -> TcS ()
keepAlive :: Name -> TcS ()
keepAlive = forall a. TcM a -> TcS a
wrapTcS forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM ()
TcM.keepAlive
checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
checkWellStagedDFun :: CtLoc -> InstanceWhat -> Type -> TcS ()
checkWellStagedDFun CtLoc
loc InstanceWhat
what Type
pred
| TopLevInstance { iw_dfun_id :: InstanceWhat -> TcTyVar
iw_dfun_id = TcTyVar
dfun_id } <- InstanceWhat
what
, let bind_lvl :: Int
bind_lvl = TcTyVar -> Int
TcM.topIdLvl TcTyVar
dfun_id
, Int
bind_lvl forall a. Ord a => a -> a -> Bool
> Int
impLevel
= forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ forall a. CtLoc -> TcM a -> TcM a
TcM.setCtLocM CtLoc
loc 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) }
| Bool
otherwise
= forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
pp_thing :: SDoc
pp_thing = String -> SDoc
text String
"instance for" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (forall a. Outputable a => a -> SDoc
ppr Type
pred)
pprEq :: TcType -> TcType -> SDoc
pprEq :: Type -> Type -> SDoc
pprEq Type
ty1 Type
ty2 = Type -> SDoc
pprParendType Type
ty1 SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> Type -> SDoc
pprParendType Type
ty2
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe TcTyVar
tv = forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM (Maybe Type)
TcM.isFilledMetaTyVar_maybe TcTyVar
tv)
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar TcTyVar
tv = forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM Bool
TcM.isFilledMetaTyVar TcTyVar
tv)
zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
zonkTyCoVarsAndFV :: VarSet -> TcS VarSet
zonkTyCoVarsAndFV VarSet
tvs = forall a. TcM a -> TcS a
wrapTcS (VarSet -> TcM VarSet
TcM.zonkTyCoVarsAndFV VarSet
tvs)
zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
zonkTyCoVarsAndFVList :: [TcTyVar] -> TcS [TcTyVar]
zonkTyCoVarsAndFVList [TcTyVar]
tvs = forall a. TcM a -> TcS a
wrapTcS ([TcTyVar] -> TcM [TcTyVar]
TcM.zonkTyCoVarsAndFVList [TcTyVar]
tvs)
zonkCo :: Coercion -> TcS Coercion
zonkCo :: Coercion -> TcS Coercion
zonkCo = forall a. TcM a -> TcS a
wrapTcS 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 = 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 = forall a. TcM a -> TcS a
wrapTcS ([Type] -> TcM [Type]
TcM.zonkTcTypes [Type]
tys)
zonkTcTyVar :: TcTyVar -> TcS TcType
zonkTcTyVar :: TcTyVar -> TcS Type
zonkTcTyVar TcTyVar
tv = forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM Type
TcM.zonkTcTyVar TcTyVar
tv)
zonkSimples :: Cts -> TcS Cts
zonkSimples :: Bag Ct -> TcS (Bag Ct)
zonkSimples Bag Ct
cts = forall a. TcM a -> TcS a
wrapTcS (Bag Ct -> TcM (Bag Ct)
TcM.zonkSimples Bag Ct
cts)
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC WantedConstraints
wc = forall a. TcM a -> TcS a
wrapTcS (WantedConstraints -> TcM WantedConstraints
TcM.zonkWC WantedConstraints
wc)
zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
zonkTyCoVarKind :: TcTyVar -> TcS TcTyVar
zonkTyCoVarKind TcTyVar
tv = forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM TcTyVar
TcM.zonkTyCoVarKind TcTyVar
tv)
pprKicked :: Int -> SDoc
pprKicked :: Int -> SDoc
pprKicked Int
0 = SDoc
empty
pprKicked Int
n = SDoc -> SDoc
parens (Int -> SDoc
int Int
n SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"kicked out")
resetUnificationFlag :: TcS Bool
resetUnificationFlag :: TcS Bool
resetUnificationFlag
= forall a. (TcSEnv -> TcM a) -> TcS a
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
; TcLevel
ambient_lvl <- TcM TcLevel
TcM.getTcLevel
; Maybe TcLevel
mb_lvl <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef (Maybe TcLevel)
ref
; String -> SDoc -> TcM ()
TcM.traceTc String
"resetUnificationFlag" forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"ambient:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcLevel
ambient_lvl
, String -> SDoc
text String
"unif_lvl:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Maybe TcLevel
mb_lvl ]
; case Maybe TcLevel
mb_lvl of
Maybe TcLevel
Nothing -> 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
-> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise
-> do { forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef (Maybe TcLevel)
ref forall a. Maybe a
Nothing
; forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True } }
setUnificationFlag :: TcLevel -> TcS ()
setUnificationFlag :: TcLevel -> TcS ()
setUnificationFlag TcLevel
lvl
= forall a. (TcSEnv -> TcM a) -> TcS a
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 <- 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
-> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe TcLevel
_ -> forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef (Maybe TcLevel)
ref (forall a. a -> Maybe a
Just TcLevel
lvl) }
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
instDFunType :: TcTyVar -> [Maybe Type] -> TcS ([Type], [Type])
instDFunType TcTyVar
dfun_id [Maybe Type]
inst_tys
= forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ TcTyVar -> [Maybe Type] -> TcM ([Type], [Type])
TcM.instDFunType TcTyVar
dfun_id [Maybe Type]
inst_tys
newFlexiTcSTy :: Kind -> TcS TcType
newFlexiTcSTy :: Type -> TcS Type
newFlexiTcSTy Type
knd = forall a. TcM a -> TcS a
wrapTcS (Type -> TcM Type
TcM.newFlexiTyVarTy Type
knd)
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar TcTyVar
tv = forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM TcTyVar
TcM.cloneMetaTyVar TcTyVar
tv)
instFlexi :: [TKVar] -> TcS TCvSubst
instFlexi :: [TcTyVar] -> TcS TCvSubst
instFlexi = TCvSubst -> [TcTyVar] -> TcS TCvSubst
instFlexiX TCvSubst
emptyTCvSubst
instFlexiX :: TCvSubst -> [TKVar] -> TcS TCvSubst
instFlexiX :: TCvSubst -> [TcTyVar] -> TcS TCvSubst
instFlexiX TCvSubst
subst [TcTyVar]
tvs
= forall a. TcM a -> TcS a
wrapTcS (forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM TCvSubst -> TcTyVar -> TcM TCvSubst
instFlexiHelper TCvSubst
subst [TcTyVar]
tvs)
instFlexiHelper :: TCvSubst -> TKVar -> TcM TCvSubst
instFlexiHelper :: TCvSubst -> TcTyVar -> TcM TCvSubst
instFlexiHelper TCvSubst
subst TcTyVar
tv
= do { Unique
uniq <- 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 (TcTyVar -> Name
tyVarName TcTyVar
tv) Unique
uniq
kind :: Type
kind = TCvSubst -> Type -> Type
substTyUnchecked TCvSubst
subst (TcTyVar -> Type
tyVarKind TcTyVar
tv)
ty' :: Type
ty' = TcTyVar -> Type
mkTyVarTy (Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
name Type
kind TcTyVarDetails
details)
; String -> SDoc -> TcM ()
TcM.traceTc String
"instFlexi" (forall a. Outputable a => a -> SDoc
ppr Type
ty')
; forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst -> TcTyVar -> Type -> TCvSubst
extendTvSubst TCvSubst
subst TcTyVar
tv Type
ty') }
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
= 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 :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX :: TCvSubst -> [TcTyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX TCvSubst
subst [TcTyVar]
tvs = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ TCvSubst -> [TcTyVar] -> TcM (TCvSubst, [TcTyVar])
TcM.tcInstSkolTyVarsX TCvSubst
subst [TcTyVar]
tvs
data MaybeNew = Fresh CtEvidence | Cached EvExpr
isFresh :: MaybeNew -> Bool
isFresh :: MaybeNew -> Bool
isFresh (Fresh {}) = Bool
True
isFresh (Cached {}) = Bool
False
freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals [MaybeNew]
mns = [ CtEvidence
ctev | Fresh CtEvidence
ctev <- [MaybeNew]
mns ]
getEvExpr :: MaybeNew -> EvExpr
getEvExpr :: MaybeNew -> EvExpr
getEvExpr (Fresh CtEvidence
ctev) = 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
; forall a. TcM a -> TcS a
wrapTcS 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
; forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$
do { VarSet
tcvs <- 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
; forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef VarSet
ref VarSet
tcvs' } }
setWantedEq :: TcEvDest -> Coercion -> TcS ()
setWantedEq :: TcEvDest -> Coercion -> TcS ()
setWantedEq (HoleDest CoercionHole
hole) Coercion
co
= do { VarSet -> TcS ()
useVars (Coercion -> VarSet
coVarsOfCo Coercion
co)
; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole Coercion
co }
setWantedEq (EvVarDest TcTyVar
ev) Coercion
_ = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setWantedEq" (forall a. Outputable a => a -> SDoc
ppr TcTyVar
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 :: TcTyVar
co_var = CoercionHole -> TcTyVar
coHoleCoVar CoercionHole
hole
; EvBind -> TcS ()
setEvBind (TcTyVar -> EvTerm -> EvBind
mkWantedEvBind TcTyVar
co_var EvTerm
tm)
; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole (TcTyVar -> Coercion
mkTcCoVarCo TcTyVar
co_var) }
setWantedEvTerm (EvVarDest TcTyVar
ev_id) EvTerm
tm
= EvBind -> TcS ()
setEvBind (TcTyVar -> EvTerm -> EvBind
mkWantedEvBind TcTyVar
ev_id EvTerm
tm)
fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole Coercion
co
= do { forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ CoercionHole -> Coercion -> TcM ()
TcM.fillCoercionHole CoercionHole
hole Coercion
co
; CoercionHole -> Coercion -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole Coercion
co }
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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds = forall a. TcM a -> TcS a
wrapTcS TcM EvBindsVar
TcM.newTcEvBinds
newNoTcEvBinds :: TcS EvBindsVar
newNoTcEvBinds :: TcS EvBindsVar
newNoTcEvBinds = forall a. TcM a -> TcS a
wrapTcS TcM EvBindsVar
TcM.newNoTcEvBinds
newEvVar :: TcPredType -> TcS EvVar
newEvVar :: Type -> TcS TcTyVar
newEvVar Type
pred = forall a. TcM a -> TcS a
wrapTcS (forall gbl lcl. Type -> TcRnIf gbl lcl TcTyVar
TcM.newEvVar Type
pred)
newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar :: CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (Type
pred, EvTerm
rhs)
= do { TcTyVar
new_ev <- Type -> EvTerm -> TcS TcTyVar
newBoundEvVarId Type
pred EvTerm
rhs
; forall (m :: * -> *) a. Monad m => a -> m a
return (CtGiven { ctev_pred :: Type
ctev_pred = Type
pred, ctev_evar :: TcTyVar
ctev_evar = TcTyVar
new_ev, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }) }
newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
newBoundEvVarId :: Type -> EvTerm -> TcS TcTyVar
newBoundEvVarId Type
pred EvTerm
rhs
= do { TcTyVar
new_ev <- Type -> TcS TcTyVar
newEvVar Type
pred
; EvBind -> TcS ()
setEvBind (TcTyVar -> EvTerm -> EvBind
mkGivenEvBind TcTyVar
new_ev EvTerm
rhs)
; forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
new_ev }
newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars :: CtLoc -> [(Type, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars CtLoc
loc [(Type, EvTerm)]
pts = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc) [(Type, EvTerm)]
pts
emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
emitNewWantedEq :: CtLoc -> Role -> Type -> Type -> TcS Coercion
emitNewWantedEq CtLoc
loc Role
role Type
ty1 Type
ty2
= do { (CtEvidence
ev, Coercion
co) <- CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc Role
role Type
ty1 Type
ty2
; (WorkList -> WorkList) -> TcS ()
updWorkListTcS (Ct -> WorkList -> WorkList
extendWorkListEq (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev))
; forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co }
newWantedEq :: CtLoc -> Role -> TcType -> TcType
-> TcS (CtEvidence, Coercion)
newWantedEq :: CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq = ShadowInfo
-> CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq_SI ShadowInfo
WDeriv
newWantedEq_SI :: ShadowInfo -> CtLoc -> Role
-> TcType -> TcType
-> TcS (CtEvidence, Coercion)
newWantedEq_SI :: ShadowInfo
-> CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq_SI ShadowInfo
si CtLoc
loc Role
role Type
ty1 Type
ty2
= do { CoercionHole
hole <- forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ Type -> TcM CoercionHole
TcM.newCoercionHole Type
pty
; String -> SDoc -> TcS ()
traceTcS String
"Emitting new coercion hole" (forall a. Outputable a => a -> SDoc
ppr CoercionHole
hole SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
pty)
; 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_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
si
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc}
, CoercionHole -> Coercion
mkHoleCo CoercionHole
hole ) }
where
pty :: Type
pty = Role -> Type -> Type -> Type
mkPrimEqPredRole Role
role Type
ty1 Type
ty2
newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC :: CtLoc -> Type -> TcS CtEvidence
newWantedEvVarNC = ShadowInfo -> CtLoc -> Type -> TcS CtEvidence
newWantedEvVarNC_SI ShadowInfo
WDeriv
newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> Type -> TcS CtEvidence
newWantedEvVarNC_SI ShadowInfo
si CtLoc
loc Type
pty
= do { TcTyVar
new_ev <- Type -> TcS TcTyVar
newEvVar Type
pty
; String -> SDoc -> TcS ()
traceTcS String
"Emitting new wanted" (forall a. Outputable a => a -> SDoc
ppr TcTyVar
new_ev SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
pty SDoc -> SDoc -> SDoc
$$
CtLoc -> SDoc
pprCtLoc CtLoc
loc)
; forall (m :: * -> *) a. Monad m => a -> m a
return (CtWanted { ctev_pred :: Type
ctev_pred = Type
pty, ctev_dest :: TcEvDest
ctev_dest = TcTyVar -> TcEvDest
EvVarDest TcTyVar
new_ev
, ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
si
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc })}
newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar :: CtLoc -> Type -> TcS MaybeNew
newWantedEvVar = ShadowInfo -> CtLoc -> Type -> TcS MaybeNew
newWantedEvVar_SI ShadowInfo
WDeriv
newWantedEvVar_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar_SI :: ShadowInfo -> CtLoc -> Type -> TcS MaybeNew
newWantedEvVar_SI ShadowInfo
si CtLoc
loc Type
pty
= do { Maybe CtEvidence
mb_ct <- CtLoc -> Type -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc Type
pty
; case Maybe CtEvidence
mb_ct of
Just CtEvidence
ctev
| Bool -> Bool
not (CtEvidence -> Bool
isDerived CtEvidence
ctev)
-> do { String -> SDoc -> TcS ()
traceTcS String
"newWantedEvVar/cache hit" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ EvExpr -> MaybeNew
Cached (CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev) }
Maybe CtEvidence
_ -> do { CtEvidence
ctev <- ShadowInfo -> CtLoc -> Type -> TcS CtEvidence
newWantedEvVarNC_SI ShadowInfo
si CtLoc
loc Type
pty
; forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> MaybeNew
Fresh CtEvidence
ctev) } }
newWanted :: CtLoc -> PredType -> TcS MaybeNew
newWanted :: CtLoc -> Type -> TcS MaybeNew
newWanted = ShadowInfo -> CtLoc -> Type -> TcS MaybeNew
newWanted_SI ShadowInfo
WDeriv
newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew
newWanted_SI :: ShadowInfo -> CtLoc -> Type -> TcS MaybeNew
newWanted_SI ShadowInfo
si CtLoc
loc Type
pty
| Just (Role
role, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pty
= CtEvidence -> MaybeNew
Fresh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ShadowInfo
-> CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq_SI ShadowInfo
si CtLoc
loc Role
role Type
ty1 Type
ty2
| Bool
otherwise
= ShadowInfo -> CtLoc -> Type -> TcS MaybeNew
newWantedEvVar_SI ShadowInfo
si CtLoc
loc Type
pty
newWantedNC :: CtLoc -> PredType -> TcS CtEvidence
newWantedNC :: CtLoc -> Type -> TcS CtEvidence
newWantedNC CtLoc
loc Type
pty
| Just (Role
role, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pty
= forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc Role
role Type
ty1 Type
ty2
| Bool
otherwise
= CtLoc -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc Type
pty
emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
emitNewDeriveds :: CtLoc -> [Type] -> TcS ()
emitNewDeriveds CtLoc
loc [Type]
preds
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
preds
= forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { [CtEvidence]
evs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CtLoc -> Type -> TcS CtEvidence
newDerivedNC CtLoc
loc) [Type]
preds
; String -> SDoc -> TcS ()
traceTcS String
"Emitting new deriveds" (forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
evs)
; (WorkList -> WorkList) -> TcS ()
updWorkListTcS ([CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds [CtEvidence]
evs) }
emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
emitNewDerivedEq :: CtLoc -> Role -> Type -> Type -> TcS ()
emitNewDerivedEq CtLoc
loc Role
role Type
ty1 Type
ty2
= do { CtEvidence
ev <- CtLoc -> Type -> TcS CtEvidence
newDerivedNC CtLoc
loc (Role -> Type -> Type -> Type
mkPrimEqPredRole Role
role Type
ty1 Type
ty2)
; String -> SDoc -> TcS ()
traceTcS String
"Emitting new derived equality" (forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
$$ CtLoc -> SDoc
pprCtLoc CtLoc
loc)
; (WorkList -> WorkList) -> TcS ()
updWorkListTcS (Ct -> WorkList -> WorkList
extendWorkListEq (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev)) }
newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
newDerivedNC :: CtLoc -> Type -> TcS CtEvidence
newDerivedNC CtLoc
loc Type
pred
= forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CtDerived { ctev_pred :: Type
ctev_pred = Type
pred, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }
checkReductionDepth :: CtLoc -> TcType
-> TcS ()
checkReductionDepth :: CtLoc -> Type -> TcS ()
checkReductionDepth CtLoc
loc Type
ty
= do { DynFlags
dflags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DynFlags -> SubGoalDepth -> Bool
subGoalDepthExceeded DynFlags
dflags (CtLoc -> SubGoalDepth
ctLocDepth CtLoc
loc)) forall a b. (a -> b) -> a -> b
$
forall a. TcM a -> TcS a
wrapErrTcS forall a b. (a -> b) -> a -> b
$
forall a. CtLoc -> Type -> TcM a
solverDepthErrorTcS CtLoc
loc Type
ty }
matchFam :: TyCon -> [Type] -> TcS (Maybe (CoercionN, TcType))
matchFam :: TyCon -> [Type] -> TcS (Maybe (Coercion, Type))
matchFam TyCon
tycon [Type]
args = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Coercion -> Coercion
mkTcSymCo)) forall a b. (a -> b) -> a -> b
$ forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> TcM (Maybe (Coercion, Type))
matchFamTcM TyCon
tycon [Type]
args
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (CoercionN, TcType))
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, Type))
matchFamTcM TyCon
tycon [Type]
args
= do { (FamInstEnv, FamInstEnv)
fam_envs <- TcM (FamInstEnv, FamInstEnv)
FamInst.tcGetFamInstEnvs
; let match_fam_result :: Maybe (Coercion, Type)
match_fam_result
= (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
fam_envs Role
Nominal TyCon
tycon [Type]
args
; String -> SDoc -> TcM ()
TcM.traceTc String
"matchFamTcM" forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Matching:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
tycon [Type]
args)
, forall {a} {a}.
(Outputable a, Outputable a) =>
Maybe (a, a) -> SDoc
ppr_res Maybe (Coercion, Type)
match_fam_result ]
; forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Coercion, Type)
match_fam_result }
where
ppr_res :: Maybe (a, a) -> SDoc
ppr_res Maybe (a, a)
Nothing = String -> SDoc
text String
"Match failed"
ppr_res (Just (a
co,a
ty)) = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Match succeeded:")
Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Rewrites to:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr a
ty
, String -> SDoc
text String
"Coercion:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr a
co ])
breakTyEqCycle_maybe :: CtEvidence
-> CheckTyEqResult
-> CanEqLHS
-> TcType
-> TcS (Maybe (CoercionN, TcType))
breakTyEqCycle_maybe :: CtEvidence
-> CheckTyEqResult
-> CanEqLHS
-> Type
-> TcS (Maybe (Coercion, Type))
breakTyEqCycle_maybe (CtLoc -> CtOrigin
ctLocOrigin forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> CtLoc
ctEvLoc -> CycleBreakerOrigin CtOrigin
_) CheckTyEqResult
_ CanEqLHS
_ Type
_
= forall (m :: * -> *) a. Monad m => a -> m a
return 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 { Bool
should_break <- TcS Bool
final_check
; if Bool
should_break then do { (Coercion
co, Type
new_rhs) <- Type -> TcS (Coercion, Type)
go Type
rhs
; forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Coercion
co, Type
new_rhs)) }
else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing }
where
flavour :: CtFlavour
flavour = CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev
eq_rel :: EqRel
eq_rel = CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev
final_check :: TcS Bool
final_check
| CtFlavour
Given <- CtFlavour
flavour
= forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
| CtFlavour -> Bool
ctFlavourContainsDerived CtFlavour
flavour
, TyVarLHS TcTyVar
lhs_tv <- CanEqLHS
lhs
= do { TouchabilityTestResult
result <- CtFlavour -> TcTyVar -> Type -> TcS TouchabilityTestResult
touchabilityTest CtFlavour
Derived TcTyVar
lhs_tv Type
rhs
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case TouchabilityTestResult
result of
TouchabilityTestResult
Untouchable -> Bool
False
TouchabilityTestResult
_ -> Bool
True }
| Bool
otherwise
= forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
go :: TcType -> TcS (CoercionN, TcType)
go :: Type -> TcS (Coercion, Type)
go Type
ty | Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty = Type -> TcS (Coercion, Type)
go Type
ty'
go (Rep.TyConApp TyCon
tc [Type]
tys)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
= do { let ([Type]
fun_args, [Type]
extra_args) = 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 = HasDebugCallStack => Type -> Type
tcTypeKind Type
fun_app
; (Coercion
co, Type
new_ty) <- Type -> Type -> TcS (Coercion, Type)
emit_work Type
fun_app_kind Type
fun_app
; ([Coercion]
extra_args_cos, [Type]
extra_args') <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM Type -> TcS (Coercion, Type)
go [Type]
extra_args
; forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
co [Coercion]
extra_args_cos, Type -> [Type] -> Type
mkAppTys Type
new_ty [Type]
extra_args') }
| Bool
otherwise
= do { ([Coercion]
cos, [Type]
tys) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM Type -> TcS (Coercion, Type)
go [Type]
tys
; forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc [Coercion]
cos, TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys) }
go (Rep.AppTy Type
ty1 Type
ty2)
= do { (Coercion
co1, Type
ty1') <- Type -> TcS (Coercion, Type)
go Type
ty1
; (Coercion
co2, Type
ty2') <- Type -> TcS (Coercion, Type)
go Type
ty2
; forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Coercion -> Coercion
mkAppCo Coercion
co1 Coercion
co2, Type -> Type -> Type
mkAppTy Type
ty1' Type
ty2') }
go (Rep.FunTy AnonArgFlag
vis Type
w Type
arg Type
res)
= do { (Coercion
co_w, Type
w') <- Type -> TcS (Coercion, Type)
go Type
w
; (Coercion
co_arg, Type
arg') <- Type -> TcS (Coercion, Type)
go Type
arg
; (Coercion
co_res, Type
res') <- Type -> TcS (Coercion, Type)
go Type
res
; forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
Nominal Coercion
co_w Coercion
co_arg Coercion
co_res, AnonArgFlag -> Type -> Type -> Type -> Type
mkFunTy AnonArgFlag
vis Type
w' Type
arg' Type
res') }
go (Rep.CastTy Type
ty Coercion
cast_co)
= do { (Coercion
co, Type
ty') <- Type -> TcS (Coercion, Type)
go Type
ty
; forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Role -> Type -> Type -> Coercion -> Coercion
castCoercionKind1 Coercion
co Role
Nominal Type
ty' Type
ty Coercion
cast_co, Type -> Coercion -> Type
mkCastTy Type
ty' Coercion
cast_co) }
go ty :: Type
ty@(Rep.TyVarTy {}) = forall {m :: * -> *}. Monad m => Type -> m (Coercion, Type)
skip Type
ty
go ty :: Type
ty@(Rep.LitTy {}) = forall {m :: * -> *}. Monad m => Type -> m (Coercion, Type)
skip Type
ty
go ty :: Type
ty@(Rep.ForAllTy {}) = forall {m :: * -> *}. Monad m => Type -> m (Coercion, Type)
skip Type
ty
go ty :: Type
ty@(Rep.CoercionTy {}) = forall {m :: * -> *}. Monad m => Type -> m (Coercion, Type)
skip Type
ty
skip :: Type -> m (Coercion, Type)
skip Type
ty = forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
ty, Type
ty)
emit_work :: TcKind
-> TcType
-> TcS (CoercionN, TcType)
emit_work :: Type -> Type -> TcS (Coercion, Type)
emit_work Type
fun_app_kind Type
fun_app = case CtFlavour
flavour of
CtFlavour
Given ->
do { TcTyVar
new_tv <- forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TcTyVar
TcM.newCycleBreakerTyVar Type
fun_app_kind)
; let new_ty :: Type
new_ty = TcTyVar -> Type
mkTyVarTy TcTyVar
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 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" (forall a. Outputable a => a -> SDoc
ppr CtEvidence
new_given)
; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence
new_given]
; (InertSet -> InertSet) -> TcS ()
updInertTcS forall a b. (a -> b) -> a -> b
$ \InertSet
is ->
InertSet
is { inert_cycle_breakers :: CycleBreakerVarStack
inert_cycle_breakers = TcTyVar -> Type -> CycleBreakerVarStack -> CycleBreakerVarStack
insertCycleBreakerBinding TcTyVar
new_tv Type
fun_app
(InertSet -> CycleBreakerVarStack
inert_cycle_breakers InertSet
is) }
; forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
new_ty, Type
new_ty) }
CtFlavour
_derived_or_wd ->
do { TcTyVar
new_tv <- forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TcTyVar
TcM.newFlexiTyVar Type
fun_app_kind)
; let new_ty :: Type
new_ty = TcTyVar -> Type
mkTyVarTy TcTyVar
new_tv
; Coercion
co <- CtLoc -> Role -> Type -> Type -> TcS Coercion
emitNewWantedEq CtLoc
new_loc Role
Nominal Type
new_ty Type
fun_app
; forall (m :: * -> *) a. Monad m => a -> m a
return (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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles InertSet
is
= forall (m :: * -> *).
Monad m =>
CycleBreakerVarStack -> (TcTyVar -> Type -> m ()) -> m ()
forAllCycleBreakerBindings_ (InertSet -> CycleBreakerVarStack
inert_cycle_breakers InertSet
is) TcTyVar -> 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
tcView Type
ty
rewriterView Type
_other = forall a. Maybe a
Nothing