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 )
108 import HsBinds -- for TcEvBinds stuff
113 import qualified Data.Map as Map
116 import StaticFlags( opt_PprStyle_Debug )
117 import Control.Monad( when )
122 %************************************************************************
124 %* Canonical constraints *
126 %* These are the constraints the low-level simplifier works with *
128 %************************************************************************
131 -- Types without any type functions inside. However, note that xi
132 -- types CAN contain unexpanded type synonyms; however, the
133 -- (transitive) expansions of those type synonyms will not contain any
135 type Xi = Type -- In many comments, "xi" ranges over Xi
137 type CanonicalCts = Bag CanonicalCt
140 -- Atomic canonical constraints
141 = CDictCan { -- e.g. Num xi
143 cc_flavor :: CtFlavor,
148 | CIPCan { -- ?x::tau
149 -- See note [Canonical implicit parameter constraints].
151 cc_flavor :: CtFlavor,
152 cc_ip_nm :: IPName Name,
153 cc_ip_ty :: TcTauType
156 | CTyEqCan { -- tv ~ xi (recall xi means function free)
158 -- * tv not in tvs(xi) (occurs check)
159 -- * typeKind xi `compatKind` typeKind tv
160 -- See Note [Spontaneous solving and kind compatibility]
161 -- * We prefer unification variables on the left *JUST* for efficiency
163 cc_flavor :: CtFlavor,
168 | CFunEqCan { -- F xis ~ xi
169 -- Invariant: * isSynFamilyTyCon cc_fun
170 -- * typeKind (F xis) `compatKind` typeKind xi
172 cc_flavor :: CtFlavor,
173 cc_fun :: TyCon, -- A type function
174 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
175 cc_rhs :: Xi -- *never* over-saturated (because if so
176 -- we should have decomposed)
180 | CFrozenErr { -- A "frozen error" does not interact with anything
181 -- See Note [Frozen Errors]
183 cc_flavor :: CtFlavor
186 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
187 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
189 compatKind :: Kind -> Kind -> Bool
190 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
192 deCanonicalise :: CanonicalCt -> FlavoredEvVar
193 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
195 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
196 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
197 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
198 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
199 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
200 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
202 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
203 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
204 tyVarsOfCDict _ct = emptyVarSet
206 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
207 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
209 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
210 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
212 instance Outputable CanonicalCt where
213 ppr (CDictCan d fl cls tys)
214 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
215 ppr (CIPCan ip fl ip_nm ty)
216 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
217 ppr (CTyEqCan co fl tv ty)
218 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty)
219 ppr (CFunEqCan co fl tc tys ty)
220 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty)
221 ppr (CFrozenErr co fl)
222 = ppr fl <+> pprEvVarWithType co
225 Note [Canonical implicit parameter constraints]
226 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
227 The type in a canonical implicit parameter constraint doesn't need to
228 be a xi (type-function-free type) since we can defer the flattening
229 until checking this type for equality with another type. If we
230 encounter two IP constraints with the same name, they MUST have the
231 same type, and at that point we can generate a flattened equality
232 constraint between the types. (On the other hand, the types in two
233 class constraints for the same class MAY be equal, so they need to be
234 flattened in the first place to facilitate comparing them.)
237 singleCCan :: CanonicalCt -> CanonicalCts
240 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
243 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
244 extendCCans = snocBag
246 andCCans :: [CanonicalCts] -> CanonicalCts
247 andCCans = unionManyBags
249 emptyCCan :: CanonicalCts
252 isEmptyCCan :: CanonicalCts -> Bool
253 isEmptyCCan = isEmptyBag
255 isCTyEqCan :: CanonicalCt -> Bool
256 isCTyEqCan (CTyEqCan {}) = True
257 isCTyEqCan (CFunEqCan {}) = False
260 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
261 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
262 isCDictCan_Maybe _ = Nothing
264 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
265 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
266 isCIPCan_Maybe _ = Nothing
268 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
269 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
270 isCFunEqCan_Maybe _ = Nothing
272 isCFrozenErr :: CanonicalCt -> Bool
273 isCFrozenErr (CFrozenErr {}) = True
274 isCFrozenErr _ = False
277 -- A mixture of Given, Wanted, and Derived constraints.
278 -- We split between equalities and the rest to process equalities first.
279 data WorkList = WorkList { weqs :: CanonicalCts
280 -- NB: weqs includes equalities /and/ family equalities
281 , wrest :: CanonicalCts }
283 unionWorkList :: WorkList -> WorkList -> WorkList
284 unionWorkList wl1 wl2
285 = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
286 , wrest = wrest wl1 `andCCan` wrest wl2 }
288 unionWorkLists :: [WorkList] -> WorkList
289 unionWorkLists = foldr unionWorkList emptyWorkList
291 isEmptyWorkList :: WorkList -> Bool
292 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
294 emptyWorkList :: WorkList
296 = WorkList { weqs = emptyBag, wrest = emptyBag }
298 workListFromEq :: CanonicalCt -> WorkList
299 workListFromEq = workListFromEqs . singleCCan
301 workListFromNonEq :: CanonicalCt -> WorkList
302 workListFromNonEq = workListFromNonEqs . singleCCan
304 workListFromNonEqs :: CanonicalCts -> WorkList
305 workListFromNonEqs cts
306 = WorkList { weqs = emptyCCan, wrest = cts }
308 workListFromEqs :: CanonicalCts -> WorkList
310 = WorkList { weqs = cts, wrest = emptyCCan }
312 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
313 -> r -> WorkList -> m r
314 -- Prioritizes equalities
315 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
316 = do { r1 <- foldrBagM on_ct r eqs
317 ; foldrBagM on_ct r1 rest }
319 instance Outputable WorkList where
320 ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
321 , text "WorkList (Other) = " <+> ppr (wrest wl) ]
327 %************************************************************************
330 The "flavor" of a canonical constraint
332 %************************************************************************
335 getWantedLoc :: CanonicalCt -> WantedLoc
337 = ASSERT (isWanted (cc_flavor ct))
340 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
342 isWantedCt :: CanonicalCt -> Bool
343 isWantedCt ct = isWanted (cc_flavor ct)
344 isDerivedCt :: CanonicalCt -> Bool
345 isDerivedCt ct = isDerived (cc_flavor ct)
347 isGivenCt_maybe :: CanonicalCt -> Maybe GivenKind
348 isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct)
350 isGivenOrSolvedCt :: CanonicalCt -> Bool
351 isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct)
354 canSolve :: CtFlavor -> CtFlavor -> Bool
355 -- canSolve ctid1 ctid2
356 -- The constraint ctid1 can be used to solve ctid2
357 -- "to solve" means a reaction where the active parts of the two constraints match.
358 -- active(F xis ~ xi) = F xis
359 -- active(tv ~ xi) = tv
360 -- active(D xis) = D xis
361 -- active(IP nm ty) = nm
363 -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
364 -----------------------------------------
365 canSolve (Given {}) _ = True
366 canSolve (Wanted {}) (Derived {}) = True
367 canSolve (Wanted {}) (Wanted {}) = True
368 canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
369 canSolve _ _ = False -- (There is no *evidence* for a derived.)
371 canRewrite :: CtFlavor -> CtFlavor -> Bool
372 -- canRewrite ctid1 ctid2
373 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
374 canRewrite = canSolve
376 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
377 -- Precondition: At least one of them should be wanted
378 combineCtLoc (Wanted loc) _ = loc
379 combineCtLoc _ (Wanted loc) = loc
380 combineCtLoc (Derived loc ) _ = loc
381 combineCtLoc _ (Derived loc ) = loc
382 combineCtLoc _ _ = panic "combineCtLoc: both given"
384 mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
385 -- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
386 mkSolvedFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
387 mkSolvedFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
388 mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
390 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
391 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
392 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
393 mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
395 mkWantedFlavor :: CtFlavor -> CtFlavor
396 mkWantedFlavor (Wanted loc) = Wanted loc
397 mkWantedFlavor (Derived loc) = Wanted loc
398 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl)
401 %************************************************************************
403 %* The TcS solver monad *
405 %************************************************************************
409 The TcS monad is a weak form of the main Tc monad
413 * allocate new variables
414 * fill in evidence variables
416 Filling in a dictionary evidence variable means to create a binding
417 for it, so TcS carries a mutable location where the binding can be
418 added. This is initialised from the innermost implication constraint.
423 tcs_ev_binds :: EvBindsVar,
426 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
427 -- Global type bindings
429 tcs_context :: SimplContext,
431 tcs_untch :: TcsUntouchables,
433 tcs_ic_depth :: Int, -- Implication nesting depth
434 tcs_count :: IORef Int, -- Global step count
436 tcs_flat_map :: IORef FlatCache
440 = FlatCache { givenFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor)
441 -- Invariant: all CtFlavors here satisfy isGiven
442 , wantedFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor) }
443 -- Invariant: all CtFlavors here satisfy isWanted
445 emptyFlatCache :: FlatCache
447 = FlatCache { givenFlatCache = Map.empty, wantedFlatCache = Map.empty }
449 newtype FunEqHead = FunEqHead (TyCon,[Xi])
451 instance Eq FunEqHead where
452 FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && eqTypes xis1 xis2
454 instance Ord FunEqHead where
455 FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2)
456 = case compare tc1 tc2 of
457 EQ -> cmpTypes xis1 xis2
460 type TcsUntouchables = (Untouchables,TcTyVarSet)
461 -- Like the TcM Untouchables,
462 -- but records extra TcsTv variables generated during simplification
463 -- See Note [Extra TcsTv untouchables] in TcSimplify
468 = SimplInfer SDoc -- Inferring type of a let-bound thing
469 | SimplRuleLhs RuleName -- Inferring type of a RULE lhs
470 | SimplInteractive -- Inferring type at GHCi prompt
471 | SimplCheck SDoc -- Checking a type signature or RULE rhs
473 instance Outputable SimplContext where
474 ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
475 ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
476 ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
477 ppr SimplInteractive = ptext (sLit "SimplInteractive")
479 isInteractive :: SimplContext -> Bool
480 isInteractive SimplInteractive = True
481 isInteractive _ = False
483 simplEqsOnly :: SimplContext -> Bool
484 -- Simplify equalities only, not dictionaries
485 -- This is used for the LHS of rules; ee
486 -- Note [Simplifying RULE lhs constraints] in TcSimplify
487 simplEqsOnly (SimplRuleLhs {}) = True
488 simplEqsOnly _ = False
490 performDefaulting :: SimplContext -> Bool
491 performDefaulting (SimplInfer {}) = False
492 performDefaulting (SimplRuleLhs {}) = False
493 performDefaulting SimplInteractive = True
494 performDefaulting (SimplCheck {}) = True
497 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
499 instance Functor TcS where
500 fmap f m = TcS $ fmap f . unTcS m
502 instance Monad TcS where
503 return x = TcS (\_ -> return x)
504 fail err = TcS (\_ -> fail err)
505 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
507 -- Basic functionality
508 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
509 wrapTcS :: TcM a -> TcS a
510 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
511 -- and TcS is supposed to have limited functionality
512 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
514 wrapErrTcS :: TcM a -> TcS a
515 -- The thing wrapped should just fail
516 -- There's no static check; it's up to the user
517 -- Having a variant for each error message is too painful
520 wrapWarnTcS :: TcM a -> TcS a
521 -- The thing wrapped should just add a warning, or no-op
522 -- There's no static check; it's up to the user
523 wrapWarnTcS = wrapTcS
525 failTcS, panicTcS :: SDoc -> TcS a
526 failTcS = wrapTcS . TcM.failWith
527 panicTcS doc = pprPanic "TcCanonical" doc
529 traceTcS :: String -> SDoc -> TcS ()
530 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
532 bumpStepCountTcS :: TcS ()
533 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
534 ; n <- TcM.readTcRef ref
535 ; TcM.writeTcRef ref (n+1) }
537 traceFireTcS :: Int -> SDoc -> TcS ()
538 -- Dump a rule-firing trace
539 traceFireTcS depth doc
541 TcM.ifDOptM Opt_D_dump_cs_trace $
542 do { n <- TcM.readTcRef (tcs_count env)
544 <> text (replicate (tcs_ic_depth env) '>')
545 <> brackets (int depth) <+> doc
548 runTcS :: SimplContext
549 -> Untouchables -- Untouchables
550 -> TcS a -- What to run
551 -> TcM (a, Bag EvBind)
552 runTcS context untouch tcs
553 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
554 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
555 ; step_count <- TcM.newTcRef 0
556 ; flat_cache_var <- TcM.newTcRef emptyFlatCache
557 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
558 , tcs_ty_binds = ty_binds_var
559 , tcs_context = context
560 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
561 , tcs_count = step_count
563 , tcs_flat_map = flat_cache_var
566 -- Run the computation
567 ; res <- unTcS tcs env
568 -- Perform the type unifications required
569 ; ty_binds <- TcM.readTcRef ty_binds_var
570 ; mapM_ do_unification (varEnvElts ty_binds)
573 ; count <- TcM.readTcRef step_count
574 ; when (opt_PprStyle_Debug && count > 0) $
575 TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
576 <+> int count <+> ppr context)
579 ; ev_binds <- TcM.readTcRef evb_ref
580 ; return (res, evBindMapBinds ev_binds) }
582 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
584 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
585 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
586 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
587 , tcs_untch = (_outer_range, outer_tcs)
589 , tcs_ic_depth = idepth
591 , tcs_flat_map = orig_flat_cache_var
593 do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
594 -- The inner_range should be narrower than the outer one
595 -- (thus increasing the set of untouchables) but
596 -- the inner Tcs-untouchables must be unioned with the
599 ; orig_flat_cache <- TcM.readTcRef orig_flat_cache_var
600 ; flat_cache_var <- TcM.newTcRef orig_flat_cache
601 -- One could be more conservative as well:
602 -- ; flat_cache_var <- TcM.newTcRef emptyFlatCache
604 -- Consider copying the results the tcs_flat_map of the
605 -- incomping constraint, but we must make sure that we
606 -- have pushed everything in, which seems somewhat fragile
607 ; let nest_env = TcSEnv { tcs_ev_binds = ref
608 , tcs_ty_binds = ty_binds
609 , tcs_untch = inner_untch
611 , tcs_ic_depth = idepth+1
612 , tcs_context = ctxtUnderImplic ctxt
613 , tcs_flat_map = flat_cache_var }
614 ; thing_inside nest_env }
616 recoverTcS :: TcS a -> TcS a -> TcS a
617 recoverTcS (TcS recovery_code) (TcS thing_inside)
619 TcM.recoverM (recovery_code env) (thing_inside env)
621 ctxtUnderImplic :: SimplContext -> SimplContext
622 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
623 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
624 <+> doubleQuotes (ftext n))
625 ctxtUnderImplic ctxt = ctxt
627 tryTcS :: TcS a -> TcS a
628 -- Like runTcS, but from within the TcS monad
629 -- Ignore all the evidence generated, and do not affect caller's evidence!
631 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
632 ; ev_binds_var <- TcM.newTcEvBinds
633 ; flat_cache_var <- TcM.newTcRef emptyFlatCache
634 ; let env1 = env { tcs_ev_binds = ev_binds_var
635 , tcs_ty_binds = ty_binds_var
636 , tcs_flat_map = flat_cache_var }
640 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
642 getDynFlags :: TcS DynFlags
643 getDynFlags = wrapTcS TcM.getDOpts
645 getTcSContext :: TcS SimplContext
646 getTcSContext = TcS (return . tcs_context)
648 getTcEvBinds :: TcS EvBindsVar
649 getTcEvBinds = TcS (return . tcs_ev_binds)
651 getUntouchables :: TcS TcsUntouchables
652 getUntouchables = TcS (return . tcs_untch)
654 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
655 getTcSTyBinds = TcS (return . tcs_ty_binds)
657 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
658 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
660 getFlatCacheMapVar :: TcS (IORef FlatCache)
662 = TcS (return . tcs_flat_map)
664 lookupFlatCacheMap :: TyCon -> [Xi] -> CtFlavor
665 -> TcS (Maybe (TcType,Coercion,CtFlavor))
666 -- For givens, we lookup in given flat cache
667 lookupFlatCacheMap tc xis (Given {})
668 = do { cache_ref <- getFlatCacheMapVar
669 ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
670 ; return $ Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) }
671 -- For wanteds, we first lookup in givenFlatCache.
672 -- If we get nothing back then we lookup in wantedFlatCache.
673 lookupFlatCacheMap tc xis (Wanted {})
674 = do { cache_ref <- getFlatCacheMapVar
675 ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
676 ; case Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) of
677 Nothing -> return $ Map.lookup (FunEqHead (tc,xis)) (wantedFlatCache cache_map)
678 other -> return other }
679 lookupFlatCacheMap _tc _xis (Derived {}) = return Nothing
681 updateFlatCacheMap :: TyCon -> [Xi]
682 -> TcType -> CtFlavor -> Coercion -> TcS ()
683 updateFlatCacheMap _tc _xis _tv (Derived {}) _co
684 = return () -- Not caching deriveds
685 updateFlatCacheMap tc xis ty fl co
686 = do { cache_ref <- getFlatCacheMapVar
687 ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref
690 = cache_map { givenFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
691 givenFlatCache cache_map }
693 = cache_map { wantedFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $
694 wantedFlatCache cache_map }
695 | otherwise = pprPanic "updateFlatCacheMap, met Derived!" $ empty
696 ; wrapTcS $ TcM.writeTcRef cache_ref new_cache_map }
699 getTcEvBindsBag :: TcS EvBindMap
701 = do { EvBindsVar ev_ref _ <- getTcEvBinds
702 ; wrapTcS $ TcM.readTcRef ev_ref }
705 setCoBind :: CoVar -> Coercion -> TcS ()
706 setCoBind cv co = setEvBind cv (EvCoercion co)
708 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
709 -- Add a type binding
710 -- We never do this twice!
711 setWantedTyBind tv ty
712 = do { ref <- getTcSTyBinds
714 do { ty_binds <- TcM.readTcRef ref
716 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
717 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
718 , ppr tv <+> text ":=" <+> ppr ty
719 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
721 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
723 setIPBind :: EvVar -> EvTerm -> TcS ()
724 setIPBind = setEvBind
726 setDictBind :: EvVar -> EvTerm -> TcS ()
727 setDictBind = setEvBind
729 setEvBind :: EvVar -> EvTerm -> TcS ()
732 = do { tc_evbinds <- getTcEvBinds
733 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
735 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
736 warnTcS loc warn_if doc
737 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
738 | otherwise = return ()
740 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
742 = do { ctxt <- getTcSContext
743 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
744 ; return (ctxt, tys, flags) }
746 -- Just get some environments needed for instance looking up and matching
747 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
749 getInstEnvs :: TcS (InstEnv, InstEnv)
750 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
752 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
753 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
755 getTopEnv :: TcS HscEnv
756 getTopEnv = wrapTcS $ TcM.getTopEnv
758 getGblEnv :: TcS TcGblEnv
759 getGblEnv = wrapTcS $ TcM.getGblEnv
761 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
762 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
764 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
765 checkWellStagedDFun pred dfun_id loc
766 = wrapTcS $ TcM.setCtLoc loc $
767 do { use_stage <- TcM.getStage
768 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
770 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
771 bind_lvl = TcM.topIdLvl dfun_id
773 pprEq :: TcType -> TcType -> SDoc
774 pprEq ty1 ty2 = pprPredTy $ mkEqPred (ty1,ty2)
776 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
777 isTouchableMetaTyVar tv
778 = do { untch <- getUntouchables
779 ; return $ isTouchableMetaTyVar_InRange untch tv }
781 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
782 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
783 = case tcTyVarDetails tv of
784 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
785 -- See Note [Touchable meta type variables]
786 MetaTv {} -> inTouchableRange untch tv
793 Note [Touchable meta type variables]
794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
795 Meta type variables allocated *by the constraint solver itself* are always
797 instance C a b => D [a] where...
798 if we use this instance declaration we "make up" a fresh meta type
799 variable for 'b', which we must later guess. (Perhaps C has a
800 functional dependency.) But since we aren't in the constraint *generator*
801 we can't allocate a Unique in the touchable range for this implication
802 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
807 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
809 newFlattenSkolemTy :: TcType -> TcS TcType
810 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
812 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
813 newFlattenSkolemTyVar ty
814 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
815 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
816 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
817 ; traceTcS "New Flatten Skolem Born" $
818 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
822 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
824 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
825 instDFunTypes mb_inst_tys
826 = mapM inst_tv mb_inst_tys
828 inst_tv :: Either TyVar TcType -> TcS Type
829 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
830 inst_tv (Right ty) = return ty
832 instDFunConstraints :: TcThetaType -> TcS [EvVar]
833 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
836 instFlexiTcS :: TyVar -> TcS TcTyVar
837 -- Like TcM.instMetaTyVar but the variable that is created is always
838 -- touchable; we are supposed to guess its instantiation.
839 -- See Note [Touchable meta type variables]
840 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
842 newFlexiTcSTy :: Kind -> TcS TcType
845 do { uniq <- TcM.newUnique
846 ; ref <- TcM.newMutVar Flexi
847 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
848 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
850 isFlexiTcsTv :: TyVar -> Bool
852 | not (isTcTyVar tv) = False
853 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
856 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
857 -- Create new wanted CoVar that constrains the type to have the specified kind.
858 newKindConstraint tv knd
859 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
860 ; let ty_k = mkTyVarTy tv_k
861 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
864 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
865 instFlexiTcSHelper tvname tvkind
867 do { uniq <- TcM.newUnique
868 ; ref <- TcM.newMutVar Flexi
869 ; let name = setNameUnique tvname uniq
871 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
873 -- Superclasses and recursive dictionaries
874 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
876 newEvVar :: TcPredType -> TcS EvVar
877 newEvVar pty = wrapTcS $ TcM.newEvVar pty
879 newDerivedId :: TcPredType -> TcS EvVar
880 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
882 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
883 -- Note we create immutable variables for given or derived, since we
884 -- must bind them to TcEvBinds (because their evidence may involve
885 -- superclasses). However we should be able to override existing
886 -- 'derived' evidence, even in TcEvBinds
887 newGivenCoVar ty1 ty2 co
888 = do { cv <- newCoVar ty1 ty2
889 ; setEvBind cv (EvCoercion co)
892 newCoVar :: TcType -> TcType -> TcS EvVar
893 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
895 newIPVar :: IPName Name -> TcType -> TcS EvVar
896 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
898 newDictVar :: Class -> [TcType] -> TcS EvVar
899 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
904 -- Matching and looking up classes and family instances
905 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
907 data MatchInstResult mi
908 = MatchInstNo -- No matching instance
909 | MatchInstSingle mi -- Single matching instance
910 | MatchInstMany -- Multiple matching instances
913 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
914 -- Look up a class constraint in the instance environment
916 = do { let pred = mkClassPred clas tys
917 ; instEnvs <- getInstEnvs
918 ; case lookupInstEnv instEnvs clas tys of {
919 ([], unifs) -- Nothing matches
920 -> do { traceTcS "matchClass not matching"
921 (vcat [ text "dict" <+> ppr pred,
922 text "unifs" <+> ppr unifs ])
925 ([(ispec, inst_tys)], []) -- A single match
926 -> do { let dfun_id = is_dfun ispec
927 ; traceTcS "matchClass success"
928 (vcat [text "dict" <+> ppr pred,
929 text "witness" <+> ppr dfun_id
930 <+> ppr (idType dfun_id) ])
931 -- Record that this dfun is needed
932 ; return $ MatchInstSingle (dfun_id, inst_tys)
934 (matches, unifs) -- More than one matches
935 -> do { traceTcS "matchClass multiple matches, deferring choice"
936 (vcat [text "dict" <+> ppr pred,
937 text "matches" <+> ppr matches,
938 text "unifs" <+> ppr unifs])
939 ; return MatchInstMany
946 -> TcS (MatchInstResult (TyCon, [Type]))
948 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
950 Nothing -> return MatchInstNo
951 Just res -> return $ MatchInstSingle res
952 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
953 -- multiple matches. Check.