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, canSolve,
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 constraint is given then typeKind xi == typeKind tv
145 -- See Note [Spontaneous solving and kind compatibility]
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 -- * If constraint is given then
157 -- typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
159 cc_flavor :: CtFlavor,
160 cc_fun :: TyCon, -- A type function
161 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
162 cc_rhs :: Xi -- *never* over-saturated (because if so
163 -- we should have decomposed)
167 makeGivens :: CanonicalCts -> CanonicalCts
168 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
169 -- The UnkSkol doesn't matter because these givens are
170 -- not contradictory (else we'd have rejected them already)
172 makeSolved :: CanonicalCt -> CanonicalCt
173 -- Record that a constraint is now solved
175 -- Given, Derived -> no-op
177 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc }
180 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
181 mkWantedConstraints flats implics
182 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
184 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
185 deCanonicaliseWanted ct
186 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
187 let Wanted loc = cc_flavor ct
188 in WantedEvVar (cc_id ct) loc
190 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
191 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
192 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
193 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
194 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
196 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
197 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
199 instance Outputable CanonicalCt where
200 ppr (CDictCan d fl cls tys)
201 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
202 ppr (CIPCan ip fl ip_nm ty)
203 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
204 ppr (CTyEqCan co fl tv ty)
205 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
206 ppr (CFunEqCan co fl tc tys ty)
207 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
211 Note [No touchables as FunEq RHS]
212 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
213 Notice that (F xis ~ beta), where beta is an touchable unification
214 variable, is not canonical. Why?
215 * If (F xis ~ beta) was the only wanted constraint, we'd
216 definitely want to spontaneously-unify it
218 * But suppose we had an earlier wanted (beta ~ Int), and
219 have already spontaneously unified it. Then we have an
220 identity given (id : beta ~ Int) in the inert set.
222 * But (F xis ~ beta) does not react with that given (because we
223 don't subsitute on the RHS of a function equality). So there's a
224 serious danger that we'd spontaneously unify it a second time.
228 Note [Canonical implicit parameter constraints]
229 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
230 The type in a canonical implicit parameter constraint doesn't need to
231 be a xi (type-function-free type) since we can defer the flattening
232 until checking this type for equality with another type. If we
233 encounter two IP constraints with the same name, they MUST have the
234 same type, and at that point we can generate a flattened equality
235 constraint between the types. (On the other hand, the types in two
236 class constraints for the same class MAY be equal, so they need to be
237 flattened in the first place to facilitate comparing them.)
240 singleCCan :: CanonicalCt -> CanonicalCts
243 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
246 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
247 extendCCans = snocBag
249 andCCans :: [CanonicalCts] -> CanonicalCts
250 andCCans = unionManyBags
252 emptyCCan :: CanonicalCts
255 isEmptyCCan :: CanonicalCts -> Bool
256 isEmptyCCan = isEmptyBag
259 %************************************************************************
262 The "flavor" of a canonical constraint
264 %************************************************************************
268 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
269 | Derived WantedLoc -- We have evidence for this constraint in TcEvBinds;
270 -- *however* this evidence can contain wanteds, so
271 -- it's valid only provisionally to the solution of
273 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
275 instance Outputable CtFlavor where
276 ppr (Given _) = ptext (sLit "[Given]")
277 ppr (Wanted _) = ptext (sLit "[Wanted]")
278 ppr (Derived _) = ptext (sLit "[Derived]")
280 isWanted :: CtFlavor -> Bool
281 isWanted (Wanted {}) = True
284 isGiven :: CtFlavor -> Bool
285 isGiven (Given {}) = True
288 isDerived :: CtFlavor -> Bool
289 isDerived (Derived {}) = True
292 canSolve :: CtFlavor -> CtFlavor -> Bool
293 -- canSolve ctid1 ctid2
294 -- The constraint ctid1 can be used to solve ctid2
295 canSolve (Given {}) _ = True
296 canSolve (Derived {}) (Wanted {}) = True
297 canSolve (Derived {}) (Derived {}) = True
298 canSolve (Wanted {}) (Wanted {}) = True
301 canRewrite :: CtFlavor -> CtFlavor -> Bool
302 -- canRewrite ctid1 ctid2
303 -- The *equality* constraint ctid1 can be used to rewrite inside ctid2
304 canRewrite (Given {}) _ = True
305 canRewrite (Derived {}) (Wanted {}) = True
306 canRewrite (Derived {}) (Derived {}) = True
307 -- Never use a wanted to rewrite anything!
308 canRewrite (Wanted {}) (Wanted {}) = False
309 canRewrite _ _ = False
311 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
312 -- Precondition: At least one of them should be wanted
313 combineCtLoc (Wanted loc) _ = loc
314 combineCtLoc _ (Wanted loc) = loc
315 combineCtLoc (Derived loc) _ = loc
316 combineCtLoc _ (Derived loc) = loc
317 combineCtLoc _ _ = panic "combineCtLoc: both given"
319 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
320 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
321 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
322 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
326 %************************************************************************
328 %* The TcS solver monad *
330 %************************************************************************
334 The TcS monad is a weak form of the main Tc monad
338 * allocate new variables
339 * fill in evidence variables
341 Filling in a dictionary evidence variable means to create a binding
342 for it, so TcS carries a mutable location where the binding can be
343 added. This is initialised from the innermost implication constraint.
348 tcs_ev_binds :: EvBindsVar,
351 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
352 -- Global type bindings
354 tcs_context :: SimplContext,
356 tcs_untch :: Untouchables
360 = SimplInfer -- Inferring type of a let-bound thing
361 | SimplRuleLhs -- Inferring type of a RULE lhs
362 | SimplInteractive -- Inferring type at GHCi prompt
363 | SimplCheck -- Checking a type signature or RULE rhs
365 instance Outputable SimplContext where
366 ppr SimplInfer = ptext (sLit "SimplInfer")
367 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
368 ppr SimplInteractive = ptext (sLit "SimplInteractive")
369 ppr SimplCheck = ptext (sLit "SimplCheck")
371 isInteractive :: SimplContext -> Bool
372 isInteractive SimplInteractive = True
373 isInteractive _ = False
375 simplEqsOnly :: SimplContext -> Bool
376 -- Simplify equalities only, not dictionaries
377 -- This is used for the LHS of rules; ee
378 -- Note [Simplifying RULE lhs constraints] in TcSimplify
379 simplEqsOnly SimplRuleLhs = True
380 simplEqsOnly _ = False
382 performDefaulting :: SimplContext -> Bool
383 performDefaulting SimplInfer = False
384 performDefaulting SimplRuleLhs = False
385 performDefaulting SimplInteractive = True
386 performDefaulting SimplCheck = True
389 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
391 instance Functor TcS where
392 fmap f m = TcS $ fmap f . unTcS m
394 instance Monad TcS where
395 return x = TcS (\_ -> return x)
396 fail err = TcS (\_ -> fail err)
397 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
399 -- Basic functionality
400 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
401 wrapTcS :: TcM a -> TcS a
402 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
403 -- and TcS is supposed to have limited functionality
404 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
406 wrapErrTcS :: TcM a -> TcS a
407 -- The thing wrapped should just fail
408 -- There's no static check; it's up to the user
409 -- Having a variant for each error message is too painful
412 wrapWarnTcS :: TcM a -> TcS a
413 -- The thing wrapped should just add a warning, or no-op
414 -- There's no static check; it's up to the user
415 wrapWarnTcS = wrapTcS
417 failTcS, panicTcS :: SDoc -> TcS a
418 failTcS = wrapTcS . TcM.failWith
419 panicTcS doc = pprPanic "TcCanonical" doc
421 traceTcS :: String -> SDoc -> TcS ()
422 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
424 traceTcS0 :: String -> SDoc -> TcS ()
425 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
427 runTcS :: SimplContext
428 -> Untouchables -- Untouchables
429 -> TcS a -- What to run
430 -> TcM (a, Bag EvBind)
431 runTcS context untouch tcs
432 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
433 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
434 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
435 , tcs_ty_binds = ty_binds_var
436 , tcs_context = context
437 , tcs_untch = untouch }
439 -- Run the computation
440 ; res <- unTcS tcs env
442 -- Perform the type unifications required
443 ; ty_binds <- TcM.readTcRef ty_binds_var
444 ; mapM_ do_unification (varEnvElts ty_binds)
447 ; ev_binds <- TcM.readTcRef evb_ref
448 ; return (res, evBindMapBinds ev_binds) }
450 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
453 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
454 nestImplicTcS ref untch (TcS thing_inside)
455 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
457 nest_env = TcSEnv { tcs_ev_binds = ref
458 , tcs_ty_binds = ty_binds
460 , tcs_context = ctxtUnderImplic ctxt }
462 thing_inside nest_env
464 ctxtUnderImplic :: SimplContext -> SimplContext
465 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
466 ctxtUnderImplic SimplRuleLhs = SimplCheck
467 ctxtUnderImplic ctxt = ctxt
469 tryTcS :: TcS a -> TcS a
470 -- Like runTcS, but from within the TcS monad
471 -- Ignore all the evidence generated, and do not affect caller's evidence!
473 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
474 ; ev_binds_var <- TcM.newTcEvBinds
475 ; let env1 = env { tcs_ev_binds = ev_binds_var
476 , tcs_ty_binds = ty_binds_var }
480 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
482 getDynFlags :: TcS DynFlags
483 getDynFlags = wrapTcS TcM.getDOpts
485 getTcSContext :: TcS SimplContext
486 getTcSContext = TcS (return . tcs_context)
488 getTcEvBinds :: TcS EvBindsVar
489 getTcEvBinds = TcS (return . tcs_ev_binds)
491 getUntouchables :: TcS Untouchables
492 getUntouchables = TcS (return . tcs_untch)
494 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
495 getTcSTyBinds = TcS (return . tcs_ty_binds)
497 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
498 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
501 getTcEvBindsBag :: TcS EvBindMap
503 = do { EvBindsVar ev_ref _ <- getTcEvBinds
504 ; wrapTcS $ TcM.readTcRef ev_ref }
506 setWantedCoBind :: CoVar -> Coercion -> TcS ()
507 setWantedCoBind cv co
508 = setEvBind cv (EvCoercion co)
509 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
511 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
512 setDerivedCoBind cv co
513 = setEvBind cv (EvCoercion co)
515 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
516 -- Add a type binding
517 setWantedTyBind tv ty
518 = do { ref <- getTcSTyBinds
520 do { ty_binds <- TcM.readTcRef ref
521 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
523 setIPBind :: EvVar -> EvTerm -> TcS ()
524 setIPBind = setEvBind
526 setDictBind :: EvVar -> EvTerm -> TcS ()
527 setDictBind = setEvBind
529 setEvBind :: EvVar -> EvTerm -> TcS ()
532 = do { tc_evbinds <- getTcEvBinds
533 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
535 newTcEvBindsTcS :: TcS EvBindsVar
536 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
538 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
539 warnTcS loc warn_if doc
540 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
541 | otherwise = return ()
543 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
545 = do { ctxt <- getTcSContext
546 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
547 ; return (ctxt, tys, flags) }
549 -- Just get some environments needed for instance looking up and matching
550 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
552 getInstEnvs :: TcS (InstEnv, InstEnv)
553 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
555 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
556 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
558 getTopEnv :: TcS HscEnv
559 getTopEnv = wrapTcS $ TcM.getTopEnv
561 getGblEnv :: TcS TcGblEnv
562 getGblEnv = wrapTcS $ TcM.getGblEnv
564 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
565 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
567 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
568 checkWellStagedDFun pred dfun_id loc
569 = wrapTcS $ TcM.setCtLoc loc $
570 do { use_stage <- TcM.getStage
571 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
573 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
574 bind_lvl = TcM.topIdLvl dfun_id
576 pprEq :: TcType -> TcType -> SDoc
577 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
579 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
580 isTouchableMetaTyVar tv
581 = case tcTyVarDetails tv of
582 MetaTv TcsTv _ -> return True -- See Note [Touchable meta type variables]
583 MetaTv {} -> do { untch <- getUntouchables
584 ; return (inTouchableRange untch tv) }
588 Note [Touchable meta type variables]
589 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
590 Meta type variables allocated *by the constraint solver itself* are always
592 instance C a b => D [a] where...
593 if we use this instance declaration we "make up" a fresh meta type
594 variable for 'b', which we must later guess. (Perhaps C has a
595 functional dependency.) But since we aren't in the constraint *generator*
596 we can't allocate a Unique in the touchable range for this implication
597 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
602 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604 newFlattenSkolemTy :: TcType -> TcS TcType
605 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
607 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
608 newFlattenSkolemTyVar ty
609 = wrapTcS $ do { uniq <- TcM.newUnique
610 ; let name = mkSysTvName uniq (fsLit "f")
611 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
614 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
616 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
617 instDFunTypes mb_inst_tys
618 = mapM inst_tv mb_inst_tys
620 inst_tv :: Either TyVar TcType -> TcS Type
621 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
622 inst_tv (Right ty) = return ty
624 instDFunConstraints :: TcThetaType -> TcS [EvVar]
625 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
627 newFlexiTcS :: TyVar -> TcS TcTyVar
628 -- Make a TcsTv meta tyvar; it is always touchable,
629 -- but we are supposed to guess its instantiation
630 -- See Note [Touchable meta type variables]
631 newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
633 -- Superclasses and recursive dictionaries
634 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
636 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
637 newGivOrDerEvVar pty evtrm
638 = do { ev <- wrapTcS $ TcM.newEvVar pty
642 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
643 -- Note we create immutable variables for given or derived, since we
644 -- must bind them to TcEvBinds (because their evidence may involve
645 -- superclasses). However we should be able to override existing
646 -- 'derived' evidence, even in TcEvBinds
647 newGivOrDerCoVar ty1 ty2 co
648 = do { cv <- newCoVar ty1 ty2
649 ; setEvBind cv (EvCoercion co)
652 newWantedCoVar :: TcType -> TcType -> TcS EvVar
653 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
655 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
656 newKindConstraint ty kind = wrapTcS $ TcM.newKindConstraint ty kind
658 newCoVar :: TcType -> TcType -> TcS EvVar
659 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
661 newIPVar :: IPName Name -> TcType -> TcS EvVar
662 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
664 newDictVar :: Class -> [TcType] -> TcS EvVar
665 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
670 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
671 -- In a call (isGoodRecEv ev wv), we are considering solving wv
672 -- using some term that involves ev, such as:
673 -- by setting wv = ev
674 -- or wv = EvCast x |> ev
676 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
677 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
678 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
680 -- Guarded means: more instance calls than superclass selections. We
681 -- compute this by chasing the evidence, adding +1 for every instance
682 -- call (constructor) and -1 for every superclass selection (destructor).
684 -- See Note [Superclasses and recursive dictionaries] in TcInteract
685 isGoodRecEv ev_var (WantedEvVar wv _)
686 = do { tc_evbinds <- getTcEvBindsBag
687 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
688 ; return $ case mb of
690 Just min_guardedness -> min_guardedness > 0
693 where chase_ev_var :: EvBindMap -- Evidence binds
694 -> EvVar -- Target variable whose gravity we want to return
695 -> Int -- Current gravity
696 -> [EvVar] -- Visited nodes
697 -> EvVar -- Current node
699 chase_ev_var assocs trg curr_grav visited orig
700 | trg == orig = return $ Just curr_grav
701 | orig `elem` visited = return $ Nothing
702 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
703 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
705 {- No longer needed: evidence is in the EvBinds
706 | isTcTyVar orig && isMetaTyVar orig
707 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
708 ; case meta_details of
709 Flexi -> return Nothing
710 Indirect tyco -> chase_ev assocs trg curr_grav
711 (orig:visited) (EvCoercion tyco)
714 | otherwise = return Nothing
716 chase_ev assocs trg curr_grav visited (EvId v)
717 = chase_ev_var assocs trg curr_grav visited v
718 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
719 = chase_ev_var assocs trg (curr_grav-1) visited d_id
720 chase_ev assocs trg curr_grav visited (EvCast v co)
721 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
722 ; m2 <- chase_co assocs trg curr_grav visited co
723 ; return (comb_chase_res Nothing [m1,m2]) }
725 chase_ev assocs trg curr_grav visited (EvCoercion co)
726 = chase_co assocs trg curr_grav visited co
727 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
728 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
729 ; return (comb_chase_res Nothing chase_results) }
731 chase_co assocs trg curr_grav visited co
732 = -- Look for all the coercion variables in the coercion
733 -- chase them, and combine the results. This is OK since the
734 -- coercion will not contain any superclass terms -- anything
735 -- that involves dictionaries will be bound in assocs.
736 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
738 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
739 ; return (comb_chase_res Nothing chase_results) }
741 comb_chase_res f [] = f
742 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
743 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
744 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
747 -- Matching and looking up classes and family instances
748 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
750 data MatchInstResult mi
751 = MatchInstNo -- No matching instance
752 | MatchInstSingle mi -- Single matching instance
753 | MatchInstMany -- Multiple matching instances
756 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
757 -- Look up a class constraint in the instance environment
759 = do { let pred = mkClassPred clas tys
760 ; instEnvs <- getInstEnvs
761 ; case lookupInstEnv instEnvs clas tys of {
762 ([], unifs) -- Nothing matches
763 -> do { traceTcS "matchClass not matching"
764 (vcat [ text "dict" <+> ppr pred,
765 text "unifs" <+> ppr unifs ])
768 ([(ispec, inst_tys)], []) -- A single match
769 -> do { let dfun_id = is_dfun ispec
770 ; traceTcS "matchClass success"
771 (vcat [text "dict" <+> ppr pred,
772 text "witness" <+> ppr dfun_id
773 <+> ppr (idType dfun_id) ])
774 -- Record that this dfun is needed
775 ; record_dfun_usage dfun_id
776 ; return $ MatchInstSingle (dfun_id, inst_tys)
778 (matches, unifs) -- More than one matches
779 -> do { traceTcS "matchClass multiple matches, deferring choice"
780 (vcat [text "dict" <+> ppr pred,
781 text "matches" <+> ppr matches,
782 text "unifs" <+> ppr unifs])
783 ; return MatchInstMany
787 where record_dfun_usage :: Id -> TcS ()
788 record_dfun_usage dfun_id
789 = do { hsc_env <- getTopEnv
790 ; let dfun_name = idName dfun_id
791 dfun_mod = ASSERT( isExternalName dfun_name )
793 ; if isInternalName dfun_name || -- Internal name => defined in this module
794 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
795 then return () -- internal, or in another package
796 else do updInstUses dfun_id
799 updInstUses :: Id -> TcS ()
801 = do { tcg_env <- getGblEnv
802 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
803 (`addOneToNameSet` idName dfun_id)
808 -> TcS (MatchInstResult (TyCon, [Type]))
810 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
812 Nothing -> return MatchInstNo
813 Just res -> return $ MatchInstSingle res
814 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
815 -- multiple matches. Check.
819 -- Functional dependencies, instantiation of equations
820 -------------------------------------------------------
822 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
824 mkWantedFunDepEqns _ [] = return []
825 mkWantedFunDepEqns loc eqns
826 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
827 ; wevvars <- mapM to_work_item eqns
828 ; return $ concat wevvars }
830 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
831 to_work_item ((qtvs, pairs), _, _)
832 = do { let tvs = varSetElems qtvs
833 ; tvs' <- mapM newFlexiTcS tvs
834 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
835 ; mapM (do_one subst) pairs }
837 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
838 sty2 = substTy subst ty2
839 ; ev <- newWantedCoVar sty1 sty2
840 ; return (WantedEvVar ev loc) }
842 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
843 pprEquationDoc (eqn, (p1, _), (p2, _))
844 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]