2 -- Type definitions for the constraint solver
5 -- Canonical constraints
6 CanonicalCts, emptyCCan, andCCan, andCCans,
7 singleCCan, extendCCans, isEmptyCCan,
8 CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals,
9 mkWantedConstraints, deCanonicaliseWanted,
10 makeGivens, makeSolved,
12 CtFlavor (..), isWanted, isGiven, isDerived, canRewrite,
13 combineCtLoc, mkGivenFlavor,
15 TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
16 tryTcS, nestImplicTcS, wrapErrTcS, wrapWarnTcS,
17 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
19 -- Creation of evidence variables
21 newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
22 newIPVar, newDictVar, newKindConstraint,
24 -- Setting evidence variables
25 setWantedCoBind, setDerivedCoBind,
26 setIPBind, setDictBind, setEvBind,
32 getInstEnvs, getFamInstEnvs, -- Getting the environments
33 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
34 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
37 newFlattenSkolemTy, -- Flatten skolems
40 instDFunTypes, -- Instantiation
47 getDefaultInfo, getDynFlags,
49 matchClass, matchFam, MatchInstResult (..),
52 pprEq, -- Smaller utils, re-exported from TcM
53 -- TODO (DV): these are only really used in the
54 -- instance matcher in TcSimplify. I am wondering
55 -- if the whole instance matcher simply belongs
59 mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps
63 #include "HsVersions.h"
73 import NameSet ( addOneToNameSet )
75 import qualified TcRnMonad as TcM
76 import qualified TcMType as TcM
77 import qualified TcEnv as TcM
78 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
97 import HsBinds -- for TcEvBinds stuff
107 %************************************************************************
109 %* Canonical constraints *
111 %* These are the constraints the low-level simplifier works with *
113 %************************************************************************
116 -- Types without any type functions inside. However, note that xi
117 -- types CAN contain unexpanded type synonyms; however, the
118 -- (transitive) expansions of those type synonyms will not contain any
120 type Xi = Type -- In many comments, "xi" ranges over Xi
122 type CanonicalCts = Bag CanonicalCt
125 -- Atomic canonical constraints
126 = CDictCan { -- e.g. Num xi
128 cc_flavor :: CtFlavor,
133 | CIPCan { -- ?x::tau
134 -- See note [Canonical implicit parameter constraints].
136 cc_flavor :: CtFlavor,
137 cc_ip_nm :: IPName Name,
138 cc_ip_ty :: TcTauType
141 | CTyEqCan { -- tv ~ xi (recall xi means function free)
143 -- * tv not in tvs(xi) (occurs check)
144 -- * If tv is a MetaTyVar, then typeKind xi <: typeKind tv
145 -- a skolem, then typeKind xi = typeKind tv
147 cc_flavor :: CtFlavor,
152 | CFunEqCan { -- F xis ~ xi
153 -- Invariant: * isSynFamilyTyCon cc_fun
154 -- * cc_rhs is not a touchable unification variable
155 -- See Note [No touchables as FunEq RHS]
156 -- * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
158 cc_flavor :: CtFlavor,
159 cc_fun :: TyCon, -- A type function
160 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
161 cc_rhs :: Xi -- *never* over-saturated (because if so
162 -- we should have decomposed)
166 makeGivens :: CanonicalCts -> CanonicalCts
167 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
168 -- The UnkSkol doesn't matter because these givens are
169 -- not contradictory (else we'd have rejected them already)
171 makeSolved :: CanonicalCt -> CanonicalCt
172 -- Record that a constraint is now solved
174 -- Given, Derived -> no-op
176 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc }
179 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
180 mkWantedConstraints flats implics
181 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
183 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
184 deCanonicaliseWanted ct
185 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
186 let Wanted loc = cc_flavor ct
187 in WantedEvVar (cc_id ct) loc
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
195 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
196 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
198 instance Outputable CanonicalCt where
199 ppr (CDictCan d fl cls tys)
200 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
201 ppr (CIPCan ip fl ip_nm ty)
202 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
203 ppr (CTyEqCan co fl tv ty)
204 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
205 ppr (CFunEqCan co fl tc tys ty)
206 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
210 Note [No touchables as FunEq RHS]
211 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
212 Notice that (F xis ~ beta), where beta is an touchable unification
213 variable, is not canonical. Why?
214 * If (F xis ~ beta) was the only wanted constraint, we'd
215 definitely want to spontaneously-unify it
217 * But suppose we had an earlier wanted (beta ~ Int), and
218 have already spontaneously unified it. Then we have an
219 identity given (id : beta ~ Int) in the inert set.
221 * But (F xis ~ beta) does not react with that given (because we
222 don't subsitute on the RHS of a function equality). So there's a
223 serious danger that we'd spontaneously unify it a second time.
227 Note [Canonical implicit parameter constraints]
228 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
229 The type in a canonical implicit parameter constraint doesn't need to
230 be a xi (type-function-free type) since we can defer the flattening
231 until checking this type for equality with another type. If we
232 encounter two IP constraints with the same name, they MUST have the
233 same type, and at that point we can generate a flattened equality
234 constraint between the types. (On the other hand, the types in two
235 class constraints for the same class MAY be equal, so they need to be
236 flattened in the first place to facilitate comparing them.)
239 singleCCan :: CanonicalCt -> CanonicalCts
242 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
245 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
246 extendCCans = snocBag
248 andCCans :: [CanonicalCts] -> CanonicalCts
249 andCCans = unionManyBags
251 emptyCCan :: CanonicalCts
254 isEmptyCCan :: CanonicalCts -> Bool
255 isEmptyCCan = isEmptyBag
258 %************************************************************************
261 The "flavor" of a canonical constraint
263 %************************************************************************
267 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
268 | Derived WantedLoc -- We have evidence for this constraint in TcEvBinds;
269 -- *however* this evidence can contain wanteds, so
270 -- it's valid only provisionally to the solution of
272 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
274 instance Outputable CtFlavor where
275 ppr (Given _) = ptext (sLit "[Given]")
276 ppr (Wanted _) = ptext (sLit "[Wanted]")
277 ppr (Derived _) = ptext (sLit "[Derived]")
279 isWanted :: CtFlavor -> Bool
280 isWanted (Wanted {}) = True
283 isGiven :: CtFlavor -> Bool
284 isGiven (Given {}) = True
287 isDerived :: CtFlavor -> Bool
288 isDerived (Derived {}) = True
291 canRewrite :: CtFlavor -> CtFlavor -> Bool
292 -- canRewrite ctid1 ctid2
293 -- The constraint ctid1 can be used to rewrite ctid2
294 canRewrite (Given {}) _ = True
295 canRewrite (Derived {}) (Wanted {}) = True
296 canRewrite (Derived {}) (Derived {}) = True
297 canRewrite (Wanted {}) (Wanted {}) = True
298 canRewrite _ _ = False
300 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
301 -- Precondition: At least one of them should be wanted
302 combineCtLoc (Wanted loc) _ = loc
303 combineCtLoc _ (Wanted loc) = loc
304 combineCtLoc (Derived loc) _ = loc
305 combineCtLoc _ (Derived loc) = loc
306 combineCtLoc _ _ = panic "combineCtLoc: both given"
308 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
309 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
310 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
311 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
315 %************************************************************************
317 %* The TcS solver monad *
319 %************************************************************************
323 The TcS monad is a weak form of the main Tc monad
327 * allocate new variables
328 * fill in evidence variables
330 Filling in a dictionary evidence variable means to create a binding
331 for it, so TcS carries a mutable location where the binding can be
332 added. This is initialised from the innermost implication constraint.
337 tcs_ev_binds :: EvBindsVar,
340 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
341 -- Global type bindings
343 tcs_context :: SimplContext,
345 tcs_untch :: Untouchables
349 = SimplInfer -- Inferring type of a let-bound thing
350 | SimplRuleLhs -- Inferring type of a RULE lhs
351 | SimplInteractive -- Inferring type at GHCi prompt
352 | SimplCheck -- Checking a type signature or RULE rhs
354 instance Outputable SimplContext where
355 ppr SimplInfer = ptext (sLit "SimplInfer")
356 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
357 ppr SimplInteractive = ptext (sLit "SimplInteractive")
358 ppr SimplCheck = ptext (sLit "SimplCheck")
360 isInteractive :: SimplContext -> Bool
361 isInteractive SimplInteractive = True
362 isInteractive _ = False
364 simplEqsOnly :: SimplContext -> Bool
365 -- Simplify equalities only, not dictionaries
366 -- This is used for the LHS of rules; ee
367 -- Note [Simplifying RULE lhs constraints] in TcSimplify
368 simplEqsOnly SimplRuleLhs = True
369 simplEqsOnly _ = False
371 performDefaulting :: SimplContext -> Bool
372 performDefaulting SimplInfer = False
373 performDefaulting SimplRuleLhs = False
374 performDefaulting SimplInteractive = True
375 performDefaulting SimplCheck = True
378 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
380 instance Functor TcS where
381 fmap f m = TcS $ fmap f . unTcS m
383 instance Monad TcS where
384 return x = TcS (\_ -> return x)
385 fail err = TcS (\_ -> fail err)
386 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
388 -- Basic functionality
389 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
390 wrapTcS :: TcM a -> TcS a
391 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
392 -- and TcS is supposed to have limited functionality
393 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
395 wrapErrTcS :: TcM a -> TcS a
396 -- The thing wrapped should just fail
397 -- There's no static check; it's up to the user
398 -- Having a variant for each error message is too painful
401 wrapWarnTcS :: TcM a -> TcS a
402 -- The thing wrapped should just add a warning, or no-op
403 -- There's no static check; it's up to the user
404 wrapWarnTcS = wrapTcS
406 failTcS, panicTcS :: SDoc -> TcS a
407 failTcS = wrapTcS . TcM.failWith
408 panicTcS doc = pprPanic "TcCanonical" doc
410 traceTcS :: String -> SDoc -> TcS ()
411 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
413 traceTcS0 :: String -> SDoc -> TcS ()
414 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
416 runTcS :: SimplContext
417 -> Untouchables -- Untouchables
418 -> TcS a -- What to run
419 -> TcM (a, Bag EvBind)
420 runTcS context untouch tcs
421 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
422 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
423 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
424 , tcs_ty_binds = ty_binds_var
425 , tcs_context = context
426 , tcs_untch = untouch }
428 -- Run the computation
429 ; res <- unTcS tcs env
431 -- Perform the type unifications required
432 ; ty_binds <- TcM.readTcRef ty_binds_var
433 ; mapM_ do_unification (varEnvElts ty_binds)
436 ; ev_binds <- TcM.readTcRef evb_ref
437 ; return (res, evBindMapBinds ev_binds) }
439 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
442 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
443 nestImplicTcS ref untch (TcS thing_inside)
444 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
446 nest_env = TcSEnv { tcs_ev_binds = ref
447 , tcs_ty_binds = ty_binds
449 , tcs_context = ctxtUnderImplic ctxt }
451 thing_inside nest_env
453 ctxtUnderImplic :: SimplContext -> SimplContext
454 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
455 ctxtUnderImplic SimplRuleLhs = SimplCheck
456 ctxtUnderImplic ctxt = ctxt
458 tryTcS :: TcS a -> TcS a
459 -- Like runTcS, but from within the TcS monad
460 -- Ignore all the evidence generated, and do not affect caller's evidence!
462 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
463 ; ev_binds_var <- TcM.newTcEvBinds
464 ; let env1 = env { tcs_ev_binds = ev_binds_var
465 , tcs_ty_binds = ty_binds_var }
469 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
471 getDynFlags :: TcS DynFlags
472 getDynFlags = wrapTcS TcM.getDOpts
474 getTcSContext :: TcS SimplContext
475 getTcSContext = TcS (return . tcs_context)
477 getTcEvBinds :: TcS EvBindsVar
478 getTcEvBinds = TcS (return . tcs_ev_binds)
480 getUntouchables :: TcS Untouchables
481 getUntouchables = TcS (return . tcs_untch)
483 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
484 getTcSTyBinds = TcS (return . tcs_ty_binds)
486 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
487 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
490 getTcEvBindsBag :: TcS EvBindMap
492 = do { EvBindsVar ev_ref _ <- getTcEvBinds
493 ; wrapTcS $ TcM.readTcRef ev_ref }
495 setWantedCoBind :: CoVar -> Coercion -> TcS ()
496 setWantedCoBind cv co
497 = setEvBind cv (EvCoercion co)
498 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
500 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
501 setDerivedCoBind cv co
502 = setEvBind cv (EvCoercion co)
504 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
505 -- Add a type binding
506 setWantedTyBind tv ty
507 = do { ref <- getTcSTyBinds
509 do { ty_binds <- TcM.readTcRef ref
510 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
512 setIPBind :: EvVar -> EvTerm -> TcS ()
513 setIPBind = setEvBind
515 setDictBind :: EvVar -> EvTerm -> TcS ()
516 setDictBind = setEvBind
518 setEvBind :: EvVar -> EvTerm -> TcS ()
521 = do { tc_evbinds <- getTcEvBinds
522 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
524 newTcEvBindsTcS :: TcS EvBindsVar
525 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
527 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
528 warnTcS loc warn_if doc
529 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
530 | otherwise = return ()
532 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
534 = do { ctxt <- getTcSContext
535 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
536 ; return (ctxt, tys, flags) }
538 -- Just get some environments needed for instance looking up and matching
539 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
541 getInstEnvs :: TcS (InstEnv, InstEnv)
542 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
544 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
545 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
547 getTopEnv :: TcS HscEnv
548 getTopEnv = wrapTcS $ TcM.getTopEnv
550 getGblEnv :: TcS TcGblEnv
551 getGblEnv = wrapTcS $ TcM.getGblEnv
553 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
554 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
556 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
557 checkWellStagedDFun pred dfun_id loc
558 = wrapTcS $ TcM.setCtLoc loc $
559 do { use_stage <- TcM.getStage
560 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
562 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
563 bind_lvl = TcM.topIdLvl dfun_id
565 pprEq :: TcType -> TcType -> SDoc
566 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
568 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
569 isTouchableMetaTyVar tv
570 = case tcTyVarDetails tv of
571 MetaTv TcsTv _ -> return True -- See Note [Touchable meta type variables]
572 MetaTv {} -> do { untch <- getUntouchables
573 ; return (inTouchableRange untch tv) }
577 Note [Touchable meta type variables]
578 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
579 Meta type variables allocated *by the constraint solver itself* are always
581 instance C a b => D [a] where...
582 if we use this instance declaration we "make up" a fresh meta type
583 variable for 'b', which we must later guess. (Perhaps C has a
584 functional dependency.) But since we aren't in the constraint *generator*
585 we can't allocate a Unique in the touchable range for this implication
586 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
591 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
593 newFlattenSkolemTy :: TcType -> TcS TcType
594 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
596 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
597 newFlattenSkolemTyVar ty
598 = wrapTcS $ do { uniq <- TcM.newUnique
599 ; let name = mkSysTvName uniq (fsLit "f")
600 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
603 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
605 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
606 instDFunTypes mb_inst_tys
607 = mapM inst_tv mb_inst_tys
609 inst_tv :: Either TyVar TcType -> TcS Type
610 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
611 inst_tv (Right ty) = return ty
613 instDFunConstraints :: TcThetaType -> TcS [EvVar]
614 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
616 newFlexiTcS :: TyVar -> TcS TcTyVar
617 -- Make a TcsTv meta tyvar; it is always touchable,
618 -- but we are supposed to guess its instantiation
619 -- See Note [Touchable meta type variables]
620 newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
622 -- Superclasses and recursive dictionaries
623 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
625 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
626 newGivOrDerEvVar pty evtrm
627 = do { ev <- wrapTcS $ TcM.newEvVar pty
631 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
632 -- Note we create immutable variables for given or derived, since we
633 -- must bind them to TcEvBinds (because their evidence may involve
634 -- superclasses). However we should be able to override existing
635 -- 'derived' evidence, even in TcEvBinds
636 newGivOrDerCoVar ty1 ty2 co
637 = do { cv <- newCoVar ty1 ty2
638 ; setEvBind cv (EvCoercion co)
641 newWantedCoVar :: TcType -> TcType -> TcS EvVar
642 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
644 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
645 newKindConstraint ty kind = wrapTcS $ TcM.newKindConstraint ty kind
647 newCoVar :: TcType -> TcType -> TcS EvVar
648 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
650 newIPVar :: IPName Name -> TcType -> TcS EvVar
651 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
653 newDictVar :: Class -> [TcType] -> TcS EvVar
654 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
659 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
660 -- In a call (isGoodRecEv ev wv), we are considering solving wv
661 -- using some term that involves ev, such as:
662 -- by setting wv = ev
663 -- or wv = EvCast x |> ev
665 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
666 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
667 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
669 -- Guarded means: more instance calls than superclass selections. We
670 -- compute this by chasing the evidence, adding +1 for every instance
671 -- call (constructor) and -1 for every superclass selection (destructor).
673 -- See Note [Superclasses and recursive dictionaries] in TcInteract
674 isGoodRecEv ev_var (WantedEvVar wv _)
675 = do { tc_evbinds <- getTcEvBindsBag
676 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
677 ; return $ case mb of
679 Just min_guardedness -> min_guardedness > 0
682 where chase_ev_var :: EvBindMap -- Evidence binds
683 -> EvVar -- Target variable whose gravity we want to return
684 -> Int -- Current gravity
685 -> [EvVar] -- Visited nodes
686 -> EvVar -- Current node
688 chase_ev_var assocs trg curr_grav visited orig
689 | trg == orig = return $ Just curr_grav
690 | orig `elem` visited = return $ Nothing
691 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
692 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
694 {- No longer needed: evidence is in the EvBinds
695 | isTcTyVar orig && isMetaTyVar orig
696 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
697 ; case meta_details of
698 Flexi -> return Nothing
699 Indirect tyco -> chase_ev assocs trg curr_grav
700 (orig:visited) (EvCoercion tyco)
703 | otherwise = return Nothing
705 chase_ev assocs trg curr_grav visited (EvId v)
706 = chase_ev_var assocs trg curr_grav visited v
707 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
708 = chase_ev_var assocs trg (curr_grav-1) visited d_id
709 chase_ev assocs trg curr_grav visited (EvCast v co)
710 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
711 ; m2 <- chase_co assocs trg curr_grav visited co
712 ; return (comb_chase_res Nothing [m1,m2]) }
714 chase_ev assocs trg curr_grav visited (EvCoercion co)
715 = chase_co assocs trg curr_grav visited co
716 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
717 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
718 ; return (comb_chase_res Nothing chase_results) }
720 chase_co assocs trg curr_grav visited co
721 = -- Look for all the coercion variables in the coercion
722 -- chase them, and combine the results. This is OK since the
723 -- coercion will not contain any superclass terms -- anything
724 -- that involves dictionaries will be bound in assocs.
725 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
727 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
728 ; return (comb_chase_res Nothing chase_results) }
730 comb_chase_res f [] = f
731 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
732 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
733 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
736 -- Matching and looking up classes and family instances
737 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
739 data MatchInstResult mi
740 = MatchInstNo -- No matching instance
741 | MatchInstSingle mi -- Single matching instance
742 | MatchInstMany -- Multiple matching instances
745 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
746 -- Look up a class constraint in the instance environment
748 = do { let pred = mkClassPred clas tys
749 ; instEnvs <- getInstEnvs
750 ; case lookupInstEnv instEnvs clas tys of {
751 ([], unifs) -- Nothing matches
752 -> do { traceTcS "matchClass not matching"
753 (vcat [ text "dict" <+> ppr pred,
754 text "unifs" <+> ppr unifs ])
757 ([(ispec, inst_tys)], []) -- A single match
758 -> do { let dfun_id = is_dfun ispec
759 ; traceTcS "matchClass success"
760 (vcat [text "dict" <+> ppr pred,
761 text "witness" <+> ppr dfun_id
762 <+> ppr (idType dfun_id) ])
763 -- Record that this dfun is needed
764 ; record_dfun_usage dfun_id
765 ; return $ MatchInstSingle (dfun_id, inst_tys)
767 (matches, unifs) -- More than one matches
768 -> do { traceTcS "matchClass multiple matches, deferring choice"
769 (vcat [text "dict" <+> ppr pred,
770 text "matches" <+> ppr matches,
771 text "unifs" <+> ppr unifs])
772 ; return MatchInstMany
776 where record_dfun_usage :: Id -> TcS ()
777 record_dfun_usage dfun_id
778 = do { hsc_env <- getTopEnv
779 ; let dfun_name = idName dfun_id
780 dfun_mod = ASSERT( isExternalName dfun_name )
782 ; if isInternalName dfun_name || -- Internal name => defined in this module
783 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
784 then return () -- internal, or in another package
785 else do updInstUses dfun_id
788 updInstUses :: Id -> TcS ()
790 = do { tcg_env <- getGblEnv
791 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
792 (`addOneToNameSet` idName dfun_id)
797 -> TcS (MatchInstResult (TyCon, [Type]))
799 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
801 Nothing -> return MatchInstNo
802 Just res -> return $ MatchInstSingle res
803 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
804 -- multiple matches. Check.
808 -- Functional dependencies, instantiation of equations
809 -------------------------------------------------------
811 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
813 mkWantedFunDepEqns _ [] = return []
814 mkWantedFunDepEqns loc eqns
815 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
816 ; wevvars <- mapM to_work_item eqns
817 ; return $ concat wevvars }
819 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
820 to_work_item ((qtvs, pairs), _, _)
821 = do { let tvs = varSetElems qtvs
822 ; tvs' <- mapM newFlexiTcS tvs
823 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
824 ; mapM (do_one subst) pairs }
826 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
827 sty2 = substTy subst ty2
828 ; ev <- newWantedCoVar sty1 sty2
829 ; return (WantedEvVar ev loc) }
831 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
832 pprEquationDoc (eqn, (p1, _), (p2, _))
833 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]