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, isGiven, isDerived,
19 isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
24 combineCtLoc, mkGivenFlavor, mkWantedFlavor,
27 TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
28 traceFireTcS, bumpStepCountTcS,
29 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
30 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
32 -- Creation of evidence variables
33 newEvVar, newCoVar, newGivenCoVar,
35 newIPVar, newDictVar, newKindConstraint,
37 -- Setting evidence variables
38 setCoBind, setIPBind, setDictBind, setEvBind,
42 getInstEnvs, getFamInstEnvs, -- Getting the environments
43 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
44 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
46 newFlattenSkolemTy, -- Flatten skolems
49 instDFunTypes, -- Instantiation
51 newFlexiTcSTy, instFlexiTcS,
57 isTouchableMetaTyVar_InRange,
59 getDefaultInfo, getDynFlags,
61 matchClass, matchFam, MatchInstResult (..),
64 pprEq -- Smaller utils, re-exported from TcM
65 -- TODO (DV): these are only really used in the
66 -- instance matcher in TcSimplify. I am wondering
67 -- if the whole instance matcher simply belongs
71 #include "HsVersions.h"
81 import qualified TcRnMonad as TcM
82 import qualified TcMType as TcM
83 import qualified TcEnv as TcM
84 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
102 import HsBinds -- for TcEvBinds stuff
111 %************************************************************************
113 %* Canonical constraints *
115 %* These are the constraints the low-level simplifier works with *
117 %************************************************************************
120 -- Types without any type functions inside. However, note that xi
121 -- types CAN contain unexpanded type synonyms; however, the
122 -- (transitive) expansions of those type synonyms will not contain any
124 type Xi = Type -- In many comments, "xi" ranges over Xi
126 type CanonicalCts = Bag CanonicalCt
129 -- Atomic canonical constraints
130 = CDictCan { -- e.g. Num xi
132 cc_flavor :: CtFlavor,
137 | CIPCan { -- ?x::tau
138 -- See note [Canonical implicit parameter constraints].
140 cc_flavor :: CtFlavor,
141 cc_ip_nm :: IPName Name,
142 cc_ip_ty :: TcTauType
145 | CTyEqCan { -- tv ~ xi (recall xi means function free)
147 -- * tv not in tvs(xi) (occurs check)
148 -- * typeKind xi `compatKind` typeKind tv
149 -- See Note [Spontaneous solving and kind compatibility]
150 -- * We prefer unification variables on the left *JUST* for efficiency
152 cc_flavor :: CtFlavor,
157 | CFunEqCan { -- F xis ~ xi
158 -- Invariant: * isSynFamilyTyCon cc_fun
159 -- * typeKind (F xis) `compatKind` typeKind xi
161 cc_flavor :: CtFlavor,
162 cc_fun :: TyCon, -- A type function
163 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
164 cc_rhs :: Xi -- *never* over-saturated (because if so
165 -- we should have decomposed)
169 | CFrozenErr { -- A "frozen error" does not interact with anything
170 -- See Note [Frozen Errors]
172 cc_flavor :: CtFlavor
175 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
176 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
178 compatKind :: Kind -> Kind -> Bool
179 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
181 deCanonicalise :: CanonicalCt -> FlavoredEvVar
182 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
184 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
185 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
186 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
187 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
188 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
189 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
191 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
192 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
193 tyVarsOfCDict _ct = emptyVarSet
195 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
196 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
198 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
199 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
201 instance Outputable CanonicalCt where
202 ppr (CDictCan d fl cls tys)
203 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
204 ppr (CIPCan ip fl ip_nm ty)
205 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
206 ppr (CTyEqCan co fl tv ty)
207 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
208 ppr (CFunEqCan co fl tc tys ty)
209 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
210 ppr (CFrozenErr co fl)
211 = ppr fl <+> pprEvVarWithType co
214 Note [Canonical implicit parameter constraints]
215 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
216 The type in a canonical implicit parameter constraint doesn't need to
217 be a xi (type-function-free type) since we can defer the flattening
218 until checking this type for equality with another type. If we
219 encounter two IP constraints with the same name, they MUST have the
220 same type, and at that point we can generate a flattened equality
221 constraint between the types. (On the other hand, the types in two
222 class constraints for the same class MAY be equal, so they need to be
223 flattened in the first place to facilitate comparing them.)
226 singleCCan :: CanonicalCt -> CanonicalCts
229 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
232 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
233 extendCCans = snocBag
235 andCCans :: [CanonicalCts] -> CanonicalCts
236 andCCans = unionManyBags
238 emptyCCan :: CanonicalCts
241 isEmptyCCan :: CanonicalCts -> Bool
242 isEmptyCCan = isEmptyBag
244 isCTyEqCan :: CanonicalCt -> Bool
245 isCTyEqCan (CTyEqCan {}) = True
246 isCTyEqCan (CFunEqCan {}) = False
249 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
250 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
251 isCDictCan_Maybe _ = Nothing
253 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
254 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
255 isCIPCan_Maybe _ = Nothing
257 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
258 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
259 isCFunEqCan_Maybe _ = Nothing
261 isCFrozenErr :: CanonicalCt -> Bool
262 isCFrozenErr (CFrozenErr {}) = True
263 isCFrozenErr _ = False
266 -- A mixture of Given, Wanted, and Derived constraints.
267 -- We split between equalities and the rest to process equalities first.
268 data WorkList = WorkList { weqs :: CanonicalCts
269 -- NB: weqs includes equalities /and/ family equalities
270 , wrest :: CanonicalCts }
272 unionWorkList :: WorkList -> WorkList -> WorkList
273 unionWorkList wl1 wl2
274 = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
275 , wrest = wrest wl1 `andCCan` wrest wl2 }
277 unionWorkLists :: [WorkList] -> WorkList
278 unionWorkLists = foldr unionWorkList emptyWorkList
280 isEmptyWorkList :: WorkList -> Bool
281 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
283 emptyWorkList :: WorkList
285 = WorkList { weqs = emptyBag, wrest = emptyBag }
287 workListFromEq :: CanonicalCt -> WorkList
288 workListFromEq = workListFromEqs . singleCCan
290 workListFromNonEq :: CanonicalCt -> WorkList
291 workListFromNonEq = workListFromNonEqs . singleCCan
293 workListFromNonEqs :: CanonicalCts -> WorkList
294 workListFromNonEqs cts
295 = WorkList { weqs = emptyCCan, wrest = cts }
297 workListFromEqs :: CanonicalCts -> WorkList
299 = WorkList { weqs = cts, wrest = emptyCCan }
301 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
302 -> r -> WorkList -> m r
303 -- Prioritizes equalities
304 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
305 = do { r1 <- foldrBagM on_ct r eqs
306 ; foldrBagM on_ct r1 rest }
308 instance Outputable WorkList where
309 ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
310 , text "WorkList (Other) = " <+> ppr (wrest wl) ]
316 %************************************************************************
319 The "flavor" of a canonical constraint
321 %************************************************************************
324 getWantedLoc :: CanonicalCt -> WantedLoc
326 = ASSERT (isWanted (cc_flavor ct))
329 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
331 isWantedCt :: CanonicalCt -> Bool
332 isWantedCt ct = isWanted (cc_flavor ct)
333 isGivenCt :: CanonicalCt -> Bool
334 isGivenCt ct = isGiven (cc_flavor ct)
335 isDerivedCt :: CanonicalCt -> Bool
336 isDerivedCt ct = isDerived (cc_flavor ct)
338 canSolve :: CtFlavor -> CtFlavor -> Bool
339 -- canSolve ctid1 ctid2
340 -- The constraint ctid1 can be used to solve ctid2
341 -- "to solve" means a reaction where the active parts of the two constraints match.
342 -- active(F xis ~ xi) = F xis
343 -- active(tv ~ xi) = tv
344 -- active(D xis) = D xis
345 -- active(IP nm ty) = nm
347 -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
348 -----------------------------------------
349 canSolve (Given {}) _ = True
350 canSolve (Wanted {}) (Derived {}) = True
351 canSolve (Wanted {}) (Wanted {}) = True
352 canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
353 canSolve _ _ = False -- (There is no *evidence* for a derived.)
355 canRewrite :: CtFlavor -> CtFlavor -> Bool
356 -- canRewrite ctid1 ctid2
357 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
358 canRewrite = canSolve
360 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
361 -- Precondition: At least one of them should be wanted
362 combineCtLoc (Wanted loc) _ = loc
363 combineCtLoc _ (Wanted loc) = loc
364 combineCtLoc (Derived loc ) _ = loc
365 combineCtLoc _ (Derived loc ) = loc
366 combineCtLoc _ _ = panic "combineCtLoc: both given"
368 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
369 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
370 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
371 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
374 mkWantedFlavor :: CtFlavor -> CtFlavor
375 mkWantedFlavor (Wanted loc) = Wanted loc
376 mkWantedFlavor (Derived loc) = Wanted loc
377 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
380 %************************************************************************
382 %* The TcS solver monad *
384 %************************************************************************
388 The TcS monad is a weak form of the main Tc monad
392 * allocate new variables
393 * fill in evidence variables
395 Filling in a dictionary evidence variable means to create a binding
396 for it, so TcS carries a mutable location where the binding can be
397 added. This is initialised from the innermost implication constraint.
402 tcs_ev_binds :: EvBindsVar,
405 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
406 -- Global type bindings
408 tcs_context :: SimplContext,
410 tcs_untch :: TcsUntouchables,
412 tcs_ic_depth :: Int, -- Implication nesting depth
413 tcs_count :: IORef Int -- Global step count
416 type TcsUntouchables = (Untouchables,TcTyVarSet)
417 -- Like the TcM Untouchables,
418 -- but records extra TcsTv variables generated during simplification
419 -- See Note [Extra TcsTv untouchables] in TcSimplify
424 = SimplInfer -- Inferring type of a let-bound thing
425 | SimplRuleLhs -- Inferring type of a RULE lhs
426 | SimplInteractive -- Inferring type at GHCi prompt
427 | SimplCheck -- Checking a type signature or RULE rhs
430 instance Outputable SimplContext where
431 ppr SimplInfer = ptext (sLit "SimplInfer")
432 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
433 ppr SimplInteractive = ptext (sLit "SimplInteractive")
434 ppr SimplCheck = ptext (sLit "SimplCheck")
436 isInteractive :: SimplContext -> Bool
437 isInteractive SimplInteractive = True
438 isInteractive _ = False
440 simplEqsOnly :: SimplContext -> Bool
441 -- Simplify equalities only, not dictionaries
442 -- This is used for the LHS of rules; ee
443 -- Note [Simplifying RULE lhs constraints] in TcSimplify
444 simplEqsOnly SimplRuleLhs = True
445 simplEqsOnly _ = False
447 performDefaulting :: SimplContext -> Bool
448 performDefaulting SimplInfer = False
449 performDefaulting SimplRuleLhs = False
450 performDefaulting SimplInteractive = True
451 performDefaulting SimplCheck = True
454 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
456 instance Functor TcS where
457 fmap f m = TcS $ fmap f . unTcS m
459 instance Monad TcS where
460 return x = TcS (\_ -> return x)
461 fail err = TcS (\_ -> fail err)
462 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
464 -- Basic functionality
465 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
466 wrapTcS :: TcM a -> TcS a
467 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
468 -- and TcS is supposed to have limited functionality
469 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
471 wrapErrTcS :: TcM a -> TcS a
472 -- The thing wrapped should just fail
473 -- There's no static check; it's up to the user
474 -- Having a variant for each error message is too painful
477 wrapWarnTcS :: TcM a -> TcS a
478 -- The thing wrapped should just add a warning, or no-op
479 -- There's no static check; it's up to the user
480 wrapWarnTcS = wrapTcS
482 failTcS, panicTcS :: SDoc -> TcS a
483 failTcS = wrapTcS . TcM.failWith
484 panicTcS doc = pprPanic "TcCanonical" doc
486 traceTcS :: String -> SDoc -> TcS ()
487 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
489 bumpStepCountTcS :: TcS ()
490 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
491 ; n <- TcM.readTcRef ref
492 ; TcM.writeTcRef ref (n+1) }
494 traceFireTcS :: Int -> SDoc -> TcS ()
495 -- Dump a rule-firing trace
496 traceFireTcS depth doc
498 TcM.ifDOptM Opt_D_dump_cs_trace $
499 do { n <- TcM.readTcRef (tcs_count env)
501 <> text (replicate (tcs_ic_depth env) '>')
502 <> brackets (int depth) <+> doc
505 runTcS :: SimplContext
506 -> Untouchables -- Untouchables
507 -> TcS a -- What to run
508 -> TcM (a, Bag EvBind)
509 runTcS context untouch tcs
510 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
511 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
512 ; step_count <- TcM.newTcRef 0
513 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
514 , tcs_ty_binds = ty_binds_var
515 , tcs_context = context
516 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
517 , tcs_count = step_count
521 -- Run the computation
522 ; res <- unTcS tcs env
523 -- Perform the type unifications required
524 ; ty_binds <- TcM.readTcRef ty_binds_var
525 ; mapM_ do_unification (varEnvElts ty_binds)
528 ; count <- TcM.readTcRef step_count
529 ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
532 ; ev_binds <- TcM.readTcRef evb_ref
533 ; return (res, evBindMapBinds ev_binds) }
535 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
537 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
538 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
539 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
540 , tcs_untch = (_outer_range, outer_tcs)
542 , tcs_ic_depth = idepth
543 , tcs_context = ctxt } ->
545 inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
546 -- The inner_range should be narrower than the outer one
547 -- (thus increasing the set of untouchables) but
548 -- the inner Tcs-untouchables must be unioned with the
550 nest_env = TcSEnv { tcs_ev_binds = ref
551 , tcs_ty_binds = ty_binds
552 , tcs_untch = inner_untch
554 , tcs_ic_depth = idepth+1
555 , tcs_context = ctxtUnderImplic ctxt }
557 thing_inside nest_env
559 recoverTcS :: TcS a -> TcS a -> TcS a
560 recoverTcS (TcS recovery_code) (TcS thing_inside)
562 TcM.recoverM (recovery_code env) (thing_inside env)
564 ctxtUnderImplic :: SimplContext -> SimplContext
565 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
566 ctxtUnderImplic SimplRuleLhs = SimplCheck
567 ctxtUnderImplic ctxt = ctxt
569 tryTcS :: TcS a -> TcS a
570 -- Like runTcS, but from within the TcS monad
571 -- Ignore all the evidence generated, and do not affect caller's evidence!
573 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
574 ; ev_binds_var <- TcM.newTcEvBinds
575 ; let env1 = env { tcs_ev_binds = ev_binds_var
576 , tcs_ty_binds = ty_binds_var }
580 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
582 getDynFlags :: TcS DynFlags
583 getDynFlags = wrapTcS TcM.getDOpts
585 getTcSContext :: TcS SimplContext
586 getTcSContext = TcS (return . tcs_context)
588 getTcEvBinds :: TcS EvBindsVar
589 getTcEvBinds = TcS (return . tcs_ev_binds)
591 getUntouchables :: TcS TcsUntouchables
592 getUntouchables = TcS (return . tcs_untch)
594 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
595 getTcSTyBinds = TcS (return . tcs_ty_binds)
597 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
598 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
601 getTcEvBindsBag :: TcS EvBindMap
603 = do { EvBindsVar ev_ref _ <- getTcEvBinds
604 ; wrapTcS $ TcM.readTcRef ev_ref }
606 setCoBind :: CoVar -> Coercion -> TcS ()
607 setCoBind cv co = setEvBind cv (EvCoercion co)
609 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
610 -- Add a type binding
611 -- We never do this twice!
612 setWantedTyBind tv ty
613 = do { ref <- getTcSTyBinds
615 do { ty_binds <- TcM.readTcRef ref
617 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
618 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
619 , ppr tv <+> text ":=" <+> ppr ty
620 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
622 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
624 setIPBind :: EvVar -> EvTerm -> TcS ()
625 setIPBind = setEvBind
627 setDictBind :: EvVar -> EvTerm -> TcS ()
628 setDictBind = setEvBind
630 setEvBind :: EvVar -> EvTerm -> TcS ()
633 = do { tc_evbinds <- getTcEvBinds
634 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
636 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
637 warnTcS loc warn_if doc
638 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
639 | otherwise = return ()
641 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
643 = do { ctxt <- getTcSContext
644 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
645 ; return (ctxt, tys, flags) }
647 -- Just get some environments needed for instance looking up and matching
648 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
650 getInstEnvs :: TcS (InstEnv, InstEnv)
651 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
653 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
654 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
656 getTopEnv :: TcS HscEnv
657 getTopEnv = wrapTcS $ TcM.getTopEnv
659 getGblEnv :: TcS TcGblEnv
660 getGblEnv = wrapTcS $ TcM.getGblEnv
662 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
663 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
665 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
666 checkWellStagedDFun pred dfun_id loc
667 = wrapTcS $ TcM.setCtLoc loc $
668 do { use_stage <- TcM.getStage
669 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
671 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
672 bind_lvl = TcM.topIdLvl dfun_id
674 pprEq :: TcType -> TcType -> SDoc
675 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
677 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
678 isTouchableMetaTyVar tv
679 = do { untch <- getUntouchables
680 ; return $ isTouchableMetaTyVar_InRange untch tv }
682 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
683 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
684 = case tcTyVarDetails tv of
685 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
686 -- See Note [Touchable meta type variables]
687 MetaTv {} -> inTouchableRange untch tv
694 Note [Touchable meta type variables]
695 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
696 Meta type variables allocated *by the constraint solver itself* are always
698 instance C a b => D [a] where...
699 if we use this instance declaration we "make up" a fresh meta type
700 variable for 'b', which we must later guess. (Perhaps C has a
701 functional dependency.) But since we aren't in the constraint *generator*
702 we can't allocate a Unique in the touchable range for this implication
703 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
708 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
710 newFlattenSkolemTy :: TcType -> TcS TcType
711 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
713 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
714 newFlattenSkolemTyVar ty
715 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
716 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
717 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
718 ; traceTcS "New Flatten Skolem Born" $
719 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
723 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
725 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
726 instDFunTypes mb_inst_tys
727 = mapM inst_tv mb_inst_tys
729 inst_tv :: Either TyVar TcType -> TcS Type
730 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
731 inst_tv (Right ty) = return ty
733 instDFunConstraints :: TcThetaType -> TcS [EvVar]
734 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
737 instFlexiTcS :: TyVar -> TcS TcTyVar
738 -- Like TcM.instMetaTyVar but the variable that is created is always
739 -- touchable; we are supposed to guess its instantiation.
740 -- See Note [Touchable meta type variables]
741 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
743 newFlexiTcSTy :: Kind -> TcS TcType
746 do { uniq <- TcM.newUnique
747 ; ref <- TcM.newMutVar Flexi
748 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
749 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
751 isFlexiTcsTv :: TyVar -> Bool
753 | not (isTcTyVar tv) = False
754 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
757 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
758 -- Create new wanted CoVar that constrains the type to have the specified kind.
759 newKindConstraint tv knd
760 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
761 ; let ty_k = mkTyVarTy tv_k
762 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
765 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
766 instFlexiTcSHelper tvname tvkind
768 do { uniq <- TcM.newUnique
769 ; ref <- TcM.newMutVar Flexi
770 ; let name = setNameUnique tvname uniq
772 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
774 -- Superclasses and recursive dictionaries
775 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
777 newEvVar :: TcPredType -> TcS EvVar
778 newEvVar pty = wrapTcS $ TcM.newEvVar pty
780 newDerivedId :: TcPredType -> TcS EvVar
781 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
783 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
784 -- Note we create immutable variables for given or derived, since we
785 -- must bind them to TcEvBinds (because their evidence may involve
786 -- superclasses). However we should be able to override existing
787 -- 'derived' evidence, even in TcEvBinds
788 newGivenCoVar ty1 ty2 co
789 = do { cv <- newCoVar ty1 ty2
790 ; setEvBind cv (EvCoercion co)
793 newCoVar :: TcType -> TcType -> TcS EvVar
794 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
796 newIPVar :: IPName Name -> TcType -> TcS EvVar
797 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
799 newDictVar :: Class -> [TcType] -> TcS EvVar
800 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
805 -- Matching and looking up classes and family instances
806 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
808 data MatchInstResult mi
809 = MatchInstNo -- No matching instance
810 | MatchInstSingle mi -- Single matching instance
811 | MatchInstMany -- Multiple matching instances
814 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
815 -- Look up a class constraint in the instance environment
817 = do { let pred = mkClassPred clas tys
818 ; instEnvs <- getInstEnvs
819 ; case lookupInstEnv instEnvs clas tys of {
820 ([], unifs) -- Nothing matches
821 -> do { traceTcS "matchClass not matching"
822 (vcat [ text "dict" <+> ppr pred,
823 text "unifs" <+> ppr unifs ])
826 ([(ispec, inst_tys)], []) -- A single match
827 -> do { let dfun_id = is_dfun ispec
828 ; traceTcS "matchClass success"
829 (vcat [text "dict" <+> ppr pred,
830 text "witness" <+> ppr dfun_id
831 <+> ppr (idType dfun_id) ])
832 -- Record that this dfun is needed
833 ; return $ MatchInstSingle (dfun_id, inst_tys)
835 (matches, unifs) -- More than one matches
836 -> do { traceTcS "matchClass multiple matches, deferring choice"
837 (vcat [text "dict" <+> ppr pred,
838 text "matches" <+> ppr matches,
839 text "unifs" <+> ppr unifs])
840 ; return MatchInstMany
847 -> TcS (MatchInstResult (TyCon, [Type]))
849 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
851 Nothing -> return MatchInstNo
852 Just res -> return $ MatchInstSingle res
853 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
854 -- multiple matches. Check.