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,
13 isGivenCt, isWantedCt,
17 combineCtLoc, mkGivenFlavor,
19 TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
20 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
21 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
23 -- Creation of evidence variables
25 newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
26 newIPVar, newDictVar, newKindConstraint,
28 -- Setting evidence variables
29 setWantedCoBind, setDerivedCoBind,
30 setIPBind, setDictBind, setEvBind,
36 getInstEnvs, getFamInstEnvs, -- Getting the environments
37 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
38 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
41 newFlattenSkolemTy, -- Flatten skolems
44 instDFunTypes, -- Instantiation
49 zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad
54 isTouchableMetaTyVar_InRange,
56 getDefaultInfo, getDynFlags,
58 matchClass, matchFam, MatchInstResult (..),
61 pprEq, -- Smaller utils, re-exported from TcM
62 -- TODO (DV): these are only really used in the
63 -- instance matcher in TcSimplify. I am wondering
64 -- if the whole instance matcher simply belongs
68 mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps
72 #include "HsVersions.h"
82 import NameSet ( addOneToNameSet )
84 import qualified TcRnMonad as TcM
85 import qualified TcMType as TcM
86 import qualified TcEnv as TcM
87 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
106 import HsBinds -- for TcEvBinds stuff
116 %************************************************************************
118 %* Canonical constraints *
120 %* These are the constraints the low-level simplifier works with *
122 %************************************************************************
125 -- Types without any type functions inside. However, note that xi
126 -- types CAN contain unexpanded type synonyms; however, the
127 -- (transitive) expansions of those type synonyms will not contain any
129 type Xi = Type -- In many comments, "xi" ranges over Xi
131 type CanonicalCts = Bag CanonicalCt
134 -- Atomic canonical constraints
135 = CDictCan { -- e.g. Num xi
137 cc_flavor :: CtFlavor,
142 | CIPCan { -- ?x::tau
143 -- See note [Canonical implicit parameter constraints].
145 cc_flavor :: CtFlavor,
146 cc_ip_nm :: IPName Name,
147 cc_ip_ty :: TcTauType
150 | CTyEqCan { -- tv ~ xi (recall xi means function free)
152 -- * tv not in tvs(xi) (occurs check)
153 -- * If constraint is given then typeKind xi `compatKind` typeKind tv
154 -- See Note [Spontaneous solving and kind compatibility]
155 -- * If 'xi' is a flatten skolem then 'tv' can only be:
156 -- - a flatten skolem or a unification variable
157 -- i.e. equalities prefer flatten skolems in their LHS
158 -- See Note [Loopy Spontaneous Solving, Example 4]
159 -- Also related to [Flatten Skolem Equivalence Classes]
161 cc_flavor :: CtFlavor,
166 | CFunEqCan { -- F xis ~ xi
167 -- Invariant: * isSynFamilyTyCon cc_fun
168 -- * cc_rhs is not a touchable unification variable
169 -- See Note [No touchables as FunEq RHS]
170 -- * If constraint is given then
171 -- typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs
173 cc_flavor :: CtFlavor,
174 cc_fun :: TyCon, -- A type function
175 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
176 cc_rhs :: Xi -- *never* over-saturated (because if so
177 -- we should have decomposed)
181 compatKind :: Kind -> Kind -> Bool
182 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
184 makeGivens :: CanonicalCts -> CanonicalCts
185 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
186 -- The UnkSkol doesn't matter because these givens are
187 -- not contradictory (else we'd have rejected them already)
189 makeSolvedByInst :: CanonicalCt -> CanonicalCt
190 -- Record that a constraint is now solved
192 -- Given, Derived -> no-op
194 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
197 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
198 mkWantedConstraints flats implics
199 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
201 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
202 deCanonicaliseWanted ct
203 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
204 let Wanted loc = cc_flavor ct
205 in WantedEvVar (cc_id ct) loc
207 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
208 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
209 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
210 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
211 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
213 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
214 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
215 tyVarsOfCDict _ct = emptyVarSet
217 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
218 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
220 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
221 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
223 instance Outputable CanonicalCt where
224 ppr (CDictCan d fl cls tys)
225 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
226 ppr (CIPCan ip fl ip_nm ty)
227 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
228 ppr (CTyEqCan co fl tv ty)
229 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
230 ppr (CFunEqCan co fl tc tys ty)
231 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
235 Note [No touchables as FunEq RHS]
236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
237 Notice that (F xis ~ beta), where beta is an touchable unification
238 variable, is not canonical. Why?
239 * If (F xis ~ beta) was the only wanted constraint, we'd
240 definitely want to spontaneously-unify it
242 * But suppose we had an earlier wanted (beta ~ Int), and
243 have already spontaneously unified it. Then we have an
244 identity given (id : beta ~ Int) in the inert set.
246 * But (F xis ~ beta) does not react with that given (because we
247 don't subsitute on the RHS of a function equality). So there's a
248 serious danger that we'd spontaneously unify it a second time.
254 Note [Canonical implicit parameter constraints]
255 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
256 The type in a canonical implicit parameter constraint doesn't need to
257 be a xi (type-function-free type) since we can defer the flattening
258 until checking this type for equality with another type. If we
259 encounter two IP constraints with the same name, they MUST have the
260 same type, and at that point we can generate a flattened equality
261 constraint between the types. (On the other hand, the types in two
262 class constraints for the same class MAY be equal, so they need to be
263 flattened in the first place to facilitate comparing them.)
266 singleCCan :: CanonicalCt -> CanonicalCts
269 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
272 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
273 extendCCans = snocBag
275 andCCans :: [CanonicalCts] -> CanonicalCts
276 andCCans = unionManyBags
278 emptyCCan :: CanonicalCts
281 isEmptyCCan :: CanonicalCts -> Bool
282 isEmptyCCan = isEmptyBag
284 isTyEqCCan :: CanonicalCt -> Bool
285 isTyEqCCan (CTyEqCan {}) = True
286 isTyEqCCan (CFunEqCan {}) = False
291 %************************************************************************
294 The "flavor" of a canonical constraint
296 %************************************************************************
300 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
301 | Derived WantedLoc DerivedOrig
302 -- We have evidence for this constraint in TcEvBinds;
303 -- *however* this evidence can contain wanteds, so
304 -- it's valid only provisionally to the solution of
306 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
308 data DerivedOrig = DerSC | DerInst
309 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
310 -- solved wanteds from instances.
312 instance Outputable CtFlavor where
313 ppr (Given _) = ptext (sLit "[Given]")
314 ppr (Wanted _) = ptext (sLit "[Wanted]")
315 ppr (Derived {}) = ptext (sLit "[Derived]")
317 isWanted :: CtFlavor -> Bool
318 isWanted (Wanted {}) = True
321 isGiven :: CtFlavor -> Bool
322 isGiven (Given {}) = True
325 isDerived :: CtFlavor -> Bool
326 isDerived (Derived {}) = True
329 isDerivedSC :: CtFlavor -> Bool
330 isDerivedSC (Derived _ DerSC) = True
331 isDerivedSC _ = False
333 isDerivedByInst :: CtFlavor -> Bool
334 isDerivedByInst (Derived _ DerInst) = True
335 isDerivedByInst _ = False
337 isWantedCt :: CanonicalCt -> Bool
338 isWantedCt ct = isWanted (cc_flavor ct)
339 isGivenCt :: CanonicalCt -> Bool
340 isGivenCt ct = isGiven (cc_flavor ct)
342 canSolve :: CtFlavor -> CtFlavor -> Bool
343 -- canSolve ctid1 ctid2
344 -- The constraint ctid1 can be used to solve ctid2
345 -- "to solve" means a reaction where the active parts of the two constraints match.
346 -- active(F xis ~ xi) = F xis
347 -- active(tv ~ xi) = tv
348 -- active(D xis) = D xis
349 -- active(IP nm ty) = nm
350 -----------------------------------------
351 canSolve (Given {}) _ = True
352 canSolve (Derived {}) (Wanted {}) = True
353 canSolve (Derived {}) (Derived {}) = True
354 canSolve (Wanted {}) (Wanted {}) = True
357 canRewrite :: CtFlavor -> CtFlavor -> Bool
358 -- canRewrite ctid1 ctid2
359 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
360 canRewrite = canSolve
362 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
363 -- Precondition: At least one of them should be wanted
364 combineCtLoc (Wanted loc) _ = loc
365 combineCtLoc _ (Wanted loc) = loc
366 combineCtLoc (Derived loc _) _ = loc
367 combineCtLoc _ (Derived loc _) = loc
368 combineCtLoc _ _ = panic "combineCtLoc: both given"
370 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
371 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
372 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
373 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
377 %************************************************************************
379 %* The TcS solver monad *
381 %************************************************************************
385 The TcS monad is a weak form of the main Tc monad
389 * allocate new variables
390 * fill in evidence variables
392 Filling in a dictionary evidence variable means to create a binding
393 for it, so TcS carries a mutable location where the binding can be
394 added. This is initialised from the innermost implication constraint.
399 tcs_ev_binds :: EvBindsVar,
402 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
403 -- Global type bindings
405 tcs_context :: SimplContext,
407 tcs_untch :: Untouchables
411 = SimplInfer -- Inferring type of a let-bound thing
412 | SimplRuleLhs -- Inferring type of a RULE lhs
413 | SimplInteractive -- Inferring type at GHCi prompt
414 | SimplCheck -- Checking a type signature or RULE rhs
416 instance Outputable SimplContext where
417 ppr SimplInfer = ptext (sLit "SimplInfer")
418 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
419 ppr SimplInteractive = ptext (sLit "SimplInteractive")
420 ppr SimplCheck = ptext (sLit "SimplCheck")
422 isInteractive :: SimplContext -> Bool
423 isInteractive SimplInteractive = True
424 isInteractive _ = False
426 simplEqsOnly :: SimplContext -> Bool
427 -- Simplify equalities only, not dictionaries
428 -- This is used for the LHS of rules; ee
429 -- Note [Simplifying RULE lhs constraints] in TcSimplify
430 simplEqsOnly SimplRuleLhs = True
431 simplEqsOnly _ = False
433 performDefaulting :: SimplContext -> Bool
434 performDefaulting SimplInfer = False
435 performDefaulting SimplRuleLhs = False
436 performDefaulting SimplInteractive = True
437 performDefaulting SimplCheck = True
440 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
442 instance Functor TcS where
443 fmap f m = TcS $ fmap f . unTcS m
445 instance Monad TcS where
446 return x = TcS (\_ -> return x)
447 fail err = TcS (\_ -> fail err)
448 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
450 -- Basic functionality
451 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
452 wrapTcS :: TcM a -> TcS a
453 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
454 -- and TcS is supposed to have limited functionality
455 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
457 wrapErrTcS :: TcM a -> TcS a
458 -- The thing wrapped should just fail
459 -- There's no static check; it's up to the user
460 -- Having a variant for each error message is too painful
463 wrapWarnTcS :: TcM a -> TcS a
464 -- The thing wrapped should just add a warning, or no-op
465 -- There's no static check; it's up to the user
466 wrapWarnTcS = wrapTcS
468 failTcS, panicTcS :: SDoc -> TcS a
469 failTcS = wrapTcS . TcM.failWith
470 panicTcS doc = pprPanic "TcCanonical" doc
472 traceTcS :: String -> SDoc -> TcS ()
473 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
475 traceTcS0 :: String -> SDoc -> TcS ()
476 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
478 runTcS :: SimplContext
479 -> Untouchables -- Untouchables
480 -> TcS a -- What to run
481 -> TcM (a, Bag EvBind)
482 runTcS context untouch tcs
483 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
484 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
485 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
486 , tcs_ty_binds = ty_binds_var
487 , tcs_context = context
488 , tcs_untch = untouch }
490 -- Run the computation
491 ; res <- unTcS tcs env
493 -- Perform the type unifications required
494 ; ty_binds <- TcM.readTcRef ty_binds_var
495 ; mapM_ do_unification (varEnvElts ty_binds)
498 ; ev_binds <- TcM.readTcRef evb_ref
499 ; return (res, evBindMapBinds ev_binds) }
501 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
504 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
505 nestImplicTcS ref untch (TcS thing_inside)
506 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
508 nest_env = TcSEnv { tcs_ev_binds = ref
509 , tcs_ty_binds = ty_binds
511 , tcs_context = ctxtUnderImplic ctxt }
513 thing_inside nest_env
515 recoverTcS :: TcS a -> TcS a -> TcS a
516 recoverTcS (TcS recovery_code) (TcS thing_inside)
518 TcM.recoverM (recovery_code env) (thing_inside env)
520 ctxtUnderImplic :: SimplContext -> SimplContext
521 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
522 ctxtUnderImplic SimplRuleLhs = SimplCheck
523 ctxtUnderImplic ctxt = ctxt
525 tryTcS :: TcS a -> TcS a
526 -- Like runTcS, but from within the TcS monad
527 -- Ignore all the evidence generated, and do not affect caller's evidence!
529 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
530 ; ev_binds_var <- TcM.newTcEvBinds
531 ; let env1 = env { tcs_ev_binds = ev_binds_var
532 , tcs_ty_binds = ty_binds_var }
536 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
538 getDynFlags :: TcS DynFlags
539 getDynFlags = wrapTcS TcM.getDOpts
541 getTcSContext :: TcS SimplContext
542 getTcSContext = TcS (return . tcs_context)
544 getTcEvBinds :: TcS EvBindsVar
545 getTcEvBinds = TcS (return . tcs_ev_binds)
547 getUntouchables :: TcS Untouchables
548 getUntouchables = TcS (return . tcs_untch)
550 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
551 getTcSTyBinds = TcS (return . tcs_ty_binds)
553 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
554 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
557 getTcEvBindsBag :: TcS EvBindMap
559 = do { EvBindsVar ev_ref _ <- getTcEvBinds
560 ; wrapTcS $ TcM.readTcRef ev_ref }
562 setWantedCoBind :: CoVar -> Coercion -> TcS ()
563 setWantedCoBind cv co
564 = setEvBind cv (EvCoercion co)
565 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
567 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
568 setDerivedCoBind cv co
569 = setEvBind cv (EvCoercion co)
571 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
572 -- Add a type binding
573 setWantedTyBind tv ty
574 = do { ref <- getTcSTyBinds
576 do { ty_binds <- TcM.readTcRef ref
577 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
579 setIPBind :: EvVar -> EvTerm -> TcS ()
580 setIPBind = setEvBind
582 setDictBind :: EvVar -> EvTerm -> TcS ()
583 setDictBind = setEvBind
585 setEvBind :: EvVar -> EvTerm -> TcS ()
588 = do { tc_evbinds <- getTcEvBinds
589 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
591 newTcEvBindsTcS :: TcS EvBindsVar
592 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
594 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
595 warnTcS loc warn_if doc
596 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
597 | otherwise = return ()
599 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
601 = do { ctxt <- getTcSContext
602 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
603 ; return (ctxt, tys, flags) }
605 -- Just get some environments needed for instance looking up and matching
606 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
608 getInstEnvs :: TcS (InstEnv, InstEnv)
609 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
611 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
612 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
614 getTopEnv :: TcS HscEnv
615 getTopEnv = wrapTcS $ TcM.getTopEnv
617 getGblEnv :: TcS TcGblEnv
618 getGblEnv = wrapTcS $ TcM.getGblEnv
620 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
621 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
623 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
624 checkWellStagedDFun pred dfun_id loc
625 = wrapTcS $ TcM.setCtLoc loc $
626 do { use_stage <- TcM.getStage
627 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
629 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
630 bind_lvl = TcM.topIdLvl dfun_id
632 pprEq :: TcType -> TcType -> SDoc
633 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
635 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
636 isTouchableMetaTyVar tv
637 = do { untch <- getUntouchables
638 ; return $ isTouchableMetaTyVar_InRange untch tv }
640 isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool
641 isTouchableMetaTyVar_InRange untch tv
642 = case tcTyVarDetails tv of
643 MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables]
644 MetaTv {} -> inTouchableRange untch tv
651 Note [Touchable meta type variables]
652 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
653 Meta type variables allocated *by the constraint solver itself* are always
655 instance C a b => D [a] where...
656 if we use this instance declaration we "make up" a fresh meta type
657 variable for 'b', which we must later guess. (Perhaps C has a
658 functional dependency.) But since we aren't in the constraint *generator*
659 we can't allocate a Unique in the touchable range for this implication
660 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
665 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
667 newFlattenSkolemTy :: TcType -> TcS TcType
668 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
670 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
671 newFlattenSkolemTyVar ty
672 = wrapTcS $ do { uniq <- TcM.newUnique
673 ; let name = mkSysTvName uniq (fsLit "f")
674 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
677 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
679 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
680 instDFunTypes mb_inst_tys
681 = mapM inst_tv mb_inst_tys
683 inst_tv :: Either TyVar TcType -> TcS Type
684 inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
685 inst_tv (Right ty) = return ty
687 instDFunConstraints :: TcThetaType -> TcS [EvVar]
688 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
691 -- newFlexiTcS :: TyVar -> TcS TcTyVar
692 -- -- Make a TcsTv meta tyvar; it is always touchable,
693 -- -- but we are supposed to guess its instantiation
694 -- -- See Note [Touchable meta type variables]
695 -- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
697 newFlexiTcS :: TyVar -> TcS TcTyVar
698 -- Like TcM.instMetaTyVar but the variable that is created is always
699 -- touchable; we are supposed to guess its instantiation.
700 -- See Note [Touchable meta type variables]
701 newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
703 newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)
704 -- Create new wanted CoVar that constrains the type to have the specified kind.
705 newKindConstraint tv knd
706 = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd
707 ; let ty_k = mkTyVarTy tv_k
708 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
709 ; return (co_var, ty_k) }
711 newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
712 newFlexiTcSHelper tvname tvkind
714 do { uniq <- TcM.newUnique
715 ; ref <- TcM.newMutVar Flexi
716 ; let name = setNameUnique tvname uniq
718 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
720 -- Superclasses and recursive dictionaries
721 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
723 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
724 newGivOrDerEvVar pty evtrm
725 = do { ev <- wrapTcS $ TcM.newEvVar pty
729 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
730 -- Note we create immutable variables for given or derived, since we
731 -- must bind them to TcEvBinds (because their evidence may involve
732 -- superclasses). However we should be able to override existing
733 -- 'derived' evidence, even in TcEvBinds
734 newGivOrDerCoVar ty1 ty2 co
735 = do { cv <- newCoVar ty1 ty2
736 ; setEvBind cv (EvCoercion co)
739 newWantedCoVar :: TcType -> TcType -> TcS EvVar
740 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
743 newCoVar :: TcType -> TcType -> TcS EvVar
744 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
746 newIPVar :: IPName Name -> TcType -> TcS EvVar
747 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
749 newDictVar :: Class -> [TcType] -> TcS EvVar
750 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
755 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
756 -- In a call (isGoodRecEv ev wv), we are considering solving wv
757 -- using some term that involves ev, such as:
758 -- by setting wv = ev
759 -- or wv = EvCast x |> ev
761 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
762 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
763 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
765 -- Guarded means: more instance calls than superclass selections. We
766 -- compute this by chasing the evidence, adding +1 for every instance
767 -- call (constructor) and -1 for every superclass selection (destructor).
769 -- See Note [Superclasses and recursive dictionaries] in TcInteract
770 isGoodRecEv ev_var (WantedEvVar wv _)
771 = do { tc_evbinds <- getTcEvBindsBag
772 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
773 ; return $ case mb of
775 Just min_guardedness -> min_guardedness > 0
778 where chase_ev_var :: EvBindMap -- Evidence binds
779 -> EvVar -- Target variable whose gravity we want to return
780 -> Int -- Current gravity
781 -> [EvVar] -- Visited nodes
782 -> EvVar -- Current node
784 chase_ev_var assocs trg curr_grav visited orig
785 | trg == orig = return $ Just curr_grav
786 | orig `elem` visited = return $ Nothing
787 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
788 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
790 {- No longer needed: evidence is in the EvBinds
791 | isTcTyVar orig && isMetaTyVar orig
792 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
793 ; case meta_details of
794 Flexi -> return Nothing
795 Indirect tyco -> chase_ev assocs trg curr_grav
796 (orig:visited) (EvCoercion tyco)
799 | otherwise = return Nothing
801 chase_ev assocs trg curr_grav visited (EvId v)
802 = chase_ev_var assocs trg curr_grav visited v
803 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
804 = chase_ev_var assocs trg (curr_grav-1) visited d_id
805 chase_ev assocs trg curr_grav visited (EvCast v co)
806 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
807 ; m2 <- chase_co assocs trg curr_grav visited co
808 ; return (comb_chase_res Nothing [m1,m2]) }
810 chase_ev assocs trg curr_grav visited (EvCoercion co)
811 = chase_co assocs trg curr_grav visited co
812 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
813 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
814 ; return (comb_chase_res Nothing chase_results) }
816 chase_co assocs trg curr_grav visited co
817 = -- Look for all the coercion variables in the coercion
818 -- chase them, and combine the results. This is OK since the
819 -- coercion will not contain any superclass terms -- anything
820 -- that involves dictionaries will be bound in assocs.
821 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
823 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
824 ; return (comb_chase_res Nothing chase_results) }
826 comb_chase_res f [] = f
827 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
828 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
829 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
832 -- Matching and looking up classes and family instances
833 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
835 data MatchInstResult mi
836 = MatchInstNo -- No matching instance
837 | MatchInstSingle mi -- Single matching instance
838 | MatchInstMany -- Multiple matching instances
841 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
842 -- Look up a class constraint in the instance environment
844 = do { let pred = mkClassPred clas tys
845 ; instEnvs <- getInstEnvs
846 ; case lookupInstEnv instEnvs clas tys of {
847 ([], unifs) -- Nothing matches
848 -> do { traceTcS "matchClass not matching"
849 (vcat [ text "dict" <+> ppr pred,
850 text "unifs" <+> ppr unifs ])
853 ([(ispec, inst_tys)], []) -- A single match
854 -> do { let dfun_id = is_dfun ispec
855 ; traceTcS "matchClass success"
856 (vcat [text "dict" <+> ppr pred,
857 text "witness" <+> ppr dfun_id
858 <+> ppr (idType dfun_id) ])
859 -- Record that this dfun is needed
860 ; record_dfun_usage dfun_id
861 ; return $ MatchInstSingle (dfun_id, inst_tys)
863 (matches, unifs) -- More than one matches
864 -> do { traceTcS "matchClass multiple matches, deferring choice"
865 (vcat [text "dict" <+> ppr pred,
866 text "matches" <+> ppr matches,
867 text "unifs" <+> ppr unifs])
868 ; return MatchInstMany
872 where record_dfun_usage :: Id -> TcS ()
873 record_dfun_usage dfun_id
874 = do { hsc_env <- getTopEnv
875 ; let dfun_name = idName dfun_id
876 dfun_mod = ASSERT( isExternalName dfun_name )
878 ; if isInternalName dfun_name || -- Internal name => defined in this module
879 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
880 then return () -- internal, or in another package
881 else do updInstUses dfun_id
884 updInstUses :: Id -> TcS ()
886 = do { tcg_env <- getGblEnv
887 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
888 (`addOneToNameSet` idName dfun_id)
893 -> TcS (MatchInstResult (TyCon, [Type]))
895 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
897 Nothing -> return MatchInstNo
898 Just res -> return $ MatchInstSingle res
899 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
900 -- multiple matches. Check.
904 zonkTcTypeTcS :: TcType -> TcS TcType
905 -- Zonk through the TyBinds of the Tcs Monad
907 = do { subst <- getTcSTyBindsMap >>= return . varEnvElts
908 ; let (dom,rng) = unzip subst
909 apply_once = substTyWith dom rng
910 ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ]
911 ; return (substTyWith dom rng_idemp ty) }
918 -- Functional dependencies, instantiation of equations
919 -------------------------------------------------------
921 mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
923 mkWantedFunDepEqns _ [] = return []
924 mkWantedFunDepEqns loc eqns
925 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
926 ; wevvars <- mapM to_work_item eqns
927 ; return $ concat wevvars }
929 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
930 to_work_item ((qtvs, pairs), _, _)
931 = do { let tvs = varSetElems qtvs
932 ; tvs' <- mapM newFlexiTcS tvs
933 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
934 ; mapM (do_one subst) pairs }
936 do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
937 sty2 = substTy subst ty2
938 ; ev <- newWantedCoVar sty1 sty2
939 ; return (WantedEvVar ev loc) }
941 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
942 pprEquationDoc (eqn, (p1, _), (p2, _))
943 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]