\begin{code} {-# OPTIONS -fno-warn-tabs #-} -- The above warning supression flag is a temporary kludge. -- While working on this module you are encouraged to remove it and -- detab the module (please do the detabbing in a separate patch). See -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces -- for details -- Type definitions for the constraint solver module TcSMonad ( -- Canonical constraints, definition is now in TcRnTypes WorkList(..), isEmptyWorkList, emptyWorkList, workListFromEq, workListFromNonEq, workListFromCt, extendWorkListEq, extendWorkListNonEq, extendWorkListCt, appendWorkListCt, appendWorkListEqs, unionWorkList, selectWorkItem, getTcSWorkList, updWorkListTcS, updWorkListTcS_return, keepWanted, Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts, emitFrozenError, isWanted, isGivenOrSolved, isDerived, isGivenOrSolvedCt, isGivenCt_maybe, isWantedCt, isDerivedCt, pprFlavorArising, isFlexiTcsTv, canRewrite, canSolve, combineCtLoc, mkSolvedFlavor, mkGivenFlavor, mkWantedFlavor, getWantedLoc, TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality traceFireTcS, bumpStepCountTcS, doWithInert, tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS, SimplContext(..), isInteractive, simplEqsOnly, performDefaulting, -- Creation of evidence variables newEvVar, forceNewEvVar, delCachedEvVar, updateFlatCache, flushFlatCache, newGivenEqVar, newEqVar, newKindConstraint, EvVarCreated (..), isNewEvVar, FlatEqOrigin ( .. ), origin_matches, -- Setting evidence variables setEqBind, setEvBind, setWantedTyBind, getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, getTcEvBindsMap, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSEvVarCacheMap, getTcSEvVarFlatCache, setTcSEvVarCacheMap, pprEvVarCache, newFlattenSkolemTy, -- Flatten skolems -- Inerts InertSet(..), getInertEqs, liftInertEqsTy, getCtCoercion, emptyInert, getTcSInerts, updInertSet, extractUnsolved, extractUnsolvedTcS, modifyInertTcS, updInertSetTcS, partitionCCanMap, partitionEqMap, getRelevantCts, extractRelevantInerts, CCanMap (..), CtTypeMap, pprCtTypeMap, mkPredKeyForTypeMap, partitionCtTypeMap, instDFunTypes, -- Instantiation instDFunConstraints, newFlexiTcSTy, instFlexiTcS, compatKind, compatKindTcS, isSubKindTcS, unifyKindTcS, TcsUntouchables, isTouchableMetaTyVar, isTouchableMetaTyVar_InRange, getDefaultInfo, getDynFlags, matchClass, matchFam, MatchInstResult (..), checkWellStagedDFun, warnTcS, pprEq -- Smaller utils, re-exported from TcM -- TODO (DV): these are only really used in the -- instance matcher in TcSimplify. I am wondering -- if the whole instance matcher simply belongs -- here ) where #include "HsVersions.h" import HscTypes import BasicTypes 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 {-# SOURCE #-} qualified TcUnify as TcM ( unifyKindEq, mkKindErrorCtxt ) import Kind import TcType import DynFlags import Type import TcEvidence import Class import TyCon import TypeRep import Name import Var import VarEnv import Outputable import Bag import MonadUtils import VarSet import FastString import Util import Id import TcRnTypes import Unique import UniqFM import Maybes ( orElse ) import Control.Monad( when ) import StaticFlags( opt_PprStyle_Debug ) import Data.IORef import TrieMap \end{code} \begin{code} compatKind :: Kind -> Kind -> Bool compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 compatKindTcS :: Kind -> Kind -> TcS Bool -- Because kind unification happens during constraint solving, we have -- to make sure that two kinds are zonked before we compare them. compatKindTcS k1 k2 = wrapTcS (TcM.compatKindTcM k1 k2) isSubKindTcS :: Kind -> Kind -> TcS Bool isSubKindTcS k1 k2 = wrapTcS (TcM.isSubKindTcM k1 k2) unifyKindTcS :: Type -> Type -- Context -> Kind -> Kind -- Corresponding kinds -> TcS Bool unifyKindTcS ty1 ty2 ki1 ki2 = wrapTcS $ TcM.addErrCtxtM ctxt $ do (_errs, mb_r) <- TcM.tryTc (TcM.unifyKindEq ki1 ki2) return (maybe False (const True) mb_r) where ctxt = TcM.mkKindErrorCtxt ty1 ki1 ty2 ki2 \end{code} %************************************************************************ %* * %* Worklists * %* Canonical and non-canonical constraints that the simplifier has to * %* work on. Including their simplification depths. * %* * %* * %************************************************************************ Note [WorkList] ~~~~~~~~~~~~~~~ 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} -- See Note [WorkList] data WorkList = WorkList { wl_eqs :: [Ct], wl_funeqs :: [Ct], wl_rest :: [Ct] } unionWorkList :: WorkList -> WorkList -> WorkList unionWorkList new_wl orig_wl = WorkList { wl_eqs = wl_eqs new_wl ++ wl_eqs orig_wl , wl_funeqs = wl_funeqs new_wl ++ wl_funeqs orig_wl , wl_rest = wl_rest new_wl ++ wl_rest orig_wl } extendWorkListEq :: Ct -> WorkList -> WorkList -- Extension by equality extendWorkListEq ct wl | Just {} <- isCFunEqCan_Maybe ct = wl { wl_funeqs = ct : wl_funeqs wl } | otherwise = wl { wl_eqs = ct : wl_eqs wl } extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } extendWorkListCt :: Ct -> WorkList -> WorkList -- Agnostic extendWorkListCt ct wl | isEqVar (cc_id ct) = extendWorkListEq ct wl | otherwise = extendWorkListNonEq ct wl appendWorkListCt :: [Ct] -> WorkList -> WorkList -- Agnostic appendWorkListCt cts wl = foldr extendWorkListCt wl cts appendWorkListEqs :: [Ct] -> WorkList -> WorkList -- Append a list of equalities appendWorkListEqs cts wl = foldr extendWorkListEq wl cts isEmptyWorkList :: WorkList -> Bool isEmptyWorkList wl = null (wl_eqs wl) && null (wl_rest wl) && null (wl_funeqs wl) emptyWorkList :: WorkList emptyWorkList = WorkList { wl_eqs = [], wl_rest = [], wl_funeqs = []} workListFromEq :: Ct -> WorkList workListFromEq ct = extendWorkListEq ct emptyWorkList workListFromNonEq :: Ct -> WorkList workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList workListFromCt :: Ct -> WorkList -- Agnostic workListFromCt ct | isEqVar (cc_id 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 }) (_,(ct:cts),_) -> (Just ct, wl { wl_funeqs = cts }) (_,_,(ct:cts)) -> (Just ct, wl { wl_rest = cts }) (_,_,_) -> (Nothing,wl) -- Pretty printing 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) ] keepWanted :: Cts -> Cts keepWanted = filterBag isWantedCt -- DV: there used to be a note here that read: -- ``Important: use fold*r*Bag to preserve the order of the evidence variables'' -- DV: Is this still relevant? \end{code} %************************************************************************ %* * %* Inert sets * %* * %* * %************************************************************************ Note [InertSet invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ An InertSet is a bag of canonical constraints, with the following invariants: 1 No two constraints react with each other. A tricky case is when there exists a given (solved) dictionary constraint and a wanted identical constraint in the inert set, but do not react because reaction would create loopy dictionary evidence for the wanted. See note [Recursive dictionaries] 2 Given equalities form an idempotent substitution [none of the given LHS's occur in any of the given RHS's or reactant parts] 3 Wanted equalities also form an idempotent substitution 4 The entire set of equalities is acyclic. 5 Wanted dictionaries are inert with the top-level axiom set 6 Equalities of the form tv1 ~ tv2 always have a touchable variable on the left (if possible). 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints will be marked as solved right before being pushed into the inert set. See note [Touchables and givens]. 8 No Given constraint mentions a touchable unification variable, but Given/Solved may do so. 9 Given constraints will also have their superclasses in the inert set, but Given/Solved will not. Note that 6 and 7 are /not/ enforced by canonicalization but rather by insertion in the inert list, ie by TcInteract. During the process of solving, the inert set will contain some previously given constraints, some wanted constraints, and some given constraints which have arisen from solving wanted constraints. For now we do not distinguish between given and solved constraints. Note that we must switch wanted inert items to given when going under an implication constraint (when in top-level inference mode). \begin{code} data CCanMap a = CCanMap { cts_given :: UniqFM Cts -- Invariant: all Given , cts_derived :: UniqFM Cts -- Invariant: all Derived , cts_wanted :: UniqFM Cts } -- Invariant: all Wanted cCanMapToBag :: CCanMap a -> Cts cCanMapToBag cmap = foldUFM unionBags rest_wder (cts_given cmap) where rest_wder = foldUFM unionBags rest_der (cts_wanted cmap) rest_der = foldUFM unionBags emptyCts (cts_derived cmap) emptyCCanMap :: CCanMap a emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wanted = emptyUFM } updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a updCCanMap (a,ct) cmap = case cc_flavor ct of Wanted {} -> cmap { cts_wanted = insert_into (cts_wanted cmap) } Given {} -> cmap { cts_given = insert_into (cts_given cmap) } Derived {} -> cmap { cts_derived = insert_into (cts_derived cmap) } where insert_into m = addToUFM_C unionBags m a (singleCt ct) getRelevantCts :: Uniquable a => a -> CCanMap a -> (Cts, CCanMap a) -- Gets the relevant constraints and returns the rest of the CCanMap getRelevantCts a cmap = let relevant = lookup (cts_wanted cmap) `unionBags` lookup (cts_given cmap) `unionBags` lookup (cts_derived cmap) residual_map = cmap { cts_wanted = delFromUFM (cts_wanted cmap) a , cts_given = delFromUFM (cts_given cmap) a , cts_derived = delFromUFM (cts_derived cmap) a } in (relevant, residual_map) where lookup map = lookupUFM map a `orElse` emptyCts getCtTypeMapRelevants :: PredType -> TypeMap Ct -> (Cts, TypeMap Ct) getCtTypeMapRelevants key_pty tmap = partitionCtTypeMap (\ct -> mkPredKeyForTypeMap ct `eqType` key_pty) tmap partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a) -- All constraints that /match/ the predicate go in the bag, the rest remain in the map partitionCCanMap pred cmap = let (ws_map,ws) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_wanted cmap) (ds_map,ds) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_derived cmap) (gs_map,gs) = foldUFM_Directly aux (emptyUFM,emptyCts) (cts_given cmap) in (ws `andCts` ds `andCts` gs, cmap { cts_wanted = ws_map , cts_given = gs_map , cts_derived = ds_map }) where aux k this_cts (mp,acc_cts) = (new_mp, new_acc_cts) where new_mp = addToUFM mp k cts_keep new_acc_cts = acc_cts `andCts` cts_out (cts_out, cts_keep) = partitionBag pred this_cts partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion)) partitionEqMap pred isubst = let eqs_out = foldVarEnv extend_if_pred [] isubst eqs_in = filterVarEnv_Directly (\_ (ct,_) -> not (pred ct)) isubst in (eqs_out, eqs_in) where extend_if_pred (ct,_) cts = if pred ct then ct : cts else cts extractUnsolvedCMap :: CCanMap a -> (Cts, CCanMap a) -- Gets the wanted or derived constraints and returns a residual -- CCanMap with only givens. extractUnsolvedCMap cmap = let wntd = foldUFM unionBags emptyCts (cts_wanted cmap) derd = foldUFM unionBags emptyCts (cts_derived cmap) in (wntd `unionBags` derd, cmap { cts_wanted = emptyUFM, cts_derived = emptyUFM }) -- See Note [InertSet invariants] data InertSet = IS { inert_eqs :: TyVarEnv (Ct,TcCoercion) -- Must all be CTyEqCans! If an entry exists of the form: -- a |-> ct,co -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } -- And co : a ~ xi , inert_eq_tvs :: InScopeSet -- Invariant: superset of inert_eqs tvs , inert_dicts :: CCanMap Class -- Dictionaries only, index is the class , inert_ips :: CCanMap (IPName Name) -- Implicit parameters -- NB: We do not want to use TypeMaps here because functional dependencies -- will only match on the class but not the type. Similarly IPs match on the -- name but not on the whole datatype , inert_funeqs :: CtTypeMap -- Map from family heads to CFunEqCan constraints , inert_irreds :: Cts -- Irreducible predicates , inert_frozen :: Cts -- All non-canonicals are kept here (as frozen errors) } type CtTypeMap = TypeMap Ct pprCtTypeMap :: TypeMap Ct -> SDoc pprCtTypeMap ctmap = ppr (foldTM (:) ctmap []) ctTypeMapCts :: TypeMap Ct -> Cts ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts mkPredKeyForTypeMap :: Ct -> PredType -- Create a key from a constraint to use in the inert CtTypeMap. -- The only interesting case is for family applications, where the -- key is not the whole PredType of cc_id, but rather the family -- equality left hand side (head) mkPredKeyForTypeMap (CFunEqCan { cc_fun = fn, cc_tyargs = xis }) = mkTyConApp fn xis mkPredKeyForTypeMap ct = evVarPred (cc_id ct) partitionCtTypeMap :: (Ct -> Bool) -> TypeMap Ct -> (Cts, TypeMap Ct) -- Kick out the ones that match the predicate and keep the rest in the typemap partitionCtTypeMap f ctmap = foldTM upd_acc ctmap (emptyBag,ctmap) where upd_acc ct (cts,acc_map) | f ct = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map) | otherwise = (cts,acc_map) where ct_key = mkPredKeyForTypeMap ct instance Outputable InertSet where ppr is = vcat [ vcat (map ppr (varEnvElts (inert_eqs is))) , vcat (map ppr (Bag.bagToList $ inert_irreds is)) , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is))) , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is))) , vcat (map ppr (Bag.bagToList $ ctTypeMapCts (inert_funeqs is))) , text "Frozen errors =" <+> -- Clearly print frozen errors braces (vcat (map ppr (Bag.bagToList $ inert_frozen is))) , text "Warning: Not displaying cached (solved) constraints" ] emptyInert :: InertSet emptyInert = IS { inert_eqs = emptyVarEnv , inert_eq_tvs = emptyInScopeSet , inert_frozen = emptyCts , inert_irreds = emptyCts , inert_dicts = emptyCCanMap , inert_ips = emptyCCanMap , inert_funeqs = emptyTM } type AtomicInert = Ct updInertSet :: InertSet -> AtomicInert -> InertSet -- Add a new inert element to the inert set. updInertSet is item | isCTyEqCan item = let upd_err a b = pprPanic "updInertSet" $ vcat [ text "Multiple inert equalities:" , text "Old (already inert):" <+> ppr a , text "Trying to insert :" <+> ppr b ] -- If evidence is cached, pick it up from the flavor! coercion = getCtCoercion item eqs' = extendVarEnv_C upd_err (inert_eqs is) (cc_tyvar item) (item, coercion) inscope' = extendInScopeSetSet (inert_eq_tvs is) (tyVarsOfCt item) in is { inert_eqs = eqs', inert_eq_tvs = inscope' } | Just x <- isCIPCan_Maybe item -- IP = is { inert_ips = updCCanMap (x,item) (inert_ips is) } | isCIrredEvCan item -- Presently-irreducible evidence = is { inert_irreds = inert_irreds is `Bag.snocBag` item } | Just cls <- isCDictCan_Maybe item -- Dictionary = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) } | Just _tc <- isCFunEqCan_Maybe item -- Function equality = let pty = mkPredKeyForTypeMap item upd_funeqs Nothing = Just item upd_funeqs (Just _alredy_there) = panic "updInertSet: item already there!" in is { inert_funeqs = alterTM pty upd_funeqs (inert_funeqs is) } | otherwise = is { inert_frozen = inert_frozen is `Bag.snocBag` item } updInertSetTcS :: AtomicInert -> TcS () -- Add a new item in the inerts of the monad updInertSetTcS item = do { traceTcS "updInertSetTcs {" $ text "Trying to insert new inert item:" <+> ppr item ; modifyInertTcS (\is -> ((), updInertSet is item)) ; traceTcS "updInertSetTcs }" $ empty } modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a -- Modify the inert set with the supplied function modifyInertTcS upd = do { is_var <- getTcSInertsRef ; curr_inert <- wrapTcS (TcM.readTcRef is_var) ; let (a, new_inert) = upd curr_inert ; wrapTcS (TcM.writeTcRef is_var new_inert) ; return a } extractUnsolvedTcS :: TcS (Cts,Cts) -- Extracts frozen errors and remaining unsolved and sets the -- inert set to be the remaining! extractUnsolvedTcS = modifyInertTcS extractUnsolved extractUnsolved :: InertSet -> ((Cts,Cts), InertSet) -- Postcondition -- ------------- -- When: -- ((frozen,cts),is_solved) <- extractUnsolved inert -- Then: -- ----------------------------------------------------------------------------- -- cts | The unsolved (Derived or Wanted only) residual -- | canonical constraints, that is, no CNonCanonicals. -- -----------|----------------------------------------------------------------- -- frozen | The CNonCanonicals of the original inert (frozen errors), -- | of all flavors -- -----------|----------------------------------------------------------------- -- is_solved | Whatever remains from the inert after removing the previous two. -- ----------------------------------------------------------------------------- extractUnsolved is@(IS {inert_eqs = eqs, inert_irreds = irreds}) = let is_solved = is { inert_eqs = solved_eqs , inert_eq_tvs = inert_eq_tvs is , inert_dicts = solved_dicts , inert_ips = solved_ips , inert_irreds = solved_irreds , inert_frozen = emptyCts , inert_funeqs = solved_funeqs } in ((inert_frozen is, unsolved), is_solved) where solved_eqs = filterVarEnv_Directly (\_ (ct,_) -> isGivenOrSolvedCt ct) eqs unsolved_eqs = foldVarEnv (\(ct,_co) cts -> cts `extendCts` ct) emptyCts $ eqs `minusVarEnv` solved_eqs (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenOrSolvedCt) irreds (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is) (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is) (unsolved_funeqs, solved_funeqs) = extractUnsolvedCtTypeMap (inert_funeqs is) unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags` unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs extractUnsolvedCtTypeMap :: TypeMap Ct -> (Cts,TypeMap Ct) extractUnsolvedCtTypeMap = partitionCtTypeMap (not . isGivenOrSolved . cc_flavor) extractRelevantInerts :: Ct -> TcS Cts -- Returns the constraints from the inert set that are 'relevant' to react with -- this constraint. The monad is left with the 'thinner' inerts. -- NB: This function contains logic specific to the constraint solver, maybe move there? extractRelevantInerts wi = modifyInertTcS (extract_inert_relevants wi) where extract_inert_relevants (CDictCan {cc_class = cl}) is = let (cts,dict_map) = getRelevantCts cl (inert_dicts is) in (cts, is { inert_dicts = dict_map }) extract_inert_relevants (CFunEqCan {cc_fun = tc, cc_tyargs = xis}) is = let (cts,feqs_map) = getCtTypeMapRelevants (mkTyConApp tc xis) (inert_funeqs is) in (cts, is { inert_funeqs = feqs_map }) extract_inert_relevants (CIPCan { cc_ip_nm = nm } ) is = let (cts, ips_map) = getRelevantCts nm (inert_ips is) in (cts, is { inert_ips = ips_map }) extract_inert_relevants (CIrredEvCan { }) is = let cts = inert_irreds is in (cts, is { inert_irreds = emptyCts }) extract_inert_relevants _ is = (emptyCts,is) \end{code} %************************************************************************ %* * CtFlavor The "flavor" of a canonical constraint %* * %************************************************************************ \begin{code} getWantedLoc :: Ct -> WantedLoc getWantedLoc ct = ASSERT (isWanted (cc_flavor ct)) case cc_flavor ct of Wanted wl -> wl _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty isWantedCt :: Ct -> Bool isWantedCt ct = isWanted (cc_flavor ct) isDerivedCt :: Ct -> Bool isDerivedCt ct = isDerived (cc_flavor ct) isGivenCt_maybe :: Ct -> Maybe GivenKind isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct) isGivenOrSolvedCt :: Ct -> Bool isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct) canSolve :: CtFlavor -> CtFlavor -> Bool -- canSolve ctid1 ctid2 -- The constraint ctid1 can be used to solve ctid2 -- "to solve" means a reaction where the active parts of the two constraints match. -- active(F xis ~ xi) = F xis -- active(tv ~ xi) = tv -- active(D xis) = D xis -- active(IP nm ty) = nm -- -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold ----------------------------------------- canSolve (Given {}) _ = True canSolve (Wanted {}) (Derived {}) = True canSolve (Wanted {}) (Wanted {}) = True canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given canSolve _ _ = False -- (There is no *evidence* for a derived.) canRewrite :: CtFlavor -> CtFlavor -> Bool -- canRewrite ctid1 ctid2 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 canRewrite = canSolve combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc -- Precondition: At least one of them should be wanted combineCtLoc (Wanted loc) _ = loc combineCtLoc _ (Wanted loc) = loc combineCtLoc (Derived loc ) _ = loc combineCtLoc _ (Derived loc ) = loc combineCtLoc _ _ = panic "combineCtLoc: both given" mkSolvedFlavor :: CtFlavor -> SkolemInfo -> EvTerm -> CtFlavor -- To be called when we actually solve a wanted/derived (perhaps leaving residual goals) mkSolvedFlavor (Wanted loc) sk evterm = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm)) mkSolvedFlavor (Derived loc) sk evterm = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm)) mkSolvedFlavor fl@(Given {}) _sk _evterm = pprPanic "Solving a given constraint!" $ ppr fl mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenOrig mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl mkWantedFlavor :: CtFlavor -> CtFlavor mkWantedFlavor (Wanted loc) = Wanted loc mkWantedFlavor (Derived loc) = Wanted loc mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl) \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_evvar_cache :: IORef EvVarCache, -- Evidence bindings and a cache from predicate types to the created evidence -- variables. The scope of the cache will be the same as the scope of tcs_ev_binds tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)), -- Global type bindings tcs_context :: SimplContext, tcs_untch :: TcsUntouchables, tcs_ic_depth :: Int, -- Implication nesting depth tcs_count :: IORef Int, -- Global step count tcs_inerts :: IORef InertSet, -- Current inert set tcs_worklist :: IORef WorkList -- Current worklist -- TcSEnv invariant: the tcs_evvar_cache is a superset of tcs_inerts, tcs_worklist, tcs_ev_binds which must -- all be disjoint with each other. } data EvVarCache = EvVarCache { evc_cache :: TypeMap (EvVar,CtFlavor) -- Map from PredTys to Evidence variables -- used to avoid creating new goals , evc_flat_cache :: TypeMap (TcCoercion,(Xi,CtFlavor,FlatEqOrigin)) -- Map from family-free heads (F xi) to family-free types. -- Useful during flattening to share flatten skolem generation -- The boolean flag: -- True <-> This equation was generated originally during flattening -- False <-> This equation was generated by having solved a goal } data FlatEqOrigin = WhileFlattening -- Was it generated during flattening? | WhenSolved -- Was it generated when a family equation was solved? | Any origin_matches :: FlatEqOrigin -> FlatEqOrigin -> Bool origin_matches Any _ = True origin_matches WhenSolved WhenSolved = True origin_matches WhileFlattening WhileFlattening = True origin_matches _ _ = False type TcsUntouchables = (Untouchables,TcTyVarSet) -- Like the TcM Untouchables, -- but records extra TcsTv variables generated during simplification -- See Note [Extra TcsTv untouchables] in TcSimplify \end{code} \begin{code} data SimplContext = SimplInfer SDoc -- Inferring type of a let-bound thing | SimplRuleLhs RuleName -- Inferring type of a RULE lhs | SimplInteractive -- Inferring type at GHCi prompt | SimplCheck SDoc -- Checking a type signature or RULE rhs instance Outputable SimplContext where ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n) ppr SimplInteractive = ptext (sLit "SimplInteractive") isInteractive :: SimplContext -> Bool isInteractive SimplInteractive = True isInteractive _ = False simplEqsOnly :: SimplContext -> Bool -- Simplify equalities only, not dictionaries -- This is used for the LHS of rules; ee -- Note [Simplifying RULE lhs constraints] in TcSimplify simplEqsOnly (SimplRuleLhs {}) = True simplEqsOnly _ = False performDefaulting :: SimplContext -> Bool performDefaulting (SimplInfer {}) = False performDefaulting (SimplRuleLhs {}) = False performDefaulting SimplInteractive = True performDefaulting (SimplCheck {}) = True --------------- newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } instance Functor TcS where fmap f m = TcS $ fmap f . unTcS m 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) -- Basic functionality -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ wrapTcS :: TcM a -> TcS a -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS, -- and TcS is supposed to have limited functionality wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds wrapErrTcS :: TcM a -> TcS a -- The thing wrapped should just fail -- There's no static check; it's up to the user -- Having a variant for each error message is too painful wrapErrTcS = wrapTcS wrapWarnTcS :: TcM a -> TcS a -- The thing wrapped should just add a warning, or no-op -- There's no static check; it's up to the user 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) bumpStepCountTcS :: TcS () bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env ; n <- TcM.readTcRef ref ; TcM.writeTcRef ref (n+1) } traceFireTcS :: SubGoalDepth -> SDoc -> TcS () -- Dump a rule-firing trace traceFireTcS depth doc = TcS $ \env -> TcM.ifDOptM Opt_D_dump_cs_trace $ do { n <- TcM.readTcRef (tcs_count env) ; let msg = int n <> text (replicate (tcs_ic_depth env) '>') <> brackets (int depth) <+> doc ; TcM.dumpTcRn msg } runTcS :: SimplContext -> Untouchables -- Untouchables -> InertSet -- Initial inert set -> WorkList -- Initial work list -> TcS a -- What to run -> TcM (a, Bag EvBind) runTcS context untouch is wl tcs = do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_cache_var <- TcM.newTcRef $ EvVarCache { evc_cache = emptyTM, evc_flat_cache = emptyTM } ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds ; step_count <- TcM.newTcRef 0 ; inert_var <- TcM.newTcRef is ; wl_var <- TcM.newTcRef wl ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_evvar_cache = ev_cache_var , tcs_ty_binds = ty_binds_var , tcs_context = context , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet , tcs_count = step_count , tcs_ic_depth = 0 , tcs_inerts = inert_var , tcs_worklist = wl_var } -- Run the computation ; res <- unTcS tcs env -- Perform the type unifications required ; ty_binds <- TcM.readTcRef ty_binds_var ; mapM_ do_unification (varEnvElts ty_binds) ; when debugIsOn $ do { count <- TcM.readTcRef step_count ; when (opt_PprStyle_Debug && count > 0) $ TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count <+> ppr context) } -- And return ; ev_binds <- TcM.readTcRef evb_ref ; return (res, evBindMapBinds ev_binds) } where do_unification (tv,ty) = TcM.writeMetaTyVar tv ty doWithInert :: InertSet -> TcS a -> TcS a doWithInert inert (TcS action) = TcS $ \env -> do { new_inert_var <- TcM.newTcRef inert ; orig_cache_var <- TcM.readTcRef (tcs_evvar_cache env) ; new_cache_var <- TcM.newTcRef orig_cache_var ; action (env { tcs_inerts = new_inert_var , tcs_evvar_cache = new_cache_var }) } nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside) = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds , tcs_evvar_cache = orig_evvar_cache_var , tcs_untch = (_outer_range, outer_tcs) , tcs_count = count , tcs_ic_depth = idepth , tcs_context = ctxt , tcs_inerts = inert_var , tcs_worklist = wl_var } -> do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs) -- The inner_range should be narrower than the outer one -- (thus increasing the set of untouchables) but -- the inner Tcs-untouchables must be unioned with the -- outer ones! -- Inherit the inerts from the outer scope ; orig_inerts <- TcM.readTcRef inert_var ; new_inert_var <- TcM.newTcRef orig_inerts -- Inherit EvVar cache ; orig_evvar_cache <- TcM.readTcRef orig_evvar_cache_var ; evvar_cache <- TcM.newTcRef orig_evvar_cache ; let nest_env = TcSEnv { tcs_ev_binds = ref , tcs_evvar_cache = evvar_cache , tcs_ty_binds = ty_binds , tcs_untch = inner_untch , tcs_count = count , tcs_ic_depth = idepth+1 , tcs_context = ctxtUnderImplic ctxt , tcs_inerts = new_inert_var , tcs_worklist = wl_var -- NB: worklist is going to be empty anyway, -- so reuse the same ref cell } ; thing_inside nest_env } recoverTcS :: TcS a -> TcS a -> TcS a recoverTcS (TcS recovery_code) (TcS thing_inside) = TcS $ \ env -> TcM.recoverM (recovery_code env) (thing_inside env) ctxtUnderImplic :: SimplContext -> SimplContext -- See Note [Simplifying RULE lhs constraints] in TcSimplify ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule") <+> doubleQuotes (ftext n)) ctxtUnderImplic ctxt = ctxt tryTcS :: TcS a -> TcS a -- Like runTcS, but from within the TcS monad -- Completely afresh inerts and worklist, be careful! -- Moreover, we will simply throw away all the evidence generated. tryTcS tcs = TcS (\env -> do { wl_var <- TcM.newTcRef emptyWorkList ; is_var <- TcM.newTcRef emptyInert ; ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var <- TcM.newTcEvBinds ; ev_binds_cache_var <- TcM.newTcRef (EvVarCache emptyTM emptyTM) -- Empty cache: Don't inherit cache from above, see -- Note [tryTcS for defaulting] in TcSimplify ; let env1 = env { tcs_ev_binds = ev_binds_var , tcs_evvar_cache = ev_binds_cache_var , tcs_ty_binds = ty_binds_var , tcs_inerts = is_var , tcs_worklist = wl_var } ; unTcS tcs env1 }) -- Getters and setters of TcEnv fields -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- Getter of inerts and worklist 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) getTcSWorkList :: TcS WorkList getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef) updWorkListTcS :: (WorkList -> WorkList) -> TcS () updWorkListTcS f = updWorkListTcS_return (\w -> ((),f w)) 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 } emitFrozenError :: CtFlavor -> EvVar -> SubGoalDepth -> TcS () -- Emits a non-canonical constraint that will stand for a frozen error in the inerts. emitFrozenError fl ev depth = do { traceTcS "Emit frozen error" (ppr ev <+> dcolon <+> ppr (evVarPred ev)) ; inert_ref <- getTcSInertsRef ; inerts <- wrapTcS (TcM.readTcRef inert_ref) ; let ct = CNonCanonical { cc_id = ev , cc_flavor = fl , cc_depth = depth } inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct } ; wrapTcS (TcM.writeTcRef inert_ref inerts_new) } getDynFlags :: TcS DynFlags getDynFlags = wrapTcS TcM.getDOpts getTcSContext :: TcS SimplContext getTcSContext = TcS (return . tcs_context) getTcEvBinds :: TcS EvBindsVar getTcEvBinds = TcS (return . tcs_ev_binds) getTcSEvVarCache :: TcS (IORef EvVarCache) getTcSEvVarCache = TcS (return . tcs_evvar_cache) flushFlatCache :: TcS () flushFlatCache = do { cache_var <- getTcSEvVarCache ; the_cache <- wrapTcS $ TcM.readTcRef cache_var ; wrapTcS $ TcM.writeTcRef cache_var (the_cache { evc_flat_cache = emptyTM }) } getTcSEvVarCacheMap :: TcS (TypeMap (EvVar,CtFlavor)) getTcSEvVarCacheMap = do { cache_var <- getTcSEvVarCache ; the_cache <- wrapTcS $ TcM.readTcRef cache_var ; return (evc_cache the_cache) } getTcSEvVarFlatCache :: TcS (TypeMap (TcCoercion,(Type,CtFlavor,FlatEqOrigin))) getTcSEvVarFlatCache = do { cache_var <- getTcSEvVarCache ; the_cache <- wrapTcS $ TcM.readTcRef cache_var ; return (evc_flat_cache the_cache) } setTcSEvVarCacheMap :: TypeMap (EvVar,CtFlavor) -> TcS () setTcSEvVarCacheMap cache = do { cache_var <- getTcSEvVarCache ; orig_cache <- wrapTcS $ TcM.readTcRef cache_var ; let new_cache = orig_cache { evc_cache = cache } ; wrapTcS $ TcM.writeTcRef cache_var new_cache } getUntouchables :: TcS TcsUntouchables getUntouchables = TcS (return . tcs_untch) getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType))) getTcSTyBinds = TcS (return . tcs_ty_binds) getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) getTcEvBindsMap :: TcS EvBindMap getTcEvBindsMap = do { EvBindsVar ev_ref _ <- getTcEvBinds ; wrapTcS $ TcM.readTcRef ev_ref } setEqBind :: EqVar -> TcCoercion -> CtFlavor -> TcS CtFlavor setEqBind eqv co fl = setEvBind eqv (EvCoercion co) fl setWantedTyBind :: TcTyVar -> TcType -> TcS () -- Add a type binding -- We never do this twice! setWantedTyBind tv ty = do { ref <- getTcSTyBinds ; wrapTcS $ do { 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.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } } setEvBind :: EvVar -> EvTerm -> CtFlavor -> TcS CtFlavor -- If the flavor is Solved, we cache the new evidence term inside the returned flavor -- see Note [Optimizing Spontaneously Solved Coercions] setEvBind ev t fl = do { tc_evbinds <- getTcEvBinds ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t #ifdef DEBUG ; binds <- getTcEvBindsMap ; let cycle = any (reaches binds) (evVarsOfTerm t) ; when cycle (fail_if_co_loop binds) #endif ; return $ case fl of Given gl (GivenSolved _) -> Given gl (GivenSolved (Just t)) _ -> fl } #ifdef DEBUG where fail_if_co_loop binds = pprTrace "setEvBind" (vcat [ text "Cycle in evidence binds, evvar =" <+> ppr ev , ppr (evBindMapBinds binds) ]) $ when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) reaches :: EvBindMap -> Var -> Bool -- Does this evvar reach ev? reaches ebm ev0 = go ev0 where go ev0 | ev0 == ev = True | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0 = any go (evVarsOfTerm evtrm) | otherwise = False #endif \end{code} Note [Optimizing Spontaneously Solved Coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Spontaneously solved coercions such as alpha := tau used to be bound as everything else in the evidence binds. Subsequently they were used for rewriting other wanted or solved goals. For instance: WorkItem = [S] g1 : a ~ tau Inerts = [S] g2 : b ~ [a] [S] g3 : c ~ [(a,a)] Would result, eventually, after the workitem rewrites the inerts, in the following evidence bindings: g1 = ReflCo tau g2 = ReflCo [a] g3 = ReflCo [(a,a)] g2' = g2 ; [g1] g3' = g3 ; [(g1,g1)] This ia annoying because it puts way too much stress to the zonker and desugarer, since we /know/ at the generation time (spontaneously solving) that the evidence for a particular evidence variable is the identity. For this reason, our solution is to cache inside the GivenSolved flavor of a constraint the term which is actually solving this constraint. Whenever we perform a setEvBind, a new flavor is returned so that if it was a GivenSolved to start with, it remains a GivenSolved with a new evidence term inside. Then, when we use solved goals to rewrite other constraints we simply use whatever is in the GivenSolved flavor and not the constraint cc_id. In our particular case we'd get the following evidence bindings, eventually: g1 = ReflCo tau g2 = ReflCo [a] g3 = ReflCo [(a,a)] g2'= ReflCo [a] g3'= ReflCo [(a,a)] Since we use smart constructors to get rid of g;ReflCo t ~~> g etc. \begin{code} warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS () warnTcS loc warn_if doc | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc | otherwise = return () getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool)) getDefaultInfo = do { ctxt <- getTcSContext ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt)) ; return (ctxt, tys, flags) } -- Just get some environments needed for instance looking up and matching -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> 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) isTouchableMetaTyVar :: TcTyVar -> TcS Bool isTouchableMetaTyVar tv = do { untch <- getUntouchables ; return $ isTouchableMetaTyVar_InRange untch tv } isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool isTouchableMetaTyVar_InRange (untch,untch_tcs) tv = case tcTyVarDetails tv of MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs) -- See Note [Touchable meta type variables] MetaTv {} -> inTouchableRange untch tv _ -> False \end{code} Note [Touchable meta type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Meta type variables allocated *by the constraint solver itself* are always touchable. Example: instance C a b => D [a] where... if we use this instance declaration we "make up" a fresh meta type variable for 'b', which we must later guess. (Perhaps C has a functional dependency.) But since we aren't in the constraint *generator* we can't allocate a Unique in the touchable range for this implication constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable. \begin{code} -- Flatten skolems -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ newFlattenSkolemTy :: TcType -> TcS TcType newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty newFlattenSkolemTyVar :: TcType -> TcS TcTyVar newFlattenSkolemTyVar ty = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique ; let name = TcM.mkTcTyVarName uniq (fsLit "f") ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } ; traceTcS "New Flatten Skolem Born" $ (ppr tv <+> text "[:= " <+> ppr ty <+> text "]") ; return tv } -- Instantiations -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] instDFunTypes mb_inst_tys = mapM inst_tv mb_inst_tys where inst_tv :: Either TyVar TcType -> TcS Type inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv inst_tv (Right ty) = return ty instDFunConstraints :: TcThetaType -> CtFlavor -> TcS [EvVarCreated] instDFunConstraints preds fl = mapM (newEvVar fl) preds instFlexiTcS :: TyVar -> TcS TcTyVar -- Like TcM.instMetaTyVar but the variable that is created is always -- touchable; we are supposed to guess its instantiation. -- See Note [Touchable meta type variables] instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) newFlexiTcSTy :: Kind -> TcS TcType newFlexiTcSTy knd = wrapTcS $ do { uniq <- TcM.newUnique ; ref <- TcM.newMutVar Flexi ; let name = TcM.mkTcTyVarName uniq (fsLit "uf") ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) } isFlexiTcsTv :: TyVar -> Bool isFlexiTcsTv tv | not (isTcTyVar tv) = False | MetaTv TcsTv _ <- tcTyVarDetails tv = True | otherwise = False newKindConstraint :: TcTyVar -> Kind -> CtFlavor -> TcS EvVarCreated -- Create new wanted CoVar that constrains the type to have the specified kind. newKindConstraint tv knd fl = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd ; let ty_k = mkTyVarTy tv_k ; eqv <- newEqVar fl (mkTyVarTy tv) ty_k ; return eqv } instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar instFlexiTcSHelper tvname tvkind = wrapTcS $ do { uniq <- TcM.newUnique ; ref <- TcM.newMutVar Flexi ; let name = setNameUnique tvname uniq kind = tvkind ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) } -- Superclasses and recursive dictionaries -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ data EvVarCreated = EvVarCreated { evc_is_new :: Bool -- True iff the variable was just created , evc_the_evvar :: EvVar } -- The actual evidence variable could be cached or new isNewEvVar :: EvVarCreated -> Bool isNewEvVar = evc_is_new newEvVar :: CtFlavor -> TcPredType -> TcS EvVarCreated -- Post: If Given then evc_is_new is True -- Hence it is safe to do a setEvBind right after a newEvVar with a Given flavor -- NB: newEvVar may temporarily break the TcSEnv invariant but it is expected in -- the call sites for this invariant to be quickly restored. newEvVar fl pty | isGivenOrSolved fl -- Create new variable and update the cache = do { {- We lose a lot of time if we enable this check: eref <- getTcSEvVarCache ; ecache <- wrapTcS (TcM.readTcRef eref) ; case lookupTM pty (evc_cache ecache) of Just (_,cached_fl) | cached_fl `canSolve` fl -> pprTrace "Interesting: given newEvVar, missed caching opportunity!" empty $ return () _ -> return () -} new <- forceNewEvVar fl pty ; return (EvVarCreated True new) } | otherwise -- Otherwise lookup first = {-# SCC "newEvVarWanted" #-} do { eref <- getTcSEvVarCache ; ecache <- wrapTcS (TcM.readTcRef eref) ; case lookupTM pty (evc_cache ecache) of Just (cached_evvar, cached_flavor) | cached_flavor `canSolve` fl -- NB: -- We want to use the cache /only/ if he can solve -- the workitem. If cached_flavor is Derived -- but we have a real Wanted, we want to create -- new evidence, otherwise we are in danger to -- have unsolved goals in the end. -- (Remember: Derived's are just unification hints -- but they don't come with guarantees -- that they can be solved and we don't -- quantify over them. -> do { traceTcS "newEvVar: already cached, doing nothing" (ppr (evc_cache ecache)) ; return (EvVarCreated False cached_evvar) } _ -- Not cached or cached with worse flavor -> do { new <- force_new_ev_var eref ecache fl pty ; return (EvVarCreated True new) } } forceNewEvVar :: CtFlavor -> TcPredType -> TcS EvVar -- Create a new EvVar, regardless of whether or not the -- cache already contains one like it, and update the cache forceNewEvVar fl pty = do { eref <- getTcSEvVarCache ; ecache <- wrapTcS (TcM.readTcRef eref) ; force_new_ev_var eref ecache fl pty } force_new_ev_var :: IORef EvVarCache -> EvVarCache -> CtFlavor -> TcPredType -> TcS EvVar -- Create a new EvVar, and update the cache with it force_new_ev_var eref ecache fl pty = wrapTcS $ do { TcM.traceTc "newEvVar" $ text "updating cache" ; new_evvar <-TcM.newEvVar pty -- This is THE PLACE where we finally call TcM.newEvVar ; let new_cache = updateCache ecache (new_evvar,fl,pty) ; TcM.writeTcRef eref new_cache ; return new_evvar } updateCache :: EvVarCache -> (EvVar,CtFlavor,Type) -> EvVarCache updateCache ecache (ev,fl,pty) | IPPred {} <- classifier = ecache | otherwise = ecache { evc_cache = ecache' } where classifier = classifyPredType pty ecache' = alterTM pty (\_ -> Just (ev,fl)) $ evc_cache ecache delCachedEvVar :: EvVar -> CtFlavor -> TcS () delCachedEvVar ev _fl = {-# SCC "delCachedEvVarOther" #-} do { eref <- getTcSEvVarCache ; ecache <- wrapTcS (TcM.readTcRef eref) ; wrapTcS $ TcM.writeTcRef eref (delFromCache ecache ev) } delFromCache :: EvVarCache -> EvVar -> EvVarCache delFromCache (EvVarCache { evc_cache = ecache , evc_flat_cache = flat_cache }) ev = EvVarCache { evc_cache = ecache', evc_flat_cache = flat_cache } where ecache' = alterTM pty x_del ecache x_del Nothing = Nothing x_del r@(Just (ev0,_)) | ev0 == ev = Nothing | otherwise = r pty = evVarPred ev updateFlatCache :: EvVar -> CtFlavor -> TyCon -> [Xi] -> TcType -> FlatEqOrigin -> TcS () updateFlatCache ev fl fn xis rhs_ty feq_origin = do { eref <- getTcSEvVarCache ; ecache <- wrapTcS (TcM.readTcRef eref) ; let flat_cache = evc_flat_cache ecache new_flat_cache = alterTM fun_ty x_flat_cache flat_cache new_evc = ecache { evc_flat_cache = new_flat_cache } ; wrapTcS $ TcM.writeTcRef eref new_evc } where x_flat_cache _ = Just (mkTcCoVarCo ev,(rhs_ty,fl,feq_origin)) fun_ty = mkTyConApp fn xis pprEvVarCache :: TypeMap (TcCoercion,a) -> SDoc pprEvVarCache tm = ppr (foldTM mk_pair tm []) where mk_pair (co,_) cos = (co, tcCoercionKind co) : cos newGivenEqVar :: CtFlavor -> TcType -> TcType -> TcCoercion -> TcS (CtFlavor,EvVar) -- Pre: fl is Given newGivenEqVar fl ty1 ty2 co = do { ecv <- newEqVar fl ty1 ty2 ; let v = evc_the_evvar ecv -- Will be a new EvVar by post of newEvVar ; fl' <- setEvBind v (EvCoercion co) fl ; return (fl',v) } newEqVar :: CtFlavor -> TcType -> TcType -> TcS EvVarCreated newEqVar fl ty1 ty2 = newEvVar fl (mkEqPred (ty1,ty2)) \end{code} \begin{code} -- Matching and looking up classes and family instances -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ data MatchInstResult mi = MatchInstNo -- No matching instance | MatchInstSingle mi -- Single matching instance | MatchInstMany -- Multiple matching instances matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) -- Look up a class constraint in the instance environment matchClass clas tys = do { let pred = mkClassPred clas tys ; instEnvs <- getInstEnvs ; case lookupInstEnv instEnvs clas tys of { ([], unifs, _) -- Nothing matches -> do { traceTcS "matchClass not matching" (vcat [ text "dict" <+> ppr pred, text "unifs" <+> ppr unifs ]) ; return MatchInstNo } ; ([(ispec, inst_tys)], [], _) -- A single match -> do { let dfun_id = is_dfun ispec ; traceTcS "matchClass success" (vcat [text "dict" <+> ppr pred, text "witness" <+> ppr dfun_id <+> ppr (idType dfun_id) ]) -- Record that this dfun is needed ; return $ MatchInstSingle (dfun_id, inst_tys) } ; (matches, unifs, _) -- More than one matches -> do { traceTcS "matchClass multiple matches, deferring choice" (vcat [text "dict" <+> ppr pred, text "matches" <+> ppr matches, text "unifs" <+> ppr unifs]) ; return MatchInstMany } } } matchFam :: TyCon -> [Type] -> TcS (Maybe (TyCon, [Type])) matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args \end{code} -- Rewriting with respect to the inert equalities -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} getInertEqs :: TcS (TyVarEnv (Ct,TcCoercion), InScopeSet) getInertEqs = do { inert <- getTcSInerts ; return (inert_eqs inert, inert_eq_tvs inert) } getCtCoercion :: Ct -> TcCoercion -- Precondition: A CTyEqCan. getCtCoercion ct | Just (GivenSolved (Just (EvCoercion co))) <- maybe_given = co | otherwise = mkTcCoVarCo (setVarType (cc_id ct) (ctPred ct)) -- NB: The variable could be rewritten by a spontaneously -- solved, so it is not safe to simply do a mkTcCoVarCo (cc_id ct) -- Instead we use the most accurate type, given by ctPred c where maybe_given = isGiven_maybe (cc_flavor ct) -- See Note [LiftInertEqs] liftInertEqsTy :: (TyVarEnv (Ct, TcCoercion),InScopeSet) -> CtFlavor -> PredType -> TcCoercion liftInertEqsTy (subst,inscope) fl pty = ty_cts_subst subst inscope fl pty ty_cts_subst :: TyVarEnv (Ct, TcCoercion) -> InScopeSet -> CtFlavor -> Type -> TcCoercion ty_cts_subst subst inscope fl ty = go ty where go ty = go' ty go' (TyVarTy tv) = tyvar_cts_subst tv `orElse` mkTcReflCo (TyVarTy tv) go' (AppTy ty1 ty2) = mkTcAppCo (go ty1) (go ty2) go' (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys) go' (ForAllTy v ty) = mkTcForAllCo v' $! co where (subst',inscope',v') = upd_tyvar_bndr subst inscope v co = ty_cts_subst subst' inscope' fl ty go' (FunTy ty1 ty2) = mkTcFunCo (go ty1) (go ty2) tyvar_cts_subst tv | Just (ct,co) <- lookupVarEnv subst tv, cc_flavor ct `canRewrite` fl = Just co -- Warn: use cached, not cc_id directly, because of alpha-renamings! | otherwise = Nothing upd_tyvar_bndr subst inscope v = (new_subst, (inscope `extendInScopeSet` new_v), new_v) where new_subst | no_change = delVarEnv subst v -- Otherwise we have to extend the environment with /something/. -- But we do not want to monadically create a new EvVar. So, we -- create an 'unused_ct' but we cache reflexivity as the -- associated coercion. | otherwise = extendVarEnv subst v (unused_ct, mkTcReflCo (TyVarTy new_v)) no_change = new_v == v new_v = uniqAway inscope v unused_ct = CTyEqCan { cc_id = unused_evvar , cc_flavor = fl -- canRewrite is reflexive. , cc_tyvar = v , cc_rhs = mkTyVarTy new_v , cc_depth = unused_depth } unused_depth = panic "ty_cts_subst: This depth should not be accessed!" unused_evvar = panic "ty_cts_subst: This var is just an alpha-renaming!" \end{code} Note [LiftInertEqsTy] ~~~~~~~~~~~~~~~~~~~~~~~ The function liftInertEqPred behaves almost like liftCoSubst (in Coercion), but accepts a map TyVarEnv (Ct,Coercion) instead of a LiftCoSubst. This data structure is more convenient to use since we must apply the inert substitution /only/ if the inert equality `canRewrite` the work item. There's admittedly some duplication of functionality but it would be more tedious to cache and maintain different flavors of LiftCoSubst structures in the inerts.