2 -- Type definitions for the constraint solver
5 -- Canonical constraints
6 CanonicalCts, emptyCCan, andCCan, andCCans,
7 singleCCan, extendCCans, isEmptyCCan, isCTyEqCan,
8 isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
11 WorkList, unionWorkList, unionWorkLists, isEmptyWorkList, emptyWorkList,
12 workListFromEq, workListFromNonEq,
13 workListFromEqs, workListFromNonEqs, foldrWorkListM,
15 CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
16 deCanonicalise, mkFrozenError,
18 isWanted, isGivenOrSolved, isDerived,
19 isGivenOrSolvedCt, isGivenCt_maybe,
20 isWantedCt, isDerivedCt, pprFlavorArising,
25 combineCtLoc, mkSolvedFlavor, mkGivenFlavor,
29 TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
30 traceFireTcS, bumpStepCountTcS,
31 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
32 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
34 -- Creation of evidence variables
35 newEvVar, newCoVar, newGivenCoVar,
37 newIPVar, newDictVar, newKindConstraint,
39 -- Setting evidence variables
40 setCoBind, setIPBind, setDictBind, setEvBind,
44 lookupFlatCacheMap, updateFlatCacheMap,
46 getInstEnvs, getFamInstEnvs, -- Getting the environments
47 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
48 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
50 newFlattenSkolemTy, -- Flatten skolems
53 instDFunTypes, -- Instantiation
55 newFlexiTcSTy, instFlexiTcS,
61 isTouchableMetaTyVar_InRange,
63 getDefaultInfo, getDynFlags,
65 matchClass, matchFam, MatchInstResult (..),
68 pprEq -- Smaller utils, re-exported from TcM
69 -- TODO (DV): these are only really used in the
70 -- instance matcher in TcSimplify. I am wondering
71 -- if the whole instance matcher simply belongs
75 #include "HsVersions.h"
85 import qualified TcRnMonad as TcM
86 import qualified TcMType as TcM
87 import qualified TcEnv as TcM
88 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
106 import HsBinds -- for TcEvBinds stuff
111 import qualified Data.Map as Map
114 import StaticFlags( opt_PprStyle_Debug )
115 import Control.Monad( when )
120 %************************************************************************
122 %* Canonical constraints *
124 %* These are the constraints the low-level simplifier works with *
126 %************************************************************************
129 -- Types without any type functions inside. However, note that xi
130 -- types CAN contain unexpanded type synonyms; however, the
131 -- (transitive) expansions of those type synonyms will not contain any
133 type Xi = Type -- In many comments, "xi" ranges over Xi
135 type CanonicalCts = Bag CanonicalCt
138 -- Atomic canonical constraints
139 = CDictCan { -- e.g. Num xi
141 cc_flavor :: CtFlavor,
146 | CIPCan { -- ?x::tau
147 -- See note [Canonical implicit parameter constraints].
149 cc_flavor :: CtFlavor,
150 cc_ip_nm :: IPName Name,
151 cc_ip_ty :: TcTauType
154 | CTyEqCan { -- tv ~ xi (recall xi means function free)
156 -- * tv not in tvs(xi) (occurs check)
157 -- * typeKind xi `compatKind` typeKind tv
158 -- See Note [Spontaneous solving and kind compatibility]
159 -- * We prefer unification variables on the left *JUST* for efficiency
161 cc_flavor :: CtFlavor,
166 | CFunEqCan { -- F xis ~ xi
167 -- Invariant: * isSynFamilyTyCon cc_fun
168 -- * typeKind (F xis) `compatKind` typeKind xi
170 cc_flavor :: CtFlavor,
171 cc_fun :: TyCon, -- A type function
172 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
173 cc_rhs :: Xi -- *never* over-saturated (because if so
174 -- we should have decomposed)
178 | CFrozenErr { -- A "frozen error" does not interact with anything
179 -- See Note [Frozen Errors]
181 cc_flavor :: CtFlavor
184 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
185 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
187 compatKind :: Kind -> Kind -> Bool
188 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
190 deCanonicalise :: CanonicalCt -> FlavoredEvVar
191 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
193 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
194 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
195 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
196 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
197 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
198 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
200 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
201 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
202 tyVarsOfCDict _ct = emptyVarSet
204 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
205 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
207 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
208 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
210 instance Outputable CanonicalCt where
211 ppr (CDictCan d fl cls tys)
212 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
213 ppr (CIPCan ip fl ip_nm ty)
214 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
215 ppr (CTyEqCan co fl tv ty)
216 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
217 ppr (CFunEqCan co fl tc tys ty)
218 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
219 ppr (CFrozenErr co fl)
220 = ppr fl <+> pprEvVarWithType co
223 Note [Canonical implicit parameter constraints]
224 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
225 The type in a canonical implicit parameter constraint doesn't need to
226 be a xi (type-function-free type) since we can defer the flattening
227 until checking this type for equality with another type. If we
228 encounter two IP constraints with the same name, they MUST have the
229 same type, and at that point we can generate a flattened equality
230 constraint between the types. (On the other hand, the types in two
231 class constraints for the same class MAY be equal, so they need to be
232 flattened in the first place to facilitate comparing them.)
235 singleCCan :: CanonicalCt -> CanonicalCts
238 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
241 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
242 extendCCans = snocBag
244 andCCans :: [CanonicalCts] -> CanonicalCts
245 andCCans = unionManyBags
247 emptyCCan :: CanonicalCts
250 isEmptyCCan :: CanonicalCts -> Bool
251 isEmptyCCan = isEmptyBag
253 isCTyEqCan :: CanonicalCt -> Bool
254 isCTyEqCan (CTyEqCan {}) = True
255 isCTyEqCan (CFunEqCan {}) = False
258 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
259 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
260 isCDictCan_Maybe _ = Nothing
262 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
263 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
264 isCIPCan_Maybe _ = Nothing
266 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
267 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
268 isCFunEqCan_Maybe _ = Nothing
270 isCFrozenErr :: CanonicalCt -> Bool
271 isCFrozenErr (CFrozenErr {}) = True
272 isCFrozenErr _ = False
275 -- A mixture of Given, Wanted, and Derived constraints.
276 -- We split between equalities and the rest to process equalities first.
277 data WorkList = WorkList { weqs :: CanonicalCts
278 -- NB: weqs includes equalities /and/ family equalities
279 , wrest :: CanonicalCts }
281 unionWorkList :: WorkList -> WorkList -> WorkList
282 unionWorkList wl1 wl2
283 = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
284 , wrest = wrest wl1 `andCCan` wrest wl2 }
286 unionWorkLists :: [WorkList] -> WorkList
287 unionWorkLists = foldr unionWorkList emptyWorkList
289 isEmptyWorkList :: WorkList -> Bool
290 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
292 emptyWorkList :: WorkList
294 = WorkList { weqs = emptyBag, wrest = emptyBag }
296 workListFromEq :: CanonicalCt -> WorkList
297 workListFromEq = workListFromEqs . singleCCan
299 workListFromNonEq :: CanonicalCt -> WorkList
300 workListFromNonEq = workListFromNonEqs . singleCCan
302 workListFromNonEqs :: CanonicalCts -> WorkList
303 workListFromNonEqs cts
304 = WorkList { weqs = emptyCCan, wrest = cts }
306 workListFromEqs :: CanonicalCts -> WorkList
308 = WorkList { weqs = cts, wrest = emptyCCan }
310 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
311 -> r -> WorkList -> m r
312 -- Prioritizes equalities
313 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
314 = do { r1 <- foldrBagM on_ct r eqs
315 ; foldrBagM on_ct r1 rest }
317 instance Outputable WorkList where
318 ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
319 , text "WorkList (Other) = " <+> ppr (wrest wl) ]
325 %************************************************************************
328 The "flavor" of a canonical constraint
330 %************************************************************************
333 getWantedLoc :: CanonicalCt -> WantedLoc
335 = ASSERT (isWanted (cc_flavor ct))
338 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
340 isWantedCt :: CanonicalCt -> Bool
341 isWantedCt ct = isWanted (cc_flavor ct)
342 isDerivedCt :: CanonicalCt -> Bool
343 isDerivedCt ct = isDerived (cc_flavor ct)
345 isGivenCt_maybe :: CanonicalCt -> Maybe GivenKind
346 isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct)
348 isGivenOrSolvedCt :: CanonicalCt -> Bool
349 isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct)
352 canSolve :: CtFlavor -> CtFlavor -> Bool
353 -- canSolve ctid1 ctid2
354 -- The constraint ctid1 can be used to solve ctid2
355 -- "to solve" means a reaction where the active parts of the two constraints match.
356 -- active(F xis ~ xi) = F xis
357 -- active(tv ~ xi) = tv
358 -- active(D xis) = D xis
359 -- active(IP nm ty) = nm
361 -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
362 -----------------------------------------
363 canSolve (Given {}) _ = True
364 canSolve (Wanted {}) (Derived {}) = True
365 canSolve (Wanted {}) (Wanted {}) = True
366 canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
367 canSolve _ _ = False -- (There is no *evidence* for a derived.)
369 canRewrite :: CtFlavor -> CtFlavor -> Bool
370 -- canRewrite ctid1 ctid2
371 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
372 canRewrite = canSolve
374 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
375 -- Precondition: At least one of them should be wanted
376 combineCtLoc (Wanted loc) _ = loc
377 combineCtLoc _ (Wanted loc) = loc
378 combineCtLoc (Derived loc ) _ = loc
379 combineCtLoc _ (Derived loc ) = loc
380 combineCtLoc _ _ = panic "combineCtLoc: both given"
382 mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
383 -- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
384 mkSolvedFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
385 mkSolvedFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
386 mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
388 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
389 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
390 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
391 mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
393 mkWantedFlavor :: CtFlavor -> CtFlavor
394 mkWantedFlavor (Wanted loc) = Wanted loc
395 mkWantedFlavor (Derived loc) = Wanted loc
396 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl)
399 %************************************************************************
401 %* The TcS solver monad *
403 %************************************************************************
407 The TcS monad is a weak form of the main Tc monad
411 * allocate new variables
412 * fill in evidence variables
414 Filling in a dictionary evidence variable means to create a binding
415 for it, so TcS carries a mutable location where the binding can be
416 added. This is initialised from the innermost implication constraint.
421 tcs_ev_binds :: EvBindsVar,
424 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
425 -- Global type bindings
427 tcs_context :: SimplContext,
429 tcs_untch :: TcsUntouchables,
431 tcs_ic_depth :: Int, -- Implication nesting depth
432 tcs_count :: IORef Int, -- Global step count
434 tcs_flat_map :: IORef FlatCache
438 = FlatCache { givenFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor)
439 -- Invariant: all CtFlavors here satisfy isGiven
440 , wantedFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor) }
441 -- Invariant: all CtFlavors here satisfy isWanted
443 emptyFlatCache :: FlatCache
445 = FlatCache { givenFlatCache = Map.empty, wantedFlatCache = Map.empty }
447 newtype FunEqHead = FunEqHead (TyCon,[Xi])
449 instance Eq FunEqHead where
450 FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && tcEqTypes xis1 xis2
452 instance Ord FunEqHead where
453 FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2)
454 = case compare tc1 tc2 of
455 EQ -> tcCmpTypes xis1 xis2
458 type TcsUntouchables = (Untouchables,TcTyVarSet)
459 -- Like the TcM Untouchables,
460 -- but records extra TcsTv variables generated during simplification
461 -- See Note [Extra TcsTv untouchables] in TcSimplify
466 = SimplInfer SDoc -- Inferring type of a let-bound thing
467 | SimplRuleLhs RuleName -- Inferring type of a RULE lhs
468 | SimplInteractive -- Inferring type at GHCi prompt
469 | SimplCheck SDoc -- Checking a type signature or RULE rhs
471 instance Outputable SimplContext where
472 ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
473 ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
474 ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
475 ppr SimplInteractive = ptext (sLit "SimplInteractive")
477 isInteractive :: SimplContext -> Bool
478 isInteractive SimplInteractive = True
479 isInteractive _ = False
481 simplEqsOnly :: SimplContext -> Bool
482 -- Simplify equalities only, not dictionaries
483 -- This is used for the LHS of rules; ee
484 -- Note [Simplifying RULE lhs constraints] in TcSimplify
485 simplEqsOnly (SimplRuleLhs {}) = True
486 simplEqsOnly _ = False
488 performDefaulting :: SimplContext -> Bool
489 performDefaulting (SimplInfer {}) = False
490 performDefaulting (SimplRuleLhs {}) = False
491 performDefaulting SimplInteractive = True
492 performDefaulting (SimplCheck {}) = True
495 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
497 instance Functor TcS where
498 fmap f m = TcS $ fmap f . unTcS m
500 instance Monad TcS where
501 return x = TcS (\_ -> return x)
502 fail err = TcS (\_ -> fail err)
503 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
505 -- Basic functionality
506 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
507 wrapTcS :: TcM a -> TcS a
508 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
509 -- and TcS is supposed to have limited functionality
510 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
512 wrapErrTcS :: TcM a -> TcS a
513 -- The thing wrapped should just fail
514 -- There's no static check; it's up to the user
515 -- Having a variant for each error message is too painful
518 wrapWarnTcS :: TcM a -> TcS a
519 -- The thing wrapped should just add a warning, or no-op
520 -- There's no static check; it's up to the user
521 wrapWarnTcS = wrapTcS
523 failTcS, panicTcS :: SDoc -> TcS a
524 failTcS = wrapTcS . TcM.failWith
525 panicTcS doc = pprPanic "TcCanonical" doc
527 traceTcS :: String -> SDoc -> TcS ()
528 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
530 bumpStepCountTcS :: TcS ()
531 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
532 ; n <- TcM.readTcRef ref
533 ; TcM.writeTcRef ref (n+1) }
535 traceFireTcS :: Int -> SDoc -> TcS ()
536 -- Dump a rule-firing trace
537 traceFireTcS depth doc
539 TcM.ifDOptM Opt_D_dump_cs_trace $
540 do { n <- TcM.readTcRef (tcs_count env)
542 <> text (replicate (tcs_ic_depth env) '>')
543 <> brackets (int depth) <+> doc
546 runTcS :: SimplContext
547 -> Untouchables -- Untouchables
548 -> TcS a -- What to run
549 -> TcM (a, Bag EvBind)
550 runTcS context untouch tcs
551 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
552 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
553 ; step_count <- TcM.newTcRef 0
554 ; flat_cache_var <- TcM.newTcRef emptyFlatCache
555 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
556 , tcs_ty_binds = ty_binds_var
557 , tcs_context = context
558 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
559 , tcs_count = step_count
561 , tcs_flat_map = flat_cache_var
564 -- Run the computation
565 ; res <- unTcS tcs env
566 -- Perform the type unifications required
567 ; ty_binds <- TcM.readTcRef ty_binds_var
568 ; mapM_ do_unification (varEnvElts ty_binds)
571 ; count <- TcM.readTcRef step_count
572 ; when (opt_PprStyle_Debug && count > 0) $
573 TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
574 <+> int count <+> ppr context)
577 ; ev_binds <- TcM.readTcRef evb_ref
578 ; return (res, evBindMapBinds ev_binds) }
580 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
582 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
583 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
584 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
585 , tcs_untch = (_outer_range, outer_tcs)
587 , tcs_ic_depth = idepth
589 , tcs_flat_map = orig_flat_cache_var
591 do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
592 -- The inner_range should be narrower than the outer one
593 -- (thus increasing the set of untouchables) but
594 -- the inner Tcs-untouchables must be unioned with the
597 ; orig_flat_cache <- TcM.readTcRef orig_flat_cache_var
598 ; flat_cache_var <- TcM.newTcRef orig_flat_cache -- emptyFlatCache
600 -- Consider copying the results the tcs_flat_map of the
601 -- incomping constraint, but we must make sure that we
602 -- have pushed everything in, which seems somewhat fragile
603 ; let nest_env = TcSEnv { tcs_ev_binds = ref
604 , tcs_ty_binds = ty_binds
605 , tcs_untch = inner_untch
607 , tcs_ic_depth = idepth+1
608 , tcs_context = ctxtUnderImplic ctxt
609 , tcs_flat_map = flat_cache_var }
610 ; thing_inside nest_env }
612 recoverTcS :: TcS a -> TcS a -> TcS a
613 recoverTcS (TcS recovery_code) (TcS thing_inside)
615 TcM.recoverM (recovery_code env) (thing_inside env)
617 ctxtUnderImplic :: SimplContext -> SimplContext
618 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
619 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
620 <+> doubleQuotes (ftext n))
621 ctxtUnderImplic ctxt = ctxt
623 tryTcS :: TcS a -> TcS a
624 -- Like runTcS, but from within the TcS monad
625 -- Ignore all the evidence generated, and do not affect caller's evidence!
627 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
628 ; ev_binds_var <- TcM.newTcEvBinds
629 ; flat_cache_var <- TcM.newTcRef emptyFlatCache
630 ; let env1 = env { tcs_ev_binds = ev_binds_var
631 , tcs_ty_binds = ty_binds_var
632 , tcs_flat_map = flat_cache_var }
636 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
638 getDynFlags :: TcS DynFlags
639 getDynFlags = wrapTcS TcM.getDOpts
641 getTcSContext :: TcS SimplContext
642 getTcSContext = TcS (return . tcs_context)
644 getTcEvBinds :: TcS EvBindsVar
645 getTcEvBinds = TcS (return . tcs_ev_binds)
647 getUntouchables :: TcS TcsUntouchables
648 getUntouchables = TcS (return . tcs_untch)
650 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
651 getTcSTyBinds = TcS (return . tcs_ty_binds)
653 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
654 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
656 getFlatCacheMapVar :: TcS (IORef FlatCache)
658 = TcS (return . tcs_flat_map)
660 lookupFlatCacheMap :: TyCon -> [Xi] -> CtFlavor
661 -> TcS (Maybe (TcType,Coercion,CtFlavor))
662 -- For givens, we lookup in given flat cache
663 lookupFlatCacheMap tc xis (Given {})
664 = do { cache_ref <- getFlatCacheMapVar
665 ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
666 ; return $ Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) }
667 -- For wanteds, we first lookup in givenFlatCache.
668 -- If we get nothing back then we lookup in wantedFlatCache.
669 lookupFlatCacheMap tc xis (Wanted {})
670 = do { cache_ref <- getFlatCacheMapVar
671 ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
672 ; case Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) of
673 Nothing -> return $ Map.lookup (FunEqHead (tc,xis)) (wantedFlatCache cache_map)
674 other -> return other }
675 lookupFlatCacheMap _tc _xis (Derived {}) = return Nothing
677 updateFlatCacheMap :: TyCon -> [Xi]
678 -> TcType -> CtFlavor -> Coercion -> TcS ()
679 updateFlatCacheMap _tc _xis _tv (Derived {}) _co
680 = return () -- Not caching deriveds
681 updateFlatCacheMap tc xis ty fl co
682 = do { cache_ref <- getFlatCacheMapVar
683 ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
686 = cache_map { givenFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
687 givenFlatCache cache_map }
689 = cache_map { wantedFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
690 wantedFlatCache cache_map }
691 | otherwise = pprPanic "updateFlatCacheMap, met Derived!" $ empty
692 ; wrapTcS $ TcM.writeTcRef cache_ref new_cache_map }
695 getTcEvBindsBag :: TcS EvBindMap
697 = do { EvBindsVar ev_ref _ <- getTcEvBinds
698 ; wrapTcS $ TcM.readTcRef ev_ref }
701 setCoBind :: CoVar -> Coercion -> TcS ()
702 setCoBind cv co = setEvBind cv (EvCoercion co)
704 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
705 -- Add a type binding
706 -- We never do this twice!
707 setWantedTyBind tv ty
708 = do { ref <- getTcSTyBinds
710 do { ty_binds <- TcM.readTcRef ref
712 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
713 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
714 , ppr tv <+> text ":=" <+> ppr ty
715 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
717 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
719 setIPBind :: EvVar -> EvTerm -> TcS ()
720 setIPBind = setEvBind
722 setDictBind :: EvVar -> EvTerm -> TcS ()
723 setDictBind = setEvBind
725 setEvBind :: EvVar -> EvTerm -> TcS ()
728 = do { tc_evbinds <- getTcEvBinds
729 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
731 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
732 warnTcS loc warn_if doc
733 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
734 | otherwise = return ()
736 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
738 = do { ctxt <- getTcSContext
739 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
740 ; return (ctxt, tys, flags) }
742 -- Just get some environments needed for instance looking up and matching
743 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
745 getInstEnvs :: TcS (InstEnv, InstEnv)
746 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
748 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
749 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
751 getTopEnv :: TcS HscEnv
752 getTopEnv = wrapTcS $ TcM.getTopEnv
754 getGblEnv :: TcS TcGblEnv
755 getGblEnv = wrapTcS $ TcM.getGblEnv
757 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
758 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
760 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
761 checkWellStagedDFun pred dfun_id loc
762 = wrapTcS $ TcM.setCtLoc loc $
763 do { use_stage <- TcM.getStage
764 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
766 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
767 bind_lvl = TcM.topIdLvl dfun_id
769 pprEq :: TcType -> TcType -> SDoc
770 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
772 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
773 isTouchableMetaTyVar tv
774 = do { untch <- getUntouchables
775 ; return $ isTouchableMetaTyVar_InRange untch tv }
777 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
778 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
779 = case tcTyVarDetails tv of
780 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
781 -- See Note [Touchable meta type variables]
782 MetaTv {} -> inTouchableRange untch tv
789 Note [Touchable meta type variables]
790 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
791 Meta type variables allocated *by the constraint solver itself* are always
793 instance C a b => D [a] where...
794 if we use this instance declaration we "make up" a fresh meta type
795 variable for 'b', which we must later guess. (Perhaps C has a
796 functional dependency.) But since we aren't in the constraint *generator*
797 we can't allocate a Unique in the touchable range for this implication
798 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
803 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
805 newFlattenSkolemTy :: TcType -> TcS TcType
806 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
808 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
809 newFlattenSkolemTyVar ty
810 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
811 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
812 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
813 ; traceTcS "New Flatten Skolem Born" $
814 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
818 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
820 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
821 instDFunTypes mb_inst_tys
822 = mapM inst_tv mb_inst_tys
824 inst_tv :: Either TyVar TcType -> TcS Type
825 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
826 inst_tv (Right ty) = return ty
828 instDFunConstraints :: TcThetaType -> TcS [EvVar]
829 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
832 instFlexiTcS :: TyVar -> TcS TcTyVar
833 -- Like TcM.instMetaTyVar but the variable that is created is always
834 -- touchable; we are supposed to guess its instantiation.
835 -- See Note [Touchable meta type variables]
836 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
838 newFlexiTcSTy :: Kind -> TcS TcType
841 do { uniq <- TcM.newUnique
842 ; ref <- TcM.newMutVar Flexi
843 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
844 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
846 isFlexiTcsTv :: TyVar -> Bool
848 | not (isTcTyVar tv) = False
849 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
852 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
853 -- Create new wanted CoVar that constrains the type to have the specified kind.
854 newKindConstraint tv knd
855 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
856 ; let ty_k = mkTyVarTy tv_k
857 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
860 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
861 instFlexiTcSHelper tvname tvkind
863 do { uniq <- TcM.newUnique
864 ; ref <- TcM.newMutVar Flexi
865 ; let name = setNameUnique tvname uniq
867 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
869 -- Superclasses and recursive dictionaries
870 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
872 newEvVar :: TcPredType -> TcS EvVar
873 newEvVar pty = wrapTcS $ TcM.newEvVar pty
875 newDerivedId :: TcPredType -> TcS EvVar
876 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
878 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
879 -- Note we create immutable variables for given or derived, since we
880 -- must bind them to TcEvBinds (because their evidence may involve
881 -- superclasses). However we should be able to override existing
882 -- 'derived' evidence, even in TcEvBinds
883 newGivenCoVar ty1 ty2 co
884 = do { cv <- newCoVar ty1 ty2
885 ; setEvBind cv (EvCoercion co)
888 newCoVar :: TcType -> TcType -> TcS EvVar
889 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
891 newIPVar :: IPName Name -> TcType -> TcS EvVar
892 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
894 newDictVar :: Class -> [TcType] -> TcS EvVar
895 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
900 -- Matching and looking up classes and family instances
901 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
903 data MatchInstResult mi
904 = MatchInstNo -- No matching instance
905 | MatchInstSingle mi -- Single matching instance
906 | MatchInstMany -- Multiple matching instances
909 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
910 -- Look up a class constraint in the instance environment
912 = do { let pred = mkClassPred clas tys
913 ; instEnvs <- getInstEnvs
914 ; case lookupInstEnv instEnvs clas tys of {
915 ([], unifs) -- Nothing matches
916 -> do { traceTcS "matchClass not matching"
917 (vcat [ text "dict" <+> ppr pred,
918 text "unifs" <+> ppr unifs ])
921 ([(ispec, inst_tys)], []) -- A single match
922 -> do { let dfun_id = is_dfun ispec
923 ; traceTcS "matchClass success"
924 (vcat [text "dict" <+> ppr pred,
925 text "witness" <+> ppr dfun_id
926 <+> ppr (idType dfun_id) ])
927 -- Record that this dfun is needed
928 ; return $ MatchInstSingle (dfun_id, inst_tys)
930 (matches, unifs) -- More than one matches
931 -> do { traceTcS "matchClass multiple matches, deferring choice"
932 (vcat [text "dict" <+> ppr pred,
933 text "matches" <+> ppr matches,
934 text "unifs" <+> ppr unifs])
935 ; return MatchInstMany
942 -> TcS (MatchInstResult (TyCon, [Type]))
944 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
946 Nothing -> return MatchInstNo
947 Just res -> return $ MatchInstSingle res
948 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
949 -- multiple matches. Check.