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
110 import StaticFlags( opt_PprStyle_Debug )
111 import Control.Monad( when )
116 %************************************************************************
118 %* Canonical constraints *
120 %* These are the constraints the low-level simplifier works with *
122 %************************************************************************
125 -- Types without any type functions inside. However, note that xi
126 -- types CAN contain unexpanded type synonyms; however, the
127 -- (transitive) expansions of those type synonyms will not contain any
129 type Xi = Type -- In many comments, "xi" ranges over Xi
131 type CanonicalCts = Bag CanonicalCt
134 -- Atomic canonical constraints
135 = CDictCan { -- e.g. Num xi
137 cc_flavor :: CtFlavor,
142 | CIPCan { -- ?x::tau
143 -- See note [Canonical implicit parameter constraints].
145 cc_flavor :: CtFlavor,
146 cc_ip_nm :: IPName Name,
147 cc_ip_ty :: TcTauType
150 | CTyEqCan { -- tv ~ xi (recall xi means function free)
152 -- * tv not in tvs(xi) (occurs check)
153 -- * typeKind xi `compatKind` typeKind tv
154 -- See Note [Spontaneous solving and kind compatibility]
155 -- * We prefer unification variables on the left *JUST* for efficiency
157 cc_flavor :: CtFlavor,
162 | CFunEqCan { -- F xis ~ xi
163 -- Invariant: * isSynFamilyTyCon cc_fun
164 -- * typeKind (F xis) `compatKind` typeKind xi
166 cc_flavor :: CtFlavor,
167 cc_fun :: TyCon, -- A type function
168 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
169 cc_rhs :: Xi -- *never* over-saturated (because if so
170 -- we should have decomposed)
174 | CFrozenErr { -- A "frozen error" does not interact with anything
175 -- See Note [Frozen Errors]
177 cc_flavor :: CtFlavor
180 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
181 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
183 compatKind :: Kind -> Kind -> Bool
184 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
186 deCanonicalise :: CanonicalCt -> FlavoredEvVar
187 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
189 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
190 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
191 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
192 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
193 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
194 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
196 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
197 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
198 tyVarsOfCDict _ct = emptyVarSet
200 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
201 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
203 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
204 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
206 instance Outputable CanonicalCt where
207 ppr (CDictCan d fl cls tys)
208 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
209 ppr (CIPCan ip fl ip_nm ty)
210 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
211 ppr (CTyEqCan co fl tv ty)
212 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty)
213 ppr (CFunEqCan co fl tc tys ty)
214 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty)
215 ppr (CFrozenErr co fl)
216 = ppr fl <+> pprEvVarWithType co
219 Note [Canonical implicit parameter constraints]
220 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
221 The type in a canonical implicit parameter constraint doesn't need to
222 be a xi (type-function-free type) since we can defer the flattening
223 until checking this type for equality with another type. If we
224 encounter two IP constraints with the same name, they MUST have the
225 same type, and at that point we can generate a flattened equality
226 constraint between the types. (On the other hand, the types in two
227 class constraints for the same class MAY be equal, so they need to be
228 flattened in the first place to facilitate comparing them.)
231 singleCCan :: CanonicalCt -> CanonicalCts
234 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
237 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
238 extendCCans = snocBag
240 andCCans :: [CanonicalCts] -> CanonicalCts
241 andCCans = unionManyBags
243 emptyCCan :: CanonicalCts
246 isEmptyCCan :: CanonicalCts -> Bool
247 isEmptyCCan = isEmptyBag
249 isCTyEqCan :: CanonicalCt -> Bool
250 isCTyEqCan (CTyEqCan {}) = True
251 isCTyEqCan (CFunEqCan {}) = False
254 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
255 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
256 isCDictCan_Maybe _ = Nothing
258 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
259 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
260 isCIPCan_Maybe _ = Nothing
262 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
263 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
264 isCFunEqCan_Maybe _ = Nothing
266 isCFrozenErr :: CanonicalCt -> Bool
267 isCFrozenErr (CFrozenErr {}) = True
268 isCFrozenErr _ = False
271 -- A mixture of Given, Wanted, and Derived constraints.
272 -- We split between equalities and the rest to process equalities first.
273 data WorkList = WorkList { weqs :: CanonicalCts
274 -- NB: weqs includes equalities /and/ family equalities
275 , wrest :: CanonicalCts }
277 unionWorkList :: WorkList -> WorkList -> WorkList
278 unionWorkList wl1 wl2
279 = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
280 , wrest = wrest wl1 `andCCan` wrest wl2 }
282 unionWorkLists :: [WorkList] -> WorkList
283 unionWorkLists = foldr unionWorkList emptyWorkList
285 isEmptyWorkList :: WorkList -> Bool
286 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
288 emptyWorkList :: WorkList
290 = WorkList { weqs = emptyBag, wrest = emptyBag }
292 workListFromEq :: CanonicalCt -> WorkList
293 workListFromEq = workListFromEqs . singleCCan
295 workListFromNonEq :: CanonicalCt -> WorkList
296 workListFromNonEq = workListFromNonEqs . singleCCan
298 workListFromNonEqs :: CanonicalCts -> WorkList
299 workListFromNonEqs cts
300 = WorkList { weqs = emptyCCan, wrest = cts }
302 workListFromEqs :: CanonicalCts -> WorkList
304 = WorkList { weqs = cts, wrest = emptyCCan }
306 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
307 -> r -> WorkList -> m r
308 -- Prioritizes equalities
309 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
310 = do { r1 <- foldrBagM on_ct r eqs
311 ; foldrBagM on_ct r1 rest }
313 instance Outputable WorkList where
314 ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
315 , text "WorkList (Other) = " <+> ppr (wrest wl) ]
321 %************************************************************************
324 The "flavor" of a canonical constraint
326 %************************************************************************
329 getWantedLoc :: CanonicalCt -> WantedLoc
331 = ASSERT (isWanted (cc_flavor ct))
334 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
336 isWantedCt :: CanonicalCt -> Bool
337 isWantedCt ct = isWanted (cc_flavor ct)
338 isGivenCt :: CanonicalCt -> Bool
339 isGivenCt ct = isGiven (cc_flavor ct)
340 isDerivedCt :: CanonicalCt -> Bool
341 isDerivedCt ct = isDerived (cc_flavor ct)
343 canSolve :: CtFlavor -> CtFlavor -> Bool
344 -- canSolve ctid1 ctid2
345 -- The constraint ctid1 can be used to solve ctid2
346 -- "to solve" means a reaction where the active parts of the two constraints match.
347 -- active(F xis ~ xi) = F xis
348 -- active(tv ~ xi) = tv
349 -- active(D xis) = D xis
350 -- active(IP nm ty) = nm
352 -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
353 -----------------------------------------
354 canSolve (Given {}) _ = True
355 canSolve (Wanted {}) (Derived {}) = True
356 canSolve (Wanted {}) (Wanted {}) = True
357 canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
358 canSolve _ _ = False -- (There is no *evidence* for a derived.)
360 canRewrite :: CtFlavor -> CtFlavor -> Bool
361 -- canRewrite ctid1 ctid2
362 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
363 canRewrite = canSolve
365 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
366 -- Precondition: At least one of them should be wanted
367 combineCtLoc (Wanted loc) _ = loc
368 combineCtLoc _ (Wanted loc) = loc
369 combineCtLoc (Derived loc ) _ = loc
370 combineCtLoc _ (Derived loc ) = loc
371 combineCtLoc _ _ = panic "combineCtLoc: both given"
373 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
374 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
375 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
376 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
379 mkWantedFlavor :: CtFlavor -> CtFlavor
380 mkWantedFlavor (Wanted loc) = Wanted loc
381 mkWantedFlavor (Derived loc) = Wanted loc
382 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
385 %************************************************************************
387 %* The TcS solver monad *
389 %************************************************************************
393 The TcS monad is a weak form of the main Tc monad
397 * allocate new variables
398 * fill in evidence variables
400 Filling in a dictionary evidence variable means to create a binding
401 for it, so TcS carries a mutable location where the binding can be
402 added. This is initialised from the innermost implication constraint.
407 tcs_ev_binds :: EvBindsVar,
410 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
411 -- Global type bindings
413 tcs_context :: SimplContext,
415 tcs_untch :: TcsUntouchables,
417 tcs_ic_depth :: Int, -- Implication nesting depth
418 tcs_count :: IORef Int -- Global step count
421 type TcsUntouchables = (Untouchables,TcTyVarSet)
422 -- Like the TcM Untouchables,
423 -- but records extra TcsTv variables generated during simplification
424 -- See Note [Extra TcsTv untouchables] in TcSimplify
429 = SimplInfer SDoc -- Inferring type of a let-bound thing
430 | SimplRuleLhs RuleName -- Inferring type of a RULE lhs
431 | SimplInteractive -- Inferring type at GHCi prompt
432 | SimplCheck SDoc -- Checking a type signature or RULE rhs
434 instance Outputable SimplContext where
435 ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
436 ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
437 ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
438 ppr SimplInteractive = ptext (sLit "SimplInteractive")
440 isInteractive :: SimplContext -> Bool
441 isInteractive SimplInteractive = True
442 isInteractive _ = False
444 simplEqsOnly :: SimplContext -> Bool
445 -- Simplify equalities only, not dictionaries
446 -- This is used for the LHS of rules; ee
447 -- Note [Simplifying RULE lhs constraints] in TcSimplify
448 simplEqsOnly (SimplRuleLhs {}) = True
449 simplEqsOnly _ = False
451 performDefaulting :: SimplContext -> Bool
452 performDefaulting (SimplInfer {}) = False
453 performDefaulting (SimplRuleLhs {}) = False
454 performDefaulting SimplInteractive = True
455 performDefaulting (SimplCheck {}) = True
458 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
460 instance Functor TcS where
461 fmap f m = TcS $ fmap f . unTcS m
463 instance Monad TcS where
464 return x = TcS (\_ -> return x)
465 fail err = TcS (\_ -> fail err)
466 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
468 -- Basic functionality
469 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
470 wrapTcS :: TcM a -> TcS a
471 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
472 -- and TcS is supposed to have limited functionality
473 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
475 wrapErrTcS :: TcM a -> TcS a
476 -- The thing wrapped should just fail
477 -- There's no static check; it's up to the user
478 -- Having a variant for each error message is too painful
481 wrapWarnTcS :: TcM a -> TcS a
482 -- The thing wrapped should just add a warning, or no-op
483 -- There's no static check; it's up to the user
484 wrapWarnTcS = wrapTcS
486 failTcS, panicTcS :: SDoc -> TcS a
487 failTcS = wrapTcS . TcM.failWith
488 panicTcS doc = pprPanic "TcCanonical" doc
490 traceTcS :: String -> SDoc -> TcS ()
491 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
493 bumpStepCountTcS :: TcS ()
494 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
495 ; n <- TcM.readTcRef ref
496 ; TcM.writeTcRef ref (n+1) }
498 traceFireTcS :: Int -> SDoc -> TcS ()
499 -- Dump a rule-firing trace
500 traceFireTcS depth doc
502 TcM.ifDOptM Opt_D_dump_cs_trace $
503 do { n <- TcM.readTcRef (tcs_count env)
505 <> text (replicate (tcs_ic_depth env) '>')
506 <> brackets (int depth) <+> doc
509 runTcS :: SimplContext
510 -> Untouchables -- Untouchables
511 -> TcS a -- What to run
512 -> TcM (a, Bag EvBind)
513 runTcS context untouch tcs
514 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
515 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
516 ; step_count <- TcM.newTcRef 0
517 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
518 , tcs_ty_binds = ty_binds_var
519 , tcs_context = context
520 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
521 , tcs_count = step_count
525 -- Run the computation
526 ; res <- unTcS tcs env
527 -- Perform the type unifications required
528 ; ty_binds <- TcM.readTcRef ty_binds_var
529 ; mapM_ do_unification (varEnvElts ty_binds)
532 ; count <- TcM.readTcRef step_count
533 ; when (opt_PprStyle_Debug && count > 0) $
534 TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
535 <+> int count <+> ppr context)
538 ; ev_binds <- TcM.readTcRef evb_ref
539 ; return (res, evBindMapBinds ev_binds) }
541 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
543 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
544 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
545 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
546 , tcs_untch = (_outer_range, outer_tcs)
548 , tcs_ic_depth = idepth
549 , tcs_context = ctxt } ->
551 inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
552 -- The inner_range should be narrower than the outer one
553 -- (thus increasing the set of untouchables) but
554 -- the inner Tcs-untouchables must be unioned with the
556 nest_env = TcSEnv { tcs_ev_binds = ref
557 , tcs_ty_binds = ty_binds
558 , tcs_untch = inner_untch
560 , tcs_ic_depth = idepth+1
561 , tcs_context = ctxtUnderImplic ctxt }
563 thing_inside nest_env
565 recoverTcS :: TcS a -> TcS a -> TcS a
566 recoverTcS (TcS recovery_code) (TcS thing_inside)
568 TcM.recoverM (recovery_code env) (thing_inside env)
570 ctxtUnderImplic :: SimplContext -> SimplContext
571 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
572 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
573 <+> doubleQuotes (ftext n))
574 ctxtUnderImplic ctxt = ctxt
576 tryTcS :: TcS a -> TcS a
577 -- Like runTcS, but from within the TcS monad
578 -- Ignore all the evidence generated, and do not affect caller's evidence!
580 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
581 ; ev_binds_var <- TcM.newTcEvBinds
582 ; let env1 = env { tcs_ev_binds = ev_binds_var
583 , tcs_ty_binds = ty_binds_var }
587 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
589 getDynFlags :: TcS DynFlags
590 getDynFlags = wrapTcS TcM.getDOpts
592 getTcSContext :: TcS SimplContext
593 getTcSContext = TcS (return . tcs_context)
595 getTcEvBinds :: TcS EvBindsVar
596 getTcEvBinds = TcS (return . tcs_ev_binds)
598 getUntouchables :: TcS TcsUntouchables
599 getUntouchables = TcS (return . tcs_untch)
601 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
602 getTcSTyBinds = TcS (return . tcs_ty_binds)
604 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
605 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
608 getTcEvBindsBag :: TcS EvBindMap
610 = do { EvBindsVar ev_ref _ <- getTcEvBinds
611 ; wrapTcS $ TcM.readTcRef ev_ref }
613 setCoBind :: CoVar -> Coercion -> TcS ()
614 setCoBind cv co = setEvBind cv (EvCoercion co)
616 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
617 -- Add a type binding
618 -- We never do this twice!
619 setWantedTyBind tv ty
620 = do { ref <- getTcSTyBinds
622 do { ty_binds <- TcM.readTcRef ref
624 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
625 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
626 , ppr tv <+> text ":=" <+> ppr ty
627 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
629 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
631 setIPBind :: EvVar -> EvTerm -> TcS ()
632 setIPBind = setEvBind
634 setDictBind :: EvVar -> EvTerm -> TcS ()
635 setDictBind = setEvBind
637 setEvBind :: EvVar -> EvTerm -> TcS ()
640 = do { tc_evbinds <- getTcEvBinds
641 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
643 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
644 warnTcS loc warn_if doc
645 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
646 | otherwise = return ()
648 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
650 = do { ctxt <- getTcSContext
651 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
652 ; return (ctxt, tys, flags) }
654 -- Just get some environments needed for instance looking up and matching
655 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
657 getInstEnvs :: TcS (InstEnv, InstEnv)
658 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
660 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
661 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
663 getTopEnv :: TcS HscEnv
664 getTopEnv = wrapTcS $ TcM.getTopEnv
666 getGblEnv :: TcS TcGblEnv
667 getGblEnv = wrapTcS $ TcM.getGblEnv
669 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
670 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
672 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
673 checkWellStagedDFun pred dfun_id loc
674 = wrapTcS $ TcM.setCtLoc loc $
675 do { use_stage <- TcM.getStage
676 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
678 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
679 bind_lvl = TcM.topIdLvl dfun_id
681 pprEq :: TcType -> TcType -> SDoc
682 pprEq ty1 ty2 = pprPredTy $ mkEqPred (ty1,ty2)
684 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
685 isTouchableMetaTyVar tv
686 = do { untch <- getUntouchables
687 ; return $ isTouchableMetaTyVar_InRange untch tv }
689 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
690 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
691 = case tcTyVarDetails tv of
692 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
693 -- See Note [Touchable meta type variables]
694 MetaTv {} -> inTouchableRange untch tv
701 Note [Touchable meta type variables]
702 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
703 Meta type variables allocated *by the constraint solver itself* are always
705 instance C a b => D [a] where...
706 if we use this instance declaration we "make up" a fresh meta type
707 variable for 'b', which we must later guess. (Perhaps C has a
708 functional dependency.) But since we aren't in the constraint *generator*
709 we can't allocate a Unique in the touchable range for this implication
710 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
715 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
717 newFlattenSkolemTy :: TcType -> TcS TcType
718 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
720 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
721 newFlattenSkolemTyVar ty
722 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
723 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
724 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
725 ; traceTcS "New Flatten Skolem Born" $
726 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
730 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
732 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
733 instDFunTypes mb_inst_tys
734 = mapM inst_tv mb_inst_tys
736 inst_tv :: Either TyVar TcType -> TcS Type
737 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
738 inst_tv (Right ty) = return ty
740 instDFunConstraints :: TcThetaType -> TcS [EvVar]
741 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
744 instFlexiTcS :: TyVar -> TcS TcTyVar
745 -- Like TcM.instMetaTyVar but the variable that is created is always
746 -- touchable; we are supposed to guess its instantiation.
747 -- See Note [Touchable meta type variables]
748 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
750 newFlexiTcSTy :: Kind -> TcS TcType
753 do { uniq <- TcM.newUnique
754 ; ref <- TcM.newMutVar Flexi
755 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
756 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
758 isFlexiTcsTv :: TyVar -> Bool
760 | not (isTcTyVar tv) = False
761 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
764 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
765 -- Create new wanted CoVar that constrains the type to have the specified kind.
766 newKindConstraint tv knd
767 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
768 ; let ty_k = mkTyVarTy tv_k
769 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
772 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
773 instFlexiTcSHelper tvname tvkind
775 do { uniq <- TcM.newUnique
776 ; ref <- TcM.newMutVar Flexi
777 ; let name = setNameUnique tvname uniq
779 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
781 -- Superclasses and recursive dictionaries
782 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
784 newEvVar :: TcPredType -> TcS EvVar
785 newEvVar pty = wrapTcS $ TcM.newEvVar pty
787 newDerivedId :: TcPredType -> TcS EvVar
788 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
790 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
791 -- Note we create immutable variables for given or derived, since we
792 -- must bind them to TcEvBinds (because their evidence may involve
793 -- superclasses). However we should be able to override existing
794 -- 'derived' evidence, even in TcEvBinds
795 newGivenCoVar ty1 ty2 co
796 = do { cv <- newCoVar ty1 ty2
797 ; setEvBind cv (EvCoercion co)
800 newCoVar :: TcType -> TcType -> TcS EvVar
801 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
803 newIPVar :: IPName Name -> TcType -> TcS EvVar
804 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
806 newDictVar :: Class -> [TcType] -> TcS EvVar
807 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
812 -- Matching and looking up classes and family instances
813 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
815 data MatchInstResult mi
816 = MatchInstNo -- No matching instance
817 | MatchInstSingle mi -- Single matching instance
818 | MatchInstMany -- Multiple matching instances
821 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
822 -- Look up a class constraint in the instance environment
824 = do { let pred = mkClassPred clas tys
825 ; instEnvs <- getInstEnvs
826 ; case lookupInstEnv instEnvs clas tys of {
827 ([], unifs) -- Nothing matches
828 -> do { traceTcS "matchClass not matching"
829 (vcat [ text "dict" <+> ppr pred,
830 text "unifs" <+> ppr unifs ])
833 ([(ispec, inst_tys)], []) -- A single match
834 -> do { let dfun_id = is_dfun ispec
835 ; traceTcS "matchClass success"
836 (vcat [text "dict" <+> ppr pred,
837 text "witness" <+> ppr dfun_id
838 <+> ppr (idType dfun_id) ])
839 -- Record that this dfun is needed
840 ; return $ MatchInstSingle (dfun_id, inst_tys)
842 (matches, unifs) -- More than one matches
843 -> do { traceTcS "matchClass multiple matches, deferring choice"
844 (vcat [text "dict" <+> ppr pred,
845 text "matches" <+> ppr matches,
846 text "unifs" <+> ppr unifs])
847 ; return MatchInstMany
854 -> TcS (MatchInstResult (TyCon, [Type]))
856 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
858 Nothing -> return MatchInstNo
859 Just res -> return $ MatchInstSingle res
860 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
861 -- multiple matches. Check.