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 -- "to solve" means a reaction where the active parts of the two constraints match.
296 -- active(F xis ~ xi) = F xis
297 -- active(tv ~ xi) = tv
298 -- active(D xis) = D xis
299 -- active(IP nm ty) = nm
300 -----------------------------------------
301 canSolve (Given {}) _ = True
302 canSolve (Derived {}) (Wanted {}) = True
303 canSolve (Derived {}) (Derived {}) = True
304 canSolve (Wanted {}) (Wanted {}) = True
307 canRewrite :: CtFlavor -> CtFlavor -> Bool
308 -- canRewrite ctid1 ctid2
309 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
310 canRewrite (Given {}) _ = True
311 canRewrite (Derived {}) (Wanted {}) = True
312 canRewrite (Derived {}) (Derived {}) = True
313 -- See note [Rewriting wanteds with wanteds]
314 canRewrite (Wanted {}) (Wanted {}) = False
315 canRewrite _ _ = False
318 Note [Rewriting wanteds with wanteds]
319 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
320 We will currently never use a wanted to rewrite any other
321 constraint (function @canRewrite@). If a rewriting was possible at all,
322 we simply wait until the wanted equality becomes given or derived and
323 then use it. This way we avoid rewriting by eventually insoluble wanteds,
324 such as in the following situation:
328 where 'a' is a skolem variable. If we rewrite using w1 inside w2 we will
329 get the perhaps mystifying error at the end that we could not solve
330 (a ~ Int) and (G Bool ~ Int). But there is no point in rewriting with
331 a ~ Int as long as it is still wanted.
333 Notice that on the other hand we often do solve one wanted from another,
334 (function @canSolve@) for instance in dictionary interactions, which is
335 a reaction that enables sharing both in the solver and in the final evidence
340 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
341 -- Precondition: At least one of them should be wanted
342 combineCtLoc (Wanted loc) _ = loc
343 combineCtLoc _ (Wanted loc) = loc
344 combineCtLoc (Derived loc) _ = loc
345 combineCtLoc _ (Derived loc) = loc
346 combineCtLoc _ _ = panic "combineCtLoc: both given"
348 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
349 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
350 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
351 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
355 %************************************************************************
357 %* The TcS solver monad *
359 %************************************************************************
363 The TcS monad is a weak form of the main Tc monad
367 * allocate new variables
368 * fill in evidence variables
370 Filling in a dictionary evidence variable means to create a binding
371 for it, so TcS carries a mutable location where the binding can be
372 added. This is initialised from the innermost implication constraint.
377 tcs_ev_binds :: EvBindsVar,
380 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
381 -- Global type bindings
383 tcs_context :: SimplContext,
385 tcs_untch :: Untouchables
389 = SimplInfer -- Inferring type of a let-bound thing
390 | SimplRuleLhs -- Inferring type of a RULE lhs
391 | SimplInteractive -- Inferring type at GHCi prompt
392 | SimplCheck -- Checking a type signature or RULE rhs
394 instance Outputable SimplContext where
395 ppr SimplInfer = ptext (sLit "SimplInfer")
396 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
397 ppr SimplInteractive = ptext (sLit "SimplInteractive")
398 ppr SimplCheck = ptext (sLit "SimplCheck")
400 isInteractive :: SimplContext -> Bool
401 isInteractive SimplInteractive = True
402 isInteractive _ = False
404 simplEqsOnly :: SimplContext -> Bool
405 -- Simplify equalities only, not dictionaries
406 -- This is used for the LHS of rules; ee
407 -- Note [Simplifying RULE lhs constraints] in TcSimplify
408 simplEqsOnly SimplRuleLhs = True
409 simplEqsOnly _ = False
411 performDefaulting :: SimplContext -> Bool
412 performDefaulting SimplInfer = False
413 performDefaulting SimplRuleLhs = False
414 performDefaulting SimplInteractive = True
415 performDefaulting SimplCheck = True
418 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
420 instance Functor TcS where
421 fmap f m = TcS $ fmap f . unTcS m
423 instance Monad TcS where
424 return x = TcS (\_ -> return x)
425 fail err = TcS (\_ -> fail err)
426 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
428 -- Basic functionality
429 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
430 wrapTcS :: TcM a -> TcS a
431 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
432 -- and TcS is supposed to have limited functionality
433 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
435 wrapErrTcS :: TcM a -> TcS a
436 -- The thing wrapped should just fail
437 -- There's no static check; it's up to the user
438 -- Having a variant for each error message is too painful
441 wrapWarnTcS :: TcM a -> TcS a
442 -- The thing wrapped should just add a warning, or no-op
443 -- There's no static check; it's up to the user
444 wrapWarnTcS = wrapTcS
446 failTcS, panicTcS :: SDoc -> TcS a
447 failTcS = wrapTcS . TcM.failWith
448 panicTcS doc = pprPanic "TcCanonical" doc
450 traceTcS :: String -> SDoc -> TcS ()
451 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
453 traceTcS0 :: String -> SDoc -> TcS ()
454 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
456 runTcS :: SimplContext
457 -> Untouchables -- Untouchables
458 -> TcS a -- What to run
459 -> TcM (a, Bag EvBind)
460 runTcS context untouch tcs
461 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
462 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
463 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
464 , tcs_ty_binds = ty_binds_var
465 , tcs_context = context
466 , tcs_untch = untouch }
468 -- Run the computation
469 ; res <- unTcS tcs env
471 -- Perform the type unifications required
472 ; ty_binds <- TcM.readTcRef ty_binds_var
473 ; mapM_ do_unification (varEnvElts ty_binds)
476 ; ev_binds <- TcM.readTcRef evb_ref
477 ; return (res, evBindMapBinds ev_binds) }
479 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
482 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
483 nestImplicTcS ref untch (TcS thing_inside)
484 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
486 nest_env = TcSEnv { tcs_ev_binds = ref
487 , tcs_ty_binds = ty_binds
489 , tcs_context = ctxtUnderImplic ctxt }
491 thing_inside nest_env
493 ctxtUnderImplic :: SimplContext -> SimplContext
494 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
495 ctxtUnderImplic SimplRuleLhs = SimplCheck
496 ctxtUnderImplic ctxt = ctxt
498 tryTcS :: TcS a -> TcS a
499 -- Like runTcS, but from within the TcS monad
500 -- Ignore all the evidence generated, and do not affect caller's evidence!
502 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
503 ; ev_binds_var <- TcM.newTcEvBinds
504 ; let env1 = env { tcs_ev_binds = ev_binds_var
505 , tcs_ty_binds = ty_binds_var }
509 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
511 getDynFlags :: TcS DynFlags
512 getDynFlags = wrapTcS TcM.getDOpts
514 getTcSContext :: TcS SimplContext
515 getTcSContext = TcS (return . tcs_context)
517 getTcEvBinds :: TcS EvBindsVar
518 getTcEvBinds = TcS (return . tcs_ev_binds)
520 getUntouchables :: TcS Untouchables
521 getUntouchables = TcS (return . tcs_untch)
523 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
524 getTcSTyBinds = TcS (return . tcs_ty_binds)
526 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
527 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
530 getTcEvBindsBag :: TcS EvBindMap
532 = do { EvBindsVar ev_ref _ <- getTcEvBinds
533 ; wrapTcS $ TcM.readTcRef ev_ref }
535 setWantedCoBind :: CoVar -> Coercion -> TcS ()
536 setWantedCoBind cv co
537 = setEvBind cv (EvCoercion co)
538 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
540 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
541 setDerivedCoBind cv co
542 = setEvBind cv (EvCoercion co)
544 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
545 -- Add a type binding
546 setWantedTyBind tv ty
547 = do { ref <- getTcSTyBinds
549 do { ty_binds <- TcM.readTcRef ref
550 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
552 setIPBind :: EvVar -> EvTerm -> TcS ()
553 setIPBind = setEvBind
555 setDictBind :: EvVar -> EvTerm -> TcS ()
556 setDictBind = setEvBind
558 setEvBind :: EvVar -> EvTerm -> TcS ()
561 = do { tc_evbinds <- getTcEvBinds
562 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
564 newTcEvBindsTcS :: TcS EvBindsVar
565 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
567 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
568 warnTcS loc warn_if doc
569 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
570 | otherwise = return ()
572 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
574 = do { ctxt <- getTcSContext
575 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
576 ; return (ctxt, tys, flags) }
578 -- Just get some environments needed for instance looking up and matching
579 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
581 getInstEnvs :: TcS (InstEnv, InstEnv)
582 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
584 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
585 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
587 getTopEnv :: TcS HscEnv
588 getTopEnv = wrapTcS $ TcM.getTopEnv
590 getGblEnv :: TcS TcGblEnv
591 getGblEnv = wrapTcS $ TcM.getGblEnv
593 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
594 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
596 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
597 checkWellStagedDFun pred dfun_id loc
598 = wrapTcS $ TcM.setCtLoc loc $
599 do { use_stage <- TcM.getStage
600 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
602 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
603 bind_lvl = TcM.topIdLvl dfun_id
605 pprEq :: TcType -> TcType -> SDoc
606 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
608 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
609 isTouchableMetaTyVar tv
610 = case tcTyVarDetails tv of
611 MetaTv TcsTv _ -> return True -- See Note [Touchable meta type variables]
612 MetaTv {} -> do { untch <- getUntouchables
613 ; return (inTouchableRange untch tv) }
617 Note [Touchable meta type variables]
618 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
619 Meta type variables allocated *by the constraint solver itself* are always
621 instance C a b => D [a] where...
622 if we use this instance declaration we "make up" a fresh meta type
623 variable for 'b', which we must later guess. (Perhaps C has a
624 functional dependency.) But since we aren't in the constraint *generator*
625 we can't allocate a Unique in the touchable range for this implication
626 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
631 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
633 newFlattenSkolemTy :: TcType -> TcS TcType
634 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
636 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
637 newFlattenSkolemTyVar ty
638 = wrapTcS $ do { uniq <- TcM.newUnique
639 ; let name = mkSysTvName uniq (fsLit "f")
640 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
643 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
645 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
646 instDFunTypes mb_inst_tys
647 = mapM inst_tv mb_inst_tys
649 inst_tv :: Either TyVar TcType -> TcS Type
650 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
651 inst_tv (Right ty) = return ty
653 instDFunConstraints :: TcThetaType -> TcS [EvVar]
654 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
656 newFlexiTcS :: TyVar -> TcS TcTyVar
657 -- Make a TcsTv meta tyvar; it is always touchable,
658 -- but we are supposed to guess its instantiation
659 -- See Note [Touchable meta type variables]
660 newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
662 -- Superclasses and recursive dictionaries
663 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
665 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
666 newGivOrDerEvVar pty evtrm
667 = do { ev <- wrapTcS $ TcM.newEvVar pty
671 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
672 -- Note we create immutable variables for given or derived, since we
673 -- must bind them to TcEvBinds (because their evidence may involve
674 -- superclasses). However we should be able to override existing
675 -- 'derived' evidence, even in TcEvBinds
676 newGivOrDerCoVar ty1 ty2 co
677 = do { cv <- newCoVar ty1 ty2
678 ; setEvBind cv (EvCoercion co)
681 newWantedCoVar :: TcType -> TcType -> TcS EvVar
682 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
684 newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
685 newKindConstraint ty kind = wrapTcS $ TcM.newKindConstraint ty kind
687 newCoVar :: TcType -> TcType -> TcS EvVar
688 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
690 newIPVar :: IPName Name -> TcType -> TcS EvVar
691 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
693 newDictVar :: Class -> [TcType] -> TcS EvVar
694 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
699 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
700 -- In a call (isGoodRecEv ev wv), we are considering solving wv
701 -- using some term that involves ev, such as:
702 -- by setting wv = ev
703 -- or wv = EvCast x |> ev
705 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
706 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
707 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
709 -- Guarded means: more instance calls than superclass selections. We
710 -- compute this by chasing the evidence, adding +1 for every instance
711 -- call (constructor) and -1 for every superclass selection (destructor).
713 -- See Note [Superclasses and recursive dictionaries] in TcInteract
714 isGoodRecEv ev_var (WantedEvVar wv _)
715 = do { tc_evbinds <- getTcEvBindsBag
716 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
717 ; return $ case mb of
719 Just min_guardedness -> min_guardedness > 0
722 where chase_ev_var :: EvBindMap -- Evidence binds
723 -> EvVar -- Target variable whose gravity we want to return
724 -> Int -- Current gravity
725 -> [EvVar] -- Visited nodes
726 -> EvVar -- Current node
728 chase_ev_var assocs trg curr_grav visited orig
729 | trg == orig = return $ Just curr_grav
730 | orig `elem` visited = return $ Nothing
731 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
732 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
734 {- No longer needed: evidence is in the EvBinds
735 | isTcTyVar orig && isMetaTyVar orig
736 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
737 ; case meta_details of
738 Flexi -> return Nothing
739 Indirect tyco -> chase_ev assocs trg curr_grav
740 (orig:visited) (EvCoercion tyco)
743 | otherwise = return Nothing
745 chase_ev assocs trg curr_grav visited (EvId v)
746 = chase_ev_var assocs trg curr_grav visited v
747 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
748 = chase_ev_var assocs trg (curr_grav-1) visited d_id
749 chase_ev assocs trg curr_grav visited (EvCast v co)
750 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
751 ; m2 <- chase_co assocs trg curr_grav visited co
752 ; return (comb_chase_res Nothing [m1,m2]) }
754 chase_ev assocs trg curr_grav visited (EvCoercion co)
755 = chase_co assocs trg curr_grav visited co
756 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
757 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
758 ; return (comb_chase_res Nothing chase_results) }
760 chase_co assocs trg curr_grav visited co
761 = -- Look for all the coercion variables in the coercion
762 -- chase them, and combine the results. This is OK since the
763 -- coercion will not contain any superclass terms -- anything
764 -- that involves dictionaries will be bound in assocs.
765 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
767 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
768 ; return (comb_chase_res Nothing chase_results) }
770 comb_chase_res f [] = f
771 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
772 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
773 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
776 -- Matching and looking up classes and family instances
777 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
779 data MatchInstResult mi
780 = MatchInstNo -- No matching instance
781 | MatchInstSingle mi -- Single matching instance
782 | MatchInstMany -- Multiple matching instances
785 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
786 -- Look up a class constraint in the instance environment
788 = do { let pred = mkClassPred clas tys
789 ; instEnvs <- getInstEnvs
790 ; case lookupInstEnv instEnvs clas tys of {
791 ([], unifs) -- Nothing matches
792 -> do { traceTcS "matchClass not matching"
793 (vcat [ text "dict" <+> ppr pred,
794 text "unifs" <+> ppr unifs ])
797 ([(ispec, inst_tys)], []) -- A single match
798 -> do { let dfun_id = is_dfun ispec
799 ; traceTcS "matchClass success"
800 (vcat [text "dict" <+> ppr pred,
801 text "witness" <+> ppr dfun_id
802 <+> ppr (idType dfun_id) ])
803 -- Record that this dfun is needed
804 ; record_dfun_usage dfun_id
805 ; return $ MatchInstSingle (dfun_id, inst_tys)
807 (matches, unifs) -- More than one matches
808 -> do { traceTcS "matchClass multiple matches, deferring choice"
809 (vcat [text "dict" <+> ppr pred,
810 text "matches" <+> ppr matches,
811 text "unifs" <+> ppr unifs])
812 ; return MatchInstMany
816 where record_dfun_usage :: Id -> TcS ()
817 record_dfun_usage dfun_id
818 = do { hsc_env <- getTopEnv
819 ; let dfun_name = idName dfun_id
820 dfun_mod = ASSERT( isExternalName dfun_name )
822 ; if isInternalName dfun_name || -- Internal name => defined in this module
823 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
824 then return () -- internal, or in another package
825 else do updInstUses dfun_id
828 updInstUses :: Id -> TcS ()
830 = do { tcg_env <- getGblEnv
831 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
832 (`addOneToNameSet` idName dfun_id)
837 -> TcS (MatchInstResult (TyCon, [Type]))
839 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
841 Nothing -> return MatchInstNo
842 Just res -> return $ MatchInstSingle res
843 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
844 -- multiple matches. Check.
848 -- Functional dependencies, instantiation of equations
849 -------------------------------------------------------
851 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
853 mkWantedFunDepEqns _ [] = return []
854 mkWantedFunDepEqns loc eqns
855 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
856 ; wevvars <- mapM to_work_item eqns
857 ; return $ concat wevvars }
859 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
860 to_work_item ((qtvs, pairs), _, _)
861 = do { let tvs = varSetElems qtvs
862 ; tvs' <- mapM newFlexiTcS tvs
863 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
864 ; mapM (do_one subst) pairs }
866 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
867 sty2 = substTy subst ty2
868 ; ev <- newWantedCoVar sty1 sty2
869 ; return (WantedEvVar ev loc) }
871 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
872 pprEquationDoc (eqn, (p1, _), (p2, _))
873 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]