\begin{code}
module TcSMonad (
WorkList(..), isEmptyWorkList, emptyWorkList,
workListFromEq, workListFromNonEq, workListFromCt,
extendWorkListEq, extendWorkListFunEq,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
withWorkList, workListSize,
updWorkListTcS, updWorkListTcS_return,
updTcSImplics,
Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
emitInsoluble,
isWanted, isDerived,
isGivenCt, isWantedCt, isDerivedCt,
canRewrite,
mkGivenLoc,
TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS,
traceFireTcS, bumpStepCountTcS,
tryTcS, nestTcS, nestImplicTcS, recoverTcS,
wrapErrTcS, wrapWarnTcS,
addSolvedDict, addSolvedFunEq, getGivenInfo,
addUsedRdrNamesTcS,
deferTcSForAllEq,
setEvBind,
XEvTerm(..),
MaybeNew (..), isFresh, freshGoal, freshGoals, getEvTerm, getEvTerms,
xCtEvidence,
rewriteEvidence,
rewriteEqEvidence,
maybeSym,
newWantedEvVar, newWantedEvVarNC, newWantedEvVarNonrec, newDerived,
instDFunConstraints,
setWantedTyBind, reportUnifications,
getInstEnvs, getFamInstEnvs,
getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
getTcEvBindsMap, getTcSTyBindsMap,
lookupFlatEqn, newFlattenSkolem,
Deque(..), insertDeque, emptyDeque,
InertSet(..), InertCans(..),
getInertEqs,
emptyInert, getTcSInerts, setTcSInerts,
getInertUnsolved, checkAllSolved,
prepareInertsForImplications,
addInertCan, insertInertItemTcS,
EqualCtList,
lookupSolvedDict, extendFlatCache,
findFunEq, findTyEqs,
findDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
findFunEqsByTyCon, findFunEqs, addFunEq, replaceFunEqs, partitionFunEqs,
instDFunType,
newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
cloneMetaTyVar,
Untouchables, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe,
zonkTyVarsAndFV,
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam, matchOpenFam,
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 CoAxiom(sfMatchFam)
import TcEvidence
import Class
import TyCon
import Name
import RdrName (RdrName, GlobalRdrEnv)
import RnEnv (addUsedRdrNames)
import Var
import VarEnv
import Outputable
import Bag
import MonadUtils
import UniqSupply
import FastString
import Util
import Id
import TcRnTypes
import BasicTypes
import Unique
import UniqFM
import Maybes ( orElse, catMaybes, firstJust )
import Pair ( pSnd )
import TrieMap
import Control.Monad( ap, when )
import Data.IORef
import Data.List( partition )
#ifdef DEBUG
import VarSet
import Digraph
#endif
\end{code}
%************************************************************************
%* *
%* Worklists *
%* Canonical and non-canonical constraints that the simplifier has to *
%* work on. Including their simplification depths. *
%* *
%* *
%************************************************************************
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
A WorkList contains canonical and non-canonical items (of all flavors).
Notice that each Ct now has a simplification depth. We may
consider using this depth for prioritization as well in the future.
As a simple form of priority queue, our worklist separates out
equalities (wl_eqs) from the rest of the canonical constraints,
so that it's easier to deal with them first, but the separation
is not strictly necessary. Notice that non-canonical constraints
are also parts of the worklist.
Note [NonCanonical Semantics]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note that canonical constraints involve a CNonCanonical constructor. In the worklist
we use this constructor for constraints that have not yet been canonicalized such as
[Int] ~ [a]
In other words, all constraints start life as NonCanonicals.
On the other hand, in the Inert Set (see below) the presence of a NonCanonical somewhere
means that we have a ``frozen error''.
NonCanonical constraints never interact directly with other constraints -- but they can
be rewritten by equalities (for instance if a non canonical exists in the inert, we'd
better rewrite it as much as possible before reporting it as an error to the user)
\begin{code}
data Deque a = DQ [a] [a]
instance Outputable a => Outputable (Deque a) where
ppr (DQ as bs) = ppr (as ++ reverse bs)
emptyDeque :: Deque a
emptyDeque = DQ [] []
isEmptyDeque :: Deque a -> Bool
isEmptyDeque (DQ as bs) = null as && null bs
dequeSize :: Deque a -> Int
dequeSize (DQ as bs) = length as + length bs
insertDeque :: a -> Deque a -> Deque a
insertDeque b (DQ as bs) = DQ as (b:bs)
appendDeque :: Deque a -> Deque a -> Deque a
appendDeque (DQ as1 bs1) (DQ as2 bs2) = DQ (as1 ++ reverse bs1 ++ as2) bs2
extractDeque :: Deque a -> Maybe (Deque a, a)
extractDeque (DQ [] []) = Nothing
extractDeque (DQ (a:as) bs) = Just (DQ as bs, a)
extractDeque (DQ [] bs) = case reverse bs of
(a:as) -> Just (DQ as [], a)
[] -> panic "extractDeque"
data WorkList = WorkList { wl_eqs :: [Ct]
, wl_funeqs :: Deque Ct
, wl_rest :: [Ct]
}
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList new_wl orig_wl
= WorkList { wl_eqs = wl_eqs new_wl ++ wl_eqs orig_wl
, wl_funeqs = wl_funeqs new_wl `appendDeque` wl_funeqs orig_wl
, wl_rest = wl_rest new_wl ++ wl_rest orig_wl }
workListSize :: WorkList -> Int
workListSize (WorkList { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
= length eqs + dequeSize funeqs + length rest
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq ct wl
| Just {} <- isCFunEqCan_maybe ct
= extendWorkListFunEq ct wl
| otherwise
= wl { wl_eqs = ct : wl_eqs wl }
extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq ct wl
= wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
extendWorkListEqs :: [Ct] -> WorkList -> WorkList
extendWorkListEqs cts wl = foldr extendWorkListEq wl cts
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq ct wl
= wl { wl_rest = ct : wl_rest wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt ct wl
| isEqPred (ctPred ct) = extendWorkListEq ct wl
| otherwise = extendWorkListNonEq ct wl
extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList wl
= null (wl_eqs wl) && null (wl_rest wl) && isEmptyDeque (wl_funeqs wl)
emptyWorkList :: WorkList
emptyWorkList = WorkList { wl_eqs = [], wl_rest = [], wl_funeqs = emptyDeque }
workListFromEq :: Ct -> WorkList
workListFromEq ct = extendWorkListEq ct emptyWorkList
workListFromNonEq :: Ct -> WorkList
workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
workListFromCt :: Ct -> WorkList
workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct
| otherwise = workListFromNonEq ct
selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
= case (eqs,feqs,rest) of
(ct:cts,_,_) -> (Just ct, wl { wl_eqs = cts })
(_,fun_eqs,_) | Just (fun_eqs', ct) <- extractDeque fun_eqs
-> (Just ct, wl { wl_funeqs = fun_eqs' })
(_,_,(ct:cts)) -> (Just ct, wl { wl_rest = cts })
(_,_,_) -> (Nothing,wl)
instance Outputable WorkList where
ppr wl = vcat [ text "WorkList (eqs) = " <+> ppr (wl_eqs wl)
, text "WorkList (funeqs)= " <+> ppr (wl_funeqs wl)
, text "WorkList (rest) = " <+> ppr (wl_rest wl)
]
\end{code}
%************************************************************************
%* *
%* Inert Sets *
%* *
%* *
%************************************************************************
Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
* All canonical
* No two dictionaries with the same head
* No two CIrreds with the same type
* Family equations inert wrt top-level family axioms
* Dictionaries have no matching top-level instance
* Given family or dictionary constraints don't mention touchable
unification variables
* Non-CTyEqCan constraints are fully rewritten with respect
to the CTyEqCan equalities (modulo canRewrite of course;
eg a wanted cannot rewrite a given)
* CTyEqCan equalities _do_not_ form an idempotent substitution, but
they are guaranteed to not have any occurs errors. Additional notes:
- The lack of idempotence of the inert substitution implies
that we must make sure that when we rewrite a constraint we
apply the substitution /recursively/ to the types
involved. Currently the one AND ONLY way in the whole
constraint solver that we rewrite types and constraints wrt
to the inert substitution is TcCanonical/flattenTyVar.
- In the past we did try to have the inert substitution as
idempotent as possible but this would only be true for
constraints of the same flavor, so in total the inert
substitution could not be idempotent, due to flavor-related
issued. Note [Non-idempotent inert substitution] explains
what is going on.
- Whenever a constraint ends up in the worklist we do
recursively apply exhaustively the inert substitution to it
to check for occurs errors. But if an equality is already in
the inert set and we can guarantee that adding a new equality
will not cause the first equality to have an occurs check
then we do not rewrite the inert equality. This happens in
TcInteract, rewriteInertEqsFromInertEq.
See Note [Delicate equality kick-out] to see which inert
equalities can safely stay in the inert set and which must be
kicked out to be rewritten and re-checked for occurs errors.
Note [Solved constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~
When we take a step to simplify a constraint 'c', we call the original constraint "solved".
For example: Wanted: ev :: [s] ~ [t]
New goal: ev1 :: s ~ t
Then 'ev' is now "solved".
The reason for all this is simply to avoid re-solving goals we have solved already.
* A solved Wanted may depend on as-yet-unsolved goals, so (for example) we should not
use it to rewrite a Given; in that sense the solved goal is still a Wanted
* A solved Given is just given
* A solved Derived in inert_solved is possible; purpose is to avoid
creating tons of identical Derived goals.
But there are no solved Deriveds in inert_solved_funeqs
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Type-family equations, of form (ev : F tys ~ ty), live in four places
* The work-list, of course
* The inert_flat_cache. This is used when flattening, to get maximal
sharing. It contains lots of things that are still in the work-list.
E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
work list. Then we flatten w1, dumping (w3: G a ~ f1) in the work
list. Now if we flatten w2 before we get to w3, we still want to
share that (G a).
Because it contains work-list things, DO NOT use the flat cache to solve
a top-level goal. Eg in the above example we don't want to solve w3
using w3 itself!
* The inert_solved_funeqs. These are all "solved" goals (see Note [Solved constraints]),
the result of using a top-level type-family instance.
* THe inert_funeqs are un-solved but fully processed and in the InertCans.
\begin{code}
data InertCans
= IC { inert_eqs :: TyVarEnv EqualCtList
, inert_funeqs :: FunEqMap EqualCtList
, inert_dicts :: DictMap Ct
, inert_irreds :: Cts
, inert_insols :: Cts
, inert_no_eqs :: !Bool
}
type EqualCtList = [Ct]
data InertSet
= IS { inert_cans :: InertCans
, inert_flat_cache :: FunEqMap (CtEvidence, TcType)
, inert_fsks :: [TcTyVar]
, inert_solved_funeqs :: FunEqMap (CtEvidence, TcType)
, inert_solved_dicts :: DictMap CtEvidence
}
instance Outputable InertCans where
ppr ics = vcat [ ptext (sLit "Equalities:")
<+> vcat (map ppr (varEnvElts (inert_eqs ics)))
, ptext (sLit "Type-function equalities:")
<+> vcat (map ppr (funEqsToList (inert_funeqs ics)))
, ptext (sLit "No-eqs:") <+> ppr (inert_no_eqs ics)
, ptext (sLit "Dictionaries:")
<+> vcat (map ppr (Bag.bagToList $ dictsToBag (inert_dicts ics)))
, ptext (sLit "Irreds:")
<+> vcat (map ppr (Bag.bagToList $ 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" <+> int (sizeDictMap (inert_solved_dicts is))
, text "Solved funeqs" <+> int (sizeFunEqMap (inert_solved_funeqs is))]
emptyInert :: InertSet
emptyInert
= IS { inert_cans = IC { inert_eqs = emptyVarEnv
, inert_dicts = emptyDicts
, inert_funeqs = emptyFunEqs
, inert_irreds = emptyCts
, inert_insols = emptyCts
, inert_no_eqs = True
}
, inert_fsks = []
, inert_flat_cache = emptyFunEqs
, inert_solved_funeqs = emptyFunEqs
, inert_solved_dicts = emptyDictMap }
addInertCan :: InertCans -> Ct -> InertCans
addInertCan ics item@(CTyEqCan { cc_ev = ev })
= ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs)
(inert_eqs ics)
(cc_tyvar item) [item]
, inert_no_eqs = isFlatSkolEv ev && inert_no_eqs ics }
addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys, cc_ev = ev })
= ics { inert_funeqs = addFunEq (inert_funeqs ics) tc tys item
, inert_no_eqs = isFlatSkolEv ev && inert_no_eqs ics }
addInertCan ics item@(CIrredEvCan {})
= ics { inert_irreds = inert_irreds ics `Bag.snocBag` item
, inert_no_eqs = False }
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
isFlatSkolEv :: CtEvidence -> Bool
isFlatSkolEv ev = case ctLocOrigin (ctev_loc ev) of
FlatSkolOrigin -> True
_ -> False
insertInertItemTcS :: Ct -> TcS ()
insertInertItemTcS item
= do { traceTcS "insertInertItemTcS {" $
text "Trying to insert new inert item:" <+> ppr item
; updInertTcS (\ics -> ics { inert_cans = addInertCan (inert_cans 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 } }
addSolvedFunEq :: TyCon -> [TcType] -> CtEvidence -> TcType -> TcS ()
addSolvedFunEq fam_tc tys ev rhs_ty
= updInertTcS $ \ inert ->
inert { inert_solved_funeqs = insertFunEq (inert_solved_funeqs inert)
fam_tc tys (ev, rhs_ty) }
updInertTcS :: (InertSet -> InertSet) -> TcS ()
updInertTcS upd
= do { is_var <- getTcSInertsRef
; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
; TcM.writeTcRef is_var (upd curr_inert) }) }
prepareInertsForImplications :: InertSet -> InertSet
prepareInertsForImplications is
= is { inert_cans = getGivens (inert_cans is)
, inert_fsks = []
, 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_eq eqs
, inert_funeqs = foldFunEqs given_from_wanted funeqs emptyFunEqs
, inert_irreds = Bag.filterBag isGivenCt irreds
, inert_dicts = filterDicts isGivenCt dicts
, inert_insols = emptyCts
, inert_no_eqs = True
}
is_given_eq :: [Ct] -> Bool
is_given_eq (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
is_given_eq _ = False
given_from_wanted :: EqualCtList -> FunEqMap EqualCtList -> FunEqMap EqualCtList
given_from_wanted (funeq:_) fhm
| isWanted ev = insert_one (funeq { cc_ev = given_ev }) fhm
| isGiven ev = insert_one funeq fhm
where
ev = ctEvidence funeq
given_ev = CtGiven { ctev_evtm = EvId (ctev_evar ev)
, ctev_pred = ctev_pred ev
, ctev_loc = ctev_loc ev }
given_from_wanted _ fhm = fhm
insert_one :: Ct -> FunEqMap EqualCtList -> FunEqMap EqualCtList
insert_one item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys }) fhm
= addFunEq fhm tc tys item
insert_one item _ = pprPanic "insert_one" (ppr item)
\end{code}
Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we trim the inert set,
retaining only Givens. These givens can be used when solving
the inner implications.
With one wrinkle! We take all *wanted* *funeqs*, and turn them into givens.
Consider (Trac #4935)
type instance F True a b = a
type instance F False a b = b
[w] F c a b ~ gamma
(c ~ True) => a ~ gamma
(c ~ False) => b ~ gamma
Obviously this is soluble with gamma := F c a b. But
Since solveCTyFunEqs happens at the very end of solving, the only way
to solve the two implications is temporarily consider (F c a b ~ gamma)
as Given and push it inside the implications. Now, when we come
out again at the end, having solved the implications solveCTyFunEqs
will solve this equality.
Turning type-function equalities into Givens is easy becase they
*stay inert*. No need to re-process them.
We don't try to turn any *other* Wanteds into Givens:
* For example, we should not push given dictionaries in because
of example LongWayOverlapping.hs, where we might get strange
overlap errors between far-away constraints in the program.
There might be cases where interactions between wanteds can help
to solve a constraint. For example
class C a b | a -> b
(C Int alpha), (forall d. C d blah => C Int a)
If we push the (C Int alpha) inwards, as a given, it can produce a
fundep (alpha~a) and this can float out again and be used to fix
alpha. (In general we can't float class constraints out just in case
(C d blah) might help to solve (C Int a).) But we ignore this possiblity.
For Derived constraints we don't have evidence, so we do not turn
them into Givens. There can *be* deriving CFunEqCans; see Trac #8129.
\begin{code}
getInertEqs :: TcS (TyVarEnv [Ct])
getInertEqs = do { inert <- getTcSInerts
; return (inert_eqs (inert_cans inert)) }
getInertUnsolved :: TcS (Cts, Cts)
getInertUnsolved
= do { is <- getTcSInerts
; let icans = inert_cans is
unsolved_irreds = Bag.filterBag is_unsolved (inert_irreds icans)
unsolved_dicts = foldDicts add_if_unsolved (inert_dicts icans) emptyCts
unsolved_funeqs = foldFunEqs add_if_unsolveds (inert_funeqs icans) emptyCts
unsolved_eqs = foldVarEnv add_if_unsolveds emptyCts (inert_eqs icans)
unsolved_flats = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
unsolved_dicts `unionBags` unsolved_funeqs
; return (unsolved_flats, inert_insols icans) }
where
add_if_unsolved :: Ct -> Cts -> Cts
add_if_unsolved ct cts | is_unsolved ct = cts `extendCts` ct
| otherwise = cts
add_if_unsolveds :: [Ct] -> Cts -> Cts
add_if_unsolveds eqs cts = foldr add_if_unsolved cts eqs
is_unsolved ct = not (isGivenCt ct)
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 ((||) . any 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)))) }
lookupFlatEqn :: TyCon -> [Type] -> TcS (Maybe (CtEvidence, TcType))
lookupFlatEqn fam_tc tys
= do { IS { inert_solved_funeqs = solved_funeqs
, inert_flat_cache = flat_cache
, inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
; return (findFunEq solved_funeqs fam_tc tys `firstJust`
lookup_inerts inert_funeqs `firstJust`
findFunEq flat_cache fam_tc tys) }
where
lookup_inerts inert_funeqs
| (ct:_) <- findFunEqs inert_funeqs fam_tc tys
= Just (ctEvidence ct, cc_rhs ct)
| otherwise
= Nothing
lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts pty
= do { IS { inert_solved_dicts = solved_dicts
, inert_cans = inert_cans }
<- getTcSInerts
; return $ case (classifyPredType pty) of
ClassPred cls tys
| Just ctev <- findDict solved_dicts cls tys
-> Just ctev
| Just ct <- findDict (inert_dicts inert_cans) cls tys
-> Just (ctEvidence ct)
EqPred ty1 _ty2
| Just tv <- getTyVar_maybe ty1
-> foldr exact_match Nothing (findTyEqs (inert_eqs inert_cans) tv)
| Just (tc, tys) <- splitTyConApp_maybe ty1
-> foldr exact_match Nothing (findFunEqs (inert_funeqs inert_cans) tc tys)
IrredPred {} -> foldrBag exact_match Nothing (inert_irreds inert_cans)
_other -> Nothing
}
where
exact_match :: Ct -> Maybe CtEvidence -> Maybe CtEvidence
exact_match ct deflt | let ctev = ctEvidence ct
, ctEvPred ctev `tcEqType` pty
= Just ctev
| otherwise
= deflt
lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
= findDict solved cls tys
\end{code}
%************************************************************************
%* *
TyEqMap
%* *
%************************************************************************
\begin{code}
type TyEqMap a = TyVarEnv a
findTyEqs :: TyEqMap EqualCtList -> TyVar -> EqualCtList
findTyEqs m tv = lookupVarEnv m tv `orElse` []
\end{code}
%************************************************************************
%* *
TcAppMap, DictMap, FunEqMap
%* *
%************************************************************************
\begin{code}
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))
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
sizeDictMap :: DictMap a -> Int
sizeDictMap m = foldDicts (\ _ x -> x+1) m 0
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 = mapUFM do_tm m
where
do_tm tm = foldTM insert_mb tm emptyTM
insert_mb ct@(CDictCan { cc_tyargs = tys }) tm
| f ct = insertTM tys ct tm
| otherwise = tm
insert_mb ct _ = pprPanic "filterDicts" (ppr ct)
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] -> [a]
findFunEqs m tc tys = findTcApp m (getUnique tc) tys `orElse` []
funEqsToList :: FunEqMap [a] -> [a]
funEqsToList m = foldTcAppMap (++) m []
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
insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
addFunEq :: FunEqMap EqualCtList -> TyCon -> [Type] -> Ct -> FunEqMap EqualCtList
addFunEq m tc tys item
= alterUFM alter_tm m (getUnique tc)
where
alter_tm mb_tm = Just (alterTM tys alter_cts (mb_tm `orElse` emptyTM))
alter_cts Nothing = Just [item]
alter_cts (Just funeqs) = Just (item : funeqs)
replaceFunEqs :: FunEqMap EqualCtList -> TyCon -> [Type] -> Ct -> FunEqMap EqualCtList
replaceFunEqs m tc tys ct = insertTcApp m (getUnique tc) tys [ct]
partitionFunEqs :: (Ct -> Bool) -> FunEqMap EqualCtList -> (Bag Ct, FunEqMap EqualCtList)
partitionFunEqs f m = foldTcAppMap k m (emptyBag, emptyFunEqs)
where
k cts (yeses, noes)
= ( case eqs_out of
[] -> yeses
_ -> yeses `unionBags` listToBag eqs_out
, case eqs_in of
CFunEqCan { cc_fun = tc, cc_tyargs = tys } : _
-> insertTcApp noes (getUnique tc) tys eqs_in
_ -> noes )
where
(eqs_out, eqs_in) = partition f cts
\end{code}
%************************************************************************
%* *
%* The TcS solver monad *
%* *
%************************************************************************
Note [The TcS monad]
~~~~~~~~~~~~~~~~~~~~
The TcS monad is a weak form of the main Tc monad
All you can do is
* fail
* allocate new variables
* fill in evidence variables
Filling in a dictionary evidence variable means to create a binding
for it, so TcS carries a mutable location where the binding can be
added. This is initialised from the innermost implication constraint.
\begin{code}
data TcSEnv
= TcSEnv {
tcs_ev_binds :: EvBindsVar,
tcs_ty_binds :: IORef (Bool, TyVarEnv (TcTyVar, TcType)),
tcs_count :: IORef Int,
tcs_inerts :: IORef InertSet,
tcs_worklist :: IORef WorkList,
tcs_implics :: IORef (Bag Implication)
}
\end{code}
\begin{code}
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)
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) }
traceFireTcS :: Ct -> SDoc -> TcS ()
traceFireTcS ct doc
= TcS $ \env ->
do { dflags <- getDynFlags
; when (dopt Opt_D_dump_cs_trace dflags && traceLevel dflags >= 1) $
do { n <- TcM.readTcRef (tcs_count env)
; let msg = int n <> brackets (ppr (ctLocDepth (ctev_loc ev)))
<+> ppr ev <> colon <+> doc
; TcM.debugDumpTcRn msg } }
where ev = cc_ev ct
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 { ty_binds_var <- TcM.newTcRef (False, emptyVarEnv)
; step_count <- TcM.newTcRef 0
; inert_var <- TcM.newTcRef is
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
, tcs_ty_binds = ty_binds_var
, tcs_count = step_count
, tcs_inerts = inert_var
, tcs_worklist = panic "runTcS: worklist"
, tcs_implics = panic "runTcS: implics" }
; res <- unTcS tcs env
; (_, ty_binds) <- TcM.readTcRef ty_binds_var
; mapM_ do_unification (varEnvElts ty_binds)
; TcM.whenDOptM Opt_D_dump_cs_trace $
do { count <- TcM.readTcRef step_count
; when (count > 0) $
TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count ) }
#ifdef DEBUG
; ev_binds <- TcM.getTcEvBinds ev_binds_var
; checkForCyclicBinds ev_binds
#endif
; return res }
where
do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
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 -> Untouchables -> InertSet -> TcS a -> TcS a
nestImplicTcS ref inner_untch inerts (TcS thing_inside)
= TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
, tcs_count = count } ->
do { new_inert_var <- TcM.newTcRef inerts
; let nest_env = TcSEnv { tcs_ev_binds = ref
, tcs_ty_binds = ty_binds
, tcs_count = count
, tcs_inerts = new_inert_var
, tcs_worklist = panic "nextImplicTcS: worklist"
, tcs_implics = panic "nextImplicTcS: implics"
}
; res <- TcM.setUntouchables inner_untch $
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
; let nest_env = env { tcs_inerts = new_inert_var
, tcs_worklist = panic "nextImplicTcS: worklist"
, tcs_implics = panic "nextImplicTcS: implics" }
; thing_inside nest_env }
tryTcS :: TcS a -> TcS a
tryTcS (TcS thing_inside)
= TcS $ \env ->
do { is_var <- TcM.newTcRef emptyInert
; ty_binds_var <- TcM.newTcRef (False, emptyVarEnv)
; ev_binds_var <- TcM.newTcEvBinds
; let nest_env = env { tcs_ev_binds = ev_binds_var
, tcs_ty_binds = ty_binds_var
, tcs_inerts = is_var
, tcs_worklist = panic "nextImplicTcS: worklist"
, tcs_implics = panic "nextImplicTcS: implics" }
; 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) }
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)
; let (res,new_work) = f wl_curr
; wrapTcS (TcM.writeTcRef wl_var new_work)
; return res }
withWorkList :: Cts -> TcS () -> TcS (Bag Implication)
withWorkList work_items (TcS thing_inside)
= TcS $ \ tcs_env ->
do { let init_work_list = foldrBag extendWorkListCt emptyWorkList work_items
; new_wl_var <- TcM.newTcRef init_work_list
; new_implics_var <- TcM.newTcRef emptyBag
; thing_inside (tcs_env { tcs_worklist = new_wl_var
, tcs_implics = new_implics_var })
; final_wl <- TcM.readTcRef new_wl_var
; implics <- TcM.readTcRef new_implics_var
; ASSERT( isEmptyWorkList final_wl )
return implics }
updTcSImplics :: (Bag Implication -> Bag Implication) -> TcS ()
updTcSImplics f
= do { impl_ref <- getTcSImplicsRef
; wrapTcS $ do { implics <- TcM.readTcRef impl_ref
; TcM.writeTcRef impl_ref (f implics) } }
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 = extendCts old_insols ct } }
where
already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
getTcSImplicsRef :: TcS (IORef (Bag Implication))
getTcSImplicsRef = TcS (return . tcs_implics)
getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds)
getUntouchables :: TcS Untouchables
getUntouchables = wrapTcS TcM.getUntouchables
getGivenInfo :: TcS a -> TcS (Bool, [TcTyVar], a)
getGivenInfo thing_inside
= do { updInertTcS reset_vars
; res <- thing_inside
; is <- getTcSInerts
; return (inert_no_eqs (inert_cans is), inert_fsks is, res) }
where
reset_vars :: InertSet -> InertSet
reset_vars is = is { inert_cans = (inert_cans is) { inert_no_eqs = True }
, inert_fsks = [] }
getTcSTyBinds :: TcS (IORef (Bool, TyVarEnv (TcTyVar, TcType)))
getTcSTyBinds = TcS (return . tcs_ty_binds)
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
getTcSTyBindsMap = do { ref <- getTcSTyBinds
; wrapTcS $ do { (_, binds) <- TcM.readTcRef ref
; return binds } }
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 )
do { ref <- getTcSTyBinds
; wrapTcS $
do { (_dirty, ty_binds) <- TcM.readTcRef ref
; when debugIsOn $
TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
vcat [ text "TERRIBLE ERROR: double set of meta type variable"
, ppr tv <+> text ":=" <+> ppr ty
, text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
; TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty)
; TcM.writeTcRef ref (True, extendVarEnv ty_binds tv (tv,ty)) } }
reportUnifications :: TcS a -> TcS (Bool, a)
reportUnifications thing_inside
= do { ty_binds_var <- getTcSTyBinds
; outer_dirty <- wrapTcS $
do { (outer_dirty, binds1) <- TcM.readTcRef ty_binds_var
; TcM.writeTcRef ty_binds_var (False, binds1)
; return outer_dirty }
; res <- thing_inside
; wrapTcS $
do { (inner_dirty, binds2) <- TcM.readTcRef ty_binds_var
; if inner_dirty then
return (True, res)
else
do { TcM.writeTcRef ty_binds_var (outer_dirty, binds2)
; return (False, res) } } }
\end{code}
\begin{code}
getDefaultInfo :: TcS ([Type], (Bool, Bool))
getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
getInstEnvs :: TcS (InstEnv, InstEnv)
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 = pprType $ mkEqPred ty1 ty2
isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
isTouchableMetaTyVarTcS tv
= do { untch <- getUntouchables
; return $ isTouchableMetaTyVar untch 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
zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
\end{code}
Note [Do not add duplicate derived insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In general we *must* add an insoluble (Int ~ Bool) even if there is
one such there already, because they may come from distinct call
sites. Not only do we want an error message for each, but with
-fdefer-type-errors we must generate evidence for each. But for
*derived* insolubles, we only want to report each one once. Why?
(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
equality many times, as the original constraint is sucessively rewritten.
(b) Ditto the successive iterations of the main solver itself, as it traverses
the constraint tree. See example below.
Also for *given* insolubles we may get repeated errors, as we
repeatedly traverse the constraint tree. These are relatively rare
anyway, so removing duplicates seems ok. (Alternatively we could take
the SrcLoc into account.)
Note that the test does not need to be particularly efficient because
it is only used if the program has a type error anyway.
Example of (b): assume a top-level class and instance declaration:
class D a b | a -> b
instance D [a] [a]
Assume we have started with an implication:
forall c. Eq c => { wc_flat = D [c] c [W] }
which we have simplified to:
forall c. Eq c => { wc_flat = D [c] c [W]
, wc_insols = (c ~ [c]) [D] }
For some reason, e.g. because we floated an equality somewhere else,
we might try to re-solve this implication. If we do not do a
dropDerivedWC, then we will end up trying to solve the following
constraints the second time:
(D [c] c) [W]
(c ~ [c]) [D]
which will result in two Deriveds to end up in the insoluble set:
wc_flat = D [c] c [W]
wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
\begin{code}
newFlattenSkolem :: CtEvidence
-> TcType
-> TcS (CtEvidence, TcType)
newFlattenSkolem ev fam_ty
| isGiven ev
= do { tv <- wrapTcS $
do { uniq <- TcM.newUnique
; let name = TcM.mkTcTyVarName uniq (fsLit "f")
; return $ mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty) }
; traceTcS "New Flatten Skolem Born" $
ppr tv <+> text "[:= " <+> ppr fam_ty <+> text "]"
; updInertTcS $ \ is -> is { inert_fsks = tv : inert_fsks is }
; let rhs_ty = mkTyVarTy tv
ctev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
, ctev_evtm = EvCoercion (mkTcNomReflCo fam_ty)
, ctev_loc = (ctev_loc ev) { ctl_origin = FlatSkolOrigin } }
; return (ctev, rhs_ty) }
| otherwise
= do { rhs_ty <- newFlexiTcSTy (typeKind fam_ty)
; ctev <- newWantedEvVarNC (ctev_loc ev) (mkTcEqPred fam_ty rhs_ty)
; return (ctev, rhs_ty) }
extendFlatCache :: TyCon -> [Type] -> CtEvidence -> TcType -> TcS ()
extendFlatCache tc xi_args ev rhs_xi
= do { dflags <- getDynFlags
; when (gopt Opt_FlatCache dflags) $
updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
is { inert_flat_cache = insertFunEq fc tc xi_args (ev, rhs_xi) } }
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)
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
; 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 MaybeNew = Fresh CtEvidence | Cached EvTerm
isFresh :: MaybeNew -> Bool
isFresh (Fresh {}) = True
isFresh _ = False
getEvTerm :: MaybeNew -> EvTerm
getEvTerm (Fresh ctev) = ctEvTerm ctev
getEvTerm (Cached tm) = tm
getEvTerms :: [MaybeNew] -> [EvTerm]
getEvTerms = map getEvTerm
freshGoal :: MaybeNew -> Maybe CtEvidence
freshGoal (Fresh ctev) = Just ctev
freshGoal _ = Nothing
freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals mns = [ ctev | Fresh ctev <- mns ]
setEvBind :: EvVar -> EvTerm -> TcS ()
setEvBind the_ev tm
= do { traceTcS "setEvBind" $ vcat [ text "ev =" <+> ppr the_ev
, text "tm =" <+> ppr tm ]
; tc_evbinds <- getTcEvBinds
; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev tm }
newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar loc (pred, rhs)
= do { new_ev <- wrapTcS $ TcM.newEvVar pred
; setEvBind new_ev rhs
; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC loc pty
= do { new_ev <- wrapTcS $ TcM.newEvVar pty
; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
newWantedEvVarNonrec :: CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVarNonrec loc pty
= do { mb_ct <- lookupInInerts pty
; case mb_ct of
Just ctev | not (isDerived ctev) && ctEvCheckDepth (ctLocDepth loc) ctev
-> do { traceTcS "newWantedEvVarNonrec/cache hit" $ ppr ctev
; return (Cached (ctEvTerm ctev)) }
_ -> do { ctev <- newWantedEvVarNC loc pty
; traceTcS "newWantedEvVarNonrec/cache miss" $ ppr ctev
; return (Fresh ctev) } }
newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar loc pty
= do { mb_ct <- lookupInInerts pty
; case mb_ct of
Just ctev | not (isDerived ctev)
-> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
; return (Cached (ctEvTerm ctev)) }
_ -> do { ctev <- newWantedEvVarNC loc pty
; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
; return (Fresh ctev) } }
newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
newDerived loc pty
= do { mb_ct <- lookupInInerts pty
; return (case mb_ct of
Just {} -> Nothing
Nothing -> Just (CtDerived { ctev_pred = pty, ctev_loc = loc })) }
instDFunConstraints :: CtLoc -> TcThetaType -> TcS [MaybeNew]
instDFunConstraints loc = mapM (newWantedEvVar loc)
\end{code}
Note [xCFlavor]
~~~~~~~~~~~~~~~
A call might look like this:
xCtFlavor ev subgoal-preds evidence-transformer
ev is Given => use ev_decomp to create new Givens for subgoal-preds,
and return them
ev is Wanted => create new wanteds for subgoal-preds,
use ev_comp to bind ev,
return fresh wanteds (ie ones not cached in inert_cans or solved)
ev is Derived => create new deriveds for subgoal-preds
(unless cached in inert_cans or solved)
Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
Ones that are already cached are not returned
Example
ev : Tree a b ~ Tree c d
xCtEvidence ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. c1 c2
, ev_decomp = \c. [nth 1 c, nth 2 c] })
(\fresh-goals. stuff)
Note [Bind new Givens immediately]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For Givens we make new EvVars and bind them immediately. We don't worry
about caching, but we don't expect complicated calculations among Givens.
It is important to bind each given:
class (a~b) => C a b where ....
f :: C a b => ....
Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
But that superclass selector can't (yet) appear in a coercion
(see evTermCoercion), so the easy thing is to bind it to an Id.
See Note [Coercion evidence terms] in TcEvidence.
Note [Do not create Given kind equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We do not want to create a Given like
kv ~ k -- kv is a skolem kind variable
-- Reason we don't yet support non-Refl kind equalities
or t1::k1 ~ t2::k2 -- k1 and k2 are un-equal kinds
-- Reason: (~) is kind-uniform at the moment, and
-- k1/k2 may be distinct kind skolems
This showed up in Trac #8566, where we had a data type
data I (u :: U *) (r :: [*]) :: * where
A :: I (AA t as) r -- Existential k
so A has type
A :: forall (u:U *) (r:[*]) Universal
(k:BOX) (t:k) (as:[U *]). Existential
(u ~ AA * k t as) => I u r
There is no direct kind equality, but in a pattern match where 'u' is
instantiated to, say, (AA * kk t1 as1), we'd decompose to get
k ~ kk, t ~ t1, as ~ as1
This is bad. We "fix" this by simply ignoring
* the Given kind equality
* AND the Given type equality (t:k1) ~ (t1:kk)
But the Right Thing is to add kind equalities!
\begin{code}
xCtEvidence :: CtEvidence
-> XEvTerm
-> TcS [CtEvidence]
xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
(XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
= ASSERT( equalLength ptys (decomp_fn tm) )
mapM (newGivenEvVar loc)
(filterOut bad_given_pred (ptys `zip` decomp_fn tm))
where
bad_given_pred (pred_ty, _)
| EqPred t1 t2 <- classifyPredType pred_ty
= isKind t1 || not (typeKind t1 `tcEqKind` typeKind t2)
| otherwise
= False
xCtEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc })
(XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
= do { new_evars <- mapM (newWantedEvVar loc) ptys
; setEvBind evar (comp_fn (getEvTerms new_evars))
; return (freshGoals new_evars) }
xCtEvidence (CtDerived { ctev_loc = loc })
(XEvTerm { ev_preds = ptys })
= do { ders <- mapM (newDerived loc) ptys
; return (catMaybes ders) }
rewriteEvidence :: CtEvidence
-> TcPredType
-> TcCoercion
-> TcS (Maybe CtEvidence)
rewriteEvidence (CtDerived { ctev_loc = loc }) new_pred _co
=
newDerived loc new_pred
rewriteEvidence old_ev new_pred co
| isTcReflCo co
= return (Just (if ctEvPred old_ev `tcEqType` new_pred
then old_ev
else old_ev { ctev_pred = new_pred }))
rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
; return (Just new_ev) }
where
new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co))
rewriteEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
= do { new_evar <- newWantedEvVar loc new_pred
; MASSERT( tcCoercionRole co == Nominal )
; setEvBind evar (mkEvCast (getEvTerm new_evar) (mkTcSubCo co))
; return (freshGoal new_evar) }
rewriteEqEvidence :: CtEvidence
-> SwapFlag
-> TcType -> TcType
-> TcCoercion
-> TcCoercion
-> TcS (Maybe CtEvidence)
rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
| CtDerived { ctev_loc = loc } <- old_ev
= newDerived loc (mkEqPred nlhs nrhs)
| NotSwapped <- swapped
, isTcReflCo lhs_co
, isTcReflCo rhs_co
, let new_pred = mkTcEqPred nlhs nrhs
= return (Just (if ctEvPred old_ev `tcEqType` new_pred
then old_ev
else old_ev { ctev_pred = new_pred }))
| CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
= do { let new_tm = EvCoercion (lhs_co
`mkTcTransCo` maybeSym swapped (evTermCoercion old_tm)
`mkTcTransCo` mkTcSymCo rhs_co)
; new_ev <- newGivenEvVar loc (new_pred, new_tm)
; return (Just new_ev) }
| CtWanted { ctev_evar = evar, ctev_loc = loc } <- old_ev
= do { new_evar <- newWantedEvVar loc new_pred
; let co = maybeSym swapped $
mkTcSymCo lhs_co
`mkTcTransCo` evTermCoercion (getEvTerm new_evar)
`mkTcTransCo` rhs_co
; setEvBind evar (EvCoercion co)
; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
; return (freshGoal new_evar) }
| otherwise
= panic "rewriteEvidence"
where
new_pred = mkEqPred nlhs nrhs
maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
maybeSym IsSwapped co = mkTcSymCo co
maybeSym NotSwapped co = co
matchOpenFam :: TyCon -> [Type] -> TcS (Maybe FamInstMatch)
matchOpenFam tycon args = wrapTcS $ tcLookupFamInst tycon args
matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
matchFam tycon args
| isOpenSynFamilyTyCon tycon
= do { maybe_match <- matchOpenFam tycon args
; case maybe_match of
Nothing -> return Nothing
Just (FamInstMatch { fim_instance = famInst
, fim_tys = inst_tys })
-> let co = mkTcUnbranchedAxInstCo Nominal (famInstAxiom famInst) inst_tys
ty = pSnd $ tcCoercionKind co
in return $ Just (co, ty) }
| Just ax <- isClosedSynFamilyTyCon_maybe tycon
, Just (ind, inst_tys) <- chooseBranch ax args
= let co = mkTcAxInstCo Nominal ax ind inst_tys
ty = pSnd (tcCoercionKind co)
in return $ Just (co, ty)
| Just ops <- isBuiltInSynFamTyCon_maybe tycon =
return $ do (r,ts,ty) <- sfMatchFam ops args
return (mkTcAxiomRuleCo r ts [], ty)
| otherwise
= return Nothing
\end{code}
\begin{code}
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
; mev <- newWantedEvVar loc $ case role of
Nominal -> mkTcEqPred phi1 phi2
Representational -> mkCoerciblePred phi1 phi2
Phantom -> panic "deferTcSForAllEq Phantom"
; coe_inside <- case mev of
Cached ev_tm -> return (evTermCoercion ev_tm)
Fresh ctev -> do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds
; env <- wrapTcS $ TcM.getLclEnv
; let ev_binds = TcEvBinds ev_binds_var
new_ct = mkNonCanonical ctev
new_co = evTermCoercion (ctEvTerm ctev)
new_untch = pushUntouchables (tcl_untch env)
; let wc = WC { wc_flat = singleCt new_ct
, wc_impl = emptyBag
, wc_insol = emptyCts }
imp = Implic { ic_untch = new_untch
, ic_skols = skol_tvs
, ic_fsks = []
, ic_no_eqs = True
, ic_given = []
, ic_wanted = wc
, ic_insol = False
, ic_binds = ev_binds_var
, ic_env = env
, ic_info = skol_info }
; updTcSImplics (consBag imp)
; return (TcLetCo ev_binds new_co) }
; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs)
}
\end{code}