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 )
104 import HsBinds -- for TcEvBinds stuff
109 import Control.Monad( when )
115 %************************************************************************
117 %* Canonical constraints *
119 %* These are the constraints the low-level simplifier works with *
121 %************************************************************************
124 -- Types without any type functions inside. However, note that xi
125 -- types CAN contain unexpanded type synonyms; however, the
126 -- (transitive) expansions of those type synonyms will not contain any
128 type Xi = Type -- In many comments, "xi" ranges over Xi
130 type CanonicalCts = Bag CanonicalCt
133 -- Atomic canonical constraints
134 = CDictCan { -- e.g. Num xi
136 cc_flavor :: CtFlavor,
141 | CIPCan { -- ?x::tau
142 -- See note [Canonical implicit parameter constraints].
144 cc_flavor :: CtFlavor,
145 cc_ip_nm :: IPName Name,
146 cc_ip_ty :: TcTauType
149 | CTyEqCan { -- tv ~ xi (recall xi means function free)
151 -- * tv not in tvs(xi) (occurs check)
152 -- * typeKind xi `compatKind` typeKind tv
153 -- See Note [Spontaneous solving and kind compatibility]
154 -- * We prefer unification variables on the left *JUST* for efficiency
156 cc_flavor :: CtFlavor,
161 | CFunEqCan { -- F xis ~ xi
162 -- Invariant: * isSynFamilyTyCon cc_fun
163 -- * typeKind (F xis) `compatKind` typeKind xi
165 cc_flavor :: CtFlavor,
166 cc_fun :: TyCon, -- A type function
167 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
168 cc_rhs :: Xi -- *never* over-saturated (because if so
169 -- we should have decomposed)
173 | CFrozenErr { -- A "frozen error" does not interact with anything
174 -- See Note [Frozen Errors]
176 cc_flavor :: CtFlavor
179 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
180 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
182 compatKind :: Kind -> Kind -> Bool
183 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
185 deCanonicalise :: CanonicalCt -> FlavoredEvVar
186 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
188 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
189 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
190 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
191 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
192 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
193 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
195 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
196 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
197 tyVarsOfCDict _ct = emptyVarSet
199 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
200 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
202 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
203 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
205 instance Outputable CanonicalCt where
206 ppr (CDictCan d fl cls tys)
207 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
208 ppr (CIPCan ip fl ip_nm ty)
209 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
210 ppr (CTyEqCan co fl tv ty)
211 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty)
212 ppr (CFunEqCan co fl tc tys ty)
213 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty)
214 ppr (CFrozenErr co fl)
215 = ppr fl <+> pprEvVarWithType co
218 Note [Canonical implicit parameter constraints]
219 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
220 The type in a canonical implicit parameter constraint doesn't need to
221 be a xi (type-function-free type) since we can defer the flattening
222 until checking this type for equality with another type. If we
223 encounter two IP constraints with the same name, they MUST have the
224 same type, and at that point we can generate a flattened equality
225 constraint between the types. (On the other hand, the types in two
226 class constraints for the same class MAY be equal, so they need to be
227 flattened in the first place to facilitate comparing them.)
230 singleCCan :: CanonicalCt -> CanonicalCts
233 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
236 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
237 extendCCans = snocBag
239 andCCans :: [CanonicalCts] -> CanonicalCts
240 andCCans = unionManyBags
242 emptyCCan :: CanonicalCts
245 isEmptyCCan :: CanonicalCts -> Bool
246 isEmptyCCan = isEmptyBag
248 isCTyEqCan :: CanonicalCt -> Bool
249 isCTyEqCan (CTyEqCan {}) = True
250 isCTyEqCan (CFunEqCan {}) = False
253 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
254 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
255 isCDictCan_Maybe _ = Nothing
257 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
258 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
259 isCIPCan_Maybe _ = Nothing
261 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
262 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
263 isCFunEqCan_Maybe _ = Nothing
265 isCFrozenErr :: CanonicalCt -> Bool
266 isCFrozenErr (CFrozenErr {}) = True
267 isCFrozenErr _ = False
270 -- A mixture of Given, Wanted, and Derived constraints.
271 -- We split between equalities and the rest to process equalities first.
272 data WorkList = WorkList { weqs :: CanonicalCts
273 -- NB: weqs includes equalities /and/ family equalities
274 , wrest :: CanonicalCts }
276 unionWorkList :: WorkList -> WorkList -> WorkList
277 unionWorkList wl1 wl2
278 = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
279 , wrest = wrest wl1 `andCCan` wrest wl2 }
281 unionWorkLists :: [WorkList] -> WorkList
282 unionWorkLists = foldr unionWorkList emptyWorkList
284 isEmptyWorkList :: WorkList -> Bool
285 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
287 emptyWorkList :: WorkList
289 = WorkList { weqs = emptyBag, wrest = emptyBag }
291 workListFromEq :: CanonicalCt -> WorkList
292 workListFromEq = workListFromEqs . singleCCan
294 workListFromNonEq :: CanonicalCt -> WorkList
295 workListFromNonEq = workListFromNonEqs . singleCCan
297 workListFromNonEqs :: CanonicalCts -> WorkList
298 workListFromNonEqs cts
299 = WorkList { weqs = emptyCCan, wrest = cts }
301 workListFromEqs :: CanonicalCts -> WorkList
303 = WorkList { weqs = cts, wrest = emptyCCan }
305 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
306 -> r -> WorkList -> m r
307 -- Prioritizes equalities
308 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
309 = do { r1 <- foldrBagM on_ct r eqs
310 ; foldrBagM on_ct r1 rest }
312 instance Outputable WorkList where
313 ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
314 , text "WorkList (Other) = " <+> ppr (wrest wl) ]
320 %************************************************************************
323 The "flavor" of a canonical constraint
325 %************************************************************************
328 getWantedLoc :: CanonicalCt -> WantedLoc
330 = ASSERT (isWanted (cc_flavor ct))
333 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
335 isWantedCt :: CanonicalCt -> Bool
336 isWantedCt ct = isWanted (cc_flavor ct)
337 isGivenCt :: CanonicalCt -> Bool
338 isGivenCt ct = isGiven (cc_flavor ct)
339 isDerivedCt :: CanonicalCt -> Bool
340 isDerivedCt ct = isDerived (cc_flavor ct)
342 canSolve :: CtFlavor -> CtFlavor -> Bool
343 -- canSolve ctid1 ctid2
344 -- The constraint ctid1 can be used to solve ctid2
345 -- "to solve" means a reaction where the active parts of the two constraints match.
346 -- active(F xis ~ xi) = F xis
347 -- active(tv ~ xi) = tv
348 -- active(D xis) = D xis
349 -- active(IP nm ty) = nm
351 -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
352 -----------------------------------------
353 canSolve (Given {}) _ = True
354 canSolve (Wanted {}) (Derived {}) = True
355 canSolve (Wanted {}) (Wanted {}) = True
356 canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
357 canSolve _ _ = False -- (There is no *evidence* for a derived.)
359 canRewrite :: CtFlavor -> CtFlavor -> Bool
360 -- canRewrite ctid1 ctid2
361 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
362 canRewrite = canSolve
364 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
365 -- Precondition: At least one of them should be wanted
366 combineCtLoc (Wanted loc) _ = loc
367 combineCtLoc _ (Wanted loc) = loc
368 combineCtLoc (Derived loc ) _ = loc
369 combineCtLoc _ (Derived loc ) = loc
370 combineCtLoc _ _ = panic "combineCtLoc: both given"
372 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
373 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
374 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
375 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
378 mkWantedFlavor :: CtFlavor -> CtFlavor
379 mkWantedFlavor (Wanted loc) = Wanted loc
380 mkWantedFlavor (Derived loc) = Wanted loc
381 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
384 %************************************************************************
386 %* The TcS solver monad *
388 %************************************************************************
392 The TcS monad is a weak form of the main Tc monad
396 * allocate new variables
397 * fill in evidence variables
399 Filling in a dictionary evidence variable means to create a binding
400 for it, so TcS carries a mutable location where the binding can be
401 added. This is initialised from the innermost implication constraint.
406 tcs_ev_binds :: EvBindsVar,
409 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
410 -- Global type bindings
412 tcs_context :: SimplContext,
414 tcs_untch :: TcsUntouchables,
416 tcs_ic_depth :: Int, -- Implication nesting depth
417 tcs_count :: IORef Int -- Global step count
420 type TcsUntouchables = (Untouchables,TcTyVarSet)
421 -- Like the TcM Untouchables,
422 -- but records extra TcsTv variables generated during simplification
423 -- See Note [Extra TcsTv untouchables] in TcSimplify
428 = SimplInfer SDoc -- Inferring type of a let-bound thing
429 | SimplRuleLhs RuleName -- Inferring type of a RULE lhs
430 | SimplInteractive -- Inferring type at GHCi prompt
431 | SimplCheck SDoc -- Checking a type signature or RULE rhs
433 instance Outputable SimplContext where
434 ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
435 ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
436 ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
437 ppr SimplInteractive = ptext (sLit "SimplInteractive")
439 isInteractive :: SimplContext -> Bool
440 isInteractive SimplInteractive = True
441 isInteractive _ = False
443 simplEqsOnly :: SimplContext -> Bool
444 -- Simplify equalities only, not dictionaries
445 -- This is used for the LHS of rules; ee
446 -- Note [Simplifying RULE lhs constraints] in TcSimplify
447 simplEqsOnly (SimplRuleLhs {}) = True
448 simplEqsOnly _ = False
450 performDefaulting :: SimplContext -> Bool
451 performDefaulting (SimplInfer {}) = False
452 performDefaulting (SimplRuleLhs {}) = False
453 performDefaulting SimplInteractive = True
454 performDefaulting (SimplCheck {}) = True
457 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
459 instance Functor TcS where
460 fmap f m = TcS $ fmap f . unTcS m
462 instance Monad TcS where
463 return x = TcS (\_ -> return x)
464 fail err = TcS (\_ -> fail err)
465 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
467 -- Basic functionality
468 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
469 wrapTcS :: TcM a -> TcS a
470 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
471 -- and TcS is supposed to have limited functionality
472 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
474 wrapErrTcS :: TcM a -> TcS a
475 -- The thing wrapped should just fail
476 -- There's no static check; it's up to the user
477 -- Having a variant for each error message is too painful
480 wrapWarnTcS :: TcM a -> TcS a
481 -- The thing wrapped should just add a warning, or no-op
482 -- There's no static check; it's up to the user
483 wrapWarnTcS = wrapTcS
485 failTcS, panicTcS :: SDoc -> TcS a
486 failTcS = wrapTcS . TcM.failWith
487 panicTcS doc = pprPanic "TcCanonical" doc
489 traceTcS :: String -> SDoc -> TcS ()
490 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
492 bumpStepCountTcS :: TcS ()
493 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
494 ; n <- TcM.readTcRef ref
495 ; TcM.writeTcRef ref (n+1) }
497 traceFireTcS :: Int -> SDoc -> TcS ()
498 -- Dump a rule-firing trace
499 traceFireTcS depth doc
501 TcM.ifDOptM Opt_D_dump_cs_trace $
502 do { n <- TcM.readTcRef (tcs_count env)
504 <> text (replicate (tcs_ic_depth env) '>')
505 <> brackets (int depth) <+> doc
508 runTcS :: SimplContext
509 -> Untouchables -- Untouchables
510 -> TcS a -- What to run
511 -> TcM (a, Bag EvBind)
512 runTcS context untouch tcs
513 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
514 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
515 ; step_count <- TcM.newTcRef 0
516 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
517 , tcs_ty_binds = ty_binds_var
518 , tcs_context = context
519 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
520 , tcs_count = step_count
524 -- Run the computation
525 ; res <- unTcS tcs env
526 -- Perform the type unifications required
527 ; ty_binds <- TcM.readTcRef ty_binds_var
528 ; mapM_ do_unification (varEnvElts ty_binds)
531 ; count <- TcM.readTcRef step_count
533 TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
534 <+> int count <+> ppr context)
537 ; ev_binds <- TcM.readTcRef evb_ref
538 ; return (res, evBindMapBinds ev_binds) }
540 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
542 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
543 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
544 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
545 , tcs_untch = (_outer_range, outer_tcs)
547 , tcs_ic_depth = idepth
548 , tcs_context = ctxt } ->
550 inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
551 -- The inner_range should be narrower than the outer one
552 -- (thus increasing the set of untouchables) but
553 -- the inner Tcs-untouchables must be unioned with the
555 nest_env = TcSEnv { tcs_ev_binds = ref
556 , tcs_ty_binds = ty_binds
557 , tcs_untch = inner_untch
559 , tcs_ic_depth = idepth+1
560 , tcs_context = ctxtUnderImplic ctxt }
562 thing_inside nest_env
564 recoverTcS :: TcS a -> TcS a -> TcS a
565 recoverTcS (TcS recovery_code) (TcS thing_inside)
567 TcM.recoverM (recovery_code env) (thing_inside env)
569 ctxtUnderImplic :: SimplContext -> SimplContext
570 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
571 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
572 <+> doubleQuotes (ftext n))
573 ctxtUnderImplic ctxt = ctxt
575 tryTcS :: TcS a -> TcS a
576 -- Like runTcS, but from within the TcS monad
577 -- Ignore all the evidence generated, and do not affect caller's evidence!
579 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
580 ; ev_binds_var <- TcM.newTcEvBinds
581 ; let env1 = env { tcs_ev_binds = ev_binds_var
582 , tcs_ty_binds = ty_binds_var }
586 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
588 getDynFlags :: TcS DynFlags
589 getDynFlags = wrapTcS TcM.getDOpts
591 getTcSContext :: TcS SimplContext
592 getTcSContext = TcS (return . tcs_context)
594 getTcEvBinds :: TcS EvBindsVar
595 getTcEvBinds = TcS (return . tcs_ev_binds)
597 getUntouchables :: TcS TcsUntouchables
598 getUntouchables = TcS (return . tcs_untch)
600 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
601 getTcSTyBinds = TcS (return . tcs_ty_binds)
603 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
604 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
607 getTcEvBindsBag :: TcS EvBindMap
609 = do { EvBindsVar ev_ref _ <- getTcEvBinds
610 ; wrapTcS $ TcM.readTcRef ev_ref }
612 setCoBind :: CoVar -> Coercion -> TcS ()
613 setCoBind cv co = setEvBind cv (EvCoercion co)
615 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
616 -- Add a type binding
617 -- We never do this twice!
618 setWantedTyBind tv ty
619 = do { ref <- getTcSTyBinds
621 do { ty_binds <- TcM.readTcRef ref
623 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
624 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
625 , ppr tv <+> text ":=" <+> ppr ty
626 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
628 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
630 setIPBind :: EvVar -> EvTerm -> TcS ()
631 setIPBind = setEvBind
633 setDictBind :: EvVar -> EvTerm -> TcS ()
634 setDictBind = setEvBind
636 setEvBind :: EvVar -> EvTerm -> TcS ()
639 = do { tc_evbinds <- getTcEvBinds
640 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
642 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
643 warnTcS loc warn_if doc
644 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
645 | otherwise = return ()
647 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
649 = do { ctxt <- getTcSContext
650 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
651 ; return (ctxt, tys, flags) }
653 -- Just get some environments needed for instance looking up and matching
654 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
656 getInstEnvs :: TcS (InstEnv, InstEnv)
657 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
659 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
660 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
662 getTopEnv :: TcS HscEnv
663 getTopEnv = wrapTcS $ TcM.getTopEnv
665 getGblEnv :: TcS TcGblEnv
666 getGblEnv = wrapTcS $ TcM.getGblEnv
668 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
669 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
671 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
672 checkWellStagedDFun pred dfun_id loc
673 = wrapTcS $ TcM.setCtLoc loc $
674 do { use_stage <- TcM.getStage
675 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
677 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
678 bind_lvl = TcM.topIdLvl dfun_id
680 pprEq :: TcType -> TcType -> SDoc
681 pprEq ty1 ty2 = pprPredTy $ mkEqPred (ty1,ty2)
683 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
684 isTouchableMetaTyVar tv
685 = do { untch <- getUntouchables
686 ; return $ isTouchableMetaTyVar_InRange untch tv }
688 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
689 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
690 = case tcTyVarDetails tv of
691 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
692 -- See Note [Touchable meta type variables]
693 MetaTv {} -> inTouchableRange untch tv
700 Note [Touchable meta type variables]
701 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
702 Meta type variables allocated *by the constraint solver itself* are always
704 instance C a b => D [a] where...
705 if we use this instance declaration we "make up" a fresh meta type
706 variable for 'b', which we must later guess. (Perhaps C has a
707 functional dependency.) But since we aren't in the constraint *generator*
708 we can't allocate a Unique in the touchable range for this implication
709 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
714 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
716 newFlattenSkolemTy :: TcType -> TcS TcType
717 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
719 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
720 newFlattenSkolemTyVar ty
721 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
722 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
723 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
724 ; traceTcS "New Flatten Skolem Born" $
725 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
729 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
731 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
732 instDFunTypes mb_inst_tys
733 = mapM inst_tv mb_inst_tys
735 inst_tv :: Either TyVar TcType -> TcS Type
736 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
737 inst_tv (Right ty) = return ty
739 instDFunConstraints :: TcThetaType -> TcS [EvVar]
740 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
743 instFlexiTcS :: TyVar -> TcS TcTyVar
744 -- Like TcM.instMetaTyVar but the variable that is created is always
745 -- touchable; we are supposed to guess its instantiation.
746 -- See Note [Touchable meta type variables]
747 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
749 newFlexiTcSTy :: Kind -> TcS TcType
752 do { uniq <- TcM.newUnique
753 ; ref <- TcM.newMutVar Flexi
754 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
755 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
757 isFlexiTcsTv :: TyVar -> Bool
759 | not (isTcTyVar tv) = False
760 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
763 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
764 -- Create new wanted CoVar that constrains the type to have the specified kind.
765 newKindConstraint tv knd
766 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
767 ; let ty_k = mkTyVarTy tv_k
768 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
771 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
772 instFlexiTcSHelper tvname tvkind
774 do { uniq <- TcM.newUnique
775 ; ref <- TcM.newMutVar Flexi
776 ; let name = setNameUnique tvname uniq
778 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
780 -- Superclasses and recursive dictionaries
781 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
783 newEvVar :: TcPredType -> TcS EvVar
784 newEvVar pty = wrapTcS $ TcM.newEvVar pty
786 newDerivedId :: TcPredType -> TcS EvVar
787 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
789 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
790 -- Note we create immutable variables for given or derived, since we
791 -- must bind them to TcEvBinds (because their evidence may involve
792 -- superclasses). However we should be able to override existing
793 -- 'derived' evidence, even in TcEvBinds
794 newGivenCoVar ty1 ty2 co
795 = do { cv <- newCoVar ty1 ty2
796 ; setEvBind cv (EvCoercion co)
799 newCoVar :: TcType -> TcType -> TcS EvVar
800 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
802 newIPVar :: IPName Name -> TcType -> TcS EvVar
803 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
805 newDictVar :: Class -> [TcType] -> TcS EvVar
806 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
811 -- Matching and looking up classes and family instances
812 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
814 data MatchInstResult mi
815 = MatchInstNo -- No matching instance
816 | MatchInstSingle mi -- Single matching instance
817 | MatchInstMany -- Multiple matching instances
820 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
821 -- Look up a class constraint in the instance environment
823 = do { let pred = mkClassPred clas tys
824 ; instEnvs <- getInstEnvs
825 ; case lookupInstEnv instEnvs clas tys of {
826 ([], unifs) -- Nothing matches
827 -> do { traceTcS "matchClass not matching"
828 (vcat [ text "dict" <+> ppr pred,
829 text "unifs" <+> ppr unifs ])
832 ([(ispec, inst_tys)], []) -- A single match
833 -> do { let dfun_id = is_dfun ispec
834 ; traceTcS "matchClass success"
835 (vcat [text "dict" <+> ppr pred,
836 text "witness" <+> ppr dfun_id
837 <+> ppr (idType dfun_id) ])
838 -- Record that this dfun is needed
839 ; return $ MatchInstSingle (dfun_id, inst_tys)
841 (matches, unifs) -- More than one matches
842 -> do { traceTcS "matchClass multiple matches, deferring choice"
843 (vcat [text "dict" <+> ppr pred,
844 text "matches" <+> ppr matches,
845 text "unifs" <+> ppr unifs])
846 ; return MatchInstMany
853 -> TcS (MatchInstResult (TyCon, [Type]))
855 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
857 Nothing -> return MatchInstNo
858 Just res -> return $ MatchInstSingle res
859 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
860 -- multiple matches. Check.