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 joinFlavors, 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, getUntouchablesTcS,
34 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsBag,
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 )
96 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 joinFlavors :: CtFlavor -> CtFlavor -> CtFlavor
301 joinFlavors (Wanted loc) _ = Wanted loc
302 joinFlavors _ (Wanted loc) = Wanted loc
303 joinFlavors (Derived loc) _ = Derived loc
304 joinFlavors _ (Derived loc) = Derived loc
305 joinFlavors (Given loc) _ = Given loc
307 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
308 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
309 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
310 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
314 %************************************************************************
316 %* The TcS solver monad *
318 %************************************************************************
322 The TcS monad is a weak form of the main Tc monad
326 * allocate new variables
327 * fill in evidence variables
329 Filling in a dictionary evidence variable means to create a binding
330 for it, so TcS carries a mutable location where the binding can be
331 added. This is initialised from the innermost implication constraint.
336 tcs_ev_binds :: EvBindsVar,
339 tcs_ty_binds :: IORef (Bag (TcTyVar, TcType)),
340 -- Global type bindings
342 tcs_context :: SimplContext
346 = SimplInfer -- Inferring type of a let-bound thing
347 | SimplRuleLhs -- Inferring type of a RULE lhs
348 | SimplInteractive -- Inferring type at GHCi prompt
349 | SimplCheck -- Checking a type signature or RULE rhs
351 instance Outputable SimplContext where
352 ppr SimplInfer = ptext (sLit "SimplInfer")
353 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
354 ppr SimplInteractive = ptext (sLit "SimplInteractive")
355 ppr SimplCheck = ptext (sLit "SimplCheck")
357 isInteractive :: SimplContext -> Bool
358 isInteractive SimplInteractive = True
359 isInteractive _ = False
361 simplEqsOnly :: SimplContext -> Bool
362 -- Simplify equalities only, not dictionaries
363 -- This is used for the LHS of rules; ee
364 -- Note [Simplifying RULE lhs constraints] in TcSimplify
365 simplEqsOnly SimplRuleLhs = True
366 simplEqsOnly _ = False
368 performDefaulting :: SimplContext -> Bool
369 performDefaulting SimplInfer = False
370 performDefaulting SimplRuleLhs = False
371 performDefaulting SimplInteractive = True
372 performDefaulting SimplCheck = True
375 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
377 instance Functor TcS where
378 fmap f m = TcS $ fmap f . unTcS m
380 instance Monad TcS where
381 return x = TcS (\_ -> return x)
382 fail err = TcS (\_ -> fail err)
383 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
385 -- Basic functionality
386 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
387 wrapTcS :: TcM a -> TcS a
388 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
389 -- and TcS is supposed to have limited functionality
390 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
392 wrapErrTcS :: TcM a -> TcS a
393 -- The thing wrapped should just fail
394 -- There's no static check; it's up to the user
395 -- Having a variant for each error message is too painful
398 wrapWarnTcS :: TcM a -> TcS a
399 -- The thing wrapped should just add a warning, or no-op
400 -- There's no static check; it's up to the user
401 wrapWarnTcS = wrapTcS
403 failTcS, panicTcS :: SDoc -> TcS a
404 failTcS = wrapTcS . TcM.failWith
405 panicTcS doc = pprPanic "TcCanonical" doc
407 traceTcS :: String -> SDoc -> TcS ()
408 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
410 traceTcS0 :: String -> SDoc -> TcS ()
411 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
413 runTcS :: SimplContext
414 -> TcTyVarSet -- Untouchables
415 -> TcS a -- What to run
416 -> TcM (a, Bag EvBind)
417 runTcS context untouch tcs
418 = do { ty_binds_var <- TcM.newTcRef emptyBag
419 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
420 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
421 , tcs_ty_binds = ty_binds_var
422 , tcs_context = context }
424 -- Run the computation
425 ; res <- TcM.setUntouchables untouch (unTcS tcs env)
427 -- Perform the type unifications required
428 ; ty_binds <- TcM.readTcRef ty_binds_var
429 ; mapBagM_ do_unification ty_binds
432 ; ev_binds <- TcM.readTcRef evb_ref
433 ; return (res, evBindMapBinds ev_binds) }
435 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
438 nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a
439 nestImplicTcS ref untouch tcs
440 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
442 nest_env = TcSEnv { tcs_ev_binds = ref
443 , tcs_ty_binds = ty_binds
444 , tcs_context = ctxtUnderImplic ctxt }
446 TcM.setUntouchables untouch (unTcS tcs nest_env)
448 ctxtUnderImplic :: SimplContext -> SimplContext
449 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
450 ctxtUnderImplic SimplRuleLhs = SimplCheck
451 ctxtUnderImplic ctxt = ctxt
453 tryTcS :: TcTyVarSet -> TcS a -> TcS a
454 -- Like runTcS, but from within the TcS monad
455 -- Ignore all the evidence generated, and do not affect caller's evidence!
457 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyBag
458 ; ev_binds_var <- TcM.newTcEvBinds
459 ; let env1 = env { tcs_ev_binds = ev_binds_var
460 , tcs_ty_binds = ty_binds_var }
461 ; TcM.setUntouchables untch (unTcS tcs env1) })
464 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
466 getDynFlags :: TcS DynFlags
467 getDynFlags = wrapTcS TcM.getDOpts
469 getTcSContext :: TcS SimplContext
470 getTcSContext = TcS (return . tcs_context)
472 getTcEvBinds :: TcS EvBindsVar
473 getTcEvBinds = TcS (return . tcs_ev_binds)
475 getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType)))
476 getTcSTyBinds = TcS (return . tcs_ty_binds)
478 getTcSTyBindsBag :: TcS (Bag (TcTyVar, TcType))
479 getTcSTyBindsBag = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
482 getTcEvBindsBag :: TcS EvBindMap
484 = do { EvBindsVar ev_ref _ <- getTcEvBinds
485 ; wrapTcS $ TcM.readTcRef ev_ref }
487 setWantedCoBind :: CoVar -> Coercion -> TcS ()
488 setWantedCoBind cv co
489 = setEvBind cv (EvCoercion co)
490 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
492 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
493 setDerivedCoBind cv co
494 = setEvBind cv (EvCoercion co)
496 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
497 -- Add a type binding
498 setWantedTyBind tv ty
499 = do { ref <- getTcSTyBinds
501 do { ty_binds <- TcM.readTcRef ref
502 ; TcM.writeTcRef ref (ty_binds `snocBag` (tv,ty)) } }
504 setIPBind :: EvVar -> EvTerm -> TcS ()
505 setIPBind = setEvBind
507 setDictBind :: EvVar -> EvTerm -> TcS ()
508 setDictBind = setEvBind
510 setEvBind :: EvVar -> EvTerm -> TcS ()
513 = do { tc_evbinds <- getTcEvBinds
514 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
516 newTcEvBindsTcS :: TcS EvBindsVar
517 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
519 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
520 warnTcS loc warn_if doc
521 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
522 | otherwise = return ()
524 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
526 = do { ctxt <- getTcSContext
527 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
528 ; return (ctxt, tys, flags) }
530 -- Just get some environments needed for instance looking up and matching
531 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
533 getInstEnvs :: TcS (InstEnv, InstEnv)
534 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
536 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
537 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
539 getTopEnv :: TcS HscEnv
540 getTopEnv = wrapTcS $ TcM.getTopEnv
542 getGblEnv :: TcS TcGblEnv
543 getGblEnv = wrapTcS $ TcM.getGblEnv
545 getUntouchablesTcS :: TcS TcTyVarSet
546 getUntouchablesTcS = wrapTcS $ TcM.getUntouchables
548 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
549 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
551 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
552 checkWellStagedDFun pred dfun_id loc
553 = wrapTcS $ TcM.setCtLoc loc $
554 do { use_stage <- TcM.getStage
555 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
557 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
558 bind_lvl = TcM.topIdLvl dfun_id
560 pprEq :: TcType -> TcType -> SDoc
561 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
563 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
564 -- is touchable variable!
565 isTouchableMetaTyVar v
566 | isMetaTyVar v = wrapTcS $ do { untch <- TcM.isUntouchable v;
567 ; return (not untch) }
568 | otherwise = return False
572 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
574 newFlattenSkolemTy :: TcType -> TcS TcType
575 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
576 where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
577 newFlattenSkolemTyVar ty
578 = wrapTcS $ do { uniq <- TcM.newUnique
579 ; let name = mkSysTvName uniq (fsLit "f")
581 mkTcTyVar name (typeKind ty) (FlatSkol ty)
585 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
587 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
588 instDFunTypes mb_inst_tys =
589 let inst_tv :: Either TyVar TcType -> TcS Type
590 inst_tv (Left tv) = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy
591 inst_tv (Right ty) = return ty
592 in mapM inst_tv mb_inst_tys
595 instDFunConstraints :: TcThetaType -> TcS [EvVar]
596 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
599 -- Superclasses and recursive dictionaries
600 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
602 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
603 newGivOrDerEvVar pty evtrm
604 = do { ev <- wrapTcS $ TcM.newEvVar pty
608 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
609 -- Note we create immutable variables for given or derived, since we
610 -- must bind them to TcEvBinds (because their evidence may involve
611 -- superclasses). However we should be able to override existing
612 -- 'derived' evidence, even in TcEvBinds
613 newGivOrDerCoVar ty1 ty2 co
614 = do { cv <- newCoVar ty1 ty2
615 ; setEvBind cv (EvCoercion co)
618 newWantedCoVar :: TcType -> TcType -> TcS EvVar
619 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
621 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
622 newKindConstraint ty kind = wrapTcS $ TcM.newKindConstraint ty kind
624 newCoVar :: TcType -> TcType -> TcS EvVar
625 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
627 newIPVar :: IPName Name -> TcType -> TcS EvVar
628 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
630 newDictVar :: Class -> [TcType] -> TcS EvVar
631 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
636 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
637 -- In a call (isGoodRecEv ev wv), we are considering solving wv
638 -- using some term that involves ev, such as:
639 -- by setting wv = ev
640 -- or wv = EvCast x |> ev
642 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
643 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
644 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
646 -- Guarded means: more instance calls than superclass selections. We
647 -- compute this by chasing the evidence, adding +1 for every instance
648 -- call (constructor) and -1 for every superclass selection (destructor).
650 -- See Note [Superclasses and recursive dictionaries] in TcInteract
651 isGoodRecEv ev_var (WantedEvVar wv _)
652 = do { tc_evbinds <- getTcEvBindsBag
653 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
654 ; return $ case mb of
656 Just min_guardedness -> min_guardedness > 0
659 where chase_ev_var :: EvBindMap -- Evidence binds
660 -> EvVar -- Target variable whose gravity we want to return
661 -> Int -- Current gravity
662 -> [EvVar] -- Visited nodes
663 -> EvVar -- Current node
665 chase_ev_var assocs trg curr_grav visited orig
666 | trg == orig = return $ Just curr_grav
667 | orig `elem` visited = return $ Nothing
668 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
669 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
671 {- No longer needed: evidence is in the EvBinds
672 | isTcTyVar orig && isMetaTyVar orig
673 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
674 ; case meta_details of
675 Flexi -> return Nothing
676 Indirect tyco -> chase_ev assocs trg curr_grav
677 (orig:visited) (EvCoercion tyco)
680 | otherwise = return Nothing
682 chase_ev assocs trg curr_grav visited (EvId v)
683 = chase_ev_var assocs trg curr_grav visited v
684 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
685 = chase_ev_var assocs trg (curr_grav-1) visited d_id
686 chase_ev assocs trg curr_grav visited (EvCast v co)
687 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
688 ; m2 <- chase_co assocs trg curr_grav visited co
689 ; return (comb_chase_res Nothing [m1,m2]) }
691 chase_ev assocs trg curr_grav visited (EvCoercion co)
692 = chase_co assocs trg curr_grav visited co
693 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
694 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
695 ; return (comb_chase_res Nothing chase_results) }
697 chase_co assocs trg curr_grav visited co
698 = -- Look for all the coercion variables in the coercion
699 -- chase them, and combine the results. This is OK since the
700 -- coercion will not contain any superclass terms -- anything
701 -- that involves dictionaries will be bound in assocs.
702 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
704 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
705 ; return (comb_chase_res Nothing chase_results) }
707 comb_chase_res f [] = f
708 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
709 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
710 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
713 -- Matching and looking up classes and family instances
714 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
716 data MatchInstResult mi
717 = MatchInstNo -- No matching instance
718 | MatchInstSingle mi -- Single matching instance
719 | MatchInstMany -- Multiple matching instances
722 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
723 -- Look up a class constraint in the instance environment
725 = do { let pred = mkClassPred clas tys
726 ; instEnvs <- getInstEnvs
727 ; case lookupInstEnv instEnvs clas tys of {
728 ([], unifs) -- Nothing matches
729 -> do { traceTcS "matchClass not matching"
730 (vcat [ text "dict" <+> ppr pred,
731 text "unifs" <+> ppr unifs ])
734 ([(ispec, inst_tys)], []) -- A single match
735 -> do { let dfun_id = is_dfun ispec
736 ; traceTcS "matchClass success"
737 (vcat [text "dict" <+> ppr pred,
738 text "witness" <+> ppr dfun_id
739 <+> ppr (idType dfun_id) ])
740 -- Record that this dfun is needed
741 ; record_dfun_usage dfun_id
742 ; return $ MatchInstSingle (dfun_id, inst_tys)
744 (matches, unifs) -- More than one matches
745 -> do { traceTcS "matchClass multiple matches, deferring choice"
746 (vcat [text "dict" <+> ppr pred,
747 text "matches" <+> ppr matches,
748 text "unifs" <+> ppr unifs])
749 ; return MatchInstMany
753 where record_dfun_usage :: Id -> TcS ()
754 record_dfun_usage dfun_id
755 = do { hsc_env <- getTopEnv
756 ; let dfun_name = idName dfun_id
757 dfun_mod = ASSERT( isExternalName dfun_name )
759 ; if isInternalName dfun_name || -- Internal name => defined in this module
760 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
761 then return () -- internal, or in another package
762 else do updInstUses dfun_id
765 updInstUses :: Id -> TcS ()
767 = do { tcg_env <- getGblEnv
768 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
769 (`addOneToNameSet` idName dfun_id)
774 -> TcS (MatchInstResult (TyCon, [Type]))
776 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
778 Nothing -> return MatchInstNo
779 Just res -> return $ MatchInstSingle res
780 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
781 -- multiple matches. Check.
785 -- Functional dependencies, instantiation of equations
786 -------------------------------------------------------
788 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
790 mkWantedFunDepEqns _ [] = return []
791 mkWantedFunDepEqns loc eqns
792 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
793 ; wevvars <- mapM to_work_item eqns
794 ; return $ concat wevvars }
796 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
797 to_work_item ((qtvs, pairs), _, _)
798 = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs)
799 ; mapM (do_one tenv) pairs }
801 do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1
802 sty2 = substTy tenv ty2
803 ; ev <- newWantedCoVar sty1 sty2
804 ; return (WantedEvVar ev loc) }
806 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
807 pprEquationDoc (eqn, (p1, _), (p2, _))
808 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]