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]
151 cc_flavor :: CtFlavor,
156 | CFunEqCan { -- F xis ~ xi
157 -- Invariant: * isSynFamilyTyCon cc_fun
158 -- * cc_rhs is not a touchable unification variable
159 -- See Note [No touchables as FunEq RHS]
160 -- * If constraint is given then
161 -- typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
163 cc_flavor :: CtFlavor,
164 cc_fun :: TyCon, -- A type function
165 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
166 cc_rhs :: Xi -- *never* over-saturated (because if so
167 -- we should have decomposed)
171 makeGivens :: CanonicalCts -> CanonicalCts
172 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
173 -- The UnkSkol doesn't matter because these givens are
174 -- not contradictory (else we'd have rejected them already)
176 makeSolvedByInst :: CanonicalCt -> CanonicalCt
177 -- Record that a constraint is now solved
179 -- Given, Derived -> no-op
181 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
184 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
185 mkWantedConstraints flats implics
186 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
188 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
189 deCanonicaliseWanted ct
190 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
191 let Wanted loc = cc_flavor ct
192 in WantedEvVar (cc_id ct) loc
194 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
195 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
196 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
197 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
198 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
200 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
201 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
202 tyVarsOfCDict _ct = emptyVarSet
204 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
205 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
207 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
208 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
210 instance Outputable CanonicalCt where
211 ppr (CDictCan d fl cls tys)
212 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
213 ppr (CIPCan ip fl ip_nm ty)
214 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
215 ppr (CTyEqCan co fl tv ty)
216 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
217 ppr (CFunEqCan co fl tc tys ty)
218 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
222 Note [No touchables as FunEq RHS]
223 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
224 Notice that (F xis ~ beta), where beta is an touchable unification
225 variable, is not canonical. Why?
226 * If (F xis ~ beta) was the only wanted constraint, we'd
227 definitely want to spontaneously-unify it
229 * But suppose we had an earlier wanted (beta ~ Int), and
230 have already spontaneously unified it. Then we have an
231 identity given (id : beta ~ Int) in the inert set.
233 * But (F xis ~ beta) does not react with that given (because we
234 don't subsitute on the RHS of a function equality). So there's a
235 serious danger that we'd spontaneously unify it a second time.
241 Note [Canonical implicit parameter constraints]
242 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
243 The type in a canonical implicit parameter constraint doesn't need to
244 be a xi (type-function-free type) since we can defer the flattening
245 until checking this type for equality with another type. If we
246 encounter two IP constraints with the same name, they MUST have the
247 same type, and at that point we can generate a flattened equality
248 constraint between the types. (On the other hand, the types in two
249 class constraints for the same class MAY be equal, so they need to be
250 flattened in the first place to facilitate comparing them.)
253 singleCCan :: CanonicalCt -> CanonicalCts
256 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
259 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
260 extendCCans = snocBag
262 andCCans :: [CanonicalCts] -> CanonicalCts
263 andCCans = unionManyBags
265 emptyCCan :: CanonicalCts
268 isEmptyCCan :: CanonicalCts -> Bool
269 isEmptyCCan = isEmptyBag
271 isTyEqCCan :: CanonicalCt -> Bool
272 isTyEqCCan (CTyEqCan {}) = True
273 isTyEqCCan (CFunEqCan {}) = False
278 %************************************************************************
281 The "flavor" of a canonical constraint
283 %************************************************************************
287 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
288 | Derived WantedLoc DerivedOrig
289 -- We have evidence for this constraint in TcEvBinds;
290 -- *however* this evidence can contain wanteds, so
291 -- it's valid only provisionally to the solution of
293 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
295 data DerivedOrig = DerSC | DerInst
296 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
297 -- solved wanteds from instances.
299 instance Outputable CtFlavor where
300 ppr (Given _) = ptext (sLit "[Given]")
301 ppr (Wanted _) = ptext (sLit "[Wanted]")
302 ppr (Derived {}) = ptext (sLit "[Derived]")
304 isWanted :: CtFlavor -> Bool
305 isWanted (Wanted {}) = True
308 isGiven :: CtFlavor -> Bool
309 isGiven (Given {}) = True
312 isDerived :: CtFlavor -> Bool
313 isDerived (Derived {}) = True
316 isDerivedSC :: CtFlavor -> Bool
317 isDerivedSC (Derived _ DerSC) = True
318 isDerivedSC _ = False
320 isDerivedByInst :: CtFlavor -> Bool
321 isDerivedByInst (Derived _ DerInst) = True
322 isDerivedByInst _ = False
324 canSolve :: CtFlavor -> CtFlavor -> Bool
325 -- canSolve ctid1 ctid2
326 -- The constraint ctid1 can be used to solve ctid2
327 -- "to solve" means a reaction where the active parts of the two constraints match.
328 -- active(F xis ~ xi) = F xis
329 -- active(tv ~ xi) = tv
330 -- active(D xis) = D xis
331 -- active(IP nm ty) = nm
332 -----------------------------------------
333 canSolve (Given {}) _ = True
334 canSolve (Derived {}) (Wanted {}) = True
335 canSolve (Derived {}) (Derived {}) = True
336 canSolve (Wanted {}) (Wanted {}) = True
339 canRewrite :: CtFlavor -> CtFlavor -> Bool
340 -- canRewrite ctid1 ctid2
341 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
342 canRewrite = canSolve
344 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
345 -- Precondition: At least one of them should be wanted
346 combineCtLoc (Wanted loc) _ = loc
347 combineCtLoc _ (Wanted loc) = loc
348 combineCtLoc (Derived loc _) _ = loc
349 combineCtLoc _ (Derived loc _) = loc
350 combineCtLoc _ _ = panic "combineCtLoc: both given"
352 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
353 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
354 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
355 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
359 %************************************************************************
361 %* The TcS solver monad *
363 %************************************************************************
367 The TcS monad is a weak form of the main Tc monad
371 * allocate new variables
372 * fill in evidence variables
374 Filling in a dictionary evidence variable means to create a binding
375 for it, so TcS carries a mutable location where the binding can be
376 added. This is initialised from the innermost implication constraint.
381 tcs_ev_binds :: EvBindsVar,
384 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
385 -- Global type bindings
387 tcs_context :: SimplContext,
389 tcs_untch :: Untouchables
393 = SimplInfer -- Inferring type of a let-bound thing
394 | SimplRuleLhs -- Inferring type of a RULE lhs
395 | SimplInteractive -- Inferring type at GHCi prompt
396 | SimplCheck -- Checking a type signature or RULE rhs
398 instance Outputable SimplContext where
399 ppr SimplInfer = ptext (sLit "SimplInfer")
400 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
401 ppr SimplInteractive = ptext (sLit "SimplInteractive")
402 ppr SimplCheck = ptext (sLit "SimplCheck")
404 isInteractive :: SimplContext -> Bool
405 isInteractive SimplInteractive = True
406 isInteractive _ = False
408 simplEqsOnly :: SimplContext -> Bool
409 -- Simplify equalities only, not dictionaries
410 -- This is used for the LHS of rules; ee
411 -- Note [Simplifying RULE lhs constraints] in TcSimplify
412 simplEqsOnly SimplRuleLhs = True
413 simplEqsOnly _ = False
415 performDefaulting :: SimplContext -> Bool
416 performDefaulting SimplInfer = False
417 performDefaulting SimplRuleLhs = False
418 performDefaulting SimplInteractive = True
419 performDefaulting SimplCheck = True
422 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
424 instance Functor TcS where
425 fmap f m = TcS $ fmap f . unTcS m
427 instance Monad TcS where
428 return x = TcS (\_ -> return x)
429 fail err = TcS (\_ -> fail err)
430 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
432 -- Basic functionality
433 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
434 wrapTcS :: TcM a -> TcS a
435 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
436 -- and TcS is supposed to have limited functionality
437 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
439 wrapErrTcS :: TcM a -> TcS a
440 -- The thing wrapped should just fail
441 -- There's no static check; it's up to the user
442 -- Having a variant for each error message is too painful
445 wrapWarnTcS :: TcM a -> TcS a
446 -- The thing wrapped should just add a warning, or no-op
447 -- There's no static check; it's up to the user
448 wrapWarnTcS = wrapTcS
450 failTcS, panicTcS :: SDoc -> TcS a
451 failTcS = wrapTcS . TcM.failWith
452 panicTcS doc = pprPanic "TcCanonical" doc
454 traceTcS :: String -> SDoc -> TcS ()
455 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
457 traceTcS0 :: String -> SDoc -> TcS ()
458 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
460 runTcS :: SimplContext
461 -> Untouchables -- Untouchables
462 -> TcS a -- What to run
463 -> TcM (a, Bag EvBind)
464 runTcS context untouch tcs
465 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
466 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
467 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
468 , tcs_ty_binds = ty_binds_var
469 , tcs_context = context
470 , tcs_untch = untouch }
472 -- Run the computation
473 ; res <- unTcS tcs env
475 -- Perform the type unifications required
476 ; ty_binds <- TcM.readTcRef ty_binds_var
477 ; mapM_ do_unification (varEnvElts ty_binds)
480 ; ev_binds <- TcM.readTcRef evb_ref
481 ; return (res, evBindMapBinds ev_binds) }
483 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
486 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
487 nestImplicTcS ref untch (TcS thing_inside)
488 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
490 nest_env = TcSEnv { tcs_ev_binds = ref
491 , tcs_ty_binds = ty_binds
493 , tcs_context = ctxtUnderImplic ctxt }
495 thing_inside nest_env
497 recoverTcS :: TcS a -> TcS a -> TcS a
498 recoverTcS (TcS recovery_code) (TcS thing_inside)
500 TcM.recoverM (recovery_code env) (thing_inside env)
502 ctxtUnderImplic :: SimplContext -> SimplContext
503 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
504 ctxtUnderImplic SimplRuleLhs = SimplCheck
505 ctxtUnderImplic ctxt = ctxt
507 tryTcS :: TcS a -> TcS a
508 -- Like runTcS, but from within the TcS monad
509 -- Ignore all the evidence generated, and do not affect caller's evidence!
511 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
512 ; ev_binds_var <- TcM.newTcEvBinds
513 ; let env1 = env { tcs_ev_binds = ev_binds_var
514 , tcs_ty_binds = ty_binds_var }
518 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
520 getDynFlags :: TcS DynFlags
521 getDynFlags = wrapTcS TcM.getDOpts
523 getTcSContext :: TcS SimplContext
524 getTcSContext = TcS (return . tcs_context)
526 getTcEvBinds :: TcS EvBindsVar
527 getTcEvBinds = TcS (return . tcs_ev_binds)
529 getUntouchables :: TcS Untouchables
530 getUntouchables = TcS (return . tcs_untch)
532 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
533 getTcSTyBinds = TcS (return . tcs_ty_binds)
535 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
536 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
539 getTcEvBindsBag :: TcS EvBindMap
541 = do { EvBindsVar ev_ref _ <- getTcEvBinds
542 ; wrapTcS $ TcM.readTcRef ev_ref }
544 setWantedCoBind :: CoVar -> Coercion -> TcS ()
545 setWantedCoBind cv co
546 = setEvBind cv (EvCoercion co)
547 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
549 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
550 setDerivedCoBind cv co
551 = setEvBind cv (EvCoercion co)
553 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
554 -- Add a type binding
555 setWantedTyBind tv ty
556 = do { ref <- getTcSTyBinds
558 do { ty_binds <- TcM.readTcRef ref
559 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
561 setIPBind :: EvVar -> EvTerm -> TcS ()
562 setIPBind = setEvBind
564 setDictBind :: EvVar -> EvTerm -> TcS ()
565 setDictBind = setEvBind
567 setEvBind :: EvVar -> EvTerm -> TcS ()
570 = do { tc_evbinds <- getTcEvBinds
571 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
573 newTcEvBindsTcS :: TcS EvBindsVar
574 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
576 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
577 warnTcS loc warn_if doc
578 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
579 | otherwise = return ()
581 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
583 = do { ctxt <- getTcSContext
584 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
585 ; return (ctxt, tys, flags) }
587 -- Just get some environments needed for instance looking up and matching
588 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
590 getInstEnvs :: TcS (InstEnv, InstEnv)
591 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
593 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
594 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
596 getTopEnv :: TcS HscEnv
597 getTopEnv = wrapTcS $ TcM.getTopEnv
599 getGblEnv :: TcS TcGblEnv
600 getGblEnv = wrapTcS $ TcM.getGblEnv
602 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
603 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
605 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
606 checkWellStagedDFun pred dfun_id loc
607 = wrapTcS $ TcM.setCtLoc loc $
608 do { use_stage <- TcM.getStage
609 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
611 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
612 bind_lvl = TcM.topIdLvl dfun_id
614 pprEq :: TcType -> TcType -> SDoc
615 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
617 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
618 isTouchableMetaTyVar tv
619 = do { untch <- getUntouchables
620 ; return $ isTouchableMetaTyVar_InRange untch tv }
622 isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool
623 isTouchableMetaTyVar_InRange untch tv
624 = case tcTyVarDetails tv of
625 MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables]
626 MetaTv {} -> inTouchableRange untch tv
633 Note [Touchable meta type variables]
634 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
635 Meta type variables allocated *by the constraint solver itself* are always
637 instance C a b => D [a] where...
638 if we use this instance declaration we "make up" a fresh meta type
639 variable for 'b', which we must later guess. (Perhaps C has a
640 functional dependency.) But since we aren't in the constraint *generator*
641 we can't allocate a Unique in the touchable range for this implication
642 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
647 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
649 newFlattenSkolemTy :: TcType -> TcS TcType
650 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
652 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
653 newFlattenSkolemTyVar ty
654 = wrapTcS $ do { uniq <- TcM.newUnique
655 ; let name = mkSysTvName uniq (fsLit "f")
656 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
659 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
661 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
662 instDFunTypes mb_inst_tys
663 = mapM inst_tv mb_inst_tys
665 inst_tv :: Either TyVar TcType -> TcS Type
666 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
667 inst_tv (Right ty) = return ty
669 instDFunConstraints :: TcThetaType -> TcS [EvVar]
670 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
673 -- newFlexiTcS :: TyVar -> TcS TcTyVar
674 -- -- Make a TcsTv meta tyvar; it is always touchable,
675 -- -- but we are supposed to guess its instantiation
676 -- -- See Note [Touchable meta type variables]
677 -- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
679 newFlexiTcS :: TyVar -> TcS TcTyVar
680 -- Like TcM.instMetaTyVar but the variable that is created is always
681 -- touchable; we are supposed to guess its instantiation.
682 -- See Note [Touchable meta type variables]
683 newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
685 newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)
686 -- Create new wanted CoVar that constrains the type to have the specified kind.
687 newKindConstraint tv knd
688 = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd
689 ; let ty_k = mkTyVarTy tv_k
690 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
691 ; return (co_var, ty_k) }
693 newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
694 newFlexiTcSHelper tvname tvkind
696 do { uniq <- TcM.newUnique
697 ; ref <- TcM.newMutVar Flexi
698 ; let name = setNameUnique tvname uniq
700 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
702 -- Superclasses and recursive dictionaries
703 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
705 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
706 newGivOrDerEvVar pty evtrm
707 = do { ev <- wrapTcS $ TcM.newEvVar pty
711 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
712 -- Note we create immutable variables for given or derived, since we
713 -- must bind them to TcEvBinds (because their evidence may involve
714 -- superclasses). However we should be able to override existing
715 -- 'derived' evidence, even in TcEvBinds
716 newGivOrDerCoVar ty1 ty2 co
717 = do { cv <- newCoVar ty1 ty2
718 ; setEvBind cv (EvCoercion co)
721 newWantedCoVar :: TcType -> TcType -> TcS EvVar
722 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
725 newCoVar :: TcType -> TcType -> TcS EvVar
726 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
728 newIPVar :: IPName Name -> TcType -> TcS EvVar
729 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
731 newDictVar :: Class -> [TcType] -> TcS EvVar
732 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
737 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
738 -- In a call (isGoodRecEv ev wv), we are considering solving wv
739 -- using some term that involves ev, such as:
740 -- by setting wv = ev
741 -- or wv = EvCast x |> ev
743 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
744 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
745 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
747 -- Guarded means: more instance calls than superclass selections. We
748 -- compute this by chasing the evidence, adding +1 for every instance
749 -- call (constructor) and -1 for every superclass selection (destructor).
751 -- See Note [Superclasses and recursive dictionaries] in TcInteract
752 isGoodRecEv ev_var (WantedEvVar wv _)
753 = do { tc_evbinds <- getTcEvBindsBag
754 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
755 ; return $ case mb of
757 Just min_guardedness -> min_guardedness > 0
760 where chase_ev_var :: EvBindMap -- Evidence binds
761 -> EvVar -- Target variable whose gravity we want to return
762 -> Int -- Current gravity
763 -> [EvVar] -- Visited nodes
764 -> EvVar -- Current node
766 chase_ev_var assocs trg curr_grav visited orig
767 | trg == orig = return $ Just curr_grav
768 | orig `elem` visited = return $ Nothing
769 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
770 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
772 {- No longer needed: evidence is in the EvBinds
773 | isTcTyVar orig && isMetaTyVar orig
774 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
775 ; case meta_details of
776 Flexi -> return Nothing
777 Indirect tyco -> chase_ev assocs trg curr_grav
778 (orig:visited) (EvCoercion tyco)
781 | otherwise = return Nothing
783 chase_ev assocs trg curr_grav visited (EvId v)
784 = chase_ev_var assocs trg curr_grav visited v
785 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
786 = chase_ev_var assocs trg (curr_grav-1) visited d_id
787 chase_ev assocs trg curr_grav visited (EvCast v co)
788 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
789 ; m2 <- chase_co assocs trg curr_grav visited co
790 ; return (comb_chase_res Nothing [m1,m2]) }
792 chase_ev assocs trg curr_grav visited (EvCoercion co)
793 = chase_co assocs trg curr_grav visited co
794 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
795 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
796 ; return (comb_chase_res Nothing chase_results) }
798 chase_co assocs trg curr_grav visited co
799 = -- Look for all the coercion variables in the coercion
800 -- chase them, and combine the results. This is OK since the
801 -- coercion will not contain any superclass terms -- anything
802 -- that involves dictionaries will be bound in assocs.
803 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
805 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
806 ; return (comb_chase_res Nothing chase_results) }
808 comb_chase_res f [] = f
809 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
810 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
811 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
814 -- Matching and looking up classes and family instances
815 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
817 data MatchInstResult mi
818 = MatchInstNo -- No matching instance
819 | MatchInstSingle mi -- Single matching instance
820 | MatchInstMany -- Multiple matching instances
823 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
824 -- Look up a class constraint in the instance environment
826 = do { let pred = mkClassPred clas tys
827 ; instEnvs <- getInstEnvs
828 ; case lookupInstEnv instEnvs clas tys of {
829 ([], unifs) -- Nothing matches
830 -> do { traceTcS "matchClass not matching"
831 (vcat [ text "dict" <+> ppr pred,
832 text "unifs" <+> ppr unifs ])
835 ([(ispec, inst_tys)], []) -- A single match
836 -> do { let dfun_id = is_dfun ispec
837 ; traceTcS "matchClass success"
838 (vcat [text "dict" <+> ppr pred,
839 text "witness" <+> ppr dfun_id
840 <+> ppr (idType dfun_id) ])
841 -- Record that this dfun is needed
842 ; record_dfun_usage dfun_id
843 ; return $ MatchInstSingle (dfun_id, inst_tys)
845 (matches, unifs) -- More than one matches
846 -> do { traceTcS "matchClass multiple matches, deferring choice"
847 (vcat [text "dict" <+> ppr pred,
848 text "matches" <+> ppr matches,
849 text "unifs" <+> ppr unifs])
850 ; return MatchInstMany
854 where record_dfun_usage :: Id -> TcS ()
855 record_dfun_usage dfun_id
856 = do { hsc_env <- getTopEnv
857 ; let dfun_name = idName dfun_id
858 dfun_mod = ASSERT( isExternalName dfun_name )
860 ; if isInternalName dfun_name || -- Internal name => defined in this module
861 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
862 then return () -- internal, or in another package
863 else do updInstUses dfun_id
866 updInstUses :: Id -> TcS ()
868 = do { tcg_env <- getGblEnv
869 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
870 (`addOneToNameSet` idName dfun_id)
875 -> TcS (MatchInstResult (TyCon, [Type]))
877 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
879 Nothing -> return MatchInstNo
880 Just res -> return $ MatchInstSingle res
881 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
882 -- multiple matches. Check.
886 -- Functional dependencies, instantiation of equations
887 -------------------------------------------------------
889 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
891 mkWantedFunDepEqns _ [] = return []
892 mkWantedFunDepEqns loc eqns
893 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
894 ; wevvars <- mapM to_work_item eqns
895 ; return $ concat wevvars }
897 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
898 to_work_item ((qtvs, pairs), _, _)
899 = do { let tvs = varSetElems qtvs
900 ; tvs' <- mapM newFlexiTcS tvs
901 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
902 ; mapM (do_one subst) pairs }
904 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
905 sty2 = substTy subst ty2
906 ; ev <- newWantedCoVar sty1 sty2
907 ; return (WantedEvVar ev loc) }
909 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
910 pprEquationDoc (eqn, (p1, _), (p2, _))
911 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]