module TcSMonad (
WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, appendWorkList, selectWorkItem,
workListSize,
updWorkListTcS, updWorkListTcS_return,
runFlatten, emitFlatWork,
TcS, runTcS, runTcSWithEvBinds,
failTcS, tryTcS, nestTcS, nestImplicTcS, recoverTcS,
runTcPluginTcS, addUsedRdrNamesTcS, deferTcSForAllEq,
panicTcS, traceTcS,
traceFireTcS, bumpStepCountTcS, csTraceTcS,
wrapErrTcS, wrapWarnTcS,
XEvTerm(..),
Freshness(..), freshGoals, isFresh,
newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
setWantedTyBind, reportUnifications,
setEvBind,
newEvVar, newGivenEvVar, newGivenEvVars,
newDerived, emitNewDerived,
instDFunConstraints,
getInstEnvs, getFamInstEnvs,
getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
getTcEvBindsMap,
InertSet(..), InertCans(..),
updInertTcS, updInertCans, updInertDicts, updInertIrreds,
getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
emptyInert, getTcSInerts, setTcSInerts,
getUnsolvedInerts, checkAllSolved,
splitInertCans, removeInertCts,
prepareInertsForImplications,
addInertCan, insertInertItemTcS, insertFunEq,
emitInsoluble, emitWorkNC,
EqualCtList,
lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
findTyEqs,
addSolvedDict, lookupSolvedDict,
lookupFlatCache, extendFlatCache, newFlattenSkolem,
updInertFunEqs, findFunEq, sizeFunEqMap,
findFunEqsByTyCon, findFunEqs, partitionFunEqs,
instDFunType,
newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
cloneMetaTyVar, demoteUnfilledFmv,
TcLevel, isTouchableMetaTyVarTcS,
isFilledMetaTyVar_maybe, isFilledMetaTyVar,
zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkSimples,
newTcRef, readTcRef, updTcRef,
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam, matchFamTcM,
checkWellStagedDFun,
pprEq
) where
#include "HsVersions.h"
import HscTypes
import Inst
import InstEnv
import FamInst
import FamInstEnv
import qualified TcRnMonad as TcM
import qualified TcMType as TcM
import qualified TcEnv as TcM
( checkWellStaged, topIdLvl, tcGetDefaultTys )
import Kind
import TcType
import DynFlags
import Type
import TcEvidence
import Class
import TyCon
import Name
import RdrName (RdrName, GlobalRdrEnv)
import RnEnv (addUsedRdrNames)
import Var
import VarEnv
import VarSet
import Outputable
import Bag
import UniqSupply
import FastString
import Util
import Id
import TcRnTypes
import Unique
import UniqFM
import Maybes ( orElse, firstJusts )
import TrieMap
import Control.Arrow ( first )
import Control.Monad( ap, when, unless, MonadPlus(..) )
import MonadUtils
import Data.IORef
import Data.List ( partition, foldl' )
#ifdef DEBUG
import Digraph
#endif
data WorkList
= WL { wl_eqs :: [Ct]
, wl_funeqs :: [Ct]
, wl_rest :: [Ct]
, wl_implics :: Bag Implication
}
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
(WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1, wl_implics = implics1 })
(WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 })
= WL { wl_eqs = eqs1 ++ eqs2
, wl_funeqs = funeqs1 ++ funeqs2
, wl_rest = rest1 ++ rest2
, wl_implics = implics1 `unionBags` implics2 }
workListSize :: WorkList -> Int
workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
= length eqs + length funeqs + length rest
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq ct wl
= wl { wl_eqs = ct : wl_eqs wl }
extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq ct wl
= wl { wl_funeqs = ct : wl_funeqs wl }
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq ct wl
= wl { wl_rest = ct : wl_rest wl }
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic implic wl
= wl { wl_implics = implic `consBag` wl_implics wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt ct wl
= case classifyPredType (ctPred ct) of
EqPred NomEq ty1 _
| Just (tc,_) <- tcSplitTyConApp_maybe ty1
, isTypeFamilyTyCon tc
-> extendWorkListFunEq ct wl
EqPred {}
-> extendWorkListEq ct wl
_ -> extendWorkListNonEq ct wl
extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
, wl_rest = rest, wl_implics = implics })
= null eqs && null rest && null funeqs && isEmptyBag implics
emptyWorkList :: WorkList
emptyWorkList = WL { wl_eqs = [], wl_rest = []
, wl_funeqs = [], wl_implics = emptyBag }
selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
= case (eqs,feqs,rest) of
(ct:cts,_,_) -> (Just ct, wl { wl_eqs = cts })
(_,ct:fes,_) -> (Just ct, wl { wl_funeqs = fes })
(_,_,ct:cts) -> (Just ct, wl { wl_rest = cts })
(_,_,_) -> (Nothing,wl)
instance Outputable WorkList where
ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
, wl_rest = rest, wl_implics = implics })
= text "WL" <+> (braces $
vcat [ ppUnless (null eqs) $
ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
, ppUnless (null feqs) $
ptext (sLit "Funeqs =") <+> vcat (map ppr feqs)
, ppUnless (null rest) $
ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
, ppUnless (isEmptyBag implics) $
ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
])
emitFlatWork :: Ct -> TcS ()
emitFlatWork ct
= TcS $ \env ->
do { let flat_ref = tcs_flat_work env
; TcM.updTcRef flat_ref (ct :) }
runFlatten :: TcS a -> TcS a
runFlatten (TcS thing_inside)
= TcS $ \env ->
do { let flat_ref = tcs_flat_work env
; old_flats <- TcM.updTcRefX flat_ref (\_ -> [])
; res <- thing_inside env
; new_flats <- TcM.updTcRefX flat_ref (\_ -> old_flats)
; TcM.updTcRef (tcs_worklist env) (add_flats new_flats)
; return res }
where
add_flats new_flats wl
= wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }
add_funeqs [] wl = wl
add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
data InertCans
= IC { inert_eqs :: TyVarEnv EqualCtList
, inert_funeqs :: FunEqMap Ct
, inert_dicts :: DictMap Ct
, inert_irreds :: Cts
, inert_insols :: Cts
}
type EqualCtList = [Ct]
data InertSet
= IS { inert_cans :: InertCans
, inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour)
, inert_solved_dicts :: DictMap CtEvidence
}
instance Outputable InertCans where
ppr ics = vcat [ ptext (sLit "Equalities:")
<+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest)
emptyCts (inert_eqs ics))
, ptext (sLit "Type-function equalities:")
<+> pprCts (funEqsToBag (inert_funeqs ics))
, ptext (sLit "Dictionaries:")
<+> pprCts (dictsToBag (inert_dicts ics))
, ptext (sLit "Irreds:")
<+> pprCts (inert_irreds ics)
, text "Insolubles =" <+>
braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
]
instance Outputable InertSet where
ppr is = vcat [ ppr $ inert_cans is
, text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
emptyInert :: InertSet
emptyInert
= IS { inert_cans = IC { inert_eqs = emptyVarEnv
, inert_dicts = emptyDicts
, inert_funeqs = emptyFunEqs
, inert_irreds = emptyCts
, inert_insols = emptyCts
}
, inert_flat_cache = emptyFunEqs
, inert_solved_dicts = emptyDictMap }
addInertCan :: InertCans -> Ct -> InertCans
addInertCan ics item@(CTyEqCan {})
= ics { inert_eqs = add_eq (inert_eqs ics) item }
where
add_eq :: TyVarEnv EqualCtList -> Ct -> TyVarEnv EqualCtList
add_eq old_list it
= extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
old_list (cc_tyvar it) [it]
addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
= ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
addInertCan ics item@(CIrredEvCan {})
= ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
addInertCan ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
= ics { inert_dicts = addDict (inert_dicts ics) cls tys item }
addInertCan _ item
= pprPanic "upd_inert set: can't happen! Inserting " $
ppr item
insertInertItemTcS :: Ct -> TcS ()
insertInertItemTcS item
= do { traceTcS "insertInertItemTcS {" $
text "Trying to insert new inert item:" <+> ppr item
; updInertCans (\ics -> addInertCan ics item)
; traceTcS "insertInertItemTcS }" $ empty }
addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
addSolvedDict item cls tys
| isIPPred (ctEvPred item)
= return ()
| otherwise
= do { traceTcS "updSolvedSetTcs:" $ ppr item
; updInertTcS $ \ ics ->
ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
updInertTcS :: (InertSet -> InertSet) -> TcS ()
updInertTcS upd_fn
= do { is_var <- getTcSInertsRef
; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
getInertCans :: TcS InertCans
getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
setInertCans :: InertCans -> TcS ()
setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
updInertCans :: (InertCans -> InertCans) -> TcS ()
updInertCans upd_fn
= updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertDicts upd_fn
= updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
updInertFunEqs upd_fn
= updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }
updInertIrreds :: (Cts -> Cts) -> TcS ()
updInertIrreds upd_fn
= updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
prepareInertsForImplications :: InertSet -> (InertSet)
prepareInertsForImplications is@(IS { inert_cans = cans })
= is { inert_cans = getGivens cans
, inert_flat_cache = emptyFunEqs }
where
getGivens (IC { inert_eqs = eqs
, inert_irreds = irreds
, inert_funeqs = funeqs
, inert_dicts = dicts })
= IC { inert_eqs = filterVarEnv is_given_ecl eqs
, inert_funeqs = filterFunEqs isGivenCt funeqs
, inert_irreds = Bag.filterBag isGivenCt irreds
, inert_dicts = filterDicts isGivenCt dicts
, inert_insols = emptyCts }
is_given_ecl :: EqualCtList -> Bool
is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
is_given_ecl _ = False
getInertEqs :: TcS (TyVarEnv EqualCtList)
getInertEqs
= do { inert <- getTcSInerts
; return (inert_eqs (inert_cans inert)) }
getUnsolvedInerts :: TcS ( Bag Implication
, Cts
, Cts
, Cts
, Cts )
getUnsolvedInerts
= do { IC { inert_eqs = tv_eqs
, inert_funeqs = fun_eqs
, inert_irreds = irreds, inert_dicts = idicts
, inert_insols = insols } <- getInertCans
; let unsolved_tv_eqs = foldVarEnv (\cts rest ->
foldr add_if_unsolved rest cts)
emptyCts tv_eqs
unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
unsolved_irreds = Bag.filterBag is_unsolved irreds
unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
others = unsolved_irreds `unionBags` unsolved_dicts
; implics <- getWorkListImplics
; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
where
add_if_unsolved :: Ct -> Cts -> Cts
add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
| otherwise = cts
is_unsolved ct = not (isGivenCt ct)
getNoGivenEqs :: TcLevel
-> [TcTyVar]
-> TcS Bool
getNoGivenEqs tclvl skol_tvs
= do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
<- getInertCans
; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False iirreds
|| foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs
; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
; return (not has_given_eqs) }
where
eqs_given_here :: VarSet -> EqualCtList -> Bool
eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
= not (skolem_bound_here local_fsks tv) && ev_given_here ev
eqs_given_here _ _ = False
ev_given_here :: CtEvidence -> Bool
ev_given_here ev
= isGiven ev
&& tclvl == tcl_tclvl (ctl_env (ctEvLoc ev))
add_fsk :: Ct -> VarSet -> VarSet
add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
, isGiven ev = extendVarSet fsks tv
| otherwise = fsks
skol_tv_set = mkVarSet skol_tvs
skolem_bound_here local_fsks tv
= case tcTyVarDetails tv of
SkolemTv {} -> tv `elemVarSet` skol_tv_set
FlatSkol {} -> not (tv `elemVarSet` local_fsks)
_ -> False
splitInertCans :: InertCans -> ([Ct], [Ct], [Ct])
splitInertCans iCans = (given,derived,wanted)
where
allCts = foldDicts (:) (inert_dicts iCans)
$ foldFunEqs (:) (inert_funeqs iCans)
$ concat (varEnvElts (inert_eqs iCans))
(derived,other) = partition isDerivedCt allCts
(wanted,given) = partition isWantedCt other
removeInertCts :: [Ct] -> InertCans -> InertCans
removeInertCts cts icans = foldl' removeInertCt icans cts
removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt is ct =
case ct of
CDictCan { cc_class = cl, cc_tyargs = tys } ->
is { inert_dicts = delDict (inert_dicts is) cl tys }
CFunEqCan { cc_fun = tf, cc_tyargs = tys } ->
is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
CTyEqCan { cc_tyvar = x, cc_rhs = ty } ->
is { inert_eqs = delTyEq (inert_eqs is) x ty }
CIrredEvCan {} -> panic "removeInertCt: CIrredEvCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
CHoleCan {} -> panic "removeInertCt: CHoleCan"
checkAllSolved :: TcS Bool
checkAllSolved
= do { is <- getTcSInerts
; let icans = inert_cans is
unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
unsolved_dicts = foldDicts ((||) . isWantedCt)
(inert_dicts icans) False
unsolved_funeqs = foldFunEqs ((||) . isWantedCt)
(inert_funeqs icans) False
unsolved_eqs = foldVarEnv ((||) . any isWantedCt) False
(inert_eqs icans)
; return (not (unsolved_eqs || unsolved_irreds
|| unsolved_dicts || unsolved_funeqs
|| not (isEmptyBag (inert_insols icans)))) }
lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
lookupFlatCache fam_tc tys
= do { IS { inert_flat_cache = flat_cache
, inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
; return (firstJusts [lookup_inerts inert_funeqs,
lookup_flats flat_cache]) }
where
lookup_inerts inert_funeqs
| Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
<- findFunEqs inert_funeqs fam_tc tys
= Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
| otherwise = Nothing
lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts loc pty
| ClassPred cls tys <- classifyPredType pty
= do { inerts <- getTcSInerts
; return (lookupSolvedDict inerts loc cls tys `mplus`
lookupInertDict (inert_cans inerts) loc cls tys) }
| otherwise
= return Nothing
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
= case findDict dicts cls tys of
Just ct | let ev = ctEvidence ct
, ctEvCheckDepth cls loc ev
-> Just ev
_ -> Nothing
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
= case findDict solved cls tys of
Just ev | ctEvCheckDepth cls loc ev -> Just ev
_ -> Nothing
type TyEqMap a = TyVarEnv a
findTyEqs :: InertCans -> TyVar -> EqualCtList
findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` []
delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
isThisOne _ = False
type TcAppMap a = UniqFM (ListMap TypeMap a)
emptyTcAppMap :: TcAppMap a
emptyTcAppMap = emptyUFM
findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
findTcApp m u tys = do { tys_map <- lookupUFM m u
; lookupTM tys tys_map }
delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
delTcApp m cls tys = adjustUFM (deleteTM tys) m cls
insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
insertTcApp m cls tys ct = alterUFM alter_tm m cls
where
alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
filterTcAppMap f m
= mapUFM do_tm m
where
do_tm tm = foldTM insert_mb tm emptyTM
insert_mb ct tm
| f ct = insertTM tys ct tm
| otherwise = tm
where
tys = case ct of
CFunEqCan { cc_tyargs = tys } -> tys
CDictCan { cc_tyargs = tys } -> tys
_ -> pprPanic "filterTcAppMap" (ppr ct)
tcAppMapToBag :: TcAppMap a -> Bag a
tcAppMapToBag m = foldTcAppMap consBag m emptyBag
foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap k m z = foldUFM (foldTM k) z m
type DictMap a = TcAppMap a
emptyDictMap :: DictMap a
emptyDictMap = emptyTcAppMap
findDict :: DictMap a -> Class -> [Type] -> Maybe a
findDict m cls tys = findTcApp m (getUnique cls) tys
findDictsByClass :: DictMap a -> Class -> Bag a
findDictsByClass m cls
| Just tm <- lookupUFM m cls = foldTM consBag tm emptyBag
| otherwise = emptyBag
delDict :: DictMap a -> Class -> [Type] -> DictMap a
delDict m cls tys = delTcApp m (getUnique cls) tys
addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
addDict m cls tys item = insertTcApp m (getUnique cls) tys item
addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
addDictsByClass m cls items
= addToUFM m cls (foldrBag add emptyTM items)
where
add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
add ct _ = pprPanic "addDictsByClass" (ppr ct)
filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
filterDicts f m = filterTcAppMap f m
partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts)
where
k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes)
| otherwise = (yeses, add ct noes)
add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
= addDict m cls tys ct
add ct _ = pprPanic "partitionDicts" (ppr ct)
dictsToBag :: DictMap a -> Bag a
dictsToBag = tcAppMapToBag
foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
foldDicts = foldTcAppMap
emptyDicts :: DictMap a
emptyDicts = emptyTcAppMap
type FunEqMap a = TcAppMap a
emptyFunEqs :: TcAppMap a
emptyFunEqs = emptyTcAppMap
sizeFunEqMap :: FunEqMap a -> Int
sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0
findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq m tc tys = findTcApp m (getUnique tc) tys
findFunEqs :: FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEqs m tc tys = findTcApp m (getUnique tc) tys
funEqsToBag :: FunEqMap a -> Bag a
funEqsToBag m = foldTcAppMap consBag m emptyBag
findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
findFunEqsByTyCon m tc
| Just tm <- lookupUFM m tc = foldTM (:) tm []
| otherwise = []
foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs = foldTcAppMap
filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
filterFunEqs = filterTcAppMap
insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
partitionFunEqs f m = (yeses, foldr del m yeses)
where
yeses = foldTcAppMap k m []
k ct yeses | f ct = ct : yeses
| otherwise = yeses
del (CFunEqCan { cc_fun = tc, cc_tyargs = tys }) m
= delFunEq m tc tys
del ct _ = pprPanic "partitionFunEqs" (ppr ct)
delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
delFunEq m tc tys = delTcApp m (getUnique tc) tys
data TcSEnv
= TcSEnv {
tcs_ev_binds :: EvBindsVar,
tcs_unified :: IORef Bool,
tcs_count :: IORef Int,
tcs_inerts :: IORef InertSet,
tcs_worklist :: IORef WorkList,
tcs_flat_work :: IORef [Ct]
}
newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
instance Functor TcS where
fmap f m = TcS $ fmap f . unTcS m
instance Applicative TcS where
pure = return
(<*>) = ap
instance Monad TcS where
return x = TcS (\_ -> return x)
fail err = TcS (\_ -> fail err)
m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
instance MonadUnique TcS where
getUniqueSupplyM = wrapTcS getUniqueSupplyM
wrapTcS :: TcM a -> TcS a
wrapTcS = TcS . const
wrapErrTcS :: TcM a -> TcS a
wrapErrTcS = wrapTcS
wrapWarnTcS :: TcM a -> TcS a
wrapWarnTcS = wrapTcS
failTcS, panicTcS :: SDoc -> TcS a
failTcS = wrapTcS . TcM.failWith
panicTcS doc = pprPanic "TcCanonical" doc
traceTcS :: String -> SDoc -> TcS ()
traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
runTcPluginTcS :: TcPluginM a -> TcS a
runTcPluginTcS = wrapTcS . runTcPluginM
instance HasDynFlags TcS where
getDynFlags = wrapTcS getDynFlags
getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
; n <- TcM.readTcRef ref
; TcM.writeTcRef ref (n+1) }
csTraceTcS :: SDoc -> TcS ()
csTraceTcS doc
= wrapTcS $ csTraceTcM 1 (return doc)
traceFireTcS :: CtEvidence -> SDoc -> TcS ()
traceFireTcS ev doc
= TcS $ \env -> csTraceTcM 1 $
do { n <- TcM.readTcRef (tcs_count env)
; tclvl <- TcM.getTcLevel
; return (hang (int n <> brackets (ptext (sLit "U:") <> ppr tclvl
<> ppr (ctLocDepth (ctEvLoc ev)))
<+> doc <> colon)
4 (ppr ev)) }
csTraceTcM :: Int -> TcM SDoc -> TcM ()
csTraceTcM trace_level mk_doc
= do { dflags <- getDynFlags
; when ( (dopt Opt_D_dump_cs_trace dflags || dopt Opt_D_dump_tc_trace dflags)
&& trace_level <= traceLevel dflags ) $
do { msg <- mk_doc
; TcM.traceTcRn Opt_D_dump_cs_trace msg } }
runTcS :: TcS a
-> TcM (a, Bag EvBind)
runTcS tcs
= do { ev_binds_var <- TcM.newTcEvBinds
; res <- runTcSWithEvBinds ev_binds_var tcs
; ev_binds <- TcM.getTcEvBinds ev_binds_var
; return (res, ev_binds) }
runTcSWithEvBinds :: EvBindsVar
-> TcS a
-> TcM a
runTcSWithEvBinds ev_binds_var tcs
= do { unified_var <- TcM.newTcRef False
; step_count <- TcM.newTcRef 0
; inert_var <- TcM.newTcRef is
; wl_var <- TcM.newTcRef emptyWorkList
; fw_var <- TcM.newTcRef (panic "Flat work list")
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
, tcs_unified = unified_var
, tcs_count = step_count
, tcs_inerts = inert_var
, tcs_worklist = wl_var
, tcs_flat_work = fw_var }
; res <- unTcS tcs env
; count <- TcM.readTcRef step_count
; when (count > 0) $
csTraceTcM 0 $ return (ptext (sLit "Constraint solver steps =") <+> int count)
#ifdef DEBUG
; ev_binds <- TcM.getTcEvBinds ev_binds_var
; checkForCyclicBinds ev_binds
#endif
; return res }
where
is = emptyInert
#ifdef DEBUG
checkForCyclicBinds :: Bag EvBind -> TcM ()
checkForCyclicBinds ev_binds
| null cycles
= return ()
| null coercion_cycles
= TcM.traceTc "Cycle in evidence binds" $ ppr cycles
| otherwise
= pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
where
cycles :: [[EvBind]]
cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVertices edges]
coercion_cycles = [c | c <- cycles, any is_co_bind c]
is_co_bind (EvBind b _) = isEqVar b
edges :: [(EvBind, EvVar, [EvVar])]
edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs)) | bind@(EvBind bndr rhs) <- bagToList ev_binds]
#endif
nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
nestImplicTcS ref inner_tclvl (TcS thing_inside)
= TcS $ \ TcSEnv { tcs_unified = unified_var
, tcs_inerts = old_inert_var
, tcs_count = count } ->
do { inerts <- TcM.readTcRef old_inert_var
; let nest_inert = inerts { inert_flat_cache = emptyFunEqs }
; new_inert_var <- TcM.newTcRef nest_inert
; new_wl_var <- TcM.newTcRef emptyWorkList
; new_fw_var <- TcM.newTcRef (panic "Flat work list")
; let nest_env = TcSEnv { tcs_ev_binds = ref
, tcs_unified = unified_var
, tcs_count = count
, tcs_inerts = new_inert_var
, tcs_worklist = new_wl_var
, tcs_flat_work = new_fw_var }
; res <- TcM.setTcLevel inner_tclvl $
thing_inside nest_env
#ifdef DEBUG
; ev_binds <- TcM.getTcEvBinds ref
; checkForCyclicBinds ev_binds
#endif
; return res }
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
= TcS $ \ env ->
TcM.recoverM (recovery_code env) (thing_inside env)
nestTcS :: TcS a -> TcS a
nestTcS (TcS thing_inside)
= TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
do { inerts <- TcM.readTcRef inerts_var
; new_inert_var <- TcM.newTcRef inerts
; new_wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = env { tcs_inerts = new_inert_var
, tcs_worklist = new_wl_var }
; res <- thing_inside nest_env
; new_inerts <- TcM.readTcRef new_inert_var
; TcM.writeTcRef inerts_var
(inerts { inert_solved_dicts = inert_solved_dicts new_inerts })
; return res }
tryTcS :: TcS a -> TcS a
tryTcS (TcS thing_inside)
= TcS $ \env ->
do { is_var <- TcM.newTcRef emptyInert
; unified_var <- TcM.newTcRef False
; ev_binds_var <- TcM.newTcEvBinds
; wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = env { tcs_ev_binds = ev_binds_var
, tcs_unified = unified_var
, tcs_inerts = is_var
, tcs_worklist = wl_var }
; thing_inside nest_env }
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef = TcS (return . tcs_inerts)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef = TcS (return . tcs_worklist)
getTcSInerts :: TcS InertSet
getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
setTcSInerts :: InertSet -> TcS ()
setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics
= do { wl_var <- getTcSWorkListRef
; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
; return (wl_implics wl_curr) }
updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS f
= do { wl_var <- getTcSWorkListRef
; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
; let new_work = f wl_curr
; wrapTcS (TcM.writeTcRef wl_var new_work) }
updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
updWorkListTcS_return f
= do { wl_var <- getTcSWorkListRef
; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
; traceTcS "updWorkList" (ppr wl_curr)
; let (res,new_work) = f wl_curr
; wrapTcS (TcM.writeTcRef wl_var new_work)
; return res }
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC evs
| null evs
= return ()
| otherwise
= do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
; updWorkListTcS (extendWorkListCts (map mkNonCanonical evs)) }
emitInsoluble :: Ct -> TcS ()
emitInsoluble ct
= do { traceTcS "Emit insoluble" (ppr ct)
; updInertTcS add_insol }
where
this_pred = ctPred ct
add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
| already_there = is
| otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
where
already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
newTcRef :: a -> TcS (TcRef a)
newTcRef x = wrapTcS (TcM.newTcRef x)
readTcRef :: TcRef a -> TcS a
readTcRef ref = wrapTcS (TcM.readTcRef ref)
updTcRef :: TcRef a -> (a->a) -> TcS ()
updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds)
getTcLevel :: TcS TcLevel
getTcLevel = wrapTcS TcM.getTcLevel
getTcEvBindsMap :: TcS EvBindMap
getTcEvBindsMap
= do { EvBindsVar ev_ref _ <- getTcEvBinds
; wrapTcS $ TcM.readTcRef ev_ref }
setWantedTyBind :: TcTyVar -> TcType -> TcS ()
setWantedTyBind tv ty
| ASSERT2( isMetaTyVar tv, ppr tv )
isFmvTyVar tv
= ASSERT2( isMetaTyVar tv, ppr tv )
wrapTcS (TcM.writeMetaTyVar tv ty)
| otherwise
= TcS $ \ env ->
do { TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty)
; TcM.writeMetaTyVar tv ty
; TcM.writeTcRef (tcs_unified env) True }
reportUnifications :: TcS a -> TcS (Bool, a)
reportUnifications (TcS thing_inside)
= TcS $ \ env ->
do { inner_unified <- TcM.newTcRef False
; res <- thing_inside (env { tcs_unified = inner_unified })
; dirty <- TcM.readTcRef inner_unified
; return (dirty, res) }
getDefaultInfo :: TcS ([Type], (Bool, Bool))
getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
getInstEnvs :: TcS InstEnvs
getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
getTopEnv :: TcS HscEnv
getTopEnv = wrapTcS $ TcM.getTopEnv
getGblEnv :: TcS TcGblEnv
getGblEnv = wrapTcS $ TcM.getGblEnv
addUsedRdrNamesTcS :: [RdrName] -> TcS ()
addUsedRdrNamesTcS names = wrapTcS $ addUsedRdrNames names
checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
checkWellStagedDFun pred dfun_id loc
= wrapTcS $ TcM.setCtLoc loc $
do { use_stage <- TcM.getStage
; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
where
pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
bind_lvl = TcM.topIdLvl dfun_id
pprEq :: TcType -> TcType -> SDoc
pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
isTouchableMetaTyVarTcS tv
= do { tclvl <- getTcLevel
; return $ isTouchableMetaTyVar tclvl tv }
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_ref = ref }
-> do { cts <- wrapTcS (TcM.readTcRef ref)
; case cts of
Indirect ty -> return (Just ty)
Flexi -> return Nothing }
_ -> return Nothing
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
zonkTcType :: TcType -> TcS TcType
zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
zonkTcTyVar :: TcTyVar -> TcS TcType
zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
zonkSimples :: Cts -> TcS Cts
zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
newFlattenSkolem :: CtFlavour -> CtLoc
-> TcType
-> TcS (CtEvidence, TcTyVar)
newFlattenSkolem Given loc fam_ty
= do { fsk <- wrapTcS $
do { uniq <- TcM.newUnique
; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
; let ev = CtGiven { ctev_pred = mkTcEqPred fam_ty (mkTyVarTy fsk)
, ctev_evtm = EvCoercion (mkTcNomReflCo fam_ty)
, ctev_loc = loc }
; return (ev, fsk) }
newFlattenSkolem _ loc fam_ty
= do { fuv <- wrapTcS $
do { uniq <- TcM.newUnique
; ref <- TcM.newMutVar Flexi
; let details = MetaTv { mtv_info = FlatMetaTv
, mtv_ref = ref
, mtv_tclvl = fskTcLevel }
name = TcM.mkTcTyVarName uniq (fsLit "s")
; return (mkTcTyVar name (typeKind fam_ty) details) }
; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv))
; return (ev, fuv) }
extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
extendFlatCache tc xi_args stuff
= do { dflags <- getDynFlags
; when (gopt Opt_FlatCache dflags) $
updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
is { inert_flat_cache = insertFunEq fc tc xi_args stuff } }
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
instDFunType dfun_id mb_inst_tys
= wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
where
(dfun_tvs, dfun_phi) = tcSplitForAllTys (idType dfun_id)
go :: [TyVar] -> [DFunInstType] -> TvSubst -> TcM ([TcType], TcType)
go [] [] subst = return ([], substTy subst dfun_phi)
go (tv:tvs) (Just ty : mb_tys) subst
= do { (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
; return (ty : tys, phi) }
go (tv:tvs) (Nothing : mb_tys) subst
= do { ty <- instFlexiTcSHelper (tyVarName tv) (substTy subst (tyVarKind tv))
; (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
; return (ty : tys, phi) }
go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr mb_inst_tys)
newFlexiTcSTy :: Kind -> TcS TcType
newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
demoteUnfilledFmv :: TcTyVar -> TcS ()
demoteUnfilledFmv fmv
= wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
; unless is_filled $
do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
; TcM.writeMetaTyVar fmv tv_ty } }
instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
where
inst_one subst tv
= do { ty' <- instFlexiTcSHelper (tyVarName tv)
(substTy subst (tyVarKind tv))
; return (extendTvSubst subst tv ty', ty') }
instFlexiTcSHelper :: Name -> Kind -> TcM TcType
instFlexiTcSHelper tvname kind
= do { uniq <- TcM.newUnique
; details <- TcM.newMetaDetails (TauTv False)
; let name = setNameUnique tvname uniq
; return (mkTyVarTy (mkTcTyVar name kind details)) }
instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
data XEvTerm
= XEvTerm { ev_preds :: [PredType]
, ev_comp :: [EvTerm] -> EvTerm
, ev_decomp :: EvTerm -> [EvTerm]
}
data Freshness = Fresh | Cached
isFresh :: Freshness -> Bool
isFresh Fresh = True
isFresh Cached = False
freshGoals :: [(CtEvidence, Freshness)] -> [CtEvidence]
freshGoals mns = [ ctev | (ctev, Fresh) <- mns ]
setEvBind :: EvVar -> EvTerm -> TcS ()
setEvBind the_ev tm
= do { tc_evbinds <- getTcEvBinds
; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev tm }
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds = wrapTcS TcM.newTcEvBinds
newEvVar :: TcPredType -> TcS EvVar
newEvVar pred = wrapTcS (TcM.newEvVar pred)
newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar loc (pred, rhs)
= ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
do { new_ev <- newEvVar pred
; setEvBind new_ev rhs
; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
isKindEquality :: TcPredType -> Bool
isKindEquality pred = case classifyPredType pred of
EqPred _ t1 _ -> isKind t1
_ -> False
newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC loc pty
= do { new_ev <- newEvVar pty
; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
newWantedEvVar loc pty
= do { mb_ct <- lookupInInerts loc pty
; case mb_ct of
Just ctev | not (isDerived ctev)
-> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
; return (ctev, Cached) }
_ -> do { ctev <- newWantedEvVarNC loc pty
; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
; return (ctev, Fresh) } }
emitNewDerived :: CtLoc -> TcPredType -> TcS ()
emitNewDerived loc pred
= do { mb_ev <- newDerived loc pred
; case mb_ev of
Nothing -> return ()
Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
newDerived loc pred
= do { mb_ct <- lookupInInerts loc pred
; return (case mb_ct of
Just {} -> Nothing
Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
instDFunConstraints :: CtLoc -> TcThetaType -> TcS [(CtEvidence, Freshness)]
instDFunConstraints loc = mapM (newWantedEvVar loc)
matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
matchFam tycon args = wrapTcS $ matchFamTcM tycon args
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (TcCoercion, TcType))
matchFamTcM tycon args
= do { fam_envs <- FamInst.tcGetFamInstEnvs
; return $ fmap (first TcCoercion) $
reduceTyFamApp_maybe fam_envs Nominal tycon args }
deferTcSForAllEq :: Role
-> CtLoc
-> ([TyVar],TcType)
-> ([TyVar],TcType)
-> TcS EvTerm
deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
= do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
; let tys = mkTyVarTys skol_tvs
phi1 = Type.substTy subst1 body1
phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
skol_info = UnifyForAllSkol skol_tvs phi1
eq_pred = case role of
Nominal -> mkTcEqPred phi1 phi2
Representational -> mkCoerciblePred phi1 phi2
Phantom -> panic "deferTcSForAllEq Phantom"
; (ctev, freshness) <- newWantedEvVar loc eq_pred
; coe_inside <- case freshness of
Cached -> return (ctEvCoercion ctev)
Fresh -> do { ev_binds_var <- newTcEvBinds
; env <- wrapTcS $ TcM.getLclEnv
; let ev_binds = TcEvBinds ev_binds_var
new_ct = mkNonCanonical ctev
new_co = ctEvCoercion ctev
new_tclvl = pushTcLevel (tcl_tclvl env)
; let wc = WC { wc_simple = singleCt new_ct
, wc_impl = emptyBag
, wc_insol = emptyCts }
imp = Implic { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_no_eqs = True
, ic_given = []
, ic_wanted = wc
, ic_insol = False
, ic_binds = ev_binds_var
, ic_env = env
, ic_info = skol_info }
; updWorkListTcS (extendWorkListImplic imp)
; return (TcLetCo ev_binds new_co) }
; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }