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,
11 WorkList, unionWorkList, unionWorkLists, isEmptyWorkList, emptyWorkList,
12 workListFromEq, workListFromNonEq,
13 workListFromEqs, workListFromNonEqs, foldrWorkListM,
15 CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
16 deCanonicalise, mkFrozenError,
18 isWanted, isGiven, isDerived,
19 isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
24 combineCtLoc, mkGivenFlavor, mkWantedFlavor,
27 TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
28 traceFireTcS, bumpStepCountTcS,
29 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
30 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
32 -- Creation of evidence variables
33 newEvVar, newCoVar, newGivenCoVar,
35 newIPVar, newDictVar, newKindConstraint,
37 -- Setting evidence variables
38 setCoBind, setIPBind, setDictBind, setEvBind,
42 getInstEnvs, getFamInstEnvs, -- Getting the environments
43 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
44 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
46 newFlattenSkolemTy, -- Flatten skolems
49 instDFunTypes, -- Instantiation
51 newFlexiTcSTy, instFlexiTcS,
57 isTouchableMetaTyVar_InRange,
59 getDefaultInfo, getDynFlags,
61 matchClass, matchFam, MatchInstResult (..),
64 pprEq -- Smaller utils, re-exported from TcM
65 -- TODO (DV): these are only really used in the
66 -- instance matcher in TcSimplify. I am wondering
67 -- if the whole instance matcher simply belongs
71 #include "HsVersions.h"
81 import qualified TcRnMonad as TcM
82 import qualified TcMType as TcM
83 import qualified TcEnv as TcM
84 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
102 import HsBinds -- for TcEvBinds stuff
107 import Control.Monad( when )
113 %************************************************************************
115 %* Canonical constraints *
117 %* These are the constraints the low-level simplifier works with *
119 %************************************************************************
122 -- Types without any type functions inside. However, note that xi
123 -- types CAN contain unexpanded type synonyms; however, the
124 -- (transitive) expansions of those type synonyms will not contain any
126 type Xi = Type -- In many comments, "xi" ranges over Xi
128 type CanonicalCts = Bag CanonicalCt
131 -- Atomic canonical constraints
132 = CDictCan { -- e.g. Num xi
134 cc_flavor :: CtFlavor,
139 | CIPCan { -- ?x::tau
140 -- See note [Canonical implicit parameter constraints].
142 cc_flavor :: CtFlavor,
143 cc_ip_nm :: IPName Name,
144 cc_ip_ty :: TcTauType
147 | CTyEqCan { -- tv ~ xi (recall xi means function free)
149 -- * tv not in tvs(xi) (occurs check)
150 -- * typeKind xi `compatKind` typeKind tv
151 -- See Note [Spontaneous solving and kind compatibility]
152 -- * We prefer unification variables on the left *JUST* for efficiency
154 cc_flavor :: CtFlavor,
159 | CFunEqCan { -- F xis ~ xi
160 -- Invariant: * isSynFamilyTyCon cc_fun
161 -- * typeKind (F xis) `compatKind` typeKind xi
163 cc_flavor :: CtFlavor,
164 cc_fun :: TyCon, -- A type function
165 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
166 cc_rhs :: Xi -- *never* over-saturated (because if so
167 -- we should have decomposed)
171 | CFrozenErr { -- A "frozen error" does not interact with anything
172 -- See Note [Frozen Errors]
174 cc_flavor :: CtFlavor
177 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
178 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
180 compatKind :: Kind -> Kind -> Bool
181 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
183 deCanonicalise :: CanonicalCt -> FlavoredEvVar
184 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
186 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
187 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
188 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
189 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
190 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
191 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
193 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
194 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
195 tyVarsOfCDict _ct = emptyVarSet
197 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
198 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
200 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
201 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
203 instance Outputable CanonicalCt where
204 ppr (CDictCan d fl cls tys)
205 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
206 ppr (CIPCan ip fl ip_nm ty)
207 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
208 ppr (CTyEqCan co fl tv ty)
209 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
210 ppr (CFunEqCan co fl tc tys ty)
211 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
212 ppr (CFrozenErr co fl)
213 = ppr fl <+> pprEvVarWithType co
216 Note [Canonical implicit parameter constraints]
217 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
218 The type in a canonical implicit parameter constraint doesn't need to
219 be a xi (type-function-free type) since we can defer the flattening
220 until checking this type for equality with another type. If we
221 encounter two IP constraints with the same name, they MUST have the
222 same type, and at that point we can generate a flattened equality
223 constraint between the types. (On the other hand, the types in two
224 class constraints for the same class MAY be equal, so they need to be
225 flattened in the first place to facilitate comparing them.)
228 singleCCan :: CanonicalCt -> CanonicalCts
231 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
234 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
235 extendCCans = snocBag
237 andCCans :: [CanonicalCts] -> CanonicalCts
238 andCCans = unionManyBags
240 emptyCCan :: CanonicalCts
243 isEmptyCCan :: CanonicalCts -> Bool
244 isEmptyCCan = isEmptyBag
246 isCTyEqCan :: CanonicalCt -> Bool
247 isCTyEqCan (CTyEqCan {}) = True
248 isCTyEqCan (CFunEqCan {}) = False
251 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
252 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
253 isCDictCan_Maybe _ = Nothing
255 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
256 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
257 isCIPCan_Maybe _ = Nothing
259 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
260 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
261 isCFunEqCan_Maybe _ = Nothing
263 isCFrozenErr :: CanonicalCt -> Bool
264 isCFrozenErr (CFrozenErr {}) = True
265 isCFrozenErr _ = False
268 -- A mixture of Given, Wanted, and Derived constraints.
269 -- We split between equalities and the rest to process equalities first.
270 data WorkList = WorkList { weqs :: CanonicalCts
271 -- NB: weqs includes equalities /and/ family equalities
272 , wrest :: CanonicalCts }
274 unionWorkList :: WorkList -> WorkList -> WorkList
275 unionWorkList wl1 wl2
276 = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
277 , wrest = wrest wl1 `andCCan` wrest wl2 }
279 unionWorkLists :: [WorkList] -> WorkList
280 unionWorkLists = foldr unionWorkList emptyWorkList
282 isEmptyWorkList :: WorkList -> Bool
283 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
285 emptyWorkList :: WorkList
287 = WorkList { weqs = emptyBag, wrest = emptyBag }
289 workListFromEq :: CanonicalCt -> WorkList
290 workListFromEq = workListFromEqs . singleCCan
292 workListFromNonEq :: CanonicalCt -> WorkList
293 workListFromNonEq = workListFromNonEqs . singleCCan
295 workListFromNonEqs :: CanonicalCts -> WorkList
296 workListFromNonEqs cts
297 = WorkList { weqs = emptyCCan, wrest = cts }
299 workListFromEqs :: CanonicalCts -> WorkList
301 = WorkList { weqs = cts, wrest = emptyCCan }
303 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
304 -> r -> WorkList -> m r
305 -- Prioritizes equalities
306 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
307 = do { r1 <- foldrBagM on_ct r eqs
308 ; foldrBagM on_ct r1 rest }
310 instance Outputable WorkList where
311 ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
312 , text "WorkList (Other) = " <+> ppr (wrest wl) ]
318 %************************************************************************
321 The "flavor" of a canonical constraint
323 %************************************************************************
326 getWantedLoc :: CanonicalCt -> WantedLoc
328 = ASSERT (isWanted (cc_flavor ct))
331 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
333 isWantedCt :: CanonicalCt -> Bool
334 isWantedCt ct = isWanted (cc_flavor ct)
335 isGivenCt :: CanonicalCt -> Bool
336 isGivenCt ct = isGiven (cc_flavor ct)
337 isDerivedCt :: CanonicalCt -> Bool
338 isDerivedCt ct = isDerived (cc_flavor ct)
340 canSolve :: CtFlavor -> CtFlavor -> Bool
341 -- canSolve ctid1 ctid2
342 -- The constraint ctid1 can be used to solve ctid2
343 -- "to solve" means a reaction where the active parts of the two constraints match.
344 -- active(F xis ~ xi) = F xis
345 -- active(tv ~ xi) = tv
346 -- active(D xis) = D xis
347 -- active(IP nm ty) = nm
349 -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
350 -----------------------------------------
351 canSolve (Given {}) _ = True
352 canSolve (Wanted {}) (Derived {}) = True
353 canSolve (Wanted {}) (Wanted {}) = True
354 canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
355 canSolve _ _ = False -- (There is no *evidence* for a derived.)
357 canRewrite :: CtFlavor -> CtFlavor -> Bool
358 -- canRewrite ctid1 ctid2
359 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
360 canRewrite = canSolve
362 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
363 -- Precondition: At least one of them should be wanted
364 combineCtLoc (Wanted loc) _ = loc
365 combineCtLoc _ (Wanted loc) = loc
366 combineCtLoc (Derived loc ) _ = loc
367 combineCtLoc _ (Derived loc ) = loc
368 combineCtLoc _ _ = panic "combineCtLoc: both given"
370 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
371 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
372 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
373 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
376 mkWantedFlavor :: CtFlavor -> CtFlavor
377 mkWantedFlavor (Wanted loc) = Wanted loc
378 mkWantedFlavor (Derived loc) = Wanted loc
379 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
382 %************************************************************************
384 %* The TcS solver monad *
386 %************************************************************************
390 The TcS monad is a weak form of the main Tc monad
394 * allocate new variables
395 * fill in evidence variables
397 Filling in a dictionary evidence variable means to create a binding
398 for it, so TcS carries a mutable location where the binding can be
399 added. This is initialised from the innermost implication constraint.
404 tcs_ev_binds :: EvBindsVar,
407 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
408 -- Global type bindings
410 tcs_context :: SimplContext,
412 tcs_untch :: TcsUntouchables,
414 tcs_ic_depth :: Int, -- Implication nesting depth
415 tcs_count :: IORef Int -- Global step count
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
426 = SimplInfer SDoc -- Inferring type of a let-bound thing
427 | SimplRuleLhs RuleName -- Inferring type of a RULE lhs
428 | SimplInteractive -- Inferring type at GHCi prompt
429 | SimplCheck SDoc -- Checking a type signature or RULE rhs
431 instance Outputable SimplContext where
432 ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
433 ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
434 ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
435 ppr SimplInteractive = ptext (sLit "SimplInteractive")
437 isInteractive :: SimplContext -> Bool
438 isInteractive SimplInteractive = True
439 isInteractive _ = False
441 simplEqsOnly :: SimplContext -> Bool
442 -- Simplify equalities only, not dictionaries
443 -- This is used for the LHS of rules; ee
444 -- Note [Simplifying RULE lhs constraints] in TcSimplify
445 simplEqsOnly (SimplRuleLhs {}) = True
446 simplEqsOnly _ = False
448 performDefaulting :: SimplContext -> Bool
449 performDefaulting (SimplInfer {}) = False
450 performDefaulting (SimplRuleLhs {}) = False
451 performDefaulting SimplInteractive = True
452 performDefaulting (SimplCheck {}) = True
455 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
457 instance Functor TcS where
458 fmap f m = TcS $ fmap f . unTcS m
460 instance Monad TcS where
461 return x = TcS (\_ -> return x)
462 fail err = TcS (\_ -> fail err)
463 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
465 -- Basic functionality
466 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
467 wrapTcS :: TcM a -> TcS a
468 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
469 -- and TcS is supposed to have limited functionality
470 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
472 wrapErrTcS :: TcM a -> TcS a
473 -- The thing wrapped should just fail
474 -- There's no static check; it's up to the user
475 -- Having a variant for each error message is too painful
478 wrapWarnTcS :: TcM a -> TcS a
479 -- The thing wrapped should just add a warning, or no-op
480 -- There's no static check; it's up to the user
481 wrapWarnTcS = wrapTcS
483 failTcS, panicTcS :: SDoc -> TcS a
484 failTcS = wrapTcS . TcM.failWith
485 panicTcS doc = pprPanic "TcCanonical" doc
487 traceTcS :: String -> SDoc -> TcS ()
488 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
490 bumpStepCountTcS :: TcS ()
491 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
492 ; n <- TcM.readTcRef ref
493 ; TcM.writeTcRef ref (n+1) }
495 traceFireTcS :: Int -> SDoc -> TcS ()
496 -- Dump a rule-firing trace
497 traceFireTcS depth doc
499 TcM.ifDOptM Opt_D_dump_cs_trace $
500 do { n <- TcM.readTcRef (tcs_count env)
502 <> text (replicate (tcs_ic_depth env) '>')
503 <> brackets (int depth) <+> doc
506 runTcS :: SimplContext
507 -> Untouchables -- Untouchables
508 -> TcS a -- What to run
509 -> TcM (a, Bag EvBind)
510 runTcS context untouch tcs
511 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
512 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
513 ; step_count <- TcM.newTcRef 0
514 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
515 , tcs_ty_binds = ty_binds_var
516 , tcs_context = context
517 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
518 , tcs_count = step_count
522 -- Run the computation
523 ; res <- unTcS tcs env
524 -- Perform the type unifications required
525 ; ty_binds <- TcM.readTcRef ty_binds_var
526 ; mapM_ do_unification (varEnvElts ty_binds)
529 ; count <- TcM.readTcRef step_count
531 TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count <+> ppr context)
534 ; ev_binds <- TcM.readTcRef evb_ref
535 ; return (res, evBindMapBinds ev_binds) }
537 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
539 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
540 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
541 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
542 , tcs_untch = (_outer_range, outer_tcs)
544 , tcs_ic_depth = idepth
545 , tcs_context = ctxt } ->
547 inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
548 -- The inner_range should be narrower than the outer one
549 -- (thus increasing the set of untouchables) but
550 -- the inner Tcs-untouchables must be unioned with the
552 nest_env = TcSEnv { tcs_ev_binds = ref
553 , tcs_ty_binds = ty_binds
554 , tcs_untch = inner_untch
556 , tcs_ic_depth = idepth+1
557 , tcs_context = ctxtUnderImplic ctxt }
559 thing_inside nest_env
561 recoverTcS :: TcS a -> TcS a -> TcS a
562 recoverTcS (TcS recovery_code) (TcS thing_inside)
564 TcM.recoverM (recovery_code env) (thing_inside env)
566 ctxtUnderImplic :: SimplContext -> SimplContext
567 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
568 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
569 <+> doubleQuotes (ftext n))
570 ctxtUnderImplic ctxt = ctxt
572 tryTcS :: TcS a -> TcS a
573 -- Like runTcS, but from within the TcS monad
574 -- Ignore all the evidence generated, and do not affect caller's evidence!
576 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
577 ; ev_binds_var <- TcM.newTcEvBinds
578 ; let env1 = env { tcs_ev_binds = ev_binds_var
579 , tcs_ty_binds = ty_binds_var }
583 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
585 getDynFlags :: TcS DynFlags
586 getDynFlags = wrapTcS TcM.getDOpts
588 getTcSContext :: TcS SimplContext
589 getTcSContext = TcS (return . tcs_context)
591 getTcEvBinds :: TcS EvBindsVar
592 getTcEvBinds = TcS (return . tcs_ev_binds)
594 getUntouchables :: TcS TcsUntouchables
595 getUntouchables = TcS (return . tcs_untch)
597 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
598 getTcSTyBinds = TcS (return . tcs_ty_binds)
600 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
601 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
604 getTcEvBindsBag :: TcS EvBindMap
606 = do { EvBindsVar ev_ref _ <- getTcEvBinds
607 ; wrapTcS $ TcM.readTcRef ev_ref }
609 setCoBind :: CoVar -> Coercion -> TcS ()
610 setCoBind cv co = setEvBind cv (EvCoercion co)
612 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
613 -- Add a type binding
614 -- We never do this twice!
615 setWantedTyBind tv ty
616 = do { ref <- getTcSTyBinds
618 do { ty_binds <- TcM.readTcRef ref
620 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
621 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
622 , ppr tv <+> text ":=" <+> ppr ty
623 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
625 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
627 setIPBind :: EvVar -> EvTerm -> TcS ()
628 setIPBind = setEvBind
630 setDictBind :: EvVar -> EvTerm -> TcS ()
631 setDictBind = setEvBind
633 setEvBind :: EvVar -> EvTerm -> TcS ()
636 = do { tc_evbinds <- getTcEvBinds
637 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
639 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
640 warnTcS loc warn_if doc
641 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
642 | otherwise = return ()
644 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
646 = do { ctxt <- getTcSContext
647 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
648 ; return (ctxt, tys, flags) }
650 -- Just get some environments needed for instance looking up and matching
651 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
653 getInstEnvs :: TcS (InstEnv, InstEnv)
654 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
656 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
657 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
659 getTopEnv :: TcS HscEnv
660 getTopEnv = wrapTcS $ TcM.getTopEnv
662 getGblEnv :: TcS TcGblEnv
663 getGblEnv = wrapTcS $ TcM.getGblEnv
665 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
666 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
668 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
669 checkWellStagedDFun pred dfun_id loc
670 = wrapTcS $ TcM.setCtLoc loc $
671 do { use_stage <- TcM.getStage
672 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
674 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
675 bind_lvl = TcM.topIdLvl dfun_id
677 pprEq :: TcType -> TcType -> SDoc
678 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
680 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
681 isTouchableMetaTyVar tv
682 = do { untch <- getUntouchables
683 ; return $ isTouchableMetaTyVar_InRange untch tv }
685 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
686 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
687 = case tcTyVarDetails tv of
688 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
689 -- See Note [Touchable meta type variables]
690 MetaTv {} -> inTouchableRange untch tv
697 Note [Touchable meta type variables]
698 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
699 Meta type variables allocated *by the constraint solver itself* are always
701 instance C a b => D [a] where...
702 if we use this instance declaration we "make up" a fresh meta type
703 variable for 'b', which we must later guess. (Perhaps C has a
704 functional dependency.) But since we aren't in the constraint *generator*
705 we can't allocate a Unique in the touchable range for this implication
706 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
711 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
713 newFlattenSkolemTy :: TcType -> TcS TcType
714 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
716 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
717 newFlattenSkolemTyVar ty
718 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
719 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
720 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
721 ; traceTcS "New Flatten Skolem Born" $
722 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
726 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
728 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
729 instDFunTypes mb_inst_tys
730 = mapM inst_tv mb_inst_tys
732 inst_tv :: Either TyVar TcType -> TcS Type
733 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
734 inst_tv (Right ty) = return ty
736 instDFunConstraints :: TcThetaType -> TcS [EvVar]
737 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
740 instFlexiTcS :: TyVar -> TcS TcTyVar
741 -- Like TcM.instMetaTyVar but the variable that is created is always
742 -- touchable; we are supposed to guess its instantiation.
743 -- See Note [Touchable meta type variables]
744 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
746 newFlexiTcSTy :: Kind -> TcS TcType
749 do { uniq <- TcM.newUnique
750 ; ref <- TcM.newMutVar Flexi
751 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
752 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
754 isFlexiTcsTv :: TyVar -> Bool
756 | not (isTcTyVar tv) = False
757 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
760 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
761 -- Create new wanted CoVar that constrains the type to have the specified kind.
762 newKindConstraint tv knd
763 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
764 ; let ty_k = mkTyVarTy tv_k
765 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
768 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
769 instFlexiTcSHelper tvname tvkind
771 do { uniq <- TcM.newUnique
772 ; ref <- TcM.newMutVar Flexi
773 ; let name = setNameUnique tvname uniq
775 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
777 -- Superclasses and recursive dictionaries
778 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
780 newEvVar :: TcPredType -> TcS EvVar
781 newEvVar pty = wrapTcS $ TcM.newEvVar pty
783 newDerivedId :: TcPredType -> TcS EvVar
784 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
786 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
787 -- Note we create immutable variables for given or derived, since we
788 -- must bind them to TcEvBinds (because their evidence may involve
789 -- superclasses). However we should be able to override existing
790 -- 'derived' evidence, even in TcEvBinds
791 newGivenCoVar ty1 ty2 co
792 = do { cv <- newCoVar ty1 ty2
793 ; setEvBind cv (EvCoercion co)
796 newCoVar :: TcType -> TcType -> TcS EvVar
797 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
799 newIPVar :: IPName Name -> TcType -> TcS EvVar
800 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
802 newDictVar :: Class -> [TcType] -> TcS EvVar
803 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
808 -- Matching and looking up classes and family instances
809 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
811 data MatchInstResult mi
812 = MatchInstNo -- No matching instance
813 | MatchInstSingle mi -- Single matching instance
814 | MatchInstMany -- Multiple matching instances
817 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
818 -- Look up a class constraint in the instance environment
820 = do { let pred = mkClassPred clas tys
821 ; instEnvs <- getInstEnvs
822 ; case lookupInstEnv instEnvs clas tys of {
823 ([], unifs) -- Nothing matches
824 -> do { traceTcS "matchClass not matching"
825 (vcat [ text "dict" <+> ppr pred,
826 text "unifs" <+> ppr unifs ])
829 ([(ispec, inst_tys)], []) -- A single match
830 -> do { let dfun_id = is_dfun ispec
831 ; traceTcS "matchClass success"
832 (vcat [text "dict" <+> ppr pred,
833 text "witness" <+> ppr dfun_id
834 <+> ppr (idType dfun_id) ])
835 -- Record that this dfun is needed
836 ; return $ MatchInstSingle (dfun_id, inst_tys)
838 (matches, unifs) -- More than one matches
839 -> do { traceTcS "matchClass multiple matches, deferring choice"
840 (vcat [text "dict" <+> ppr pred,
841 text "matches" <+> ppr matches,
842 text "unifs" <+> ppr unifs])
843 ; return MatchInstMany
850 -> TcS (MatchInstResult (TyCon, [Type]))
852 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
854 Nothing -> return MatchInstNo
855 Just res -> return $ MatchInstSingle res
856 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
857 -- multiple matches. Check.