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 :: Bag WantedEvVar -> Bag (CtFlavor,EvVar)
185 makeGivens = mapBag (\(WantedEvVar ev wloc) -> (mkGivenFlavor (Wanted wloc) UnkSkol, ev))
186 -- ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
187 -- The UnkSkol doesn't matter because these givens are
188 -- not contradictory (else we'd have rejected them already)
190 makeSolvedByInst :: CanonicalCt -> CanonicalCt
191 -- Record that a constraint is now solved
193 -- Given, Derived -> no-op
195 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
198 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
199 mkWantedConstraints flats implics
200 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
202 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
203 deCanonicaliseWanted ct
204 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
205 let Wanted loc = cc_flavor ct
206 in WantedEvVar (cc_id ct) loc
208 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
209 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
210 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
211 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
212 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
214 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
215 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
216 tyVarsOfCDict _ct = emptyVarSet
218 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
219 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
221 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
222 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
224 instance Outputable CanonicalCt where
225 ppr (CDictCan d fl cls tys)
226 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
227 ppr (CIPCan ip fl ip_nm ty)
228 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
229 ppr (CTyEqCan co fl tv ty)
230 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
231 ppr (CFunEqCan co fl tc tys ty)
232 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
235 Note [Canonical implicit parameter constraints]
236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
237 The type in a canonical implicit parameter constraint doesn't need to
238 be a xi (type-function-free type) since we can defer the flattening
239 until checking this type for equality with another type. If we
240 encounter two IP constraints with the same name, they MUST have the
241 same type, and at that point we can generate a flattened equality
242 constraint between the types. (On the other hand, the types in two
243 class constraints for the same class MAY be equal, so they need to be
244 flattened in the first place to facilitate comparing them.)
247 singleCCan :: CanonicalCt -> CanonicalCts
250 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
253 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
254 extendCCans = snocBag
256 andCCans :: [CanonicalCts] -> CanonicalCts
257 andCCans = unionManyBags
259 emptyCCan :: CanonicalCts
262 isEmptyCCan :: CanonicalCts -> Bool
263 isEmptyCCan = isEmptyBag
265 isCTyEqCan :: CanonicalCt -> Bool
266 isCTyEqCan (CTyEqCan {}) = True
267 isCTyEqCan (CFunEqCan {}) = False
270 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
271 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
272 isCDictCan_Maybe _ = Nothing
274 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
275 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
276 isCIPCan_Maybe _ = Nothing
278 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
279 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
280 isCFunEqCan_Maybe _ = Nothing
284 %************************************************************************
287 The "flavor" of a canonical constraint
289 %************************************************************************
293 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
294 | Derived WantedLoc DerivedOrig
295 -- We have evidence for this constraint in TcEvBinds;
296 -- *however* this evidence can contain wanteds, so
297 -- it's valid only provisionally to the solution of
299 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
301 data DerivedOrig = DerSC | DerInst | DerSelf
302 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
303 -- solved wanteds from instances, or 'self' dictionaries containing yet wanted
306 instance Outputable CtFlavor where
307 ppr (Given _) = ptext (sLit "[Given]")
308 ppr (Wanted _) = ptext (sLit "[Wanted]")
309 ppr (Derived {}) = ptext (sLit "[Derived]")
311 isWanted :: CtFlavor -> Bool
312 isWanted (Wanted {}) = True
315 isGiven :: CtFlavor -> Bool
316 isGiven (Given {}) = True
319 isDerived :: CtFlavor -> Bool
320 isDerived (Derived {}) = True
323 pprFlavorArising :: CtFlavor -> SDoc
324 pprFlavorArising (Derived wl _) = pprArisingAt wl
325 pprFlavorArising (Wanted wl) = pprArisingAt wl
326 pprFlavorArising (Given gl) = pprArisingAt gl
328 getWantedLoc :: CanonicalCt -> WantedLoc
330 = ASSERT (isWanted (cc_flavor ct))
333 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
336 isWantedCt :: CanonicalCt -> Bool
337 isWantedCt ct = isWanted (cc_flavor ct)
338 isGivenCt :: CanonicalCt -> Bool
339 isGivenCt ct = isGiven (cc_flavor ct)
341 canSolve :: CtFlavor -> CtFlavor -> Bool
342 -- canSolve ctid1 ctid2
343 -- The constraint ctid1 can be used to solve ctid2
344 -- "to solve" means a reaction where the active parts of the two constraints match.
345 -- active(F xis ~ xi) = F xis
346 -- active(tv ~ xi) = tv
347 -- active(D xis) = D xis
348 -- active(IP nm ty) = nm
349 -----------------------------------------
350 canSolve (Given {}) _ = True
351 canSolve (Derived {}) (Wanted {}) = True
352 canSolve (Derived {}) (Derived {}) = True
353 canSolve (Wanted {}) (Wanted {}) = True
356 canRewrite :: CtFlavor -> CtFlavor -> Bool
357 -- canRewrite ctid1 ctid2
358 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
359 canRewrite = canSolve
361 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
362 -- Precondition: At least one of them should be wanted
363 combineCtLoc (Wanted loc) _ = loc
364 combineCtLoc _ (Wanted loc) = loc
365 combineCtLoc (Derived loc _) _ = loc
366 combineCtLoc _ (Derived loc _) = loc
367 combineCtLoc _ _ = panic "combineCtLoc: both given"
369 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
370 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
371 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
372 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
374 mkWantedFlavor :: CtFlavor -> CtFlavor
375 mkWantedFlavor (Wanted loc) = Wanted loc
376 mkWantedFlavor (Derived loc _) = Wanted loc
377 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
381 %************************************************************************
383 %* The TcS solver monad *
385 %************************************************************************
389 The TcS monad is a weak form of the main Tc monad
393 * allocate new variables
394 * fill in evidence variables
396 Filling in a dictionary evidence variable means to create a binding
397 for it, so TcS carries a mutable location where the binding can be
398 added. This is initialised from the innermost implication constraint.
403 tcs_ev_binds :: EvBindsVar,
406 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
407 -- Global type bindings
409 tcs_context :: SimplContext,
411 tcs_errors :: IORef (Bag FrozenError),
412 -- Frozen errors that we defer reporting as much as possible, in order to
413 -- make them as informative as possible. See Note [Frozen Errors]
415 tcs_untch :: TcsUntouchables
418 type TcsUntouchables = (Untouchables,TcTyVarSet)
419 -- Like the TcM Untouchables,
420 -- but records extra TcsTv variables generated during simplification
421 -- See Note [Extra TcsTv untouchables] in TcSimplify
424 = FrozenError ErrorKind CtFlavor TcType TcType
427 = MisMatchError | OccCheckError | KindError
429 instance Outputable FrozenError where
430 ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"
436 Some of the errors that we get during canonicalization are best reported when all constraints
437 have been simplified as much as possible. For instance, assume that during simplification
438 the following constraints arise:
440 [Wanted] F alpha ~ uf1
441 [Wanted] beta ~ uf1 beta
443 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply
445 'Can't construct the infinite type beta ~ uf1 beta'
446 and the user has no idea what the uf1 variable is.
448 Instead our plan is that we will NOT fail immediately, but:
449 (1) Record the "frozen" error in the tcs_errors field
450 (2) Isolate the offending constraint from the rest of the inerts
451 (3) Keep on simplifying/canonicalizing
453 At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to
454 report a more informative error:
455 'Can't construct the infinite type beta ~ F alpha beta'
459 = SimplInfer -- Inferring type of a let-bound thing
460 | SimplRuleLhs -- Inferring type of a RULE lhs
461 | SimplInteractive -- Inferring type at GHCi prompt
462 | 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, emptyVarSet) -- No Tcs untouchables yet
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 -> TcsUntouchables -> TcS a -> TcS a
556 nestImplicTcS ref untch (TcS thing_inside)
557 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
559 tcs_errors = err_ref } ->
561 nest_env = TcSEnv { tcs_ev_binds = ref
562 , tcs_ty_binds = ty_binds
564 , tcs_context = ctxtUnderImplic ctxt
565 , tcs_errors = err_ref }
567 thing_inside nest_env
569 recoverTcS :: TcS a -> TcS a -> TcS a
570 recoverTcS (TcS recovery_code) (TcS thing_inside)
572 TcM.recoverM (recovery_code env) (thing_inside env)
574 ctxtUnderImplic :: SimplContext -> SimplContext
575 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
576 ctxtUnderImplic SimplRuleLhs = SimplCheck
577 ctxtUnderImplic ctxt = ctxt
579 tryTcS :: TcS a -> TcS a
580 -- Like runTcS, but from within the TcS monad
581 -- Ignore all the evidence generated, and do not affect caller's evidence!
583 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
584 ; ev_binds_var <- TcM.newTcEvBinds
585 ; err_ref <- TcM.newTcRef emptyBag
586 ; let env1 = env { tcs_ev_binds = ev_binds_var
587 , tcs_ty_binds = ty_binds_var
588 , tcs_errors = err_ref }
592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
594 getDynFlags :: TcS DynFlags
595 getDynFlags = wrapTcS TcM.getDOpts
597 getTcSContext :: TcS SimplContext
598 getTcSContext = TcS (return . tcs_context)
600 getTcEvBinds :: TcS EvBindsVar
601 getTcEvBinds = TcS (return . tcs_ev_binds)
603 getUntouchables :: TcS TcsUntouchables
604 getUntouchables = TcS (return . tcs_untch)
606 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
607 getTcSTyBinds = TcS (return . tcs_ty_binds)
609 getTcSErrors :: TcS (IORef (Bag FrozenError))
610 getTcSErrors = TcS (return . tcs_errors)
612 getTcSErrorsBag :: TcS (Bag FrozenError)
613 getTcSErrorsBag = do { err_ref <- getTcSErrors
614 ; wrapTcS $ TcM.readTcRef err_ref }
616 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
617 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
620 getTcEvBindsBag :: TcS EvBindMap
622 = do { EvBindsVar ev_ref _ <- getTcEvBinds
623 ; wrapTcS $ TcM.readTcRef ev_ref }
625 setWantedCoBind :: CoVar -> Coercion -> TcS ()
626 setWantedCoBind cv co
627 = setEvBind cv (EvCoercion co)
628 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
630 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
631 setDerivedCoBind cv co
632 = setEvBind cv (EvCoercion co)
634 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
635 -- Add a type binding
636 -- We never do this twice!
637 setWantedTyBind tv ty
638 = do { ref <- getTcSTyBinds
640 do { ty_binds <- TcM.readTcRef ref
642 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
643 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
644 , ppr tv <+> text ":=" <+> ppr ty
645 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
647 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
649 setIPBind :: EvVar -> EvTerm -> TcS ()
650 setIPBind = setEvBind
652 setDictBind :: EvVar -> EvTerm -> TcS ()
653 setDictBind = setEvBind
655 setEvBind :: EvVar -> EvTerm -> TcS ()
658 = do { tc_evbinds <- getTcEvBinds
659 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
661 newTcEvBindsTcS :: TcS EvBindsVar
662 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
664 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
665 warnTcS loc warn_if doc
666 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
667 | otherwise = return ()
669 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
671 = do { ctxt <- getTcSContext
672 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
673 ; return (ctxt, tys, flags) }
677 -- Recording errors in the TcS monad
678 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
680 addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
681 addErrorTcS frknd fl ty1 ty2
682 = do { err_ref <- getTcSErrors
684 { TcM.updTcRef err_ref $ \ errs ->
685 consBag (FrozenError frknd fl ty1 ty2) errs
687 -- If there's an error in the *given* constraints,
688 -- stop right now, to avoid a cascade of errors
690 ; when (isGiven fl) TcM.failM
694 -- Just get some environments needed for instance looking up and matching
695 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 getInstEnvs :: TcS (InstEnv, InstEnv)
698 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
700 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
701 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
703 getTopEnv :: TcS HscEnv
704 getTopEnv = wrapTcS $ TcM.getTopEnv
706 getGblEnv :: TcS TcGblEnv
707 getGblEnv = wrapTcS $ TcM.getGblEnv
709 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
710 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
712 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
713 checkWellStagedDFun pred dfun_id loc
714 = wrapTcS $ TcM.setCtLoc loc $
715 do { use_stage <- TcM.getStage
716 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
718 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
719 bind_lvl = TcM.topIdLvl dfun_id
721 pprEq :: TcType -> TcType -> SDoc
722 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
724 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
725 isTouchableMetaTyVar tv
726 = do { untch <- getUntouchables
727 ; return $ isTouchableMetaTyVar_InRange untch tv }
729 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
730 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
731 = case tcTyVarDetails tv of
732 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
733 -- See Note [Touchable meta type variables]
734 MetaTv {} -> inTouchableRange untch tv
741 Note [Touchable meta type variables]
742 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
743 Meta type variables allocated *by the constraint solver itself* are always
745 instance C a b => D [a] where...
746 if we use this instance declaration we "make up" a fresh meta type
747 variable for 'b', which we must later guess. (Perhaps C has a
748 functional dependency.) But since we aren't in the constraint *generator*
749 we can't allocate a Unique in the touchable range for this implication
750 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
755 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
757 newFlattenSkolemTy :: TcType -> TcS TcType
758 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
760 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
761 newFlattenSkolemTyVar ty
762 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
763 ; let name = mkSysTvName uniq (fsLit "f")
764 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
765 ; traceTcS "New Flatten Skolem Born" $
766 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
770 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
772 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
773 instDFunTypes mb_inst_tys
774 = mapM inst_tv mb_inst_tys
776 inst_tv :: Either TyVar TcType -> TcS Type
777 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
778 inst_tv (Right ty) = return ty
780 instDFunConstraints :: TcThetaType -> TcS [EvVar]
781 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
784 instFlexiTcS :: TyVar -> TcS TcTyVar
785 -- Like TcM.instMetaTyVar but the variable that is created is always
786 -- touchable; we are supposed to guess its instantiation.
787 -- See Note [Touchable meta type variables]
788 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
790 newFlexiTcSTy :: Kind -> TcS TcType
793 do { uniq <- TcM.newUnique
794 ; ref <- TcM.newMutVar Flexi
795 ; let name = mkSysTvName uniq (fsLit "uf")
796 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
798 isFlexiTcsTv :: TyVar -> Bool
800 | not (isTcTyVar tv) = False
801 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
804 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
805 -- Create new wanted CoVar that constrains the type to have the specified kind.
806 newKindConstraint tv knd
807 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
808 ; let ty_k = mkTyVarTy tv_k
809 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
812 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
813 instFlexiTcSHelper tvname tvkind
815 do { uniq <- TcM.newUnique
816 ; ref <- TcM.newMutVar Flexi
817 ; let name = setNameUnique tvname uniq
819 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
821 -- Superclasses and recursive dictionaries
822 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
824 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
825 newGivOrDerEvVar pty evtrm
826 = do { ev <- wrapTcS $ TcM.newEvVar pty
830 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
831 -- Note we create immutable variables for given or derived, since we
832 -- must bind them to TcEvBinds (because their evidence may involve
833 -- superclasses). However we should be able to override existing
834 -- 'derived' evidence, even in TcEvBinds
835 newGivOrDerCoVar ty1 ty2 co
836 = do { cv <- newCoVar ty1 ty2
837 ; setEvBind cv (EvCoercion co)
840 newWantedCoVar :: TcType -> TcType -> TcS EvVar
841 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
844 newCoVar :: TcType -> TcType -> TcS EvVar
845 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
847 newIPVar :: IPName Name -> TcType -> TcS EvVar
848 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
850 newDictVar :: Class -> [TcType] -> TcS EvVar
851 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
856 isGoodRecEv :: EvVar -> EvVar -> TcS Bool
857 -- In a call (isGoodRecEv ev wv), we are considering solving wv
858 -- using some term that involves ev, such as:
859 -- by setting wv = ev
860 -- or wv = EvCast x |> ev
862 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
863 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
864 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
866 -- Guarded means: more instance calls than superclass selections. We
867 -- compute this by chasing the evidence, adding +1 for every instance
868 -- call (constructor) and -1 for every superclass selection (destructor).
870 -- See Note [Superclasses and recursive dictionaries] in TcInteract
871 isGoodRecEv ev_var wv
872 = do { tc_evbinds <- getTcEvBindsBag
873 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
874 ; return $ case mb of
876 Just min_guardedness -> min_guardedness > 0
879 where chase_ev_var :: EvBindMap -- Evidence binds
880 -> EvVar -- Target variable whose gravity we want to return
881 -> Int -- Current gravity
882 -> [EvVar] -- Visited nodes
883 -> EvVar -- Current node
885 chase_ev_var assocs trg curr_grav visited orig
886 | trg == orig = return $ Just curr_grav
887 | orig `elem` visited = return $ Nothing
888 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
889 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
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_deps)
905 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
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) }