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,
15 isGivenCt, isWantedCt, pprFlavorArising,
21 combineCtLoc, mkGivenFlavor, mkWantedFlavor,
24 TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
25 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
26 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
28 -- Creation of evidence variables
30 newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
31 newIPVar, newDictVar, newKindConstraint,
33 -- Setting evidence variables
34 setWantedCoBind, setDerivedCoBind,
35 setIPBind, setDictBind, setEvBind,
41 getInstEnvs, getFamInstEnvs, -- Getting the environments
42 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
43 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
44 getTcSErrorsBag, FrozenError (..),
48 newFlattenSkolemTy, -- Flatten skolems
51 instDFunTypes, -- Instantiation
62 isTouchableMetaTyVar_InRange,
64 getDefaultInfo, getDynFlags,
66 matchClass, matchFam, MatchInstResult (..),
69 pprEq, -- Smaller utils, re-exported from TcM
70 -- TODO (DV): these are only really used in the
71 -- instance matcher in TcSimplify. I am wondering
72 -- if the whole instance matcher simply belongs
76 mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps
80 #include "HsVersions.h"
90 import qualified TcRnMonad as TcM
91 import qualified TcMType as TcM
92 import qualified TcEnv as TcM
93 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
111 import HsBinds -- for TcEvBinds stuff
122 %************************************************************************
124 %* Canonical constraints *
126 %* These are the constraints the low-level simplifier works with *
128 %************************************************************************
131 -- Types without any type functions inside. However, note that xi
132 -- types CAN contain unexpanded type synonyms; however, the
133 -- (transitive) expansions of those type synonyms will not contain any
135 type Xi = Type -- In many comments, "xi" ranges over Xi
137 type CanonicalCts = Bag CanonicalCt
140 -- Atomic canonical constraints
141 = CDictCan { -- e.g. Num xi
143 cc_flavor :: CtFlavor,
148 | CIPCan { -- ?x::tau
149 -- See note [Canonical implicit parameter constraints].
151 cc_flavor :: CtFlavor,
152 cc_ip_nm :: IPName Name,
153 cc_ip_ty :: TcTauType
156 | CTyEqCan { -- tv ~ xi (recall xi means function free)
158 -- * tv not in tvs(xi) (occurs check)
159 -- * If constraint is given then typeKind xi `compatKind` typeKind tv
160 -- See Note [Spontaneous solving and kind compatibility]
161 -- * We prefer unification variables on the left *JUST* for efficiency
163 cc_flavor :: CtFlavor,
168 | CFunEqCan { -- F xis ~ xi
169 -- Invariant: * isSynFamilyTyCon cc_fun
170 -- * If constraint is given then
171 -- typeKind (F xis) `compatKind` typeKind xi
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)
234 Note [Canonical implicit parameter constraints]
235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
236 The type in a canonical implicit parameter constraint doesn't need to
237 be a xi (type-function-free type) since we can defer the flattening
238 until checking this type for equality with another type. If we
239 encounter two IP constraints with the same name, they MUST have the
240 same type, and at that point we can generate a flattened equality
241 constraint between the types. (On the other hand, the types in two
242 class constraints for the same class MAY be equal, so they need to be
243 flattened in the first place to facilitate comparing them.)
246 singleCCan :: CanonicalCt -> CanonicalCts
249 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
252 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
253 extendCCans = snocBag
255 andCCans :: [CanonicalCts] -> CanonicalCts
256 andCCans = unionManyBags
258 emptyCCan :: CanonicalCts
261 isEmptyCCan :: CanonicalCts -> Bool
262 isEmptyCCan = isEmptyBag
264 isCTyEqCan :: CanonicalCt -> Bool
265 isCTyEqCan (CTyEqCan {}) = True
266 isCTyEqCan (CFunEqCan {}) = False
269 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
270 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
271 isCDictCan_Maybe _ = Nothing
273 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
274 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
275 isCIPCan_Maybe _ = Nothing
277 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
278 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
279 isCFunEqCan_Maybe _ = Nothing
283 %************************************************************************
286 The "flavor" of a canonical constraint
288 %************************************************************************
292 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
293 | Derived WantedLoc DerivedOrig
294 -- We have evidence for this constraint in TcEvBinds;
295 -- *however* this evidence can contain wanteds, so
296 -- it's valid only provisionally to the solution of
298 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
300 data DerivedOrig = DerSC | DerInst | DerSelf
301 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
302 -- solved wanteds from instances, or 'self' dictionaries containing yet wanted
305 instance Outputable CtFlavor where
306 ppr (Given _) = ptext (sLit "[Given]")
307 ppr (Wanted _) = ptext (sLit "[Wanted]")
308 ppr (Derived {}) = ptext (sLit "[Derived]")
310 isWanted :: CtFlavor -> Bool
311 isWanted (Wanted {}) = True
314 isGiven :: CtFlavor -> Bool
315 isGiven (Given {}) = True
318 isDerived :: CtFlavor -> Bool
319 isDerived (Derived {}) = True
322 pprFlavorArising :: CtFlavor -> SDoc
323 pprFlavorArising (Derived wl _) = pprArisingAt wl
324 pprFlavorArising (Wanted wl) = pprArisingAt wl
325 pprFlavorArising (Given gl) = pprArisingAt gl
327 getWantedLoc :: CanonicalCt -> WantedLoc
329 = ASSERT (isWanted (cc_flavor ct))
332 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
335 isWantedCt :: CanonicalCt -> Bool
336 isWantedCt ct = isWanted (cc_flavor ct)
337 isGivenCt :: CanonicalCt -> Bool
338 isGivenCt ct = isGiven (cc_flavor ct)
340 canSolve :: CtFlavor -> CtFlavor -> Bool
341 -- canSolve ctid1 ctid2
342 -- The constraint ctid1 can be used to solve ctid2
343 -- "to solve" means a reaction where the active parts of the two constraints match.
344 -- active(F xis ~ xi) = F xis
345 -- active(tv ~ xi) = tv
346 -- active(D xis) = D xis
347 -- active(IP nm ty) = nm
348 -----------------------------------------
349 canSolve (Given {}) _ = True
350 canSolve (Derived {}) (Wanted {}) = True
351 canSolve (Derived {}) (Derived {}) = True
352 canSolve (Wanted {}) (Wanted {}) = True
355 canRewrite :: CtFlavor -> CtFlavor -> Bool
356 -- canRewrite ctid1 ctid2
357 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
358 canRewrite = canSolve
360 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
361 -- Precondition: At least one of them should be wanted
362 combineCtLoc (Wanted loc) _ = loc
363 combineCtLoc _ (Wanted loc) = loc
364 combineCtLoc (Derived loc _) _ = loc
365 combineCtLoc _ (Derived loc _) = loc
366 combineCtLoc _ _ = panic "combineCtLoc: both given"
368 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
369 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
370 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
371 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
373 mkWantedFlavor :: CtFlavor -> CtFlavor
374 mkWantedFlavor (Wanted loc) = Wanted loc
375 mkWantedFlavor (Derived loc _) = Wanted loc
376 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
380 %************************************************************************
382 %* The TcS solver monad *
384 %************************************************************************
388 The TcS monad is a weak form of the main Tc monad
392 * allocate new variables
393 * fill in evidence variables
395 Filling in a dictionary evidence variable means to create a binding
396 for it, so TcS carries a mutable location where the binding can be
397 added. This is initialised from the innermost implication constraint.
402 tcs_ev_binds :: EvBindsVar,
405 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
406 -- Global type bindings
408 tcs_context :: SimplContext,
410 tcs_errors :: IORef (Bag FrozenError),
411 -- Frozen errors that we defer reporting as much as possible, in order to
412 -- make them as informative as possible. See Note [Frozen Errors]
414 tcs_untch :: TcsUntouchables
417 type TcsUntouchables = (Untouchables,TcTyVarSet)
418 -- Like the TcM Untouchables,
419 -- but records extra TcsTv variables generated during simplification
420 -- See Note [Extra TcsTv untouchables] in TcSimplify
423 = FrozenError ErrorKind CtFlavor TcType TcType
426 = MisMatchError | OccCheckError | KindError
428 instance Outputable FrozenError where
429 ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"
435 Some of the errors that we get during canonicalization are best reported when all constraints
436 have been simplified as much as possible. For instance, assume that during simplification
437 the following constraints arise:
439 [Wanted] F alpha ~ uf1
440 [Wanted] beta ~ uf1 beta
442 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply
444 'Can't construct the infinite type beta ~ uf1 beta'
445 and the user has no idea what the uf1 variable is.
447 Instead our plan is that we will NOT fail immediately, but:
448 (1) Record the "frozen" error in the tcs_errors field
449 (2) Isolate the offending constraint from the rest of the inerts
450 (3) Keep on simplifying/canonicalizing
452 At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to
453 report a more informative error:
454 'Can't construct the infinite type beta ~ F alpha beta'
458 = SimplInfer -- Inferring type of a let-bound thing
459 | SimplRuleLhs -- Inferring type of a RULE lhs
460 | SimplInteractive -- Inferring type at GHCi prompt
461 | SimplCheck -- Checking a type signature or RULE rhs
463 instance Outputable SimplContext where
464 ppr SimplInfer = ptext (sLit "SimplInfer")
465 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
466 ppr SimplInteractive = ptext (sLit "SimplInteractive")
467 ppr SimplCheck = ptext (sLit "SimplCheck")
469 isInteractive :: SimplContext -> Bool
470 isInteractive SimplInteractive = True
471 isInteractive _ = False
473 simplEqsOnly :: SimplContext -> Bool
474 -- Simplify equalities only, not dictionaries
475 -- This is used for the LHS of rules; ee
476 -- Note [Simplifying RULE lhs constraints] in TcSimplify
477 simplEqsOnly SimplRuleLhs = True
478 simplEqsOnly _ = False
480 performDefaulting :: SimplContext -> Bool
481 performDefaulting SimplInfer = False
482 performDefaulting SimplRuleLhs = False
483 performDefaulting SimplInteractive = True
484 performDefaulting SimplCheck = True
487 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
489 instance Functor TcS where
490 fmap f m = TcS $ fmap f . unTcS m
492 instance Monad TcS where
493 return x = TcS (\_ -> return x)
494 fail err = TcS (\_ -> fail err)
495 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
497 -- Basic functionality
498 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
499 wrapTcS :: TcM a -> TcS a
500 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
501 -- and TcS is supposed to have limited functionality
502 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
504 wrapErrTcS :: TcM a -> TcS a
505 -- The thing wrapped should just fail
506 -- There's no static check; it's up to the user
507 -- Having a variant for each error message is too painful
510 wrapWarnTcS :: TcM a -> TcS a
511 -- The thing wrapped should just add a warning, or no-op
512 -- There's no static check; it's up to the user
513 wrapWarnTcS = wrapTcS
515 failTcS, panicTcS :: SDoc -> TcS a
516 failTcS = wrapTcS . TcM.failWith
517 panicTcS doc = pprPanic "TcCanonical" doc
519 traceTcS :: String -> SDoc -> TcS ()
520 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
522 traceTcS0 :: String -> SDoc -> TcS ()
523 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
525 runTcS :: SimplContext
526 -> Untouchables -- Untouchables
527 -> TcS a -- What to run
528 -> TcM (a, Bag FrozenError, Bag EvBind)
529 runTcS context untouch tcs
530 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
531 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
532 ; err_ref <- TcM.newTcRef emptyBag
533 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
534 , tcs_ty_binds = ty_binds_var
535 , tcs_context = context
536 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
537 , tcs_errors = err_ref
540 -- Run the computation
541 ; res <- unTcS tcs env
542 -- Perform the type unifications required
543 ; ty_binds <- TcM.readTcRef ty_binds_var
544 ; mapM_ do_unification (varEnvElts ty_binds)
547 ; frozen_errors <- TcM.readTcRef err_ref
548 ; ev_binds <- TcM.readTcRef evb_ref
549 ; return (res, frozen_errors, evBindMapBinds ev_binds) }
551 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
553 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
554 nestImplicTcS ref untch (TcS thing_inside)
555 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
557 tcs_errors = err_ref } ->
559 nest_env = TcSEnv { tcs_ev_binds = ref
560 , tcs_ty_binds = ty_binds
562 , tcs_context = ctxtUnderImplic ctxt
563 , tcs_errors = err_ref }
565 thing_inside nest_env
567 recoverTcS :: TcS a -> TcS a -> TcS a
568 recoverTcS (TcS recovery_code) (TcS thing_inside)
570 TcM.recoverM (recovery_code env) (thing_inside env)
572 ctxtUnderImplic :: SimplContext -> SimplContext
573 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
574 ctxtUnderImplic SimplRuleLhs = SimplCheck
575 ctxtUnderImplic ctxt = ctxt
577 tryTcS :: TcS a -> TcS a
578 -- Like runTcS, but from within the TcS monad
579 -- Ignore all the evidence generated, and do not affect caller's evidence!
581 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
582 ; ev_binds_var <- TcM.newTcEvBinds
583 ; err_ref <- TcM.newTcRef emptyBag
584 ; let env1 = env { tcs_ev_binds = ev_binds_var
585 , tcs_ty_binds = ty_binds_var
586 , tcs_errors = err_ref }
590 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
592 getDynFlags :: TcS DynFlags
593 getDynFlags = wrapTcS TcM.getDOpts
595 getTcSContext :: TcS SimplContext
596 getTcSContext = TcS (return . tcs_context)
598 getTcEvBinds :: TcS EvBindsVar
599 getTcEvBinds = TcS (return . tcs_ev_binds)
601 getUntouchables :: TcS TcsUntouchables
602 getUntouchables = TcS (return . tcs_untch)
604 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
605 getTcSTyBinds = TcS (return . tcs_ty_binds)
607 getTcSErrors :: TcS (IORef (Bag FrozenError))
608 getTcSErrors = TcS (return . tcs_errors)
610 getTcSErrorsBag :: TcS (Bag FrozenError)
611 getTcSErrorsBag = do { err_ref <- getTcSErrors
612 ; wrapTcS $ TcM.readTcRef err_ref }
614 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
615 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
618 getTcEvBindsBag :: TcS EvBindMap
620 = do { EvBindsVar ev_ref _ <- getTcEvBinds
621 ; wrapTcS $ TcM.readTcRef ev_ref }
623 setWantedCoBind :: CoVar -> Coercion -> TcS ()
624 setWantedCoBind cv co
625 = setEvBind cv (EvCoercion co)
626 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
628 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
629 setDerivedCoBind cv co
630 = setEvBind cv (EvCoercion co)
632 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
633 -- Add a type binding
634 -- We never do this twice!
635 setWantedTyBind tv ty
636 = do { ref <- getTcSTyBinds
638 do { ty_binds <- TcM.readTcRef ref
640 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
641 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
642 , ppr tv <+> text ":=" <+> ppr ty
643 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
645 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
647 setIPBind :: EvVar -> EvTerm -> TcS ()
648 setIPBind = setEvBind
650 setDictBind :: EvVar -> EvTerm -> TcS ()
651 setDictBind = setEvBind
653 setEvBind :: EvVar -> EvTerm -> TcS ()
656 = do { tc_evbinds <- getTcEvBinds
657 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
659 newTcEvBindsTcS :: TcS EvBindsVar
660 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
662 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
663 warnTcS loc warn_if doc
664 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
665 | otherwise = return ()
667 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
669 = do { ctxt <- getTcSContext
670 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
671 ; return (ctxt, tys, flags) }
675 -- Recording errors in the TcS monad
676 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
678 addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
679 addErrorTcS frknd fl ty1 ty2
680 = do { err_ref <- getTcSErrors
682 { TcM.updTcRef err_ref $ \ errs ->
683 consBag (FrozenError frknd fl ty1 ty2) errs
685 -- If there's an error in the *given* constraints,
686 -- stop right now, to avoid a cascade of errors
688 ; when (isGiven fl) TcM.failM
692 -- Just get some environments needed for instance looking up and matching
693 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
695 getInstEnvs :: TcS (InstEnv, InstEnv)
696 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
698 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
699 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
701 getTopEnv :: TcS HscEnv
702 getTopEnv = wrapTcS $ TcM.getTopEnv
704 getGblEnv :: TcS TcGblEnv
705 getGblEnv = wrapTcS $ TcM.getGblEnv
707 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
708 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
710 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
711 checkWellStagedDFun pred dfun_id loc
712 = wrapTcS $ TcM.setCtLoc loc $
713 do { use_stage <- TcM.getStage
714 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
716 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
717 bind_lvl = TcM.topIdLvl dfun_id
719 pprEq :: TcType -> TcType -> SDoc
720 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
722 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
723 isTouchableMetaTyVar tv
724 = do { untch <- getUntouchables
725 ; return $ isTouchableMetaTyVar_InRange untch tv }
727 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
728 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
729 = case tcTyVarDetails tv of
730 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
731 -- See Note [Touchable meta type variables]
732 MetaTv {} -> inTouchableRange untch tv
739 Note [Touchable meta type variables]
740 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
741 Meta type variables allocated *by the constraint solver itself* are always
743 instance C a b => D [a] where...
744 if we use this instance declaration we "make up" a fresh meta type
745 variable for 'b', which we must later guess. (Perhaps C has a
746 functional dependency.) But since we aren't in the constraint *generator*
747 we can't allocate a Unique in the touchable range for this implication
748 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
753 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
755 newFlattenSkolemTy :: TcType -> TcS TcType
756 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
758 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
759 newFlattenSkolemTyVar ty
760 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
761 ; let name = mkSysTvName uniq (fsLit "f")
762 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
763 ; traceTcS "New Flatten Skolem Born" $
764 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
768 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
770 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
771 instDFunTypes mb_inst_tys
772 = mapM inst_tv mb_inst_tys
774 inst_tv :: Either TyVar TcType -> TcS Type
775 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
776 inst_tv (Right ty) = return ty
778 instDFunConstraints :: TcThetaType -> TcS [EvVar]
779 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
782 instFlexiTcS :: TyVar -> TcS TcTyVar
783 -- Like TcM.instMetaTyVar but the variable that is created is always
784 -- touchable; we are supposed to guess its instantiation.
785 -- See Note [Touchable meta type variables]
786 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
788 newFlexiTcSTy :: Kind -> TcS TcType
791 do { uniq <- TcM.newUnique
792 ; ref <- TcM.newMutVar Flexi
793 ; let name = mkSysTvName uniq (fsLit "uf")
794 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
796 isFlexiTcsTv :: TyVar -> Bool
798 | not (isTcTyVar tv) = False
799 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
802 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
803 -- Create new wanted CoVar that constrains the type to have the specified kind.
804 newKindConstraint tv knd
805 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
806 ; let ty_k = mkTyVarTy tv_k
807 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
810 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
811 instFlexiTcSHelper tvname tvkind
813 do { uniq <- TcM.newUnique
814 ; ref <- TcM.newMutVar Flexi
815 ; let name = setNameUnique tvname uniq
817 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
819 -- Superclasses and recursive dictionaries
820 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
822 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
823 newGivOrDerEvVar pty evtrm
824 = do { ev <- wrapTcS $ TcM.newEvVar pty
828 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
829 -- Note we create immutable variables for given or derived, since we
830 -- must bind them to TcEvBinds (because their evidence may involve
831 -- superclasses). However we should be able to override existing
832 -- 'derived' evidence, even in TcEvBinds
833 newGivOrDerCoVar ty1 ty2 co
834 = do { cv <- newCoVar ty1 ty2
835 ; setEvBind cv (EvCoercion co)
838 newWantedCoVar :: TcType -> TcType -> TcS EvVar
839 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
842 newCoVar :: TcType -> TcType -> TcS EvVar
843 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
845 newIPVar :: IPName Name -> TcType -> TcS EvVar
846 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
848 newDictVar :: Class -> [TcType] -> TcS EvVar
849 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
854 isGoodRecEv :: EvVar -> EvVar -> TcS Bool
855 -- In a call (isGoodRecEv ev wv), we are considering solving wv
856 -- using some term that involves ev, such as:
857 -- by setting wv = ev
858 -- or wv = EvCast x |> ev
860 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
861 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
862 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
864 -- Guarded means: more instance calls than superclass selections. We
865 -- compute this by chasing the evidence, adding +1 for every instance
866 -- call (constructor) and -1 for every superclass selection (destructor).
868 -- See Note [Superclasses and recursive dictionaries] in TcInteract
869 isGoodRecEv ev_var wv
870 = do { tc_evbinds <- getTcEvBindsBag
871 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
872 ; return $ case mb of
874 Just min_guardedness -> min_guardedness > 0
877 where chase_ev_var :: EvBindMap -- Evidence binds
878 -> EvVar -- Target variable whose gravity we want to return
879 -> Int -- Current gravity
880 -> [EvVar] -- Visited nodes
881 -> EvVar -- Current node
883 chase_ev_var assocs trg curr_grav visited orig
884 | trg == orig = return $ Just curr_grav
885 | orig `elem` visited = return $ Nothing
886 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
887 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
889 | otherwise = return Nothing
891 chase_ev assocs trg curr_grav visited (EvId v)
892 = chase_ev_var assocs trg curr_grav visited v
893 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
894 = chase_ev_var assocs trg (curr_grav-1) visited d_id
895 chase_ev assocs trg curr_grav visited (EvCast v co)
896 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
897 ; m2 <- chase_co assocs trg curr_grav visited co
898 ; return (comb_chase_res Nothing [m1,m2]) }
900 chase_ev assocs trg curr_grav visited (EvCoercion co)
901 = chase_co assocs trg curr_grav visited co
902 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ _ev_vars ev_deps)
903 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
904 -- Notice that we chase the ev_deps and not the ev_vars
905 -- See Note [Dependencies in self dictionaries] in TcSimplify
906 ; return (comb_chase_res Nothing chase_results) }
908 chase_co assocs trg curr_grav visited co
909 = -- Look for all the coercion variables in the coercion
910 -- chase them, and combine the results. This is OK since the
911 -- coercion will not contain any superclass terms -- anything
912 -- that involves dictionaries will be bound in assocs.
913 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
915 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
916 ; return (comb_chase_res Nothing chase_results) }
918 comb_chase_res f [] = f
919 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
920 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
921 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
924 -- Matching and looking up classes and family instances
925 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
927 data MatchInstResult mi
928 = MatchInstNo -- No matching instance
929 | MatchInstSingle mi -- Single matching instance
930 | MatchInstMany -- Multiple matching instances
933 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
934 -- Look up a class constraint in the instance environment
936 = do { let pred = mkClassPred clas tys
937 ; instEnvs <- getInstEnvs
938 ; case lookupInstEnv instEnvs clas tys of {
939 ([], unifs) -- Nothing matches
940 -> do { traceTcS "matchClass not matching"
941 (vcat [ text "dict" <+> ppr pred,
942 text "unifs" <+> ppr unifs ])
945 ([(ispec, inst_tys)], []) -- A single match
946 -> do { let dfun_id = is_dfun ispec
947 ; traceTcS "matchClass success"
948 (vcat [text "dict" <+> ppr pred,
949 text "witness" <+> ppr dfun_id
950 <+> ppr (idType dfun_id) ])
951 -- Record that this dfun is needed
952 ; return $ MatchInstSingle (dfun_id, inst_tys)
954 (matches, unifs) -- More than one matches
955 -> do { traceTcS "matchClass multiple matches, deferring choice"
956 (vcat [text "dict" <+> ppr pred,
957 text "matches" <+> ppr matches,
958 text "unifs" <+> ppr unifs])
959 ; return MatchInstMany
966 -> TcS (MatchInstResult (TyCon, [Type]))
968 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
970 Nothing -> return MatchInstNo
971 Just res -> return $ MatchInstSingle res
972 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
973 -- multiple matches. Check.
977 -- Functional dependencies, instantiation of equations
978 -------------------------------------------------------
980 mkWantedFunDepEqns :: WantedLoc
981 -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
983 mkWantedFunDepEqns _ [] = return []
984 mkWantedFunDepEqns loc eqns
985 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
986 ; wevvars <- mapM to_work_item eqns
987 ; return $ concat wevvars }
989 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
990 to_work_item ((qtvs, pairs), d1, d2)
991 = do { let tvs = varSetElems qtvs
992 ; tvs' <- mapM instFlexiTcS tvs
993 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
994 loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
995 ; mapM (do_one subst loc') pairs }
997 do_one subst loc' (ty1, ty2)
998 = do { let sty1 = substTy subst ty1
999 sty2 = substTy subst ty2
1000 ; ev <- newWantedCoVar sty1 sty2
1001 ; return (WantedEvVar ev loc') }
1003 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
1004 pprEquationDoc (eqn, (p1, _), (p2, _))
1005 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1007 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1008 -> TcM (TidyEnv, SDoc)
1009 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1010 = do { pred1' <- TcM.zonkTcPredType pred1
1011 ; pred2' <- TcM.zonkTcPredType pred2
1012 ; let { pred1'' = tidyPred tidy_env pred1'
1013 ; pred2'' = tidyPred tidy_env pred2' }
1014 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1015 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1016 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1017 ; return (tidy_env, msg) }