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, 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.
238 Note [Canonical implicit parameter constraints]
239 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
240 The type in a canonical implicit parameter constraint doesn't need to
241 be a xi (type-function-free type) since we can defer the flattening
242 until checking this type for equality with another type. If we
243 encounter two IP constraints with the same name, they MUST have the
244 same type, and at that point we can generate a flattened equality
245 constraint between the types. (On the other hand, the types in two
246 class constraints for the same class MAY be equal, so they need to be
247 flattened in the first place to facilitate comparing them.)
250 singleCCan :: CanonicalCt -> CanonicalCts
253 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
256 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
257 extendCCans = snocBag
259 andCCans :: [CanonicalCts] -> CanonicalCts
260 andCCans = unionManyBags
262 emptyCCan :: CanonicalCts
265 isEmptyCCan :: CanonicalCts -> Bool
266 isEmptyCCan = isEmptyBag
268 isTyEqCCan :: CanonicalCt -> Bool
269 isTyEqCCan (CTyEqCan {}) = True
270 isTyEqCCan (CFunEqCan {}) = False
275 %************************************************************************
278 The "flavor" of a canonical constraint
280 %************************************************************************
284 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
285 | Derived WantedLoc DerivedOrig
286 -- We have evidence for this constraint in TcEvBinds;
287 -- *however* this evidence can contain wanteds, so
288 -- it's valid only provisionally to the solution of
290 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
292 data DerivedOrig = DerSC | DerInst
293 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
294 -- solved wanteds from instances.
296 instance Outputable CtFlavor where
297 ppr (Given _) = ptext (sLit "[Given]")
298 ppr (Wanted _) = ptext (sLit "[Wanted]")
299 ppr (Derived {}) = ptext (sLit "[Derived]")
301 isWanted :: CtFlavor -> Bool
302 isWanted (Wanted {}) = True
305 isGiven :: CtFlavor -> Bool
306 isGiven (Given {}) = True
309 isDerived :: CtFlavor -> Bool
310 isDerived (Derived {}) = True
313 isDerivedSC :: CtFlavor -> Bool
314 isDerivedSC (Derived _ DerSC) = True
315 isDerivedSC _ = False
317 isDerivedByInst :: CtFlavor -> Bool
318 isDerivedByInst (Derived _ DerInst) = True
319 isDerivedByInst _ = False
321 canSolve :: CtFlavor -> CtFlavor -> Bool
322 -- canSolve ctid1 ctid2
323 -- The constraint ctid1 can be used to solve ctid2
324 -- "to solve" means a reaction where the active parts of the two constraints match.
325 -- active(F xis ~ xi) = F xis
326 -- active(tv ~ xi) = tv
327 -- active(D xis) = D xis
328 -- active(IP nm ty) = nm
329 -----------------------------------------
330 canSolve (Given {}) _ = True
331 canSolve (Derived {}) (Wanted {}) = True
332 canSolve (Derived {}) (Derived {}) = True
333 canSolve (Wanted {}) (Wanted {}) = True
336 canRewrite :: CtFlavor -> CtFlavor -> Bool
337 -- canRewrite ctid1 ctid2
338 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
339 canRewrite = canSolve
341 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
342 -- Precondition: At least one of them should be wanted
343 combineCtLoc (Wanted loc) _ = loc
344 combineCtLoc _ (Wanted loc) = loc
345 combineCtLoc (Derived loc _) _ = loc
346 combineCtLoc _ (Derived loc _) = loc
347 combineCtLoc _ _ = panic "combineCtLoc: both given"
349 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
350 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
351 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
352 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
356 %************************************************************************
358 %* The TcS solver monad *
360 %************************************************************************
364 The TcS monad is a weak form of the main Tc monad
368 * allocate new variables
369 * fill in evidence variables
371 Filling in a dictionary evidence variable means to create a binding
372 for it, so TcS carries a mutable location where the binding can be
373 added. This is initialised from the innermost implication constraint.
378 tcs_ev_binds :: EvBindsVar,
381 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
382 -- Global type bindings
384 tcs_context :: SimplContext,
386 tcs_untch :: Untouchables
390 = SimplInfer -- Inferring type of a let-bound thing
391 | SimplRuleLhs -- Inferring type of a RULE lhs
392 | SimplInteractive -- Inferring type at GHCi prompt
393 | SimplCheck -- Checking a type signature or RULE rhs
395 instance Outputable SimplContext where
396 ppr SimplInfer = ptext (sLit "SimplInfer")
397 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
398 ppr SimplInteractive = ptext (sLit "SimplInteractive")
399 ppr SimplCheck = ptext (sLit "SimplCheck")
401 isInteractive :: SimplContext -> Bool
402 isInteractive SimplInteractive = True
403 isInteractive _ = False
405 simplEqsOnly :: SimplContext -> Bool
406 -- Simplify equalities only, not dictionaries
407 -- This is used for the LHS of rules; ee
408 -- Note [Simplifying RULE lhs constraints] in TcSimplify
409 simplEqsOnly SimplRuleLhs = True
410 simplEqsOnly _ = False
412 performDefaulting :: SimplContext -> Bool
413 performDefaulting SimplInfer = False
414 performDefaulting SimplRuleLhs = False
415 performDefaulting SimplInteractive = True
416 performDefaulting SimplCheck = True
419 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
421 instance Functor TcS where
422 fmap f m = TcS $ fmap f . unTcS m
424 instance Monad TcS where
425 return x = TcS (\_ -> return x)
426 fail err = TcS (\_ -> fail err)
427 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
429 -- Basic functionality
430 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
431 wrapTcS :: TcM a -> TcS a
432 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
433 -- and TcS is supposed to have limited functionality
434 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
436 wrapErrTcS :: TcM a -> TcS a
437 -- The thing wrapped should just fail
438 -- There's no static check; it's up to the user
439 -- Having a variant for each error message is too painful
442 wrapWarnTcS :: TcM a -> TcS a
443 -- The thing wrapped should just add a warning, or no-op
444 -- There's no static check; it's up to the user
445 wrapWarnTcS = wrapTcS
447 failTcS, panicTcS :: SDoc -> TcS a
448 failTcS = wrapTcS . TcM.failWith
449 panicTcS doc = pprPanic "TcCanonical" doc
451 traceTcS :: String -> SDoc -> TcS ()
452 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
454 traceTcS0 :: String -> SDoc -> TcS ()
455 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
457 runTcS :: SimplContext
458 -> Untouchables -- Untouchables
459 -> TcS a -- What to run
460 -> TcM (a, Bag EvBind)
461 runTcS context untouch tcs
462 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
463 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
464 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
465 , tcs_ty_binds = ty_binds_var
466 , tcs_context = context
467 , tcs_untch = untouch }
469 -- Run the computation
470 ; res <- unTcS tcs env
472 -- Perform the type unifications required
473 ; ty_binds <- TcM.readTcRef ty_binds_var
474 ; mapM_ do_unification (varEnvElts ty_binds)
477 ; ev_binds <- TcM.readTcRef evb_ref
478 ; return (res, evBindMapBinds ev_binds) }
480 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
483 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
484 nestImplicTcS ref untch (TcS thing_inside)
485 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
487 nest_env = TcSEnv { tcs_ev_binds = ref
488 , tcs_ty_binds = ty_binds
490 , tcs_context = ctxtUnderImplic ctxt }
492 thing_inside nest_env
494 ctxtUnderImplic :: SimplContext -> SimplContext
495 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
496 ctxtUnderImplic SimplRuleLhs = SimplCheck
497 ctxtUnderImplic ctxt = ctxt
499 tryTcS :: TcS a -> TcS a
500 -- Like runTcS, but from within the TcS monad
501 -- Ignore all the evidence generated, and do not affect caller's evidence!
503 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
504 ; ev_binds_var <- TcM.newTcEvBinds
505 ; let env1 = env { tcs_ev_binds = ev_binds_var
506 , tcs_ty_binds = ty_binds_var }
510 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
512 getDynFlags :: TcS DynFlags
513 getDynFlags = wrapTcS TcM.getDOpts
515 getTcSContext :: TcS SimplContext
516 getTcSContext = TcS (return . tcs_context)
518 getTcEvBinds :: TcS EvBindsVar
519 getTcEvBinds = TcS (return . tcs_ev_binds)
521 getUntouchables :: TcS Untouchables
522 getUntouchables = TcS (return . tcs_untch)
524 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
525 getTcSTyBinds = TcS (return . tcs_ty_binds)
527 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
528 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
531 getTcEvBindsBag :: TcS EvBindMap
533 = do { EvBindsVar ev_ref _ <- getTcEvBinds
534 ; wrapTcS $ TcM.readTcRef ev_ref }
536 setWantedCoBind :: CoVar -> Coercion -> TcS ()
537 setWantedCoBind cv co
538 = setEvBind cv (EvCoercion co)
539 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
541 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
542 setDerivedCoBind cv co
543 = setEvBind cv (EvCoercion co)
545 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
546 -- Add a type binding
547 setWantedTyBind tv ty
548 = do { ref <- getTcSTyBinds
550 do { ty_binds <- TcM.readTcRef ref
551 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
553 setIPBind :: EvVar -> EvTerm -> TcS ()
554 setIPBind = setEvBind
556 setDictBind :: EvVar -> EvTerm -> TcS ()
557 setDictBind = setEvBind
559 setEvBind :: EvVar -> EvTerm -> TcS ()
562 = do { tc_evbinds <- getTcEvBinds
563 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
565 newTcEvBindsTcS :: TcS EvBindsVar
566 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
568 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
569 warnTcS loc warn_if doc
570 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
571 | otherwise = return ()
573 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
575 = do { ctxt <- getTcSContext
576 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
577 ; return (ctxt, tys, flags) }
579 -- Just get some environments needed for instance looking up and matching
580 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
582 getInstEnvs :: TcS (InstEnv, InstEnv)
583 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
585 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
586 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
588 getTopEnv :: TcS HscEnv
589 getTopEnv = wrapTcS $ TcM.getTopEnv
591 getGblEnv :: TcS TcGblEnv
592 getGblEnv = wrapTcS $ TcM.getGblEnv
594 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
595 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
598 checkWellStagedDFun pred dfun_id loc
599 = wrapTcS $ TcM.setCtLoc loc $
600 do { use_stage <- TcM.getStage
601 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
603 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
604 bind_lvl = TcM.topIdLvl dfun_id
606 pprEq :: TcType -> TcType -> SDoc
607 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
609 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
610 isTouchableMetaTyVar tv
611 = do { untch <- getUntouchables
612 ; return $ isTouchableMetaTyVar_InRange untch tv }
614 isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool
615 isTouchableMetaTyVar_InRange untch tv
616 = case tcTyVarDetails tv of
617 MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables]
618 MetaTv {} -> inTouchableRange untch tv
625 Note [Touchable meta type variables]
626 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
627 Meta type variables allocated *by the constraint solver itself* are always
629 instance C a b => D [a] where...
630 if we use this instance declaration we "make up" a fresh meta type
631 variable for 'b', which we must later guess. (Perhaps C has a
632 functional dependency.) But since we aren't in the constraint *generator*
633 we can't allocate a Unique in the touchable range for this implication
634 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
639 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
641 newFlattenSkolemTy :: TcType -> TcS TcType
642 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
644 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
645 newFlattenSkolemTyVar ty
646 = wrapTcS $ do { uniq <- TcM.newUnique
647 ; let name = mkSysTvName uniq (fsLit "f")
648 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
651 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
653 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
654 instDFunTypes mb_inst_tys
655 = mapM inst_tv mb_inst_tys
657 inst_tv :: Either TyVar TcType -> TcS Type
658 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
659 inst_tv (Right ty) = return ty
661 instDFunConstraints :: TcThetaType -> TcS [EvVar]
662 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
665 -- newFlexiTcS :: TyVar -> TcS TcTyVar
666 -- -- Make a TcsTv meta tyvar; it is always touchable,
667 -- -- but we are supposed to guess its instantiation
668 -- -- See Note [Touchable meta type variables]
669 -- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
671 newFlexiTcS :: TyVar -> TcS TcTyVar
672 -- Like TcM.instMetaTyVar but the variable that is created is always
673 -- touchable; we are supposed to guess its instantiation.
674 -- See Note [Touchable meta type variables]
675 newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
677 newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)
678 -- Create new wanted CoVar that constrains the type to have the specified kind.
679 newKindConstraint tv knd
680 = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd
681 ; let ty_k = mkTyVarTy tv_k
682 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
683 ; return (co_var, ty_k) }
685 newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
686 newFlexiTcSHelper tvname tvkind
688 do { uniq <- TcM.newUnique
689 ; ref <- TcM.newMutVar Flexi
690 ; let name = setNameUnique tvname uniq
692 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
694 -- Superclasses and recursive dictionaries
695 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
698 newGivOrDerEvVar pty evtrm
699 = do { ev <- wrapTcS $ TcM.newEvVar pty
703 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
704 -- Note we create immutable variables for given or derived, since we
705 -- must bind them to TcEvBinds (because their evidence may involve
706 -- superclasses). However we should be able to override existing
707 -- 'derived' evidence, even in TcEvBinds
708 newGivOrDerCoVar ty1 ty2 co
709 = do { cv <- newCoVar ty1 ty2
710 ; setEvBind cv (EvCoercion co)
713 newWantedCoVar :: TcType -> TcType -> TcS EvVar
714 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
717 newCoVar :: TcType -> TcType -> TcS EvVar
718 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
720 newIPVar :: IPName Name -> TcType -> TcS EvVar
721 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
723 newDictVar :: Class -> [TcType] -> TcS EvVar
724 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
729 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
730 -- In a call (isGoodRecEv ev wv), we are considering solving wv
731 -- using some term that involves ev, such as:
732 -- by setting wv = ev
733 -- or wv = EvCast x |> ev
735 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
736 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
737 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
739 -- Guarded means: more instance calls than superclass selections. We
740 -- compute this by chasing the evidence, adding +1 for every instance
741 -- call (constructor) and -1 for every superclass selection (destructor).
743 -- See Note [Superclasses and recursive dictionaries] in TcInteract
744 isGoodRecEv ev_var (WantedEvVar wv _)
745 = do { tc_evbinds <- getTcEvBindsBag
746 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
747 ; return $ case mb of
749 Just min_guardedness -> min_guardedness > 0
752 where chase_ev_var :: EvBindMap -- Evidence binds
753 -> EvVar -- Target variable whose gravity we want to return
754 -> Int -- Current gravity
755 -> [EvVar] -- Visited nodes
756 -> EvVar -- Current node
758 chase_ev_var assocs trg curr_grav visited orig
759 | trg == orig = return $ Just curr_grav
760 | orig `elem` visited = return $ Nothing
761 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
762 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
764 {- No longer needed: evidence is in the EvBinds
765 | isTcTyVar orig && isMetaTyVar orig
766 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
767 ; case meta_details of
768 Flexi -> return Nothing
769 Indirect tyco -> chase_ev assocs trg curr_grav
770 (orig:visited) (EvCoercion tyco)
773 | otherwise = return Nothing
775 chase_ev assocs trg curr_grav visited (EvId v)
776 = chase_ev_var assocs trg curr_grav visited v
777 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
778 = chase_ev_var assocs trg (curr_grav-1) visited d_id
779 chase_ev assocs trg curr_grav visited (EvCast v co)
780 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
781 ; m2 <- chase_co assocs trg curr_grav visited co
782 ; return (comb_chase_res Nothing [m1,m2]) }
784 chase_ev assocs trg curr_grav visited (EvCoercion co)
785 = chase_co assocs trg curr_grav visited co
786 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
787 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
788 ; return (comb_chase_res Nothing chase_results) }
790 chase_co assocs trg curr_grav visited co
791 = -- Look for all the coercion variables in the coercion
792 -- chase them, and combine the results. This is OK since the
793 -- coercion will not contain any superclass terms -- anything
794 -- that involves dictionaries will be bound in assocs.
795 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
797 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
798 ; return (comb_chase_res Nothing chase_results) }
800 comb_chase_res f [] = f
801 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
802 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
803 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
806 -- Matching and looking up classes and family instances
807 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
809 data MatchInstResult mi
810 = MatchInstNo -- No matching instance
811 | MatchInstSingle mi -- Single matching instance
812 | MatchInstMany -- Multiple matching instances
815 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
816 -- Look up a class constraint in the instance environment
818 = do { let pred = mkClassPred clas tys
819 ; instEnvs <- getInstEnvs
820 ; case lookupInstEnv instEnvs clas tys of {
821 ([], unifs) -- Nothing matches
822 -> do { traceTcS "matchClass not matching"
823 (vcat [ text "dict" <+> ppr pred,
824 text "unifs" <+> ppr unifs ])
827 ([(ispec, inst_tys)], []) -- A single match
828 -> do { let dfun_id = is_dfun ispec
829 ; traceTcS "matchClass success"
830 (vcat [text "dict" <+> ppr pred,
831 text "witness" <+> ppr dfun_id
832 <+> ppr (idType dfun_id) ])
833 -- Record that this dfun is needed
834 ; record_dfun_usage dfun_id
835 ; return $ MatchInstSingle (dfun_id, inst_tys)
837 (matches, unifs) -- More than one matches
838 -> do { traceTcS "matchClass multiple matches, deferring choice"
839 (vcat [text "dict" <+> ppr pred,
840 text "matches" <+> ppr matches,
841 text "unifs" <+> ppr unifs])
842 ; return MatchInstMany
846 where record_dfun_usage :: Id -> TcS ()
847 record_dfun_usage dfun_id
848 = do { hsc_env <- getTopEnv
849 ; let dfun_name = idName dfun_id
850 dfun_mod = ASSERT( isExternalName dfun_name )
852 ; if isInternalName dfun_name || -- Internal name => defined in this module
853 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
854 then return () -- internal, or in another package
855 else do updInstUses dfun_id
858 updInstUses :: Id -> TcS ()
860 = do { tcg_env <- getGblEnv
861 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
862 (`addOneToNameSet` idName dfun_id)
867 -> TcS (MatchInstResult (TyCon, [Type]))
869 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
871 Nothing -> return MatchInstNo
872 Just res -> return $ MatchInstSingle res
873 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
874 -- multiple matches. Check.
878 -- Functional dependencies, instantiation of equations
879 -------------------------------------------------------
881 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
883 mkWantedFunDepEqns _ [] = return []
884 mkWantedFunDepEqns loc eqns
885 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
886 ; wevvars <- mapM to_work_item eqns
887 ; return $ concat wevvars }
889 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
890 to_work_item ((qtvs, pairs), _, _)
891 = do { let tvs = varSetElems qtvs
892 ; tvs' <- mapM newFlexiTcS tvs
893 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
894 ; mapM (do_one subst) pairs }
896 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
897 sty2 = substTy subst ty2
898 ; ev <- newWantedCoVar sty1 sty2
899 ; return (WantedEvVar ev loc) }
901 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
902 pprEquationDoc (eqn, (p1, _), (p2, _))
903 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]