2 -- Type definitions for the constraint solver
5 -- Canonical constraints
6 CanonicalCts, emptyCCan, andCCan, andCCans,
7 singleCCan, extendCCans, isEmptyCCan, isEqCCan,
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
258 isEqCCan :: CanonicalCt -> Bool
259 isEqCCan (CTyEqCan {}) = True
260 isEqCCan (CFunEqCan {}) = True
265 %************************************************************************
268 The "flavor" of a canonical constraint
270 %************************************************************************
274 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
275 | Derived WantedLoc -- We have evidence for this constraint in TcEvBinds;
276 -- *however* this evidence can contain wanteds, so
277 -- it's valid only provisionally to the solution of
279 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
281 instance Outputable CtFlavor where
282 ppr (Given _) = ptext (sLit "[Given]")
283 ppr (Wanted _) = ptext (sLit "[Wanted]")
284 ppr (Derived _) = ptext (sLit "[Derived]")
286 isWanted :: CtFlavor -> Bool
287 isWanted (Wanted {}) = True
290 isGiven :: CtFlavor -> Bool
291 isGiven (Given {}) = True
294 isDerived :: CtFlavor -> Bool
295 isDerived (Derived {}) = True
298 canSolve :: CtFlavor -> CtFlavor -> Bool
299 -- canSolve ctid1 ctid2
300 -- The constraint ctid1 can be used to solve ctid2
301 -- "to solve" means a reaction where the active parts of the two constraints match.
302 -- active(F xis ~ xi) = F xis
303 -- active(tv ~ xi) = tv
304 -- active(D xis) = D xis
305 -- active(IP nm ty) = nm
306 -----------------------------------------
307 canSolve (Given {}) _ = True
308 canSolve (Derived {}) (Wanted {}) = True
309 canSolve (Derived {}) (Derived {}) = True
310 canSolve (Wanted {}) (Wanted {}) = True
313 canRewrite :: CtFlavor -> CtFlavor -> Bool
314 -- canRewrite ctid1 ctid2
315 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
316 canRewrite = canSolve
318 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
319 -- Precondition: At least one of them should be wanted
320 combineCtLoc (Wanted loc) _ = loc
321 combineCtLoc _ (Wanted loc) = loc
322 combineCtLoc (Derived loc) _ = loc
323 combineCtLoc _ (Derived loc) = loc
324 combineCtLoc _ _ = panic "combineCtLoc: both given"
326 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
327 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
328 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
329 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
333 %************************************************************************
335 %* The TcS solver monad *
337 %************************************************************************
341 The TcS monad is a weak form of the main Tc monad
345 * allocate new variables
346 * fill in evidence variables
348 Filling in a dictionary evidence variable means to create a binding
349 for it, so TcS carries a mutable location where the binding can be
350 added. This is initialised from the innermost implication constraint.
355 tcs_ev_binds :: EvBindsVar,
358 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
359 -- Global type bindings
361 tcs_context :: SimplContext,
363 tcs_untch :: Untouchables
367 = SimplInfer -- Inferring type of a let-bound thing
368 | SimplRuleLhs -- Inferring type of a RULE lhs
369 | SimplInteractive -- Inferring type at GHCi prompt
370 | SimplCheck -- Checking a type signature or RULE rhs
372 instance Outputable SimplContext where
373 ppr SimplInfer = ptext (sLit "SimplInfer")
374 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
375 ppr SimplInteractive = ptext (sLit "SimplInteractive")
376 ppr SimplCheck = ptext (sLit "SimplCheck")
378 isInteractive :: SimplContext -> Bool
379 isInteractive SimplInteractive = True
380 isInteractive _ = False
382 simplEqsOnly :: SimplContext -> Bool
383 -- Simplify equalities only, not dictionaries
384 -- This is used for the LHS of rules; ee
385 -- Note [Simplifying RULE lhs constraints] in TcSimplify
386 simplEqsOnly SimplRuleLhs = True
387 simplEqsOnly _ = False
389 performDefaulting :: SimplContext -> Bool
390 performDefaulting SimplInfer = False
391 performDefaulting SimplRuleLhs = False
392 performDefaulting SimplInteractive = True
393 performDefaulting SimplCheck = True
396 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
398 instance Functor TcS where
399 fmap f m = TcS $ fmap f . unTcS m
401 instance Monad TcS where
402 return x = TcS (\_ -> return x)
403 fail err = TcS (\_ -> fail err)
404 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
406 -- Basic functionality
407 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
408 wrapTcS :: TcM a -> TcS a
409 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
410 -- and TcS is supposed to have limited functionality
411 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
413 wrapErrTcS :: TcM a -> TcS a
414 -- The thing wrapped should just fail
415 -- There's no static check; it's up to the user
416 -- Having a variant for each error message is too painful
419 wrapWarnTcS :: TcM a -> TcS a
420 -- The thing wrapped should just add a warning, or no-op
421 -- There's no static check; it's up to the user
422 wrapWarnTcS = wrapTcS
424 failTcS, panicTcS :: SDoc -> TcS a
425 failTcS = wrapTcS . TcM.failWith
426 panicTcS doc = pprPanic "TcCanonical" doc
428 traceTcS :: String -> SDoc -> TcS ()
429 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
431 traceTcS0 :: String -> SDoc -> TcS ()
432 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
434 runTcS :: SimplContext
435 -> Untouchables -- Untouchables
436 -> TcS a -- What to run
437 -> TcM (a, Bag EvBind)
438 runTcS context untouch tcs
439 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
440 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
441 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
442 , tcs_ty_binds = ty_binds_var
443 , tcs_context = context
444 , tcs_untch = untouch }
446 -- Run the computation
447 ; res <- unTcS tcs env
449 -- Perform the type unifications required
450 ; ty_binds <- TcM.readTcRef ty_binds_var
451 ; mapM_ do_unification (varEnvElts ty_binds)
454 ; ev_binds <- TcM.readTcRef evb_ref
455 ; return (res, evBindMapBinds ev_binds) }
457 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
460 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
461 nestImplicTcS ref untch (TcS thing_inside)
462 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
464 nest_env = TcSEnv { tcs_ev_binds = ref
465 , tcs_ty_binds = ty_binds
467 , tcs_context = ctxtUnderImplic ctxt }
469 thing_inside nest_env
471 ctxtUnderImplic :: SimplContext -> SimplContext
472 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
473 ctxtUnderImplic SimplRuleLhs = SimplCheck
474 ctxtUnderImplic ctxt = ctxt
476 tryTcS :: TcS a -> TcS a
477 -- Like runTcS, but from within the TcS monad
478 -- Ignore all the evidence generated, and do not affect caller's evidence!
480 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
481 ; ev_binds_var <- TcM.newTcEvBinds
482 ; let env1 = env { tcs_ev_binds = ev_binds_var
483 , tcs_ty_binds = ty_binds_var }
487 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
489 getDynFlags :: TcS DynFlags
490 getDynFlags = wrapTcS TcM.getDOpts
492 getTcSContext :: TcS SimplContext
493 getTcSContext = TcS (return . tcs_context)
495 getTcEvBinds :: TcS EvBindsVar
496 getTcEvBinds = TcS (return . tcs_ev_binds)
498 getUntouchables :: TcS Untouchables
499 getUntouchables = TcS (return . tcs_untch)
501 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
502 getTcSTyBinds = TcS (return . tcs_ty_binds)
504 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
505 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
508 getTcEvBindsBag :: TcS EvBindMap
510 = do { EvBindsVar ev_ref _ <- getTcEvBinds
511 ; wrapTcS $ TcM.readTcRef ev_ref }
513 setWantedCoBind :: CoVar -> Coercion -> TcS ()
514 setWantedCoBind cv co
515 = setEvBind cv (EvCoercion co)
516 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
518 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
519 setDerivedCoBind cv co
520 = setEvBind cv (EvCoercion co)
522 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
523 -- Add a type binding
524 setWantedTyBind tv ty
525 = do { ref <- getTcSTyBinds
527 do { ty_binds <- TcM.readTcRef ref
528 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
530 setIPBind :: EvVar -> EvTerm -> TcS ()
531 setIPBind = setEvBind
533 setDictBind :: EvVar -> EvTerm -> TcS ()
534 setDictBind = setEvBind
536 setEvBind :: EvVar -> EvTerm -> TcS ()
539 = do { tc_evbinds <- getTcEvBinds
540 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
542 newTcEvBindsTcS :: TcS EvBindsVar
543 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
545 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
546 warnTcS loc warn_if doc
547 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
548 | otherwise = return ()
550 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
552 = do { ctxt <- getTcSContext
553 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
554 ; return (ctxt, tys, flags) }
556 -- Just get some environments needed for instance looking up and matching
557 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
559 getInstEnvs :: TcS (InstEnv, InstEnv)
560 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
562 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
563 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
565 getTopEnv :: TcS HscEnv
566 getTopEnv = wrapTcS $ TcM.getTopEnv
568 getGblEnv :: TcS TcGblEnv
569 getGblEnv = wrapTcS $ TcM.getGblEnv
571 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
572 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
574 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
575 checkWellStagedDFun pred dfun_id loc
576 = wrapTcS $ TcM.setCtLoc loc $
577 do { use_stage <- TcM.getStage
578 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
580 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
581 bind_lvl = TcM.topIdLvl dfun_id
583 pprEq :: TcType -> TcType -> SDoc
584 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
586 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
587 isTouchableMetaTyVar tv
588 = case tcTyVarDetails tv of
589 MetaTv TcsTv _ -> return True -- See Note [Touchable meta type variables]
590 MetaTv {} -> do { untch <- getUntouchables
591 ; return (inTouchableRange untch tv) }
595 Note [Touchable meta type variables]
596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 Meta type variables allocated *by the constraint solver itself* are always
599 instance C a b => D [a] where...
600 if we use this instance declaration we "make up" a fresh meta type
601 variable for 'b', which we must later guess. (Perhaps C has a
602 functional dependency.) But since we aren't in the constraint *generator*
603 we can't allocate a Unique in the touchable range for this implication
604 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
609 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
611 newFlattenSkolemTy :: TcType -> TcS TcType
612 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
614 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
615 newFlattenSkolemTyVar ty
616 = wrapTcS $ do { uniq <- TcM.newUnique
617 ; let name = mkSysTvName uniq (fsLit "f")
618 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
621 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
623 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
624 instDFunTypes mb_inst_tys
625 = mapM inst_tv mb_inst_tys
627 inst_tv :: Either TyVar TcType -> TcS Type
628 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
629 inst_tv (Right ty) = return ty
631 instDFunConstraints :: TcThetaType -> TcS [EvVar]
632 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
634 newFlexiTcS :: TyVar -> TcS TcTyVar
635 -- Make a TcsTv meta tyvar; it is always touchable,
636 -- but we are supposed to guess its instantiation
637 -- See Note [Touchable meta type variables]
638 newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
640 -- Superclasses and recursive dictionaries
641 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
643 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
644 newGivOrDerEvVar pty evtrm
645 = do { ev <- wrapTcS $ TcM.newEvVar pty
649 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
650 -- Note we create immutable variables for given or derived, since we
651 -- must bind them to TcEvBinds (because their evidence may involve
652 -- superclasses). However we should be able to override existing
653 -- 'derived' evidence, even in TcEvBinds
654 newGivOrDerCoVar ty1 ty2 co
655 = do { cv <- newCoVar ty1 ty2
656 ; setEvBind cv (EvCoercion co)
659 newWantedCoVar :: TcType -> TcType -> TcS EvVar
660 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
662 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
663 newKindConstraint ty kind = wrapTcS $ TcM.newKindConstraint ty kind
665 newCoVar :: TcType -> TcType -> TcS EvVar
666 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
668 newIPVar :: IPName Name -> TcType -> TcS EvVar
669 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
671 newDictVar :: Class -> [TcType] -> TcS EvVar
672 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
677 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
678 -- In a call (isGoodRecEv ev wv), we are considering solving wv
679 -- using some term that involves ev, such as:
680 -- by setting wv = ev
681 -- or wv = EvCast x |> ev
683 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
684 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
685 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
687 -- Guarded means: more instance calls than superclass selections. We
688 -- compute this by chasing the evidence, adding +1 for every instance
689 -- call (constructor) and -1 for every superclass selection (destructor).
691 -- See Note [Superclasses and recursive dictionaries] in TcInteract
692 isGoodRecEv ev_var (WantedEvVar wv _)
693 = do { tc_evbinds <- getTcEvBindsBag
694 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
695 ; return $ case mb of
697 Just min_guardedness -> min_guardedness > 0
700 where chase_ev_var :: EvBindMap -- Evidence binds
701 -> EvVar -- Target variable whose gravity we want to return
702 -> Int -- Current gravity
703 -> [EvVar] -- Visited nodes
704 -> EvVar -- Current node
706 chase_ev_var assocs trg curr_grav visited orig
707 | trg == orig = return $ Just curr_grav
708 | orig `elem` visited = return $ Nothing
709 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
710 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
712 {- No longer needed: evidence is in the EvBinds
713 | isTcTyVar orig && isMetaTyVar orig
714 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
715 ; case meta_details of
716 Flexi -> return Nothing
717 Indirect tyco -> chase_ev assocs trg curr_grav
718 (orig:visited) (EvCoercion tyco)
721 | otherwise = return Nothing
723 chase_ev assocs trg curr_grav visited (EvId v)
724 = chase_ev_var assocs trg curr_grav visited v
725 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
726 = chase_ev_var assocs trg (curr_grav-1) visited d_id
727 chase_ev assocs trg curr_grav visited (EvCast v co)
728 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
729 ; m2 <- chase_co assocs trg curr_grav visited co
730 ; return (comb_chase_res Nothing [m1,m2]) }
732 chase_ev assocs trg curr_grav visited (EvCoercion co)
733 = chase_co assocs trg curr_grav visited co
734 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
735 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
736 ; return (comb_chase_res Nothing chase_results) }
738 chase_co assocs trg curr_grav visited co
739 = -- Look for all the coercion variables in the coercion
740 -- chase them, and combine the results. This is OK since the
741 -- coercion will not contain any superclass terms -- anything
742 -- that involves dictionaries will be bound in assocs.
743 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
745 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
746 ; return (comb_chase_res Nothing chase_results) }
748 comb_chase_res f [] = f
749 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
750 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
751 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
754 -- Matching and looking up classes and family instances
755 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
757 data MatchInstResult mi
758 = MatchInstNo -- No matching instance
759 | MatchInstSingle mi -- Single matching instance
760 | MatchInstMany -- Multiple matching instances
763 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
764 -- Look up a class constraint in the instance environment
766 = do { let pred = mkClassPred clas tys
767 ; instEnvs <- getInstEnvs
768 ; case lookupInstEnv instEnvs clas tys of {
769 ([], unifs) -- Nothing matches
770 -> do { traceTcS "matchClass not matching"
771 (vcat [ text "dict" <+> ppr pred,
772 text "unifs" <+> ppr unifs ])
775 ([(ispec, inst_tys)], []) -- A single match
776 -> do { let dfun_id = is_dfun ispec
777 ; traceTcS "matchClass success"
778 (vcat [text "dict" <+> ppr pred,
779 text "witness" <+> ppr dfun_id
780 <+> ppr (idType dfun_id) ])
781 -- Record that this dfun is needed
782 ; record_dfun_usage dfun_id
783 ; return $ MatchInstSingle (dfun_id, inst_tys)
785 (matches, unifs) -- More than one matches
786 -> do { traceTcS "matchClass multiple matches, deferring choice"
787 (vcat [text "dict" <+> ppr pred,
788 text "matches" <+> ppr matches,
789 text "unifs" <+> ppr unifs])
790 ; return MatchInstMany
794 where record_dfun_usage :: Id -> TcS ()
795 record_dfun_usage dfun_id
796 = do { hsc_env <- getTopEnv
797 ; let dfun_name = idName dfun_id
798 dfun_mod = ASSERT( isExternalName dfun_name )
800 ; if isInternalName dfun_name || -- Internal name => defined in this module
801 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
802 then return () -- internal, or in another package
803 else do updInstUses dfun_id
806 updInstUses :: Id -> TcS ()
808 = do { tcg_env <- getGblEnv
809 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
810 (`addOneToNameSet` idName dfun_id)
815 -> TcS (MatchInstResult (TyCon, [Type]))
817 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
819 Nothing -> return MatchInstNo
820 Just res -> return $ MatchInstSingle res
821 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
822 -- multiple matches. Check.
826 -- Functional dependencies, instantiation of equations
827 -------------------------------------------------------
829 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
831 mkWantedFunDepEqns _ [] = return []
832 mkWantedFunDepEqns loc eqns
833 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
834 ; wevvars <- mapM to_work_item eqns
835 ; return $ concat wevvars }
837 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
838 to_work_item ((qtvs, pairs), _, _)
839 = do { let tvs = varSetElems qtvs
840 ; tvs' <- mapM newFlexiTcS tvs
841 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
842 ; mapM (do_one subst) pairs }
844 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
845 sty2 = substTy subst ty2
846 ; ev <- newWantedCoVar sty1 sty2
847 ; return (WantedEvVar ev loc) }
849 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
850 pprEquationDoc (eqn, (p1, _), (p2, _))
851 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]