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, pprFlavorArising,
19 combineCtLoc, mkGivenFlavor, mkWantedFlavor,
22 TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
23 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
24 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
26 -- Creation of evidence variables
28 newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
29 newIPVar, newDictVar, newKindConstraint,
31 -- Setting evidence variables
32 setWantedCoBind, setDerivedCoBind,
33 setIPBind, setDictBind, setEvBind,
39 getInstEnvs, getFamInstEnvs, -- Getting the environments
40 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
41 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
42 getTcSErrorsBag, FrozenError (..),
46 newFlattenSkolemTy, -- Flatten skolems
49 instDFunTypes, -- Instantiation
59 isTouchableMetaTyVar_InRange,
61 getDefaultInfo, getDynFlags,
63 matchClass, matchFam, MatchInstResult (..),
66 pprEq, -- Smaller utils, re-exported from TcM
67 -- TODO (DV): these are only really used in the
68 -- instance matcher in TcSimplify. I am wondering
69 -- if the whole instance matcher simply belongs
73 mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps
77 #include "HsVersions.h"
87 import NameSet ( addOneToNameSet )
89 import qualified TcRnMonad as TcM
90 import qualified TcMType as TcM
91 import qualified TcEnv as TcM
92 ( 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
301 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
302 -- solved wanteds from instances.
304 instance Outputable CtFlavor where
305 ppr (Given _) = ptext (sLit "[Given]")
306 ppr (Wanted _) = ptext (sLit "[Wanted]")
307 ppr (Derived {}) = ptext (sLit "[Derived]")
309 isWanted :: CtFlavor -> Bool
310 isWanted (Wanted {}) = True
313 isGiven :: CtFlavor -> Bool
314 isGiven (Given {}) = True
317 isDerived :: CtFlavor -> Bool
318 isDerived (Derived {}) = True
321 isDerivedSC :: CtFlavor -> Bool
322 isDerivedSC (Derived _ DerSC) = True
323 isDerivedSC _ = False
325 isDerivedByInst :: CtFlavor -> Bool
326 isDerivedByInst (Derived _ DerInst) = True
327 isDerivedByInst _ = False
329 pprFlavorArising :: CtFlavor -> SDoc
330 pprFlavorArising (Derived wl _) = pprArisingAt wl
331 pprFlavorArising (Wanted wl) = pprArisingAt wl
332 pprFlavorArising (Given gl) = pprArisingAt gl
334 getWantedLoc :: CanonicalCt -> WantedLoc
336 = ASSERT (isWanted (cc_flavor ct))
339 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
342 isWantedCt :: CanonicalCt -> Bool
343 isWantedCt ct = isWanted (cc_flavor ct)
344 isGivenCt :: CanonicalCt -> Bool
345 isGivenCt ct = isGiven (cc_flavor ct)
347 canSolve :: CtFlavor -> CtFlavor -> Bool
348 -- canSolve ctid1 ctid2
349 -- The constraint ctid1 can be used to solve ctid2
350 -- "to solve" means a reaction where the active parts of the two constraints match.
351 -- active(F xis ~ xi) = F xis
352 -- active(tv ~ xi) = tv
353 -- active(D xis) = D xis
354 -- active(IP nm ty) = nm
355 -----------------------------------------
356 canSolve (Given {}) _ = True
357 canSolve (Derived {}) (Wanted {}) = True
358 canSolve (Derived {}) (Derived {}) = True
359 canSolve (Wanted {}) (Wanted {}) = True
362 canRewrite :: CtFlavor -> CtFlavor -> Bool
363 -- canRewrite ctid1 ctid2
364 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
365 canRewrite = canSolve
367 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
368 -- Precondition: At least one of them should be wanted
369 combineCtLoc (Wanted loc) _ = loc
370 combineCtLoc _ (Wanted loc) = loc
371 combineCtLoc (Derived loc _) _ = loc
372 combineCtLoc _ (Derived loc _) = loc
373 combineCtLoc _ _ = panic "combineCtLoc: both given"
375 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
376 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
377 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
378 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
380 mkWantedFlavor :: CtFlavor -> CtFlavor
381 mkWantedFlavor (Wanted loc) = Wanted loc
382 mkWantedFlavor (Derived loc _) = Wanted loc
383 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
387 %************************************************************************
389 %* The TcS solver monad *
391 %************************************************************************
395 The TcS monad is a weak form of the main Tc monad
399 * allocate new variables
400 * fill in evidence variables
402 Filling in a dictionary evidence variable means to create a binding
403 for it, so TcS carries a mutable location where the binding can be
404 added. This is initialised from the innermost implication constraint.
409 tcs_ev_binds :: EvBindsVar,
412 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
413 -- Global type bindings
415 tcs_context :: SimplContext,
417 tcs_errors :: IORef (Bag FrozenError),
418 -- Frozen errors that we defer reporting as much as possible, in order to
419 -- make them as informative as possible. See Note [Frozen Errors]
421 tcs_untch :: Untouchables
425 = FrozenError ErrorKind CtFlavor TcType TcType
428 = MisMatchError | OccCheckError | KindError
430 instance Outputable FrozenError where
431 ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"
437 Some of the errors that we get during canonicalization are best reported when all constraints
438 have been simplified as much as possible. For instance, assume that during simplification
439 the following constraints arise:
441 [Wanted] F alpha ~ uf1
442 [Wanted] beta ~ uf1 beta
444 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply
446 'Can't construct the infinite type beta ~ uf1 beta'
447 and the user has no idea what the uf1 variable is.
449 Instead our plan is that we will NOT fail immediately, but:
450 (1) Record the "frozen" error in the tcs_errors field
451 (2) Isolate the offending constraint from the rest of the inerts
452 (3) Keep on simplifying/canonicalizing
454 At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to
455 report a more informative error:
456 'Can't construct the infinite type beta ~ F alpha beta'
460 = SimplInfer -- Inferring type of a let-bound thing
461 | SimplRuleLhs -- Inferring type of a RULE lhs
462 | SimplInteractive -- Inferring type at GHCi prompt
463 | SimplCheck -- Checking a type signature or RULE rhs
465 instance Outputable SimplContext where
466 ppr SimplInfer = ptext (sLit "SimplInfer")
467 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
468 ppr SimplInteractive = ptext (sLit "SimplInteractive")
469 ppr SimplCheck = ptext (sLit "SimplCheck")
471 isInteractive :: SimplContext -> Bool
472 isInteractive SimplInteractive = True
473 isInteractive _ = False
475 simplEqsOnly :: SimplContext -> Bool
476 -- Simplify equalities only, not dictionaries
477 -- This is used for the LHS of rules; ee
478 -- Note [Simplifying RULE lhs constraints] in TcSimplify
479 simplEqsOnly SimplRuleLhs = True
480 simplEqsOnly _ = False
482 performDefaulting :: SimplContext -> Bool
483 performDefaulting SimplInfer = False
484 performDefaulting SimplRuleLhs = False
485 performDefaulting SimplInteractive = True
486 performDefaulting SimplCheck = True
489 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
491 instance Functor TcS where
492 fmap f m = TcS $ fmap f . unTcS m
494 instance Monad TcS where
495 return x = TcS (\_ -> return x)
496 fail err = TcS (\_ -> fail err)
497 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
499 -- Basic functionality
500 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
501 wrapTcS :: TcM a -> TcS a
502 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
503 -- and TcS is supposed to have limited functionality
504 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
506 wrapErrTcS :: TcM a -> TcS a
507 -- The thing wrapped should just fail
508 -- There's no static check; it's up to the user
509 -- Having a variant for each error message is too painful
512 wrapWarnTcS :: TcM a -> TcS a
513 -- The thing wrapped should just add a warning, or no-op
514 -- There's no static check; it's up to the user
515 wrapWarnTcS = wrapTcS
517 failTcS, panicTcS :: SDoc -> TcS a
518 failTcS = wrapTcS . TcM.failWith
519 panicTcS doc = pprPanic "TcCanonical" doc
521 traceTcS :: String -> SDoc -> TcS ()
522 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
524 traceTcS0 :: String -> SDoc -> TcS ()
525 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
527 runTcS :: SimplContext
528 -> Untouchables -- Untouchables
529 -> TcS a -- What to run
530 -> TcM (a, Bag FrozenError, Bag EvBind)
531 runTcS context untouch tcs
532 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
533 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
534 ; err_ref <- TcM.newTcRef emptyBag
535 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
536 , tcs_ty_binds = ty_binds_var
537 , tcs_context = context
538 , tcs_untch = untouch
539 , tcs_errors = err_ref
542 -- Run the computation
543 ; res <- unTcS tcs env
544 -- Perform the type unifications required
545 ; ty_binds <- TcM.readTcRef ty_binds_var
546 ; mapM_ do_unification (varEnvElts ty_binds)
549 ; frozen_errors <- TcM.readTcRef err_ref
550 ; ev_binds <- TcM.readTcRef evb_ref
551 ; return (res, frozen_errors, evBindMapBinds ev_binds) }
553 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
555 nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a
556 nestImplicTcS ref untch (TcS thing_inside)
557 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt, 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 Untouchables
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 :: Untouchables -> TcTyVar -> Bool
728 isTouchableMetaTyVar_InRange untch tv
729 = case tcTyVarDetails tv of
730 MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables]
731 MetaTv {} -> inTouchableRange untch tv
738 Note [Touchable meta type variables]
739 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
740 Meta type variables allocated *by the constraint solver itself* are always
742 instance C a b => D [a] where...
743 if we use this instance declaration we "make up" a fresh meta type
744 variable for 'b', which we must later guess. (Perhaps C has a
745 functional dependency.) But since we aren't in the constraint *generator*
746 we can't allocate a Unique in the touchable range for this implication
747 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
752 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
754 newFlattenSkolemTy :: TcType -> TcS TcType
755 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
757 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
758 newFlattenSkolemTyVar ty
759 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
760 ; let name = mkSysTvName uniq (fsLit "f")
761 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
762 ; traceTcS "New Flatten Skolem Born" $
763 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
767 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
769 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
770 instDFunTypes mb_inst_tys
771 = mapM inst_tv mb_inst_tys
773 inst_tv :: Either TyVar TcType -> TcS Type
774 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
775 inst_tv (Right ty) = return ty
777 instDFunConstraints :: TcThetaType -> TcS [EvVar]
778 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
781 instFlexiTcS :: TyVar -> TcS TcTyVar
782 -- Like TcM.instMetaTyVar but the variable that is created is always
783 -- touchable; we are supposed to guess its instantiation.
784 -- See Note [Touchable meta type variables]
785 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
787 newFlexiTcSTy :: Kind -> TcS TcType
790 do { uniq <- TcM.newUnique
791 ; ref <- TcM.newMutVar Flexi
792 ; let name = mkSysTvName uniq (fsLit "uf")
793 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
795 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
796 -- Create new wanted CoVar that constrains the type to have the specified kind.
797 newKindConstraint tv knd
798 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
799 ; let ty_k = mkTyVarTy tv_k
800 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
803 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
804 instFlexiTcSHelper tvname tvkind
806 do { uniq <- TcM.newUnique
807 ; ref <- TcM.newMutVar Flexi
808 ; let name = setNameUnique tvname uniq
810 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
812 -- Superclasses and recursive dictionaries
813 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
815 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
816 newGivOrDerEvVar pty evtrm
817 = do { ev <- wrapTcS $ TcM.newEvVar pty
821 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
822 -- Note we create immutable variables for given or derived, since we
823 -- must bind them to TcEvBinds (because their evidence may involve
824 -- superclasses). However we should be able to override existing
825 -- 'derived' evidence, even in TcEvBinds
826 newGivOrDerCoVar ty1 ty2 co
827 = do { cv <- newCoVar ty1 ty2
828 ; setEvBind cv (EvCoercion co)
831 newWantedCoVar :: TcType -> TcType -> TcS EvVar
832 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
835 newCoVar :: TcType -> TcType -> TcS EvVar
836 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
838 newIPVar :: IPName Name -> TcType -> TcS EvVar
839 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
841 newDictVar :: Class -> [TcType] -> TcS EvVar
842 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
847 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
848 -- In a call (isGoodRecEv ev wv), we are considering solving wv
849 -- using some term that involves ev, such as:
850 -- by setting wv = ev
851 -- or wv = EvCast x |> ev
853 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
854 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
855 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
857 -- Guarded means: more instance calls than superclass selections. We
858 -- compute this by chasing the evidence, adding +1 for every instance
859 -- call (constructor) and -1 for every superclass selection (destructor).
861 -- See Note [Superclasses and recursive dictionaries] in TcInteract
862 isGoodRecEv ev_var (WantedEvVar wv _)
863 = do { tc_evbinds <- getTcEvBindsBag
864 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
865 ; return $ case mb of
867 Just min_guardedness -> min_guardedness > 0
870 where chase_ev_var :: EvBindMap -- Evidence binds
871 -> EvVar -- Target variable whose gravity we want to return
872 -> Int -- Current gravity
873 -> [EvVar] -- Visited nodes
874 -> EvVar -- Current node
876 chase_ev_var assocs trg curr_grav visited orig
877 | trg == orig = return $ Just curr_grav
878 | orig `elem` visited = return $ Nothing
879 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
880 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
882 {- No longer needed: evidence is in the EvBinds
883 | isTcTyVar orig && isMetaTyVar orig
884 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
885 ; case meta_details of
886 Flexi -> return Nothing
887 Indirect tyco -> chase_ev assocs trg curr_grav
888 (orig:visited) (EvCoercion tyco)
891 | otherwise = return Nothing
893 chase_ev assocs trg curr_grav visited (EvId v)
894 = chase_ev_var assocs trg curr_grav visited v
895 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
896 = chase_ev_var assocs trg (curr_grav-1) visited d_id
897 chase_ev assocs trg curr_grav visited (EvCast v co)
898 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
899 ; m2 <- chase_co assocs trg curr_grav visited co
900 ; return (comb_chase_res Nothing [m1,m2]) }
902 chase_ev assocs trg curr_grav visited (EvCoercion co)
903 = chase_co assocs trg curr_grav visited co
904 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
905 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
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 ; record_dfun_usage dfun_id
953 ; return $ MatchInstSingle (dfun_id, inst_tys)
955 (matches, unifs) -- More than one matches
956 -> do { traceTcS "matchClass multiple matches, deferring choice"
957 (vcat [text "dict" <+> ppr pred,
958 text "matches" <+> ppr matches,
959 text "unifs" <+> ppr unifs])
960 ; return MatchInstMany
964 where record_dfun_usage :: Id -> TcS ()
965 record_dfun_usage dfun_id
966 = do { hsc_env <- getTopEnv
967 ; let dfun_name = idName dfun_id
968 dfun_mod = ASSERT( isExternalName dfun_name )
970 ; if isInternalName dfun_name || -- Internal name => defined in this module
971 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
972 then return () -- internal, or in another package
973 else do updInstUses dfun_id
976 updInstUses :: Id -> TcS ()
978 = do { tcg_env <- getGblEnv
979 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
980 (`addOneToNameSet` idName dfun_id)
985 -> TcS (MatchInstResult (TyCon, [Type]))
987 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
989 Nothing -> return MatchInstNo
990 Just res -> return $ MatchInstSingle res
991 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
992 -- multiple matches. Check.
996 -- Functional dependencies, instantiation of equations
997 -------------------------------------------------------
999 mkWantedFunDepEqns :: WantedLoc
1000 -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
1001 -> TcS [WantedEvVar]
1002 mkWantedFunDepEqns _ [] = return []
1003 mkWantedFunDepEqns loc eqns
1004 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
1005 ; wevvars <- mapM to_work_item eqns
1006 ; return $ concat wevvars }
1008 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
1009 to_work_item ((qtvs, pairs), d1, d2)
1010 = do { let tvs = varSetElems qtvs
1011 ; tvs' <- mapM instFlexiTcS tvs
1012 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
1013 loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1014 ; mapM (do_one subst loc') pairs }
1016 do_one subst loc' (ty1, ty2)
1017 = do { let sty1 = substTy subst ty1
1018 sty2 = substTy subst ty2
1019 ; ev <- newWantedCoVar sty1 sty2
1020 ; return (WantedEvVar ev loc') }
1022 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
1023 pprEquationDoc (eqn, (p1, _), (p2, _))
1024 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1026 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1027 -> TcM (TidyEnv, SDoc)
1028 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1029 = do { pred1' <- TcM.zonkTcPredType pred1
1030 ; pred2' <- TcM.zonkTcPredType pred2
1031 ; let { pred1'' = tidyPred tidy_env pred1'
1032 ; pred2'' = tidyPred tidy_env pred2' }
1033 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1034 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1035 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1036 ; return (tidy_env, msg) }