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
108 import StaticFlags( opt_PprStyle_Debug )
109 import Control.Monad( when )
114 %************************************************************************
116 %* Canonical constraints *
118 %* These are the constraints the low-level simplifier works with *
120 %************************************************************************
123 -- Types without any type functions inside. However, note that xi
124 -- types CAN contain unexpanded type synonyms; however, the
125 -- (transitive) expansions of those type synonyms will not contain any
127 type Xi = Type -- In many comments, "xi" ranges over Xi
129 type CanonicalCts = Bag CanonicalCt
132 -- Atomic canonical constraints
133 = CDictCan { -- e.g. Num xi
135 cc_flavor :: CtFlavor,
140 | CIPCan { -- ?x::tau
141 -- See note [Canonical implicit parameter constraints].
143 cc_flavor :: CtFlavor,
144 cc_ip_nm :: IPName Name,
145 cc_ip_ty :: TcTauType
148 | CTyEqCan { -- tv ~ xi (recall xi means function free)
150 -- * tv not in tvs(xi) (occurs check)
151 -- * typeKind xi `compatKind` typeKind tv
152 -- See Note [Spontaneous solving and kind compatibility]
153 -- * We prefer unification variables on the left *JUST* for efficiency
155 cc_flavor :: CtFlavor,
160 | CFunEqCan { -- F xis ~ xi
161 -- Invariant: * isSynFamilyTyCon cc_fun
162 -- * typeKind (F xis) `compatKind` typeKind xi
164 cc_flavor :: CtFlavor,
165 cc_fun :: TyCon, -- A type function
166 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
167 cc_rhs :: Xi -- *never* over-saturated (because if so
168 -- we should have decomposed)
172 | CFrozenErr { -- A "frozen error" does not interact with anything
173 -- See Note [Frozen Errors]
175 cc_flavor :: CtFlavor
178 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
179 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
181 compatKind :: Kind -> Kind -> Bool
182 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
184 deCanonicalise :: CanonicalCt -> FlavoredEvVar
185 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
187 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
188 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
189 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
190 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
191 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
192 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
194 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
195 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
196 tyVarsOfCDict _ct = emptyVarSet
198 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
199 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
201 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
202 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
204 instance Outputable CanonicalCt where
205 ppr (CDictCan d fl cls tys)
206 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
207 ppr (CIPCan ip fl ip_nm ty)
208 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
209 ppr (CTyEqCan co fl tv ty)
210 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
211 ppr (CFunEqCan co fl tc tys ty)
212 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
213 ppr (CFrozenErr co fl)
214 = ppr fl <+> pprEvVarWithType co
217 Note [Canonical implicit parameter constraints]
218 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
219 The type in a canonical implicit parameter constraint doesn't need to
220 be a xi (type-function-free type) since we can defer the flattening
221 until checking this type for equality with another type. If we
222 encounter two IP constraints with the same name, they MUST have the
223 same type, and at that point we can generate a flattened equality
224 constraint between the types. (On the other hand, the types in two
225 class constraints for the same class MAY be equal, so they need to be
226 flattened in the first place to facilitate comparing them.)
229 singleCCan :: CanonicalCt -> CanonicalCts
232 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
235 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
236 extendCCans = snocBag
238 andCCans :: [CanonicalCts] -> CanonicalCts
239 andCCans = unionManyBags
241 emptyCCan :: CanonicalCts
244 isEmptyCCan :: CanonicalCts -> Bool
245 isEmptyCCan = isEmptyBag
247 isCTyEqCan :: CanonicalCt -> Bool
248 isCTyEqCan (CTyEqCan {}) = True
249 isCTyEqCan (CFunEqCan {}) = False
252 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
253 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
254 isCDictCan_Maybe _ = Nothing
256 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
257 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
258 isCIPCan_Maybe _ = Nothing
260 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
261 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
262 isCFunEqCan_Maybe _ = Nothing
264 isCFrozenErr :: CanonicalCt -> Bool
265 isCFrozenErr (CFrozenErr {}) = True
266 isCFrozenErr _ = False
269 -- A mixture of Given, Wanted, and Derived constraints.
270 -- We split between equalities and the rest to process equalities first.
271 data WorkList = WorkList { weqs :: CanonicalCts
272 -- NB: weqs includes equalities /and/ family equalities
273 , wrest :: CanonicalCts }
275 unionWorkList :: WorkList -> WorkList -> WorkList
276 unionWorkList wl1 wl2
277 = WorkList { weqs = weqs wl1 `andCCan` weqs wl2
278 , wrest = wrest wl1 `andCCan` wrest wl2 }
280 unionWorkLists :: [WorkList] -> WorkList
281 unionWorkLists = foldr unionWorkList emptyWorkList
283 isEmptyWorkList :: WorkList -> Bool
284 isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
286 emptyWorkList :: WorkList
288 = WorkList { weqs = emptyBag, wrest = emptyBag }
290 workListFromEq :: CanonicalCt -> WorkList
291 workListFromEq = workListFromEqs . singleCCan
293 workListFromNonEq :: CanonicalCt -> WorkList
294 workListFromNonEq = workListFromNonEqs . singleCCan
296 workListFromNonEqs :: CanonicalCts -> WorkList
297 workListFromNonEqs cts
298 = WorkList { weqs = emptyCCan, wrest = cts }
300 workListFromEqs :: CanonicalCts -> WorkList
302 = WorkList { weqs = cts, wrest = emptyCCan }
304 foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
305 -> r -> WorkList -> m r
306 -- Prioritizes equalities
307 foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
308 = do { r1 <- foldrBagM on_ct r eqs
309 ; foldrBagM on_ct r1 rest }
311 instance Outputable WorkList where
312 ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
313 , text "WorkList (Other) = " <+> ppr (wrest wl) ]
319 %************************************************************************
322 The "flavor" of a canonical constraint
324 %************************************************************************
327 getWantedLoc :: CanonicalCt -> WantedLoc
329 = ASSERT (isWanted (cc_flavor ct))
332 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
334 isWantedCt :: CanonicalCt -> Bool
335 isWantedCt ct = isWanted (cc_flavor ct)
336 isGivenCt :: CanonicalCt -> Bool
337 isGivenCt ct = isGiven (cc_flavor ct)
338 isDerivedCt :: CanonicalCt -> Bool
339 isDerivedCt ct = isDerived (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
350 -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
351 -----------------------------------------
352 canSolve (Given {}) _ = True
353 canSolve (Wanted {}) (Derived {}) = True
354 canSolve (Wanted {}) (Wanted {}) = True
355 canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
356 canSolve _ _ = False -- (There is no *evidence* for a derived.)
358 canRewrite :: CtFlavor -> CtFlavor -> Bool
359 -- canRewrite ctid1 ctid2
360 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
361 canRewrite = canSolve
363 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
364 -- Precondition: At least one of them should be wanted
365 combineCtLoc (Wanted loc) _ = loc
366 combineCtLoc _ (Wanted loc) = loc
367 combineCtLoc (Derived loc ) _ = loc
368 combineCtLoc _ (Derived loc ) = loc
369 combineCtLoc _ _ = panic "combineCtLoc: both given"
371 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
372 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
373 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
374 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
377 mkWantedFlavor :: CtFlavor -> CtFlavor
378 mkWantedFlavor (Wanted loc) = Wanted loc
379 mkWantedFlavor (Derived loc) = Wanted loc
380 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
383 %************************************************************************
385 %* The TcS solver monad *
387 %************************************************************************
391 The TcS monad is a weak form of the main Tc monad
395 * allocate new variables
396 * fill in evidence variables
398 Filling in a dictionary evidence variable means to create a binding
399 for it, so TcS carries a mutable location where the binding can be
400 added. This is initialised from the innermost implication constraint.
405 tcs_ev_binds :: EvBindsVar,
408 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
409 -- Global type bindings
411 tcs_context :: SimplContext,
413 tcs_untch :: TcsUntouchables,
415 tcs_ic_depth :: Int, -- Implication nesting depth
416 tcs_count :: IORef Int -- Global step count
419 type TcsUntouchables = (Untouchables,TcTyVarSet)
420 -- Like the TcM Untouchables,
421 -- but records extra TcsTv variables generated during simplification
422 -- See Note [Extra TcsTv untouchables] in TcSimplify
427 = SimplInfer SDoc -- Inferring type of a let-bound thing
428 | SimplRuleLhs RuleName -- Inferring type of a RULE lhs
429 | SimplInteractive -- Inferring type at GHCi prompt
430 | SimplCheck SDoc -- Checking a type signature or RULE rhs
432 instance Outputable SimplContext where
433 ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
434 ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
435 ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
436 ppr SimplInteractive = ptext (sLit "SimplInteractive")
438 isInteractive :: SimplContext -> Bool
439 isInteractive SimplInteractive = True
440 isInteractive _ = False
442 simplEqsOnly :: SimplContext -> Bool
443 -- Simplify equalities only, not dictionaries
444 -- This is used for the LHS of rules; ee
445 -- Note [Simplifying RULE lhs constraints] in TcSimplify
446 simplEqsOnly (SimplRuleLhs {}) = True
447 simplEqsOnly _ = False
449 performDefaulting :: SimplContext -> Bool
450 performDefaulting (SimplInfer {}) = False
451 performDefaulting (SimplRuleLhs {}) = False
452 performDefaulting SimplInteractive = True
453 performDefaulting (SimplCheck {}) = True
456 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
458 instance Functor TcS where
459 fmap f m = TcS $ fmap f . unTcS m
461 instance Monad TcS where
462 return x = TcS (\_ -> return x)
463 fail err = TcS (\_ -> fail err)
464 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
466 -- Basic functionality
467 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
468 wrapTcS :: TcM a -> TcS a
469 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
470 -- and TcS is supposed to have limited functionality
471 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
473 wrapErrTcS :: TcM a -> TcS a
474 -- The thing wrapped should just fail
475 -- There's no static check; it's up to the user
476 -- Having a variant for each error message is too painful
479 wrapWarnTcS :: TcM a -> TcS a
480 -- The thing wrapped should just add a warning, or no-op
481 -- There's no static check; it's up to the user
482 wrapWarnTcS = wrapTcS
484 failTcS, panicTcS :: SDoc -> TcS a
485 failTcS = wrapTcS . TcM.failWith
486 panicTcS doc = pprPanic "TcCanonical" doc
488 traceTcS :: String -> SDoc -> TcS ()
489 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
491 bumpStepCountTcS :: TcS ()
492 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
493 ; n <- TcM.readTcRef ref
494 ; TcM.writeTcRef ref (n+1) }
496 traceFireTcS :: Int -> SDoc -> TcS ()
497 -- Dump a rule-firing trace
498 traceFireTcS depth doc
500 TcM.ifDOptM Opt_D_dump_cs_trace $
501 do { n <- TcM.readTcRef (tcs_count env)
503 <> text (replicate (tcs_ic_depth env) '>')
504 <> brackets (int depth) <+> doc
507 runTcS :: SimplContext
508 -> Untouchables -- Untouchables
509 -> TcS a -- What to run
510 -> TcM (a, Bag EvBind)
511 runTcS context untouch tcs
512 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
513 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
514 ; step_count <- TcM.newTcRef 0
515 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
516 , tcs_ty_binds = ty_binds_var
517 , tcs_context = context
518 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
519 , tcs_count = step_count
523 -- Run the computation
524 ; res <- unTcS tcs env
525 -- Perform the type unifications required
526 ; ty_binds <- TcM.readTcRef ty_binds_var
527 ; mapM_ do_unification (varEnvElts ty_binds)
530 ; count <- TcM.readTcRef step_count
531 ; when (opt_PprStyle_Debug && count > 0) $
532 TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
533 <+> int count <+> ppr context)
536 ; ev_binds <- TcM.readTcRef evb_ref
537 ; return (res, evBindMapBinds ev_binds) }
539 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
541 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
542 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
543 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
544 , tcs_untch = (_outer_range, outer_tcs)
546 , tcs_ic_depth = idepth
547 , tcs_context = ctxt } ->
549 inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
550 -- The inner_range should be narrower than the outer one
551 -- (thus increasing the set of untouchables) but
552 -- the inner Tcs-untouchables must be unioned with the
554 nest_env = TcSEnv { tcs_ev_binds = ref
555 , tcs_ty_binds = ty_binds
556 , tcs_untch = inner_untch
558 , tcs_ic_depth = idepth+1
559 , tcs_context = ctxtUnderImplic ctxt }
561 thing_inside nest_env
563 recoverTcS :: TcS a -> TcS a -> TcS a
564 recoverTcS (TcS recovery_code) (TcS thing_inside)
566 TcM.recoverM (recovery_code env) (thing_inside env)
568 ctxtUnderImplic :: SimplContext -> SimplContext
569 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
570 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
571 <+> doubleQuotes (ftext n))
572 ctxtUnderImplic ctxt = ctxt
574 tryTcS :: TcS a -> TcS a
575 -- Like runTcS, but from within the TcS monad
576 -- Ignore all the evidence generated, and do not affect caller's evidence!
578 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
579 ; ev_binds_var <- TcM.newTcEvBinds
580 ; let env1 = env { tcs_ev_binds = ev_binds_var
581 , tcs_ty_binds = ty_binds_var }
585 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
587 getDynFlags :: TcS DynFlags
588 getDynFlags = wrapTcS TcM.getDOpts
590 getTcSContext :: TcS SimplContext
591 getTcSContext = TcS (return . tcs_context)
593 getTcEvBinds :: TcS EvBindsVar
594 getTcEvBinds = TcS (return . tcs_ev_binds)
596 getUntouchables :: TcS TcsUntouchables
597 getUntouchables = TcS (return . tcs_untch)
599 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
600 getTcSTyBinds = TcS (return . tcs_ty_binds)
602 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
603 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
606 getTcEvBindsBag :: TcS EvBindMap
608 = do { EvBindsVar ev_ref _ <- getTcEvBinds
609 ; wrapTcS $ TcM.readTcRef ev_ref }
611 setCoBind :: CoVar -> Coercion -> TcS ()
612 setCoBind cv co = setEvBind cv (EvCoercion co)
614 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
615 -- Add a type binding
616 -- We never do this twice!
617 setWantedTyBind tv ty
618 = do { ref <- getTcSTyBinds
620 do { ty_binds <- TcM.readTcRef ref
622 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
623 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
624 , ppr tv <+> text ":=" <+> ppr ty
625 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
627 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
629 setIPBind :: EvVar -> EvTerm -> TcS ()
630 setIPBind = setEvBind
632 setDictBind :: EvVar -> EvTerm -> TcS ()
633 setDictBind = setEvBind
635 setEvBind :: EvVar -> EvTerm -> TcS ()
638 = do { tc_evbinds <- getTcEvBinds
639 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
641 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
642 warnTcS loc warn_if doc
643 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
644 | otherwise = return ()
646 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
648 = do { ctxt <- getTcSContext
649 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
650 ; return (ctxt, tys, flags) }
652 -- Just get some environments needed for instance looking up and matching
653 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
655 getInstEnvs :: TcS (InstEnv, InstEnv)
656 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
658 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
659 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
661 getTopEnv :: TcS HscEnv
662 getTopEnv = wrapTcS $ TcM.getTopEnv
664 getGblEnv :: TcS TcGblEnv
665 getGblEnv = wrapTcS $ TcM.getGblEnv
667 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
668 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
670 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
671 checkWellStagedDFun pred dfun_id loc
672 = wrapTcS $ TcM.setCtLoc loc $
673 do { use_stage <- TcM.getStage
674 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
676 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
677 bind_lvl = TcM.topIdLvl dfun_id
679 pprEq :: TcType -> TcType -> SDoc
680 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
682 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
683 isTouchableMetaTyVar tv
684 = do { untch <- getUntouchables
685 ; return $ isTouchableMetaTyVar_InRange untch tv }
687 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
688 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
689 = case tcTyVarDetails tv of
690 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
691 -- See Note [Touchable meta type variables]
692 MetaTv {} -> inTouchableRange untch tv
699 Note [Touchable meta type variables]
700 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
701 Meta type variables allocated *by the constraint solver itself* are always
703 instance C a b => D [a] where...
704 if we use this instance declaration we "make up" a fresh meta type
705 variable for 'b', which we must later guess. (Perhaps C has a
706 functional dependency.) But since we aren't in the constraint *generator*
707 we can't allocate a Unique in the touchable range for this implication
708 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
713 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
715 newFlattenSkolemTy :: TcType -> TcS TcType
716 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
718 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
719 newFlattenSkolemTyVar ty
720 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
721 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
722 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
723 ; traceTcS "New Flatten Skolem Born" $
724 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
728 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
730 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
731 instDFunTypes mb_inst_tys
732 = mapM inst_tv mb_inst_tys
734 inst_tv :: Either TyVar TcType -> TcS Type
735 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
736 inst_tv (Right ty) = return ty
738 instDFunConstraints :: TcThetaType -> TcS [EvVar]
739 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
742 instFlexiTcS :: TyVar -> TcS TcTyVar
743 -- Like TcM.instMetaTyVar but the variable that is created is always
744 -- touchable; we are supposed to guess its instantiation.
745 -- See Note [Touchable meta type variables]
746 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
748 newFlexiTcSTy :: Kind -> TcS TcType
751 do { uniq <- TcM.newUnique
752 ; ref <- TcM.newMutVar Flexi
753 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
754 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
756 isFlexiTcsTv :: TyVar -> Bool
758 | not (isTcTyVar tv) = False
759 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
762 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
763 -- Create new wanted CoVar that constrains the type to have the specified kind.
764 newKindConstraint tv knd
765 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
766 ; let ty_k = mkTyVarTy tv_k
767 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
770 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
771 instFlexiTcSHelper tvname tvkind
773 do { uniq <- TcM.newUnique
774 ; ref <- TcM.newMutVar Flexi
775 ; let name = setNameUnique tvname uniq
777 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
779 -- Superclasses and recursive dictionaries
780 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
782 newEvVar :: TcPredType -> TcS EvVar
783 newEvVar pty = wrapTcS $ TcM.newEvVar pty
785 newDerivedId :: TcPredType -> TcS EvVar
786 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
788 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
789 -- Note we create immutable variables for given or derived, since we
790 -- must bind them to TcEvBinds (because their evidence may involve
791 -- superclasses). However we should be able to override existing
792 -- 'derived' evidence, even in TcEvBinds
793 newGivenCoVar ty1 ty2 co
794 = do { cv <- newCoVar ty1 ty2
795 ; setEvBind cv (EvCoercion co)
798 newCoVar :: TcType -> TcType -> TcS EvVar
799 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
801 newIPVar :: IPName Name -> TcType -> TcS EvVar
802 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
804 newDictVar :: Class -> [TcType] -> TcS EvVar
805 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
810 -- Matching and looking up classes and family instances
811 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
813 data MatchInstResult mi
814 = MatchInstNo -- No matching instance
815 | MatchInstSingle mi -- Single matching instance
816 | MatchInstMany -- Multiple matching instances
819 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
820 -- Look up a class constraint in the instance environment
822 = do { let pred = mkClassPred clas tys
823 ; instEnvs <- getInstEnvs
824 ; case lookupInstEnv instEnvs clas tys of {
825 ([], unifs) -- Nothing matches
826 -> do { traceTcS "matchClass not matching"
827 (vcat [ text "dict" <+> ppr pred,
828 text "unifs" <+> ppr unifs ])
831 ([(ispec, inst_tys)], []) -- A single match
832 -> do { let dfun_id = is_dfun ispec
833 ; traceTcS "matchClass success"
834 (vcat [text "dict" <+> ppr pred,
835 text "witness" <+> ppr dfun_id
836 <+> ppr (idType dfun_id) ])
837 -- Record that this dfun is needed
838 ; return $ MatchInstSingle (dfun_id, inst_tys)
840 (matches, unifs) -- More than one matches
841 -> do { traceTcS "matchClass multiple matches, deferring choice"
842 (vcat [text "dict" <+> ppr pred,
843 text "matches" <+> ppr matches,
844 text "unifs" <+> ppr unifs])
845 ; return MatchInstMany
852 -> TcS (MatchInstResult (TyCon, [Type]))
854 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
856 Nothing -> return MatchInstNo
857 Just res -> return $ MatchInstSingle res
858 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
859 -- multiple matches. Check.