2 -- Type definitions for the constraint solver
5 -- Canonical constraints
6 CanonicalCts, emptyCCan, andCCan, andCCans,
7 singleCCan, extendCCans, isEmptyCCan, isCTyEqCan,
8 isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
10 CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
11 mkWantedConstraints, deCanonicaliseWanted,
12 makeGivens, makeSolvedByInst,
14 CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst,
15 isGivenCt, isWantedCt,
19 combineCtLoc, mkGivenFlavor,
21 TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
22 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
23 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
25 -- Creation of evidence variables
27 newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
28 newIPVar, newDictVar, newKindConstraint,
30 -- Setting evidence variables
31 setWantedCoBind, setDerivedCoBind,
32 setIPBind, setDictBind, setEvBind,
38 getInstEnvs, getFamInstEnvs, -- Getting the environments
39 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
40 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
43 newFlattenSkolemTy, -- Flatten skolems
46 instDFunTypes, -- Instantiation
51 zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad
56 isTouchableMetaTyVar_InRange,
58 getDefaultInfo, getDynFlags,
60 matchClass, matchFam, MatchInstResult (..),
63 pprEq, -- Smaller utils, re-exported from TcM
64 -- TODO (DV): these are only really used in the
65 -- instance matcher in TcSimplify. I am wondering
66 -- if the whole instance matcher simply belongs
70 mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps
74 #include "HsVersions.h"
84 import NameSet ( addOneToNameSet )
86 import qualified TcRnMonad as TcM
87 import qualified TcMType as TcM
88 import qualified TcEnv as TcM
89 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
108 import HsBinds -- for TcEvBinds stuff
118 %************************************************************************
120 %* Canonical constraints *
122 %* These are the constraints the low-level simplifier works with *
124 %************************************************************************
127 -- Types without any type functions inside. However, note that xi
128 -- types CAN contain unexpanded type synonyms; however, the
129 -- (transitive) expansions of those type synonyms will not contain any
131 type Xi = Type -- In many comments, "xi" ranges over Xi
133 type CanonicalCts = Bag CanonicalCt
136 -- Atomic canonical constraints
137 = CDictCan { -- e.g. Num xi
139 cc_flavor :: CtFlavor,
144 | CIPCan { -- ?x::tau
145 -- See note [Canonical implicit parameter constraints].
147 cc_flavor :: CtFlavor,
148 cc_ip_nm :: IPName Name,
149 cc_ip_ty :: TcTauType
152 | CTyEqCan { -- tv ~ xi (recall xi means function free)
154 -- * tv not in tvs(xi) (occurs check)
155 -- * If constraint is given then typeKind xi `compatKind` typeKind tv
156 -- See Note [Spontaneous solving and kind compatibility]
157 -- * If 'xi' is a flatten skolem then 'tv' can only be:
158 -- - a flatten skolem or a unification variable
159 -- i.e. equalities prefer flatten skolems in their LHS
160 -- See Note [Loopy Spontaneous Solving, Example 4]
161 -- Also related to [Flatten Skolem Equivalence Classes]
163 cc_flavor :: CtFlavor,
168 | CFunEqCan { -- F xis ~ xi
169 -- Invariant: * isSynFamilyTyCon cc_fun
170 -- * cc_rhs is not a touchable unification variable
171 -- See Note [No touchables as FunEq RHS]
172 -- * If constraint is given then
173 -- typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs
175 cc_flavor :: CtFlavor,
176 cc_fun :: TyCon, -- A type function
177 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
178 cc_rhs :: Xi -- *never* over-saturated (because if so
179 -- we should have decomposed)
183 compatKind :: Kind -> Kind -> Bool
184 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
186 makeGivens :: CanonicalCts -> CanonicalCts
187 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
188 -- The UnkSkol doesn't matter because these givens are
189 -- not contradictory (else we'd have rejected them already)
191 makeSolvedByInst :: CanonicalCt -> CanonicalCt
192 -- Record that a constraint is now solved
194 -- Given, Derived -> no-op
196 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
199 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
200 mkWantedConstraints flats implics
201 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
203 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
204 deCanonicaliseWanted ct
205 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
206 let Wanted loc = cc_flavor ct
207 in WantedEvVar (cc_id ct) loc
209 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
210 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
211 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
212 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
213 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
215 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
216 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
217 tyVarsOfCDict _ct = emptyVarSet
219 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
220 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
222 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
223 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
225 instance Outputable CanonicalCt where
226 ppr (CDictCan d fl cls tys)
227 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
228 ppr (CIPCan ip fl ip_nm ty)
229 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
230 ppr (CTyEqCan co fl tv ty)
231 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
232 ppr (CFunEqCan co fl tc tys ty)
233 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
237 Note [No touchables as FunEq RHS]
238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
239 Notice that (F xis ~ beta), where beta is an touchable unification
240 variable, is not canonical. Why?
241 * If (F xis ~ beta) was the only wanted constraint, we'd
242 definitely want to spontaneously-unify it
244 * But suppose we had an earlier wanted (beta ~ Int), and
245 have already spontaneously unified it. Then we have an
246 identity given (id : beta ~ Int) in the inert set.
248 * But (F xis ~ beta) does not react with that given (because we
249 don't subsitute on the RHS of a function equality). So there's a
250 serious danger that we'd spontaneously unify it a second time.
256 Note [Canonical implicit parameter constraints]
257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
258 The type in a canonical implicit parameter constraint doesn't need to
259 be a xi (type-function-free type) since we can defer the flattening
260 until checking this type for equality with another type. If we
261 encounter two IP constraints with the same name, they MUST have the
262 same type, and at that point we can generate a flattened equality
263 constraint between the types. (On the other hand, the types in two
264 class constraints for the same class MAY be equal, so they need to be
265 flattened in the first place to facilitate comparing them.)
268 singleCCan :: CanonicalCt -> CanonicalCts
271 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
274 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
275 extendCCans = snocBag
277 andCCans :: [CanonicalCts] -> CanonicalCts
278 andCCans = unionManyBags
280 emptyCCan :: CanonicalCts
283 isEmptyCCan :: CanonicalCts -> Bool
284 isEmptyCCan = isEmptyBag
286 isCTyEqCan :: CanonicalCt -> Bool
287 isCTyEqCan (CTyEqCan {}) = True
288 isCTyEqCan (CFunEqCan {}) = False
291 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
292 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
293 isCDictCan_Maybe _ = Nothing
295 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
296 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
297 isCIPCan_Maybe _ = Nothing
299 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
300 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
301 isCFunEqCan_Maybe _ = Nothing
305 %************************************************************************
308 The "flavor" of a canonical constraint
310 %************************************************************************
314 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
315 | Derived WantedLoc DerivedOrig
316 -- We have evidence for this constraint in TcEvBinds;
317 -- *however* this evidence can contain wanteds, so
318 -- it's valid only provisionally to the solution of
320 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
322 data DerivedOrig = DerSC | DerInst
323 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
324 -- solved wanteds from instances.
326 instance Outputable CtFlavor where
327 ppr (Given _) = ptext (sLit "[Given]")
328 ppr (Wanted _) = ptext (sLit "[Wanted]")
329 ppr (Derived {}) = ptext (sLit "[Derived]")
331 isWanted :: CtFlavor -> Bool
332 isWanted (Wanted {}) = True
335 isGiven :: CtFlavor -> Bool
336 isGiven (Given {}) = True
339 isDerived :: CtFlavor -> Bool
340 isDerived (Derived {}) = True
343 isDerivedSC :: CtFlavor -> Bool
344 isDerivedSC (Derived _ DerSC) = True
345 isDerivedSC _ = False
347 isDerivedByInst :: CtFlavor -> Bool
348 isDerivedByInst (Derived _ DerInst) = True
349 isDerivedByInst _ = False
351 isWantedCt :: CanonicalCt -> Bool
352 isWantedCt ct = isWanted (cc_flavor ct)
353 isGivenCt :: CanonicalCt -> Bool
354 isGivenCt ct = isGiven (cc_flavor ct)
356 canSolve :: CtFlavor -> CtFlavor -> Bool
357 -- canSolve ctid1 ctid2
358 -- The constraint ctid1 can be used to solve ctid2
359 -- "to solve" means a reaction where the active parts of the two constraints match.
360 -- active(F xis ~ xi) = F xis
361 -- active(tv ~ xi) = tv
362 -- active(D xis) = D xis
363 -- active(IP nm ty) = nm
364 -----------------------------------------
365 canSolve (Given {}) _ = True
366 canSolve (Derived {}) (Wanted {}) = True
367 canSolve (Derived {}) (Derived {}) = True
368 canSolve (Wanted {}) (Wanted {}) = True
371 canRewrite :: CtFlavor -> CtFlavor -> Bool
372 -- canRewrite ctid1 ctid2
373 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
374 canRewrite = canSolve
376 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
377 -- Precondition: At least one of them should be wanted
378 combineCtLoc (Wanted loc) _ = loc
379 combineCtLoc _ (Wanted loc) = loc
380 combineCtLoc (Derived loc _) _ = loc
381 combineCtLoc _ (Derived loc _) = loc
382 combineCtLoc _ _ = panic "combineCtLoc: both given"
384 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
385 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
386 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
387 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
391 %************************************************************************
393 %* The TcS solver monad *
395 %************************************************************************
399 The TcS monad is a weak form of the main Tc monad
403 * allocate new variables
404 * fill in evidence variables
406 Filling in a dictionary evidence variable means to create a binding
407 for it, so TcS carries a mutable location where the binding can be
408 added. This is initialised from the innermost implication constraint.
413 tcs_ev_binds :: EvBindsVar,
416 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
417 -- Global type bindings
419 tcs_context :: SimplContext,
421 tcs_untch :: Untouchables
425 = SimplInfer -- Inferring type of a let-bound thing
426 | SimplRuleLhs -- Inferring type of a RULE lhs
427 | SimplInteractive -- Inferring type at GHCi prompt
428 | SimplCheck -- Checking a type signature or RULE rhs
430 instance Outputable SimplContext where
431 ppr SimplInfer = ptext (sLit "SimplInfer")
432 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
433 ppr SimplInteractive = ptext (sLit "SimplInteractive")
434 ppr SimplCheck = ptext (sLit "SimplCheck")
436 isInteractive :: SimplContext -> Bool
437 isInteractive SimplInteractive = True
438 isInteractive _ = False
440 simplEqsOnly :: SimplContext -> Bool
441 -- Simplify equalities only, not dictionaries
442 -- This is used for the LHS of rules; ee
443 -- Note [Simplifying RULE lhs constraints] in TcSimplify
444 simplEqsOnly SimplRuleLhs = True
445 simplEqsOnly _ = False
447 performDefaulting :: SimplContext -> Bool
448 performDefaulting SimplInfer = False
449 performDefaulting SimplRuleLhs = False
450 performDefaulting SimplInteractive = True
451 performDefaulting SimplCheck = True
454 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
456 instance Functor TcS where
457 fmap f m = TcS $ fmap f . unTcS m
459 instance Monad TcS where
460 return x = TcS (\_ -> return x)
461 fail err = TcS (\_ -> fail err)
462 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
464 -- Basic functionality
465 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
466 wrapTcS :: TcM a -> TcS a
467 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
468 -- and TcS is supposed to have limited functionality
469 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
471 wrapErrTcS :: TcM a -> TcS a
472 -- The thing wrapped should just fail
473 -- There's no static check; it's up to the user
474 -- Having a variant for each error message is too painful
477 wrapWarnTcS :: TcM a -> TcS a
478 -- The thing wrapped should just add a warning, or no-op
479 -- There's no static check; it's up to the user
480 wrapWarnTcS = wrapTcS
482 failTcS, panicTcS :: SDoc -> TcS a
483 failTcS = wrapTcS . TcM.failWith
484 panicTcS doc = pprPanic "TcCanonical" doc
486 traceTcS :: String -> SDoc -> TcS ()
487 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
489 traceTcS0 :: String -> SDoc -> TcS ()
490 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
492 runTcS :: SimplContext
493 -> Untouchables -- Untouchables
494 -> TcS a -- What to run
495 -> TcM (a, Bag EvBind)
496 runTcS context untouch tcs
497 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
498 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
499 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
500 , tcs_ty_binds = ty_binds_var
501 , tcs_context = context
502 , tcs_untch = untouch }
504 -- Run the computation
505 ; res <- unTcS tcs env
507 -- Perform the type unifications required
508 ; ty_binds <- TcM.readTcRef ty_binds_var
509 ; mapM_ do_unification (varEnvElts ty_binds)
512 ; ev_binds <- TcM.readTcRef evb_ref
513 ; return (res, evBindMapBinds ev_binds) }
515 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
518 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
519 nestImplicTcS ref untch (TcS thing_inside)
520 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
522 nest_env = TcSEnv { tcs_ev_binds = ref
523 , tcs_ty_binds = ty_binds
525 , tcs_context = ctxtUnderImplic ctxt }
527 thing_inside nest_env
529 recoverTcS :: TcS a -> TcS a -> TcS a
530 recoverTcS (TcS recovery_code) (TcS thing_inside)
532 TcM.recoverM (recovery_code env) (thing_inside env)
534 ctxtUnderImplic :: SimplContext -> SimplContext
535 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
536 ctxtUnderImplic SimplRuleLhs = SimplCheck
537 ctxtUnderImplic ctxt = ctxt
539 tryTcS :: TcS a -> TcS a
540 -- Like runTcS, but from within the TcS monad
541 -- Ignore all the evidence generated, and do not affect caller's evidence!
543 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
544 ; ev_binds_var <- TcM.newTcEvBinds
545 ; let env1 = env { tcs_ev_binds = ev_binds_var
546 , tcs_ty_binds = ty_binds_var }
550 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
552 getDynFlags :: TcS DynFlags
553 getDynFlags = wrapTcS TcM.getDOpts
555 getTcSContext :: TcS SimplContext
556 getTcSContext = TcS (return . tcs_context)
558 getTcEvBinds :: TcS EvBindsVar
559 getTcEvBinds = TcS (return . tcs_ev_binds)
561 getUntouchables :: TcS Untouchables
562 getUntouchables = TcS (return . tcs_untch)
564 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
565 getTcSTyBinds = TcS (return . tcs_ty_binds)
567 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
568 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
571 getTcEvBindsBag :: TcS EvBindMap
573 = do { EvBindsVar ev_ref _ <- getTcEvBinds
574 ; wrapTcS $ TcM.readTcRef ev_ref }
576 setWantedCoBind :: CoVar -> Coercion -> TcS ()
577 setWantedCoBind cv co
578 = setEvBind cv (EvCoercion co)
579 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
581 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
582 setDerivedCoBind cv co
583 = setEvBind cv (EvCoercion co)
585 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
586 -- Add a type binding
587 setWantedTyBind tv ty
588 = do { ref <- getTcSTyBinds
590 do { ty_binds <- TcM.readTcRef ref
591 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
593 setIPBind :: EvVar -> EvTerm -> TcS ()
594 setIPBind = setEvBind
596 setDictBind :: EvVar -> EvTerm -> TcS ()
597 setDictBind = setEvBind
599 setEvBind :: EvVar -> EvTerm -> TcS ()
602 = do { tc_evbinds <- getTcEvBinds
603 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
605 newTcEvBindsTcS :: TcS EvBindsVar
606 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
608 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
609 warnTcS loc warn_if doc
610 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
611 | otherwise = return ()
613 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
615 = do { ctxt <- getTcSContext
616 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
617 ; return (ctxt, tys, flags) }
619 -- Just get some environments needed for instance looking up and matching
620 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
622 getInstEnvs :: TcS (InstEnv, InstEnv)
623 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
625 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
626 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
628 getTopEnv :: TcS HscEnv
629 getTopEnv = wrapTcS $ TcM.getTopEnv
631 getGblEnv :: TcS TcGblEnv
632 getGblEnv = wrapTcS $ TcM.getGblEnv
634 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
635 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
637 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
638 checkWellStagedDFun pred dfun_id loc
639 = wrapTcS $ TcM.setCtLoc loc $
640 do { use_stage <- TcM.getStage
641 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
643 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
644 bind_lvl = TcM.topIdLvl dfun_id
646 pprEq :: TcType -> TcType -> SDoc
647 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
649 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
650 isTouchableMetaTyVar tv
651 = do { untch <- getUntouchables
652 ; return $ isTouchableMetaTyVar_InRange untch tv }
654 isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool
655 isTouchableMetaTyVar_InRange untch tv
656 = case tcTyVarDetails tv of
657 MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables]
658 MetaTv {} -> inTouchableRange untch tv
665 Note [Touchable meta type variables]
666 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
667 Meta type variables allocated *by the constraint solver itself* are always
669 instance C a b => D [a] where...
670 if we use this instance declaration we "make up" a fresh meta type
671 variable for 'b', which we must later guess. (Perhaps C has a
672 functional dependency.) But since we aren't in the constraint *generator*
673 we can't allocate a Unique in the touchable range for this implication
674 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
679 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
681 newFlattenSkolemTy :: TcType -> TcS TcType
682 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
684 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
685 newFlattenSkolemTyVar ty
686 = wrapTcS $ do { uniq <- TcM.newUnique
687 ; let name = mkSysTvName uniq (fsLit "f")
688 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
691 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
693 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
694 instDFunTypes mb_inst_tys
695 = mapM inst_tv mb_inst_tys
697 inst_tv :: Either TyVar TcType -> TcS Type
698 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
699 inst_tv (Right ty) = return ty
701 instDFunConstraints :: TcThetaType -> TcS [EvVar]
702 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
705 -- newFlexiTcS :: TyVar -> TcS TcTyVar
706 -- -- Make a TcsTv meta tyvar; it is always touchable,
707 -- -- but we are supposed to guess its instantiation
708 -- -- See Note [Touchable meta type variables]
709 -- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
711 newFlexiTcS :: TyVar -> TcS TcTyVar
712 -- Like TcM.instMetaTyVar but the variable that is created is always
713 -- touchable; we are supposed to guess its instantiation.
714 -- See Note [Touchable meta type variables]
715 newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
717 newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)
718 -- Create new wanted CoVar that constrains the type to have the specified kind.
719 newKindConstraint tv knd
720 = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd
721 ; let ty_k = mkTyVarTy tv_k
722 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
723 ; return (co_var, ty_k) }
725 newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
726 newFlexiTcSHelper tvname tvkind
728 do { uniq <- TcM.newUnique
729 ; ref <- TcM.newMutVar Flexi
730 ; let name = setNameUnique tvname uniq
732 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
734 -- Superclasses and recursive dictionaries
735 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
737 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
738 newGivOrDerEvVar pty evtrm
739 = do { ev <- wrapTcS $ TcM.newEvVar pty
743 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
744 -- Note we create immutable variables for given or derived, since we
745 -- must bind them to TcEvBinds (because their evidence may involve
746 -- superclasses). However we should be able to override existing
747 -- 'derived' evidence, even in TcEvBinds
748 newGivOrDerCoVar ty1 ty2 co
749 = do { cv <- newCoVar ty1 ty2
750 ; setEvBind cv (EvCoercion co)
753 newWantedCoVar :: TcType -> TcType -> TcS EvVar
754 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
757 newCoVar :: TcType -> TcType -> TcS EvVar
758 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
760 newIPVar :: IPName Name -> TcType -> TcS EvVar
761 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
763 newDictVar :: Class -> [TcType] -> TcS EvVar
764 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
769 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
770 -- In a call (isGoodRecEv ev wv), we are considering solving wv
771 -- using some term that involves ev, such as:
772 -- by setting wv = ev
773 -- or wv = EvCast x |> ev
775 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
776 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
777 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
779 -- Guarded means: more instance calls than superclass selections. We
780 -- compute this by chasing the evidence, adding +1 for every instance
781 -- call (constructor) and -1 for every superclass selection (destructor).
783 -- See Note [Superclasses and recursive dictionaries] in TcInteract
784 isGoodRecEv ev_var (WantedEvVar wv _)
785 = do { tc_evbinds <- getTcEvBindsBag
786 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
787 ; return $ case mb of
789 Just min_guardedness -> min_guardedness > 0
792 where chase_ev_var :: EvBindMap -- Evidence binds
793 -> EvVar -- Target variable whose gravity we want to return
794 -> Int -- Current gravity
795 -> [EvVar] -- Visited nodes
796 -> EvVar -- Current node
798 chase_ev_var assocs trg curr_grav visited orig
799 | trg == orig = return $ Just curr_grav
800 | orig `elem` visited = return $ Nothing
801 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
802 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
804 {- No longer needed: evidence is in the EvBinds
805 | isTcTyVar orig && isMetaTyVar orig
806 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
807 ; case meta_details of
808 Flexi -> return Nothing
809 Indirect tyco -> chase_ev assocs trg curr_grav
810 (orig:visited) (EvCoercion tyco)
813 | otherwise = return Nothing
815 chase_ev assocs trg curr_grav visited (EvId v)
816 = chase_ev_var assocs trg curr_grav visited v
817 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
818 = chase_ev_var assocs trg (curr_grav-1) visited d_id
819 chase_ev assocs trg curr_grav visited (EvCast v co)
820 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
821 ; m2 <- chase_co assocs trg curr_grav visited co
822 ; return (comb_chase_res Nothing [m1,m2]) }
824 chase_ev assocs trg curr_grav visited (EvCoercion co)
825 = chase_co assocs trg curr_grav visited co
826 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
827 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
828 ; return (comb_chase_res Nothing chase_results) }
830 chase_co assocs trg curr_grav visited co
831 = -- Look for all the coercion variables in the coercion
832 -- chase them, and combine the results. This is OK since the
833 -- coercion will not contain any superclass terms -- anything
834 -- that involves dictionaries will be bound in assocs.
835 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
837 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
838 ; return (comb_chase_res Nothing chase_results) }
840 comb_chase_res f [] = f
841 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
842 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
843 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
846 -- Matching and looking up classes and family instances
847 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
849 data MatchInstResult mi
850 = MatchInstNo -- No matching instance
851 | MatchInstSingle mi -- Single matching instance
852 | MatchInstMany -- Multiple matching instances
855 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
856 -- Look up a class constraint in the instance environment
858 = do { let pred = mkClassPred clas tys
859 ; instEnvs <- getInstEnvs
860 ; case lookupInstEnv instEnvs clas tys of {
861 ([], unifs) -- Nothing matches
862 -> do { traceTcS "matchClass not matching"
863 (vcat [ text "dict" <+> ppr pred,
864 text "unifs" <+> ppr unifs ])
867 ([(ispec, inst_tys)], []) -- A single match
868 -> do { let dfun_id = is_dfun ispec
869 ; traceTcS "matchClass success"
870 (vcat [text "dict" <+> ppr pred,
871 text "witness" <+> ppr dfun_id
872 <+> ppr (idType dfun_id) ])
873 -- Record that this dfun is needed
874 ; record_dfun_usage dfun_id
875 ; return $ MatchInstSingle (dfun_id, inst_tys)
877 (matches, unifs) -- More than one matches
878 -> do { traceTcS "matchClass multiple matches, deferring choice"
879 (vcat [text "dict" <+> ppr pred,
880 text "matches" <+> ppr matches,
881 text "unifs" <+> ppr unifs])
882 ; return MatchInstMany
886 where record_dfun_usage :: Id -> TcS ()
887 record_dfun_usage dfun_id
888 = do { hsc_env <- getTopEnv
889 ; let dfun_name = idName dfun_id
890 dfun_mod = ASSERT( isExternalName dfun_name )
892 ; if isInternalName dfun_name || -- Internal name => defined in this module
893 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
894 then return () -- internal, or in another package
895 else do updInstUses dfun_id
898 updInstUses :: Id -> TcS ()
900 = do { tcg_env <- getGblEnv
901 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
902 (`addOneToNameSet` idName dfun_id)
907 -> TcS (MatchInstResult (TyCon, [Type]))
909 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
911 Nothing -> return MatchInstNo
912 Just res -> return $ MatchInstSingle res
913 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
914 -- multiple matches. Check.
918 zonkTcTypeTcS :: TcType -> TcS TcType
919 -- Zonk through the TyBinds of the Tcs Monad
921 = do { subst <- getTcSTyBindsMap >>= return . varEnvElts
922 ; let (dom,rng) = unzip subst
923 apply_once = substTyWith dom rng
924 ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ]
925 ; return (substTyWith dom rng_idemp ty) }
932 -- Functional dependencies, instantiation of equations
933 -------------------------------------------------------
935 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
937 mkWantedFunDepEqns _ [] = return []
938 mkWantedFunDepEqns loc eqns
939 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
940 ; wevvars <- mapM to_work_item eqns
941 ; return $ concat wevvars }
943 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
944 to_work_item ((qtvs, pairs), _, _)
945 = do { let tvs = varSetElems qtvs
946 ; tvs' <- mapM newFlexiTcS tvs
947 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
948 ; mapM (do_one subst) pairs }
950 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
951 sty2 = substTy subst ty2
952 ; ev <- newWantedCoVar sty1 sty2
953 ; return (WantedEvVar ev loc) }
955 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
956 pprEquationDoc (eqn, (p1, _), (p2, _))
957 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]