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
47 zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad
52 isTouchableMetaTyVar_InRange,
54 getDefaultInfo, getDynFlags,
56 matchClass, matchFam, MatchInstResult (..),
59 pprEq, -- Smaller utils, re-exported from TcM
60 -- TODO (DV): these are only really used in the
61 -- instance matcher in TcSimplify. I am wondering
62 -- if the whole instance matcher simply belongs
66 mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps
70 #include "HsVersions.h"
80 import NameSet ( addOneToNameSet )
82 import qualified TcRnMonad as TcM
83 import qualified TcMType as TcM
84 import qualified TcEnv as TcM
85 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
104 import HsBinds -- for TcEvBinds stuff
114 %************************************************************************
116 %* Canonical constraints *
118 %* These are the constraints the low-level simplifier works with *
120 %************************************************************************
123 -- Types without any type functions inside. However, note that xi
124 -- types CAN contain unexpanded type synonyms; however, the
125 -- (transitive) expansions of those type synonyms will not contain any
127 type Xi = Type -- In many comments, "xi" ranges over Xi
129 type CanonicalCts = Bag CanonicalCt
132 -- Atomic canonical constraints
133 = CDictCan { -- e.g. Num xi
135 cc_flavor :: CtFlavor,
140 | CIPCan { -- ?x::tau
141 -- See note [Canonical implicit parameter constraints].
143 cc_flavor :: CtFlavor,
144 cc_ip_nm :: IPName Name,
145 cc_ip_ty :: TcTauType
148 | CTyEqCan { -- tv ~ xi (recall xi means function free)
150 -- * tv not in tvs(xi) (occurs check)
151 -- * If constraint is given then typeKind xi `compatKind` typeKind tv
152 -- See Note [Spontaneous solving and kind compatibility]
153 -- * if xi is a flatten skolem then tv must be a flatten skolem
154 -- i.e. equalities prefer flatten skolems in their LHS.
155 -- See Note [Loopy Spontaneous Solving, Example 4]
156 -- Also related to [Flatten Skolem Equivalence Classes]
158 cc_flavor :: CtFlavor,
163 | CFunEqCan { -- F xis ~ xi
164 -- Invariant: * isSynFamilyTyCon cc_fun
165 -- * cc_rhs is not a touchable unification variable
166 -- See Note [No touchables as FunEq RHS]
167 -- * If constraint is given then
168 -- typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs
170 cc_flavor :: CtFlavor,
171 cc_fun :: TyCon, -- A type function
172 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
173 cc_rhs :: Xi -- *never* over-saturated (because if so
174 -- we should have decomposed)
178 compatKind :: Kind -> Kind -> Bool
179 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
181 makeGivens :: CanonicalCts -> CanonicalCts
182 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
183 -- The UnkSkol doesn't matter because these givens are
184 -- not contradictory (else we'd have rejected them already)
186 makeSolvedByInst :: CanonicalCt -> CanonicalCt
187 -- Record that a constraint is now solved
189 -- Given, Derived -> no-op
191 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
194 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
195 mkWantedConstraints flats implics
196 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
198 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
199 deCanonicaliseWanted ct
200 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
201 let Wanted loc = cc_flavor ct
202 in WantedEvVar (cc_id ct) loc
204 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
205 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
206 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
207 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
208 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
210 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
211 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
212 tyVarsOfCDict _ct = emptyVarSet
214 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
215 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
217 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
218 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
220 instance Outputable CanonicalCt where
221 ppr (CDictCan d fl cls tys)
222 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
223 ppr (CIPCan ip fl ip_nm ty)
224 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
225 ppr (CTyEqCan co fl tv ty)
226 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
227 ppr (CFunEqCan co fl tc tys ty)
228 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
232 Note [No touchables as FunEq RHS]
233 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
234 Notice that (F xis ~ beta), where beta is an touchable unification
235 variable, is not canonical. Why?
236 * If (F xis ~ beta) was the only wanted constraint, we'd
237 definitely want to spontaneously-unify it
239 * But suppose we had an earlier wanted (beta ~ Int), and
240 have already spontaneously unified it. Then we have an
241 identity given (id : beta ~ Int) in the inert set.
243 * But (F xis ~ beta) does not react with that given (because we
244 don't subsitute on the RHS of a function equality). So there's a
245 serious danger that we'd spontaneously unify it a second time.
251 Note [Canonical implicit parameter constraints]
252 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
253 The type in a canonical implicit parameter constraint doesn't need to
254 be a xi (type-function-free type) since we can defer the flattening
255 until checking this type for equality with another type. If we
256 encounter two IP constraints with the same name, they MUST have the
257 same type, and at that point we can generate a flattened equality
258 constraint between the types. (On the other hand, the types in two
259 class constraints for the same class MAY be equal, so they need to be
260 flattened in the first place to facilitate comparing them.)
263 singleCCan :: CanonicalCt -> CanonicalCts
266 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
269 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
270 extendCCans = snocBag
272 andCCans :: [CanonicalCts] -> CanonicalCts
273 andCCans = unionManyBags
275 emptyCCan :: CanonicalCts
278 isEmptyCCan :: CanonicalCts -> Bool
279 isEmptyCCan = isEmptyBag
281 isTyEqCCan :: CanonicalCt -> Bool
282 isTyEqCCan (CTyEqCan {}) = True
283 isTyEqCCan (CFunEqCan {}) = False
288 %************************************************************************
291 The "flavor" of a canonical constraint
293 %************************************************************************
297 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
298 | Derived WantedLoc DerivedOrig
299 -- We have evidence for this constraint in TcEvBinds;
300 -- *however* this evidence can contain wanteds, so
301 -- it's valid only provisionally to the solution of
303 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
305 data DerivedOrig = DerSC | DerInst
306 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
307 -- solved wanteds from instances.
309 instance Outputable CtFlavor where
310 ppr (Given _) = ptext (sLit "[Given]")
311 ppr (Wanted _) = ptext (sLit "[Wanted]")
312 ppr (Derived {}) = ptext (sLit "[Derived]")
314 isWanted :: CtFlavor -> Bool
315 isWanted (Wanted {}) = True
318 isGiven :: CtFlavor -> Bool
319 isGiven (Given {}) = True
322 isDerived :: CtFlavor -> Bool
323 isDerived (Derived {}) = True
326 isDerivedSC :: CtFlavor -> Bool
327 isDerivedSC (Derived _ DerSC) = True
328 isDerivedSC _ = False
330 isDerivedByInst :: CtFlavor -> Bool
331 isDerivedByInst (Derived _ DerInst) = True
332 isDerivedByInst _ = False
334 canSolve :: CtFlavor -> CtFlavor -> Bool
335 -- canSolve ctid1 ctid2
336 -- The constraint ctid1 can be used to solve ctid2
337 -- "to solve" means a reaction where the active parts of the two constraints match.
338 -- active(F xis ~ xi) = F xis
339 -- active(tv ~ xi) = tv
340 -- active(D xis) = D xis
341 -- active(IP nm ty) = nm
342 -----------------------------------------
343 canSolve (Given {}) _ = True
344 canSolve (Derived {}) (Wanted {}) = True
345 canSolve (Derived {}) (Derived {}) = True
346 canSolve (Wanted {}) (Wanted {}) = True
349 canRewrite :: CtFlavor -> CtFlavor -> Bool
350 -- canRewrite ctid1 ctid2
351 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
352 canRewrite = canSolve
354 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
355 -- Precondition: At least one of them should be wanted
356 combineCtLoc (Wanted loc) _ = loc
357 combineCtLoc _ (Wanted loc) = loc
358 combineCtLoc (Derived loc _) _ = loc
359 combineCtLoc _ (Derived loc _) = loc
360 combineCtLoc _ _ = panic "combineCtLoc: both given"
362 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
363 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
364 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
365 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
369 %************************************************************************
371 %* The TcS solver monad *
373 %************************************************************************
377 The TcS monad is a weak form of the main Tc monad
381 * allocate new variables
382 * fill in evidence variables
384 Filling in a dictionary evidence variable means to create a binding
385 for it, so TcS carries a mutable location where the binding can be
386 added. This is initialised from the innermost implication constraint.
391 tcs_ev_binds :: EvBindsVar,
394 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
395 -- Global type bindings
397 tcs_context :: SimplContext,
399 tcs_untch :: Untouchables
403 = SimplInfer -- Inferring type of a let-bound thing
404 | SimplRuleLhs -- Inferring type of a RULE lhs
405 | SimplInteractive -- Inferring type at GHCi prompt
406 | SimplCheck -- Checking a type signature or RULE rhs
408 instance Outputable SimplContext where
409 ppr SimplInfer = ptext (sLit "SimplInfer")
410 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
411 ppr SimplInteractive = ptext (sLit "SimplInteractive")
412 ppr SimplCheck = ptext (sLit "SimplCheck")
414 isInteractive :: SimplContext -> Bool
415 isInteractive SimplInteractive = True
416 isInteractive _ = False
418 simplEqsOnly :: SimplContext -> Bool
419 -- Simplify equalities only, not dictionaries
420 -- This is used for the LHS of rules; ee
421 -- Note [Simplifying RULE lhs constraints] in TcSimplify
422 simplEqsOnly SimplRuleLhs = True
423 simplEqsOnly _ = False
425 performDefaulting :: SimplContext -> Bool
426 performDefaulting SimplInfer = False
427 performDefaulting SimplRuleLhs = False
428 performDefaulting SimplInteractive = True
429 performDefaulting SimplCheck = True
432 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
434 instance Functor TcS where
435 fmap f m = TcS $ fmap f . unTcS m
437 instance Monad TcS where
438 return x = TcS (\_ -> return x)
439 fail err = TcS (\_ -> fail err)
440 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
442 -- Basic functionality
443 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
444 wrapTcS :: TcM a -> TcS a
445 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
446 -- and TcS is supposed to have limited functionality
447 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
449 wrapErrTcS :: TcM a -> TcS a
450 -- The thing wrapped should just fail
451 -- There's no static check; it's up to the user
452 -- Having a variant for each error message is too painful
455 wrapWarnTcS :: TcM a -> TcS a
456 -- The thing wrapped should just add a warning, or no-op
457 -- There's no static check; it's up to the user
458 wrapWarnTcS = wrapTcS
460 failTcS, panicTcS :: SDoc -> TcS a
461 failTcS = wrapTcS . TcM.failWith
462 panicTcS doc = pprPanic "TcCanonical" doc
464 traceTcS :: String -> SDoc -> TcS ()
465 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
467 traceTcS0 :: String -> SDoc -> TcS ()
468 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
470 runTcS :: SimplContext
471 -> Untouchables -- Untouchables
472 -> TcS a -- What to run
473 -> TcM (a, Bag EvBind)
474 runTcS context untouch tcs
475 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
476 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
477 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
478 , tcs_ty_binds = ty_binds_var
479 , tcs_context = context
480 , tcs_untch = untouch }
482 -- Run the computation
483 ; res <- unTcS tcs env
485 -- Perform the type unifications required
486 ; ty_binds <- TcM.readTcRef ty_binds_var
487 ; mapM_ do_unification (varEnvElts ty_binds)
490 ; ev_binds <- TcM.readTcRef evb_ref
491 ; return (res, evBindMapBinds ev_binds) }
493 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
496 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
497 nestImplicTcS ref untch (TcS thing_inside)
498 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
500 nest_env = TcSEnv { tcs_ev_binds = ref
501 , tcs_ty_binds = ty_binds
503 , tcs_context = ctxtUnderImplic ctxt }
505 thing_inside nest_env
507 recoverTcS :: TcS a -> TcS a -> TcS a
508 recoverTcS (TcS recovery_code) (TcS thing_inside)
510 TcM.recoverM (recovery_code env) (thing_inside env)
512 ctxtUnderImplic :: SimplContext -> SimplContext
513 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
514 ctxtUnderImplic SimplRuleLhs = SimplCheck
515 ctxtUnderImplic ctxt = ctxt
517 tryTcS :: TcS a -> TcS a
518 -- Like runTcS, but from within the TcS monad
519 -- Ignore all the evidence generated, and do not affect caller's evidence!
521 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
522 ; ev_binds_var <- TcM.newTcEvBinds
523 ; let env1 = env { tcs_ev_binds = ev_binds_var
524 , tcs_ty_binds = ty_binds_var }
528 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
530 getDynFlags :: TcS DynFlags
531 getDynFlags = wrapTcS TcM.getDOpts
533 getTcSContext :: TcS SimplContext
534 getTcSContext = TcS (return . tcs_context)
536 getTcEvBinds :: TcS EvBindsVar
537 getTcEvBinds = TcS (return . tcs_ev_binds)
539 getUntouchables :: TcS Untouchables
540 getUntouchables = TcS (return . tcs_untch)
542 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
543 getTcSTyBinds = TcS (return . tcs_ty_binds)
545 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
546 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
549 getTcEvBindsBag :: TcS EvBindMap
551 = do { EvBindsVar ev_ref _ <- getTcEvBinds
552 ; wrapTcS $ TcM.readTcRef ev_ref }
554 setWantedCoBind :: CoVar -> Coercion -> TcS ()
555 setWantedCoBind cv co
556 = setEvBind cv (EvCoercion co)
557 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
559 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
560 setDerivedCoBind cv co
561 = setEvBind cv (EvCoercion co)
563 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
564 -- Add a type binding
565 setWantedTyBind tv ty
566 = do { ref <- getTcSTyBinds
568 do { ty_binds <- TcM.readTcRef ref
569 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
571 setIPBind :: EvVar -> EvTerm -> TcS ()
572 setIPBind = setEvBind
574 setDictBind :: EvVar -> EvTerm -> TcS ()
575 setDictBind = setEvBind
577 setEvBind :: EvVar -> EvTerm -> TcS ()
580 = do { tc_evbinds <- getTcEvBinds
581 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
583 newTcEvBindsTcS :: TcS EvBindsVar
584 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
586 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
587 warnTcS loc warn_if doc
588 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
589 | otherwise = return ()
591 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
593 = do { ctxt <- getTcSContext
594 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
595 ; return (ctxt, tys, flags) }
597 -- Just get some environments needed for instance looking up and matching
598 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
600 getInstEnvs :: TcS (InstEnv, InstEnv)
601 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
603 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
604 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
606 getTopEnv :: TcS HscEnv
607 getTopEnv = wrapTcS $ TcM.getTopEnv
609 getGblEnv :: TcS TcGblEnv
610 getGblEnv = wrapTcS $ TcM.getGblEnv
612 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
613 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
615 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
616 checkWellStagedDFun pred dfun_id loc
617 = wrapTcS $ TcM.setCtLoc loc $
618 do { use_stage <- TcM.getStage
619 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
621 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
622 bind_lvl = TcM.topIdLvl dfun_id
624 pprEq :: TcType -> TcType -> SDoc
625 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
627 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
628 isTouchableMetaTyVar tv
629 = do { untch <- getUntouchables
630 ; return $ isTouchableMetaTyVar_InRange untch tv }
632 isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool
633 isTouchableMetaTyVar_InRange untch tv
634 = case tcTyVarDetails tv of
635 MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables]
636 MetaTv {} -> inTouchableRange untch tv
643 Note [Touchable meta type variables]
644 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
645 Meta type variables allocated *by the constraint solver itself* are always
647 instance C a b => D [a] where...
648 if we use this instance declaration we "make up" a fresh meta type
649 variable for 'b', which we must later guess. (Perhaps C has a
650 functional dependency.) But since we aren't in the constraint *generator*
651 we can't allocate a Unique in the touchable range for this implication
652 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
657 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
659 newFlattenSkolemTy :: TcType -> TcS TcType
660 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
662 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
663 newFlattenSkolemTyVar ty
664 = wrapTcS $ do { uniq <- TcM.newUnique
665 ; let name = mkSysTvName uniq (fsLit "f")
666 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
669 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
671 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
672 instDFunTypes mb_inst_tys
673 = mapM inst_tv mb_inst_tys
675 inst_tv :: Either TyVar TcType -> TcS Type
676 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
677 inst_tv (Right ty) = return ty
679 instDFunConstraints :: TcThetaType -> TcS [EvVar]
680 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
683 -- newFlexiTcS :: TyVar -> TcS TcTyVar
684 -- -- Make a TcsTv meta tyvar; it is always touchable,
685 -- -- but we are supposed to guess its instantiation
686 -- -- See Note [Touchable meta type variables]
687 -- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
689 newFlexiTcS :: TyVar -> TcS TcTyVar
690 -- Like TcM.instMetaTyVar but the variable that is created is always
691 -- touchable; we are supposed to guess its instantiation.
692 -- See Note [Touchable meta type variables]
693 newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
695 newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)
696 -- Create new wanted CoVar that constrains the type to have the specified kind.
697 newKindConstraint tv knd
698 = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd
699 ; let ty_k = mkTyVarTy tv_k
700 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
701 ; return (co_var, ty_k) }
703 newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
704 newFlexiTcSHelper tvname tvkind
706 do { uniq <- TcM.newUnique
707 ; ref <- TcM.newMutVar Flexi
708 ; let name = setNameUnique tvname uniq
710 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
712 -- Superclasses and recursive dictionaries
713 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
715 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
716 newGivOrDerEvVar pty evtrm
717 = do { ev <- wrapTcS $ TcM.newEvVar pty
721 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
722 -- Note we create immutable variables for given or derived, since we
723 -- must bind them to TcEvBinds (because their evidence may involve
724 -- superclasses). However we should be able to override existing
725 -- 'derived' evidence, even in TcEvBinds
726 newGivOrDerCoVar ty1 ty2 co
727 = do { cv <- newCoVar ty1 ty2
728 ; setEvBind cv (EvCoercion co)
731 newWantedCoVar :: TcType -> TcType -> TcS EvVar
732 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
735 newCoVar :: TcType -> TcType -> TcS EvVar
736 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
738 newIPVar :: IPName Name -> TcType -> TcS EvVar
739 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
741 newDictVar :: Class -> [TcType] -> TcS EvVar
742 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
747 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
748 -- In a call (isGoodRecEv ev wv), we are considering solving wv
749 -- using some term that involves ev, such as:
750 -- by setting wv = ev
751 -- or wv = EvCast x |> ev
753 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
754 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
755 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
757 -- Guarded means: more instance calls than superclass selections. We
758 -- compute this by chasing the evidence, adding +1 for every instance
759 -- call (constructor) and -1 for every superclass selection (destructor).
761 -- See Note [Superclasses and recursive dictionaries] in TcInteract
762 isGoodRecEv ev_var (WantedEvVar wv _)
763 = do { tc_evbinds <- getTcEvBindsBag
764 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
765 ; return $ case mb of
767 Just min_guardedness -> min_guardedness > 0
770 where chase_ev_var :: EvBindMap -- Evidence binds
771 -> EvVar -- Target variable whose gravity we want to return
772 -> Int -- Current gravity
773 -> [EvVar] -- Visited nodes
774 -> EvVar -- Current node
776 chase_ev_var assocs trg curr_grav visited orig
777 | trg == orig = return $ Just curr_grav
778 | orig `elem` visited = return $ Nothing
779 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
780 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
782 {- No longer needed: evidence is in the EvBinds
783 | isTcTyVar orig && isMetaTyVar orig
784 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
785 ; case meta_details of
786 Flexi -> return Nothing
787 Indirect tyco -> chase_ev assocs trg curr_grav
788 (orig:visited) (EvCoercion tyco)
791 | otherwise = return Nothing
793 chase_ev assocs trg curr_grav visited (EvId v)
794 = chase_ev_var assocs trg curr_grav visited v
795 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
796 = chase_ev_var assocs trg (curr_grav-1) visited d_id
797 chase_ev assocs trg curr_grav visited (EvCast v co)
798 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
799 ; m2 <- chase_co assocs trg curr_grav visited co
800 ; return (comb_chase_res Nothing [m1,m2]) }
802 chase_ev assocs trg curr_grav visited (EvCoercion co)
803 = chase_co assocs trg curr_grav visited co
804 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
805 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
806 ; return (comb_chase_res Nothing chase_results) }
808 chase_co assocs trg curr_grav visited co
809 = -- Look for all the coercion variables in the coercion
810 -- chase them, and combine the results. This is OK since the
811 -- coercion will not contain any superclass terms -- anything
812 -- that involves dictionaries will be bound in assocs.
813 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
815 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
816 ; return (comb_chase_res Nothing chase_results) }
818 comb_chase_res f [] = f
819 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
820 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
821 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
824 -- Matching and looking up classes and family instances
825 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
827 data MatchInstResult mi
828 = MatchInstNo -- No matching instance
829 | MatchInstSingle mi -- Single matching instance
830 | MatchInstMany -- Multiple matching instances
833 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
834 -- Look up a class constraint in the instance environment
836 = do { let pred = mkClassPred clas tys
837 ; instEnvs <- getInstEnvs
838 ; case lookupInstEnv instEnvs clas tys of {
839 ([], unifs) -- Nothing matches
840 -> do { traceTcS "matchClass not matching"
841 (vcat [ text "dict" <+> ppr pred,
842 text "unifs" <+> ppr unifs ])
845 ([(ispec, inst_tys)], []) -- A single match
846 -> do { let dfun_id = is_dfun ispec
847 ; traceTcS "matchClass success"
848 (vcat [text "dict" <+> ppr pred,
849 text "witness" <+> ppr dfun_id
850 <+> ppr (idType dfun_id) ])
851 -- Record that this dfun is needed
852 ; record_dfun_usage dfun_id
853 ; return $ MatchInstSingle (dfun_id, inst_tys)
855 (matches, unifs) -- More than one matches
856 -> do { traceTcS "matchClass multiple matches, deferring choice"
857 (vcat [text "dict" <+> ppr pred,
858 text "matches" <+> ppr matches,
859 text "unifs" <+> ppr unifs])
860 ; return MatchInstMany
864 where record_dfun_usage :: Id -> TcS ()
865 record_dfun_usage dfun_id
866 = do { hsc_env <- getTopEnv
867 ; let dfun_name = idName dfun_id
868 dfun_mod = ASSERT( isExternalName dfun_name )
870 ; if isInternalName dfun_name || -- Internal name => defined in this module
871 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
872 then return () -- internal, or in another package
873 else do updInstUses dfun_id
876 updInstUses :: Id -> TcS ()
878 = do { tcg_env <- getGblEnv
879 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
880 (`addOneToNameSet` idName dfun_id)
885 -> TcS (MatchInstResult (TyCon, [Type]))
887 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
889 Nothing -> return MatchInstNo
890 Just res -> return $ MatchInstSingle res
891 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
892 -- multiple matches. Check.
896 zonkTcTypeTcS :: TcType -> TcS TcType
897 -- Zonk through the TyBinds of the Tcs Monad
899 = do { subst <- getTcSTyBindsMap >>= return . varEnvElts
900 ; let (dom,rng) = unzip subst
901 apply_once = substTyWith dom rng
902 ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ]
903 ; return (substTyWith dom rng_idemp ty) }
910 -- Functional dependencies, instantiation of equations
911 -------------------------------------------------------
913 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
915 mkWantedFunDepEqns _ [] = return []
916 mkWantedFunDepEqns loc eqns
917 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
918 ; wevvars <- mapM to_work_item eqns
919 ; return $ concat wevvars }
921 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
922 to_work_item ((qtvs, pairs), _, _)
923 = do { let tvs = varSetElems qtvs
924 ; tvs' <- mapM newFlexiTcS tvs
925 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
926 ; mapM (do_one subst) pairs }
928 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
929 sty2 = substTy subst ty2
930 ; ev <- newWantedCoVar sty1 sty2
931 ; return (WantedEvVar ev loc) }
933 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
934 pprEquationDoc (eqn, (p1, _), (p2, _))
935 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]