2 -- Type definitions for the constraint solver
5 -- Canonical constraints
6 CanonicalCts, emptyCCan, andCCan, andCCans,
7 singleCCan, extendCCans, isEmptyCCan, isTyEqCCan,
8 CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
9 mkWantedConstraints, deCanonicaliseWanted,
10 makeGivens, makeSolvedByInst,
12 CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst,
15 combineCtLoc, mkGivenFlavor,
17 TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
18 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
19 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
21 -- Creation of evidence variables
23 newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
24 newIPVar, newDictVar, newKindConstraint,
26 -- Setting evidence variables
27 setWantedCoBind, setDerivedCoBind,
28 setIPBind, setDictBind, setEvBind,
34 getInstEnvs, getFamInstEnvs, -- Getting the environments
35 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
36 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
39 newFlattenSkolemTy, -- Flatten skolems
42 instDFunTypes, -- Instantiation
48 isTouchableMetaTyVar_InRange,
50 getDefaultInfo, getDynFlags,
52 matchClass, matchFam, MatchInstResult (..),
55 pprEq, -- Smaller utils, re-exported from TcM
56 -- TODO (DV): these are only really used in the
57 -- instance matcher in TcSimplify. I am wondering
58 -- if the whole instance matcher simply belongs
62 mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps
66 #include "HsVersions.h"
76 import NameSet ( addOneToNameSet )
78 import qualified TcRnMonad as TcM
79 import qualified TcMType as TcM
80 import qualified TcEnv as TcM
81 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
100 import HsBinds -- for TcEvBinds stuff
110 %************************************************************************
112 %* Canonical constraints *
114 %* These are the constraints the low-level simplifier works with *
116 %************************************************************************
119 -- Types without any type functions inside. However, note that xi
120 -- types CAN contain unexpanded type synonyms; however, the
121 -- (transitive) expansions of those type synonyms will not contain any
123 type Xi = Type -- In many comments, "xi" ranges over Xi
125 type CanonicalCts = Bag CanonicalCt
128 -- Atomic canonical constraints
129 = CDictCan { -- e.g. Num xi
131 cc_flavor :: CtFlavor,
136 | CIPCan { -- ?x::tau
137 -- See note [Canonical implicit parameter constraints].
139 cc_flavor :: CtFlavor,
140 cc_ip_nm :: IPName Name,
141 cc_ip_ty :: TcTauType
144 | CTyEqCan { -- tv ~ xi (recall xi means function free)
146 -- * tv not in tvs(xi) (occurs check)
147 -- * If constraint is given then typeKind xi == typeKind tv
148 -- See Note [Spontaneous solving and kind compatibility]
150 cc_flavor :: CtFlavor,
155 | CFunEqCan { -- F xis ~ xi
156 -- Invariant: * isSynFamilyTyCon cc_fun
157 -- * cc_rhs is not a touchable unification variable
158 -- See Note [No touchables as FunEq RHS]
159 -- * If constraint is given then
160 -- typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
162 cc_flavor :: CtFlavor,
163 cc_fun :: TyCon, -- A type function
164 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
165 cc_rhs :: Xi -- *never* over-saturated (because if so
166 -- we should have decomposed)
170 makeGivens :: CanonicalCts -> CanonicalCts
171 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
172 -- The UnkSkol doesn't matter because these givens are
173 -- not contradictory (else we'd have rejected them already)
175 makeSolvedByInst :: CanonicalCt -> CanonicalCt
176 -- Record that a constraint is now solved
178 -- Given, Derived -> no-op
180 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
183 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
184 mkWantedConstraints flats implics
185 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
187 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
188 deCanonicaliseWanted ct
189 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
190 let Wanted loc = cc_flavor ct
191 in WantedEvVar (cc_id ct) loc
193 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
194 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
195 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
196 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
197 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
199 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
200 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
201 tyVarsOfCDict _ct = emptyVarSet
203 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
204 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
206 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
207 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
209 instance Outputable CanonicalCt where
210 ppr (CDictCan d fl cls tys)
211 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
212 ppr (CIPCan ip fl ip_nm ty)
213 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
214 ppr (CTyEqCan co fl tv ty)
215 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
216 ppr (CFunEqCan co fl tc tys ty)
217 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
221 Note [No touchables as FunEq RHS]
222 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
223 Notice that (F xis ~ beta), where beta is an touchable unification
224 variable, is not canonical. Why?
225 * If (F xis ~ beta) was the only wanted constraint, we'd
226 definitely want to spontaneously-unify it
228 * But suppose we had an earlier wanted (beta ~ Int), and
229 have already spontaneously unified it. Then we have an
230 identity given (id : beta ~ Int) in the inert set.
232 * But (F xis ~ beta) does not react with that given (because we
233 don't subsitute on the RHS of a function equality). So there's a
234 serious danger that we'd spontaneously unify it a second time.
240 Note [Canonical implicit parameter constraints]
241 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
242 The type in a canonical implicit parameter constraint doesn't need to
243 be a xi (type-function-free type) since we can defer the flattening
244 until checking this type for equality with another type. If we
245 encounter two IP constraints with the same name, they MUST have the
246 same type, and at that point we can generate a flattened equality
247 constraint between the types. (On the other hand, the types in two
248 class constraints for the same class MAY be equal, so they need to be
249 flattened in the first place to facilitate comparing them.)
252 singleCCan :: CanonicalCt -> CanonicalCts
255 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
258 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
259 extendCCans = snocBag
261 andCCans :: [CanonicalCts] -> CanonicalCts
262 andCCans = unionManyBags
264 emptyCCan :: CanonicalCts
267 isEmptyCCan :: CanonicalCts -> Bool
268 isEmptyCCan = isEmptyBag
270 isTyEqCCan :: CanonicalCt -> Bool
271 isTyEqCCan (CTyEqCan {}) = True
272 isTyEqCCan (CFunEqCan {}) = False
277 %************************************************************************
280 The "flavor" of a canonical constraint
282 %************************************************************************
286 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
287 | Derived WantedLoc DerivedOrig
288 -- We have evidence for this constraint in TcEvBinds;
289 -- *however* this evidence can contain wanteds, so
290 -- it's valid only provisionally to the solution of
292 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
294 data DerivedOrig = DerSC | DerInst
295 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
296 -- solved wanteds from instances.
298 instance Outputable CtFlavor where
299 ppr (Given _) = ptext (sLit "[Given]")
300 ppr (Wanted _) = ptext (sLit "[Wanted]")
301 ppr (Derived {}) = ptext (sLit "[Derived]")
303 isWanted :: CtFlavor -> Bool
304 isWanted (Wanted {}) = True
307 isGiven :: CtFlavor -> Bool
308 isGiven (Given {}) = True
311 isDerived :: CtFlavor -> Bool
312 isDerived (Derived {}) = True
315 isDerivedSC :: CtFlavor -> Bool
316 isDerivedSC (Derived _ DerSC) = True
317 isDerivedSC _ = False
319 isDerivedByInst :: CtFlavor -> Bool
320 isDerivedByInst (Derived _ DerInst) = True
321 isDerivedByInst _ = False
323 canSolve :: CtFlavor -> CtFlavor -> Bool
324 -- canSolve ctid1 ctid2
325 -- The constraint ctid1 can be used to solve ctid2
326 -- "to solve" means a reaction where the active parts of the two constraints match.
327 -- active(F xis ~ xi) = F xis
328 -- active(tv ~ xi) = tv
329 -- active(D xis) = D xis
330 -- active(IP nm ty) = nm
331 -----------------------------------------
332 canSolve (Given {}) _ = True
333 canSolve (Derived {}) (Wanted {}) = True
334 canSolve (Derived {}) (Derived {}) = True
335 canSolve (Wanted {}) (Wanted {}) = True
338 canRewrite :: CtFlavor -> CtFlavor -> Bool
339 -- canRewrite ctid1 ctid2
340 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
341 canRewrite = canSolve
343 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
344 -- Precondition: At least one of them should be wanted
345 combineCtLoc (Wanted loc) _ = loc
346 combineCtLoc _ (Wanted loc) = loc
347 combineCtLoc (Derived loc _) _ = loc
348 combineCtLoc _ (Derived loc _) = loc
349 combineCtLoc _ _ = panic "combineCtLoc: both given"
351 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
352 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
353 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
354 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
358 %************************************************************************
360 %* The TcS solver monad *
362 %************************************************************************
366 The TcS monad is a weak form of the main Tc monad
370 * allocate new variables
371 * fill in evidence variables
373 Filling in a dictionary evidence variable means to create a binding
374 for it, so TcS carries a mutable location where the binding can be
375 added. This is initialised from the innermost implication constraint.
380 tcs_ev_binds :: EvBindsVar,
383 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
384 -- Global type bindings
386 tcs_context :: SimplContext,
388 tcs_untch :: Untouchables
392 = SimplInfer -- Inferring type of a let-bound thing
393 | SimplRuleLhs -- Inferring type of a RULE lhs
394 | SimplInteractive -- Inferring type at GHCi prompt
395 | SimplCheck -- Checking a type signature or RULE rhs
397 instance Outputable SimplContext where
398 ppr SimplInfer = ptext (sLit "SimplInfer")
399 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
400 ppr SimplInteractive = ptext (sLit "SimplInteractive")
401 ppr SimplCheck = ptext (sLit "SimplCheck")
403 isInteractive :: SimplContext -> Bool
404 isInteractive SimplInteractive = True
405 isInteractive _ = False
407 simplEqsOnly :: SimplContext -> Bool
408 -- Simplify equalities only, not dictionaries
409 -- This is used for the LHS of rules; ee
410 -- Note [Simplifying RULE lhs constraints] in TcSimplify
411 simplEqsOnly SimplRuleLhs = True
412 simplEqsOnly _ = False
414 performDefaulting :: SimplContext -> Bool
415 performDefaulting SimplInfer = False
416 performDefaulting SimplRuleLhs = False
417 performDefaulting SimplInteractive = True
418 performDefaulting SimplCheck = True
421 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
423 instance Functor TcS where
424 fmap f m = TcS $ fmap f . unTcS m
426 instance Monad TcS where
427 return x = TcS (\_ -> return x)
428 fail err = TcS (\_ -> fail err)
429 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
431 -- Basic functionality
432 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
433 wrapTcS :: TcM a -> TcS a
434 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
435 -- and TcS is supposed to have limited functionality
436 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
438 wrapErrTcS :: TcM a -> TcS a
439 -- The thing wrapped should just fail
440 -- There's no static check; it's up to the user
441 -- Having a variant for each error message is too painful
444 wrapWarnTcS :: TcM a -> TcS a
445 -- The thing wrapped should just add a warning, or no-op
446 -- There's no static check; it's up to the user
447 wrapWarnTcS = wrapTcS
449 failTcS, panicTcS :: SDoc -> TcS a
450 failTcS = wrapTcS . TcM.failWith
451 panicTcS doc = pprPanic "TcCanonical" doc
453 traceTcS :: String -> SDoc -> TcS ()
454 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
456 traceTcS0 :: String -> SDoc -> TcS ()
457 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
459 runTcS :: SimplContext
460 -> Untouchables -- Untouchables
461 -> TcS a -- What to run
462 -> TcM (a, Bag EvBind)
463 runTcS context untouch tcs
464 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
465 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
466 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
467 , tcs_ty_binds = ty_binds_var
468 , tcs_context = context
469 , tcs_untch = untouch }
471 -- Run the computation
472 ; res <- unTcS tcs env
474 -- Perform the type unifications required
475 ; ty_binds <- TcM.readTcRef ty_binds_var
476 ; mapM_ do_unification (varEnvElts ty_binds)
479 ; ev_binds <- TcM.readTcRef evb_ref
480 ; return (res, evBindMapBinds ev_binds) }
482 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
485 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
486 nestImplicTcS ref untch (TcS thing_inside)
487 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
489 nest_env = TcSEnv { tcs_ev_binds = ref
490 , tcs_ty_binds = ty_binds
492 , tcs_context = ctxtUnderImplic ctxt }
494 thing_inside nest_env
496 recoverTcS :: TcS a -> TcS a -> TcS a
497 recoverTcS (TcS recovery_code) (TcS thing_inside)
499 TcM.recoverM (recovery_code env) (thing_inside env)
501 ctxtUnderImplic :: SimplContext -> SimplContext
502 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
503 ctxtUnderImplic SimplRuleLhs = SimplCheck
504 ctxtUnderImplic ctxt = ctxt
506 tryTcS :: TcS a -> TcS a
507 -- Like runTcS, but from within the TcS monad
508 -- Ignore all the evidence generated, and do not affect caller's evidence!
510 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
511 ; ev_binds_var <- TcM.newTcEvBinds
512 ; let env1 = env { tcs_ev_binds = ev_binds_var
513 , tcs_ty_binds = ty_binds_var }
517 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
519 getDynFlags :: TcS DynFlags
520 getDynFlags = wrapTcS TcM.getDOpts
522 getTcSContext :: TcS SimplContext
523 getTcSContext = TcS (return . tcs_context)
525 getTcEvBinds :: TcS EvBindsVar
526 getTcEvBinds = TcS (return . tcs_ev_binds)
528 getUntouchables :: TcS Untouchables
529 getUntouchables = TcS (return . tcs_untch)
531 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
532 getTcSTyBinds = TcS (return . tcs_ty_binds)
534 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
535 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
538 getTcEvBindsBag :: TcS EvBindMap
540 = do { EvBindsVar ev_ref _ <- getTcEvBinds
541 ; wrapTcS $ TcM.readTcRef ev_ref }
543 setWantedCoBind :: CoVar -> Coercion -> TcS ()
544 setWantedCoBind cv co
545 = setEvBind cv (EvCoercion co)
546 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
548 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
549 setDerivedCoBind cv co
550 = setEvBind cv (EvCoercion co)
552 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
553 -- Add a type binding
554 setWantedTyBind tv ty
555 = do { ref <- getTcSTyBinds
557 do { ty_binds <- TcM.readTcRef ref
558 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
560 setIPBind :: EvVar -> EvTerm -> TcS ()
561 setIPBind = setEvBind
563 setDictBind :: EvVar -> EvTerm -> TcS ()
564 setDictBind = setEvBind
566 setEvBind :: EvVar -> EvTerm -> TcS ()
569 = do { tc_evbinds <- getTcEvBinds
570 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
572 newTcEvBindsTcS :: TcS EvBindsVar
573 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
575 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
576 warnTcS loc warn_if doc
577 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
578 | otherwise = return ()
580 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
582 = do { ctxt <- getTcSContext
583 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
584 ; return (ctxt, tys, flags) }
586 -- Just get some environments needed for instance looking up and matching
587 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
589 getInstEnvs :: TcS (InstEnv, InstEnv)
590 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
592 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
593 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
595 getTopEnv :: TcS HscEnv
596 getTopEnv = wrapTcS $ TcM.getTopEnv
598 getGblEnv :: TcS TcGblEnv
599 getGblEnv = wrapTcS $ TcM.getGblEnv
601 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
602 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
605 checkWellStagedDFun pred dfun_id loc
606 = wrapTcS $ TcM.setCtLoc loc $
607 do { use_stage <- TcM.getStage
608 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
610 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
611 bind_lvl = TcM.topIdLvl dfun_id
613 pprEq :: TcType -> TcType -> SDoc
614 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
616 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
617 isTouchableMetaTyVar tv
618 = do { untch <- getUntouchables
619 ; return $ isTouchableMetaTyVar_InRange untch tv }
621 isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool
622 isTouchableMetaTyVar_InRange untch tv
623 = case tcTyVarDetails tv of
624 MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables]
625 MetaTv {} -> inTouchableRange untch tv
632 Note [Touchable meta type variables]
633 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
634 Meta type variables allocated *by the constraint solver itself* are always
636 instance C a b => D [a] where...
637 if we use this instance declaration we "make up" a fresh meta type
638 variable for 'b', which we must later guess. (Perhaps C has a
639 functional dependency.) But since we aren't in the constraint *generator*
640 we can't allocate a Unique in the touchable range for this implication
641 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
646 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
648 newFlattenSkolemTy :: TcType -> TcS TcType
649 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
651 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
652 newFlattenSkolemTyVar ty
653 = wrapTcS $ do { uniq <- TcM.newUnique
654 ; let name = mkSysTvName uniq (fsLit "f")
655 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
658 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
660 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
661 instDFunTypes mb_inst_tys
662 = mapM inst_tv mb_inst_tys
664 inst_tv :: Either TyVar TcType -> TcS Type
665 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
666 inst_tv (Right ty) = return ty
668 instDFunConstraints :: TcThetaType -> TcS [EvVar]
669 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
672 -- newFlexiTcS :: TyVar -> TcS TcTyVar
673 -- -- Make a TcsTv meta tyvar; it is always touchable,
674 -- -- but we are supposed to guess its instantiation
675 -- -- See Note [Touchable meta type variables]
676 -- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
678 newFlexiTcS :: TyVar -> TcS TcTyVar
679 -- Like TcM.instMetaTyVar but the variable that is created is always
680 -- touchable; we are supposed to guess its instantiation.
681 -- See Note [Touchable meta type variables]
682 newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
684 newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)
685 -- Create new wanted CoVar that constrains the type to have the specified kind.
686 newKindConstraint tv knd
687 = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd
688 ; let ty_k = mkTyVarTy tv_k
689 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
690 ; return (co_var, ty_k) }
692 newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
693 newFlexiTcSHelper tvname tvkind
695 do { uniq <- TcM.newUnique
696 ; ref <- TcM.newMutVar Flexi
697 ; let name = setNameUnique tvname uniq
699 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
701 -- Superclasses and recursive dictionaries
702 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
704 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
705 newGivOrDerEvVar pty evtrm
706 = do { ev <- wrapTcS $ TcM.newEvVar pty
710 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
711 -- Note we create immutable variables for given or derived, since we
712 -- must bind them to TcEvBinds (because their evidence may involve
713 -- superclasses). However we should be able to override existing
714 -- 'derived' evidence, even in TcEvBinds
715 newGivOrDerCoVar ty1 ty2 co
716 = do { cv <- newCoVar ty1 ty2
717 ; setEvBind cv (EvCoercion co)
720 newWantedCoVar :: TcType -> TcType -> TcS EvVar
721 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
724 newCoVar :: TcType -> TcType -> TcS EvVar
725 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
727 newIPVar :: IPName Name -> TcType -> TcS EvVar
728 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
730 newDictVar :: Class -> [TcType] -> TcS EvVar
731 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
736 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
737 -- In a call (isGoodRecEv ev wv), we are considering solving wv
738 -- using some term that involves ev, such as:
739 -- by setting wv = ev
740 -- or wv = EvCast x |> ev
742 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
743 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
744 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
746 -- Guarded means: more instance calls than superclass selections. We
747 -- compute this by chasing the evidence, adding +1 for every instance
748 -- call (constructor) and -1 for every superclass selection (destructor).
750 -- See Note [Superclasses and recursive dictionaries] in TcInteract
751 isGoodRecEv ev_var (WantedEvVar wv _)
752 = do { tc_evbinds <- getTcEvBindsBag
753 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
754 ; return $ case mb of
756 Just min_guardedness -> min_guardedness > 0
759 where chase_ev_var :: EvBindMap -- Evidence binds
760 -> EvVar -- Target variable whose gravity we want to return
761 -> Int -- Current gravity
762 -> [EvVar] -- Visited nodes
763 -> EvVar -- Current node
765 chase_ev_var assocs trg curr_grav visited orig
766 | trg == orig = return $ Just curr_grav
767 | orig `elem` visited = return $ Nothing
768 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
769 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
771 {- No longer needed: evidence is in the EvBinds
772 | isTcTyVar orig && isMetaTyVar orig
773 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
774 ; case meta_details of
775 Flexi -> return Nothing
776 Indirect tyco -> chase_ev assocs trg curr_grav
777 (orig:visited) (EvCoercion tyco)
780 | otherwise = return Nothing
782 chase_ev assocs trg curr_grav visited (EvId v)
783 = chase_ev_var assocs trg curr_grav visited v
784 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
785 = chase_ev_var assocs trg (curr_grav-1) visited d_id
786 chase_ev assocs trg curr_grav visited (EvCast v co)
787 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
788 ; m2 <- chase_co assocs trg curr_grav visited co
789 ; return (comb_chase_res Nothing [m1,m2]) }
791 chase_ev assocs trg curr_grav visited (EvCoercion co)
792 = chase_co assocs trg curr_grav visited co
793 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
794 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
795 ; return (comb_chase_res Nothing chase_results) }
797 chase_co assocs trg curr_grav visited co
798 = -- Look for all the coercion variables in the coercion
799 -- chase them, and combine the results. This is OK since the
800 -- coercion will not contain any superclass terms -- anything
801 -- that involves dictionaries will be bound in assocs.
802 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
804 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
805 ; return (comb_chase_res Nothing chase_results) }
807 comb_chase_res f [] = f
808 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
809 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
810 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
813 -- Matching and looking up classes and family instances
814 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
816 data MatchInstResult mi
817 = MatchInstNo -- No matching instance
818 | MatchInstSingle mi -- Single matching instance
819 | MatchInstMany -- Multiple matching instances
822 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
823 -- Look up a class constraint in the instance environment
825 = do { let pred = mkClassPred clas tys
826 ; instEnvs <- getInstEnvs
827 ; case lookupInstEnv instEnvs clas tys of {
828 ([], unifs) -- Nothing matches
829 -> do { traceTcS "matchClass not matching"
830 (vcat [ text "dict" <+> ppr pred,
831 text "unifs" <+> ppr unifs ])
834 ([(ispec, inst_tys)], []) -- A single match
835 -> do { let dfun_id = is_dfun ispec
836 ; traceTcS "matchClass success"
837 (vcat [text "dict" <+> ppr pred,
838 text "witness" <+> ppr dfun_id
839 <+> ppr (idType dfun_id) ])
840 -- Record that this dfun is needed
841 ; record_dfun_usage dfun_id
842 ; return $ MatchInstSingle (dfun_id, inst_tys)
844 (matches, unifs) -- More than one matches
845 -> do { traceTcS "matchClass multiple matches, deferring choice"
846 (vcat [text "dict" <+> ppr pred,
847 text "matches" <+> ppr matches,
848 text "unifs" <+> ppr unifs])
849 ; return MatchInstMany
853 where record_dfun_usage :: Id -> TcS ()
854 record_dfun_usage dfun_id
855 = do { hsc_env <- getTopEnv
856 ; let dfun_name = idName dfun_id
857 dfun_mod = ASSERT( isExternalName dfun_name )
859 ; if isInternalName dfun_name || -- Internal name => defined in this module
860 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
861 then return () -- internal, or in another package
862 else do updInstUses dfun_id
865 updInstUses :: Id -> TcS ()
867 = do { tcg_env <- getGblEnv
868 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
869 (`addOneToNameSet` idName dfun_id)
874 -> TcS (MatchInstResult (TyCon, [Type]))
876 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
878 Nothing -> return MatchInstNo
879 Just res -> return $ MatchInstSingle res
880 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
881 -- multiple matches. Check.
885 -- Functional dependencies, instantiation of equations
886 -------------------------------------------------------
888 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
890 mkWantedFunDepEqns _ [] = return []
891 mkWantedFunDepEqns loc eqns
892 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
893 ; wevvars <- mapM to_work_item eqns
894 ; return $ concat wevvars }
896 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
897 to_work_item ((qtvs, pairs), _, _)
898 = do { let tvs = varSetElems qtvs
899 ; tvs' <- mapM newFlexiTcS tvs
900 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
901 ; mapM (do_one subst) pairs }
903 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
904 sty2 = substTy subst ty2
905 ; ev <- newWantedCoVar sty1 sty2
906 ; return (WantedEvVar ev loc) }
908 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
909 pprEquationDoc (eqn, (p1, _), (p2, _))
910 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]