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,
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 NameSet ( addOneToNameSet )
92 import qualified TcRnMonad as TcM
93 import qualified TcMType as TcM
94 import qualified TcEnv as TcM
95 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
114 import HsBinds -- for TcEvBinds stuff
125 %************************************************************************
127 %* Canonical constraints *
129 %* These are the constraints the low-level simplifier works with *
131 %************************************************************************
134 -- Types without any type functions inside. However, note that xi
135 -- types CAN contain unexpanded type synonyms; however, the
136 -- (transitive) expansions of those type synonyms will not contain any
138 type Xi = Type -- In many comments, "xi" ranges over Xi
140 type CanonicalCts = Bag CanonicalCt
143 -- Atomic canonical constraints
144 = CDictCan { -- e.g. Num xi
146 cc_flavor :: CtFlavor,
151 | CIPCan { -- ?x::tau
152 -- See note [Canonical implicit parameter constraints].
154 cc_flavor :: CtFlavor,
155 cc_ip_nm :: IPName Name,
156 cc_ip_ty :: TcTauType
159 | CTyEqCan { -- tv ~ xi (recall xi means function free)
161 -- * tv not in tvs(xi) (occurs check)
162 -- * If constraint is given then typeKind xi `compatKind` typeKind tv
163 -- See Note [Spontaneous solving and kind compatibility]
164 -- * We prefer unification variables on the left *JUST* for efficiency
166 cc_flavor :: CtFlavor,
171 | CFunEqCan { -- F xis ~ xi
172 -- Invariant: * isSynFamilyTyCon cc_fun
173 -- * If constraint is given then
174 -- typeKind (F xis) `compatKind` typeKind xi
176 cc_flavor :: CtFlavor,
177 cc_fun :: TyCon, -- A type function
178 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
179 cc_rhs :: Xi -- *never* over-saturated (because if so
180 -- we should have decomposed)
184 compatKind :: Kind -> Kind -> Bool
185 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
187 makeGivens :: CanonicalCts -> CanonicalCts
188 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
189 -- The UnkSkol doesn't matter because these givens are
190 -- not contradictory (else we'd have rejected them already)
192 makeSolvedByInst :: CanonicalCt -> CanonicalCt
193 -- Record that a constraint is now solved
195 -- Given, Derived -> no-op
197 | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
200 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
201 mkWantedConstraints flats implics
202 = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
204 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
205 deCanonicaliseWanted ct
206 = WARN( not (isWanted $ cc_flavor ct), ppr ct )
207 let Wanted loc = cc_flavor ct
208 in WantedEvVar (cc_id ct) loc
210 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
211 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
212 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
213 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
214 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
216 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
217 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
218 tyVarsOfCDict _ct = emptyVarSet
220 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
221 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
223 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
224 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
226 instance Outputable CanonicalCt where
227 ppr (CDictCan d fl cls tys)
228 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
229 ppr (CIPCan ip fl ip_nm ty)
230 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
231 ppr (CTyEqCan co fl tv ty)
232 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
233 ppr (CFunEqCan co fl tc tys ty)
234 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
237 Note [Canonical implicit parameter constraints]
238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
239 The type in a canonical implicit parameter constraint doesn't need to
240 be a xi (type-function-free type) since we can defer the flattening
241 until checking this type for equality with another type. If we
242 encounter two IP constraints with the same name, they MUST have the
243 same type, and at that point we can generate a flattened equality
244 constraint between the types. (On the other hand, the types in two
245 class constraints for the same class MAY be equal, so they need to be
246 flattened in the first place to facilitate comparing them.)
249 singleCCan :: CanonicalCt -> CanonicalCts
252 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
255 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
256 extendCCans = snocBag
258 andCCans :: [CanonicalCts] -> CanonicalCts
259 andCCans = unionManyBags
261 emptyCCan :: CanonicalCts
264 isEmptyCCan :: CanonicalCts -> Bool
265 isEmptyCCan = isEmptyBag
267 isCTyEqCan :: CanonicalCt -> Bool
268 isCTyEqCan (CTyEqCan {}) = True
269 isCTyEqCan (CFunEqCan {}) = False
272 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
273 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
274 isCDictCan_Maybe _ = Nothing
276 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
277 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
278 isCIPCan_Maybe _ = Nothing
280 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
281 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
282 isCFunEqCan_Maybe _ = Nothing
286 %************************************************************************
289 The "flavor" of a canonical constraint
291 %************************************************************************
295 = Given GivenLoc -- We have evidence for this constraint in TcEvBinds
296 | Derived WantedLoc DerivedOrig
297 -- We have evidence for this constraint in TcEvBinds;
298 -- *however* this evidence can contain wanteds, so
299 -- it's valid only provisionally to the solution of
301 | Wanted WantedLoc -- We have no evidence bindings for this constraint.
303 data DerivedOrig = DerSC | DerInst
304 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
305 -- solved wanteds from instances.
307 instance Outputable CtFlavor where
308 ppr (Given _) = ptext (sLit "[Given]")
309 ppr (Wanted _) = ptext (sLit "[Wanted]")
310 ppr (Derived {}) = ptext (sLit "[Derived]")
312 isWanted :: CtFlavor -> Bool
313 isWanted (Wanted {}) = True
316 isGiven :: CtFlavor -> Bool
317 isGiven (Given {}) = True
320 isDerived :: CtFlavor -> Bool
321 isDerived (Derived {}) = True
324 isDerivedSC :: CtFlavor -> Bool
325 isDerivedSC (Derived _ DerSC) = True
326 isDerivedSC _ = False
328 isDerivedByInst :: CtFlavor -> Bool
329 isDerivedByInst (Derived _ DerInst) = True
330 isDerivedByInst _ = False
332 pprFlavorArising :: CtFlavor -> SDoc
333 pprFlavorArising (Derived wl _) = pprArisingAt wl
334 pprFlavorArising (Wanted wl) = pprArisingAt wl
335 pprFlavorArising (Given gl) = pprArisingAt gl
337 getWantedLoc :: CanonicalCt -> WantedLoc
339 = ASSERT (isWanted (cc_flavor ct))
342 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
345 isWantedCt :: CanonicalCt -> Bool
346 isWantedCt ct = isWanted (cc_flavor ct)
347 isGivenCt :: CanonicalCt -> Bool
348 isGivenCt ct = isGiven (cc_flavor ct)
350 canSolve :: CtFlavor -> CtFlavor -> Bool
351 -- canSolve ctid1 ctid2
352 -- The constraint ctid1 can be used to solve ctid2
353 -- "to solve" means a reaction where the active parts of the two constraints match.
354 -- active(F xis ~ xi) = F xis
355 -- active(tv ~ xi) = tv
356 -- active(D xis) = D xis
357 -- active(IP nm ty) = nm
358 -----------------------------------------
359 canSolve (Given {}) _ = True
360 canSolve (Derived {}) (Wanted {}) = True
361 canSolve (Derived {}) (Derived {}) = True
362 canSolve (Wanted {}) (Wanted {}) = True
365 canRewrite :: CtFlavor -> CtFlavor -> Bool
366 -- canRewrite ctid1 ctid2
367 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
368 canRewrite = canSolve
370 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
371 -- Precondition: At least one of them should be wanted
372 combineCtLoc (Wanted loc) _ = loc
373 combineCtLoc _ (Wanted loc) = loc
374 combineCtLoc (Derived loc _) _ = loc
375 combineCtLoc _ (Derived loc _) = loc
376 combineCtLoc _ _ = panic "combineCtLoc: both given"
378 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
379 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
380 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
381 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
383 mkWantedFlavor :: CtFlavor -> CtFlavor
384 mkWantedFlavor (Wanted loc) = Wanted loc
385 mkWantedFlavor (Derived loc _) = Wanted loc
386 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
390 %************************************************************************
392 %* The TcS solver monad *
394 %************************************************************************
398 The TcS monad is a weak form of the main Tc monad
402 * allocate new variables
403 * fill in evidence variables
405 Filling in a dictionary evidence variable means to create a binding
406 for it, so TcS carries a mutable location where the binding can be
407 added. This is initialised from the innermost implication constraint.
412 tcs_ev_binds :: EvBindsVar,
415 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
416 -- Global type bindings
418 tcs_context :: SimplContext,
420 tcs_errors :: IORef (Bag FrozenError),
421 -- Frozen errors that we defer reporting as much as possible, in order to
422 -- make them as informative as possible. See Note [Frozen Errors]
424 tcs_untch :: TcsUntouchables
427 type TcsUntouchables = (Untouchables,TcTyVarSet)
428 -- Like the TcM Untouchables,
429 -- but records extra TcsTv variables generated during simplification
430 -- See Note [Extra TcsTv untouchables] in TcSimplify
433 = FrozenError ErrorKind CtFlavor TcType TcType
436 = MisMatchError | OccCheckError | KindError
438 instance Outputable FrozenError where
439 ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"
445 Some of the errors that we get during canonicalization are best reported when all constraints
446 have been simplified as much as possible. For instance, assume that during simplification
447 the following constraints arise:
449 [Wanted] F alpha ~ uf1
450 [Wanted] beta ~ uf1 beta
452 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply
454 'Can't construct the infinite type beta ~ uf1 beta'
455 and the user has no idea what the uf1 variable is.
457 Instead our plan is that we will NOT fail immediately, but:
458 (1) Record the "frozen" error in the tcs_errors field
459 (2) Isolate the offending constraint from the rest of the inerts
460 (3) Keep on simplifying/canonicalizing
462 At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to
463 report a more informative error:
464 'Can't construct the infinite type beta ~ F alpha beta'
468 = SimplInfer -- Inferring type of a let-bound thing
469 | SimplRuleLhs -- Inferring type of a RULE lhs
470 | SimplInteractive -- Inferring type at GHCi prompt
471 | SimplCheck -- Checking a type signature or RULE rhs
473 instance Outputable SimplContext where
474 ppr SimplInfer = ptext (sLit "SimplInfer")
475 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
476 ppr SimplInteractive = ptext (sLit "SimplInteractive")
477 ppr SimplCheck = ptext (sLit "SimplCheck")
479 isInteractive :: SimplContext -> Bool
480 isInteractive SimplInteractive = True
481 isInteractive _ = False
483 simplEqsOnly :: SimplContext -> Bool
484 -- Simplify equalities only, not dictionaries
485 -- This is used for the LHS of rules; ee
486 -- Note [Simplifying RULE lhs constraints] in TcSimplify
487 simplEqsOnly SimplRuleLhs = True
488 simplEqsOnly _ = False
490 performDefaulting :: SimplContext -> Bool
491 performDefaulting SimplInfer = False
492 performDefaulting SimplRuleLhs = False
493 performDefaulting SimplInteractive = True
494 performDefaulting SimplCheck = True
497 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
499 instance Functor TcS where
500 fmap f m = TcS $ fmap f . unTcS m
502 instance Monad TcS where
503 return x = TcS (\_ -> return x)
504 fail err = TcS (\_ -> fail err)
505 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
507 -- Basic functionality
508 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
509 wrapTcS :: TcM a -> TcS a
510 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
511 -- and TcS is supposed to have limited functionality
512 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
514 wrapErrTcS :: TcM a -> TcS a
515 -- The thing wrapped should just fail
516 -- There's no static check; it's up to the user
517 -- Having a variant for each error message is too painful
520 wrapWarnTcS :: TcM a -> TcS a
521 -- The thing wrapped should just add a warning, or no-op
522 -- There's no static check; it's up to the user
523 wrapWarnTcS = wrapTcS
525 failTcS, panicTcS :: SDoc -> TcS a
526 failTcS = wrapTcS . TcM.failWith
527 panicTcS doc = pprPanic "TcCanonical" doc
529 traceTcS :: String -> SDoc -> TcS ()
530 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
532 traceTcS0 :: String -> SDoc -> TcS ()
533 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
535 runTcS :: SimplContext
536 -> Untouchables -- Untouchables
537 -> TcS a -- What to run
538 -> TcM (a, Bag FrozenError, Bag EvBind)
539 runTcS context untouch tcs
540 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
541 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
542 ; err_ref <- TcM.newTcRef emptyBag
543 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
544 , tcs_ty_binds = ty_binds_var
545 , tcs_context = context
546 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
547 , tcs_errors = err_ref
550 -- Run the computation
551 ; res <- unTcS tcs env
552 -- Perform the type unifications required
553 ; ty_binds <- TcM.readTcRef ty_binds_var
554 ; mapM_ do_unification (varEnvElts ty_binds)
557 ; frozen_errors <- TcM.readTcRef err_ref
558 ; ev_binds <- TcM.readTcRef evb_ref
559 ; return (res, frozen_errors, evBindMapBinds ev_binds) }
561 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
563 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
564 nestImplicTcS ref untch (TcS thing_inside)
565 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
567 tcs_errors = err_ref } ->
569 nest_env = TcSEnv { tcs_ev_binds = ref
570 , tcs_ty_binds = ty_binds
572 , tcs_context = ctxtUnderImplic ctxt
573 , tcs_errors = err_ref }
575 thing_inside nest_env
577 recoverTcS :: TcS a -> TcS a -> TcS a
578 recoverTcS (TcS recovery_code) (TcS thing_inside)
580 TcM.recoverM (recovery_code env) (thing_inside env)
582 ctxtUnderImplic :: SimplContext -> SimplContext
583 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
584 ctxtUnderImplic SimplRuleLhs = SimplCheck
585 ctxtUnderImplic ctxt = ctxt
587 tryTcS :: TcS a -> TcS a
588 -- Like runTcS, but from within the TcS monad
589 -- Ignore all the evidence generated, and do not affect caller's evidence!
591 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
592 ; ev_binds_var <- TcM.newTcEvBinds
593 ; err_ref <- TcM.newTcRef emptyBag
594 ; let env1 = env { tcs_ev_binds = ev_binds_var
595 , tcs_ty_binds = ty_binds_var
596 , tcs_errors = err_ref }
600 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
602 getDynFlags :: TcS DynFlags
603 getDynFlags = wrapTcS TcM.getDOpts
605 getTcSContext :: TcS SimplContext
606 getTcSContext = TcS (return . tcs_context)
608 getTcEvBinds :: TcS EvBindsVar
609 getTcEvBinds = TcS (return . tcs_ev_binds)
611 getUntouchables :: TcS TcsUntouchables
612 getUntouchables = TcS (return . tcs_untch)
614 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
615 getTcSTyBinds = TcS (return . tcs_ty_binds)
617 getTcSErrors :: TcS (IORef (Bag FrozenError))
618 getTcSErrors = TcS (return . tcs_errors)
620 getTcSErrorsBag :: TcS (Bag FrozenError)
621 getTcSErrorsBag = do { err_ref <- getTcSErrors
622 ; wrapTcS $ TcM.readTcRef err_ref }
624 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
625 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
628 getTcEvBindsBag :: TcS EvBindMap
630 = do { EvBindsVar ev_ref _ <- getTcEvBinds
631 ; wrapTcS $ TcM.readTcRef ev_ref }
633 setWantedCoBind :: CoVar -> Coercion -> TcS ()
634 setWantedCoBind cv co
635 = setEvBind cv (EvCoercion co)
636 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
638 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
639 setDerivedCoBind cv co
640 = setEvBind cv (EvCoercion co)
642 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
643 -- Add a type binding
644 -- We never do this twice!
645 setWantedTyBind tv ty
646 = do { ref <- getTcSTyBinds
648 do { ty_binds <- TcM.readTcRef ref
650 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
651 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
652 , ppr tv <+> text ":=" <+> ppr ty
653 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
655 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
657 setIPBind :: EvVar -> EvTerm -> TcS ()
658 setIPBind = setEvBind
660 setDictBind :: EvVar -> EvTerm -> TcS ()
661 setDictBind = setEvBind
663 setEvBind :: EvVar -> EvTerm -> TcS ()
666 = do { tc_evbinds <- getTcEvBinds
667 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
669 newTcEvBindsTcS :: TcS EvBindsVar
670 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
672 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
673 warnTcS loc warn_if doc
674 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
675 | otherwise = return ()
677 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
679 = do { ctxt <- getTcSContext
680 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
681 ; return (ctxt, tys, flags) }
685 -- Recording errors in the TcS monad
686 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
688 addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
689 addErrorTcS frknd fl ty1 ty2
690 = do { err_ref <- getTcSErrors
692 { TcM.updTcRef err_ref $ \ errs ->
693 consBag (FrozenError frknd fl ty1 ty2) errs
695 -- If there's an error in the *given* constraints,
696 -- stop right now, to avoid a cascade of errors
698 ; when (isGiven fl) TcM.failM
702 -- Just get some environments needed for instance looking up and matching
703 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
705 getInstEnvs :: TcS (InstEnv, InstEnv)
706 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
708 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
709 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
711 getTopEnv :: TcS HscEnv
712 getTopEnv = wrapTcS $ TcM.getTopEnv
714 getGblEnv :: TcS TcGblEnv
715 getGblEnv = wrapTcS $ TcM.getGblEnv
717 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
718 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
720 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
721 checkWellStagedDFun pred dfun_id loc
722 = wrapTcS $ TcM.setCtLoc loc $
723 do { use_stage <- TcM.getStage
724 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
726 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
727 bind_lvl = TcM.topIdLvl dfun_id
729 pprEq :: TcType -> TcType -> SDoc
730 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
732 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
733 isTouchableMetaTyVar tv
734 = do { untch <- getUntouchables
735 ; return $ isTouchableMetaTyVar_InRange untch tv }
737 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
738 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
739 = case tcTyVarDetails tv of
740 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
741 -- See Note [Touchable meta type variables]
742 MetaTv {} -> inTouchableRange untch tv
749 Note [Touchable meta type variables]
750 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
751 Meta type variables allocated *by the constraint solver itself* are always
753 instance C a b => D [a] where...
754 if we use this instance declaration we "make up" a fresh meta type
755 variable for 'b', which we must later guess. (Perhaps C has a
756 functional dependency.) But since we aren't in the constraint *generator*
757 we can't allocate a Unique in the touchable range for this implication
758 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
763 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
765 newFlattenSkolemTy :: TcType -> TcS TcType
766 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
768 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
769 newFlattenSkolemTyVar ty
770 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
771 ; let name = mkSysTvName uniq (fsLit "f")
772 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
773 ; traceTcS "New Flatten Skolem Born" $
774 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
778 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
780 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
781 instDFunTypes mb_inst_tys
782 = mapM inst_tv mb_inst_tys
784 inst_tv :: Either TyVar TcType -> TcS Type
785 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
786 inst_tv (Right ty) = return ty
788 instDFunConstraints :: TcThetaType -> TcS [EvVar]
789 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
792 instFlexiTcS :: TyVar -> TcS TcTyVar
793 -- Like TcM.instMetaTyVar but the variable that is created is always
794 -- touchable; we are supposed to guess its instantiation.
795 -- See Note [Touchable meta type variables]
796 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
798 newFlexiTcSTy :: Kind -> TcS TcType
801 do { uniq <- TcM.newUnique
802 ; ref <- TcM.newMutVar Flexi
803 ; let name = mkSysTvName uniq (fsLit "uf")
804 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
806 isFlexiTcsTv :: TyVar -> Bool
808 | not (isTcTyVar tv) = False
809 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
812 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
813 -- Create new wanted CoVar that constrains the type to have the specified kind.
814 newKindConstraint tv knd
815 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
816 ; let ty_k = mkTyVarTy tv_k
817 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
820 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
821 instFlexiTcSHelper tvname tvkind
823 do { uniq <- TcM.newUnique
824 ; ref <- TcM.newMutVar Flexi
825 ; let name = setNameUnique tvname uniq
827 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
829 -- Superclasses and recursive dictionaries
830 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
832 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
833 newGivOrDerEvVar pty evtrm
834 = do { ev <- wrapTcS $ TcM.newEvVar pty
838 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
839 -- Note we create immutable variables for given or derived, since we
840 -- must bind them to TcEvBinds (because their evidence may involve
841 -- superclasses). However we should be able to override existing
842 -- 'derived' evidence, even in TcEvBinds
843 newGivOrDerCoVar ty1 ty2 co
844 = do { cv <- newCoVar ty1 ty2
845 ; setEvBind cv (EvCoercion co)
848 newWantedCoVar :: TcType -> TcType -> TcS EvVar
849 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
852 newCoVar :: TcType -> TcType -> TcS EvVar
853 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
855 newIPVar :: IPName Name -> TcType -> TcS EvVar
856 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
858 newDictVar :: Class -> [TcType] -> TcS EvVar
859 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
864 isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
865 -- In a call (isGoodRecEv ev wv), we are considering solving wv
866 -- using some term that involves ev, such as:
867 -- by setting wv = ev
868 -- or wv = EvCast x |> ev
870 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
871 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
872 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
874 -- Guarded means: more instance calls than superclass selections. We
875 -- compute this by chasing the evidence, adding +1 for every instance
876 -- call (constructor) and -1 for every superclass selection (destructor).
878 -- See Note [Superclasses and recursive dictionaries] in TcInteract
879 isGoodRecEv ev_var (WantedEvVar wv _)
880 = do { tc_evbinds <- getTcEvBindsBag
881 ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
882 ; return $ case mb of
884 Just min_guardedness -> min_guardedness > 0
887 where chase_ev_var :: EvBindMap -- Evidence binds
888 -> EvVar -- Target variable whose gravity we want to return
889 -> Int -- Current gravity
890 -> [EvVar] -- Visited nodes
891 -> EvVar -- Current node
893 chase_ev_var assocs trg curr_grav visited orig
894 | trg == orig = return $ Just curr_grav
895 | orig `elem` visited = return $ Nothing
896 | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
897 = chase_ev assocs trg curr_grav (orig:visited) ev_trm
899 {- No longer needed: evidence is in the EvBinds
900 | isTcTyVar orig && isMetaTyVar orig
901 = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
902 ; case meta_details of
903 Flexi -> return Nothing
904 Indirect tyco -> chase_ev assocs trg curr_grav
905 (orig:visited) (EvCoercion tyco)
908 | otherwise = return Nothing
910 chase_ev assocs trg curr_grav visited (EvId v)
911 = chase_ev_var assocs trg curr_grav visited v
912 chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
913 = chase_ev_var assocs trg (curr_grav-1) visited d_id
914 chase_ev assocs trg curr_grav visited (EvCast v co)
915 = do { m1 <- chase_ev_var assocs trg curr_grav visited v
916 ; m2 <- chase_co assocs trg curr_grav visited co
917 ; return (comb_chase_res Nothing [m1,m2]) }
919 chase_ev assocs trg curr_grav visited (EvCoercion co)
920 = chase_co assocs trg curr_grav visited co
921 chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
922 = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
923 ; return (comb_chase_res Nothing chase_results) }
925 chase_co assocs trg curr_grav visited co
926 = -- Look for all the coercion variables in the coercion
927 -- chase them, and combine the results. This is OK since the
928 -- coercion will not contain any superclass terms -- anything
929 -- that involves dictionaries will be bound in assocs.
930 let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
932 in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
933 ; return (comb_chase_res Nothing chase_results) }
935 comb_chase_res f [] = f
936 comb_chase_res f (Nothing:rest) = comb_chase_res f rest
937 comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest
938 comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
941 -- Matching and looking up classes and family instances
942 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
944 data MatchInstResult mi
945 = MatchInstNo -- No matching instance
946 | MatchInstSingle mi -- Single matching instance
947 | MatchInstMany -- Multiple matching instances
950 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
951 -- Look up a class constraint in the instance environment
953 = do { let pred = mkClassPred clas tys
954 ; instEnvs <- getInstEnvs
955 ; case lookupInstEnv instEnvs clas tys of {
956 ([], unifs) -- Nothing matches
957 -> do { traceTcS "matchClass not matching"
958 (vcat [ text "dict" <+> ppr pred,
959 text "unifs" <+> ppr unifs ])
962 ([(ispec, inst_tys)], []) -- A single match
963 -> do { let dfun_id = is_dfun ispec
964 ; traceTcS "matchClass success"
965 (vcat [text "dict" <+> ppr pred,
966 text "witness" <+> ppr dfun_id
967 <+> ppr (idType dfun_id) ])
968 -- Record that this dfun is needed
969 ; record_dfun_usage dfun_id
970 ; return $ MatchInstSingle (dfun_id, inst_tys)
972 (matches, unifs) -- More than one matches
973 -> do { traceTcS "matchClass multiple matches, deferring choice"
974 (vcat [text "dict" <+> ppr pred,
975 text "matches" <+> ppr matches,
976 text "unifs" <+> ppr unifs])
977 ; return MatchInstMany
981 where record_dfun_usage :: Id -> TcS ()
982 record_dfun_usage dfun_id
983 = do { hsc_env <- getTopEnv
984 ; let dfun_name = idName dfun_id
985 dfun_mod = ASSERT( isExternalName dfun_name )
987 ; if isInternalName dfun_name || -- Internal name => defined in this module
988 modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
989 then return () -- internal, or in another package
990 else do updInstUses dfun_id
993 updInstUses :: Id -> TcS ()
995 = do { tcg_env <- getGblEnv
996 ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
997 (`addOneToNameSet` idName dfun_id)
1002 -> TcS (MatchInstResult (TyCon, [Type]))
1004 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
1006 Nothing -> return MatchInstNo
1007 Just res -> return $ MatchInstSingle res
1008 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
1009 -- multiple matches. Check.
1013 -- Functional dependencies, instantiation of equations
1014 -------------------------------------------------------
1016 mkWantedFunDepEqns :: WantedLoc
1017 -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
1018 -> TcS [WantedEvVar]
1019 mkWantedFunDepEqns _ [] = return []
1020 mkWantedFunDepEqns loc eqns
1021 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
1022 ; wevvars <- mapM to_work_item eqns
1023 ; return $ concat wevvars }
1025 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
1026 to_work_item ((qtvs, pairs), d1, d2)
1027 = do { let tvs = varSetElems qtvs
1028 ; tvs' <- mapM instFlexiTcS tvs
1029 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
1030 loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1031 ; mapM (do_one subst loc') pairs }
1033 do_one subst loc' (ty1, ty2)
1034 = do { let sty1 = substTy subst ty1
1035 sty2 = substTy subst ty2
1036 ; ev <- newWantedCoVar sty1 sty2
1037 ; return (WantedEvVar ev loc') }
1039 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
1040 pprEquationDoc (eqn, (p1, _), (p2, _))
1041 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1043 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1044 -> TcM (TidyEnv, SDoc)
1045 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1046 = do { pred1' <- TcM.zonkTcPredType pred1
1047 ; pred2' <- TcM.zonkTcPredType pred2
1048 ; let { pred1'' = tidyPred tidy_env pred1'
1049 ; pred2'' = tidyPred tidy_env pred2' }
1050 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1051 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1052 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1053 ; return (tidy_env, msg) }