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 StaticFlags( opt_PprStyle_Debug )
108 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
530 ; when (opt_PprStyle_Debug && count > 0) $
531 TcM.debugDumpTcRn (ptext (sLit "Constraint solver steps =")
532 <+> int count <+> ppr context)
535 ; ev_binds <- TcM.readTcRef evb_ref
536 ; return (res, evBindMapBinds ev_binds) }
538 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
540 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
541 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
542 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
543 , tcs_untch = (_outer_range, outer_tcs)
545 , tcs_ic_depth = idepth
546 , tcs_context = ctxt } ->
548 inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
549 -- The inner_range should be narrower than the outer one
550 -- (thus increasing the set of untouchables) but
551 -- the inner Tcs-untouchables must be unioned with the
553 nest_env = TcSEnv { tcs_ev_binds = ref
554 , tcs_ty_binds = ty_binds
555 , tcs_untch = inner_untch
557 , tcs_ic_depth = idepth+1
558 , tcs_context = ctxtUnderImplic ctxt }
560 thing_inside nest_env
562 recoverTcS :: TcS a -> TcS a -> TcS a
563 recoverTcS (TcS recovery_code) (TcS thing_inside)
565 TcM.recoverM (recovery_code env) (thing_inside env)
567 ctxtUnderImplic :: SimplContext -> SimplContext
568 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
569 ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
570 <+> doubleQuotes (ftext n))
571 ctxtUnderImplic ctxt = ctxt
573 tryTcS :: TcS a -> TcS a
574 -- Like runTcS, but from within the TcS monad
575 -- Ignore all the evidence generated, and do not affect caller's evidence!
577 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
578 ; ev_binds_var <- TcM.newTcEvBinds
579 ; let env1 = env { tcs_ev_binds = ev_binds_var
580 , tcs_ty_binds = ty_binds_var }
584 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
586 getDynFlags :: TcS DynFlags
587 getDynFlags = wrapTcS TcM.getDOpts
589 getTcSContext :: TcS SimplContext
590 getTcSContext = TcS (return . tcs_context)
592 getTcEvBinds :: TcS EvBindsVar
593 getTcEvBinds = TcS (return . tcs_ev_binds)
595 getUntouchables :: TcS TcsUntouchables
596 getUntouchables = TcS (return . tcs_untch)
598 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
599 getTcSTyBinds = TcS (return . tcs_ty_binds)
601 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
602 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
605 getTcEvBindsBag :: TcS EvBindMap
607 = do { EvBindsVar ev_ref _ <- getTcEvBinds
608 ; wrapTcS $ TcM.readTcRef ev_ref }
610 setCoBind :: CoVar -> Coercion -> TcS ()
611 setCoBind cv co = setEvBind cv (EvCoercion co)
613 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
614 -- Add a type binding
615 -- We never do this twice!
616 setWantedTyBind tv ty
617 = do { ref <- getTcSTyBinds
619 do { ty_binds <- TcM.readTcRef ref
621 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
622 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
623 , ppr tv <+> text ":=" <+> ppr ty
624 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
626 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
628 setIPBind :: EvVar -> EvTerm -> TcS ()
629 setIPBind = setEvBind
631 setDictBind :: EvVar -> EvTerm -> TcS ()
632 setDictBind = setEvBind
634 setEvBind :: EvVar -> EvTerm -> TcS ()
637 = do { tc_evbinds <- getTcEvBinds
638 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
640 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
641 warnTcS loc warn_if doc
642 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
643 | otherwise = return ()
645 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
647 = do { ctxt <- getTcSContext
648 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
649 ; return (ctxt, tys, flags) }
651 -- Just get some environments needed for instance looking up and matching
652 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
654 getInstEnvs :: TcS (InstEnv, InstEnv)
655 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
657 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
658 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
660 getTopEnv :: TcS HscEnv
661 getTopEnv = wrapTcS $ TcM.getTopEnv
663 getGblEnv :: TcS TcGblEnv
664 getGblEnv = wrapTcS $ TcM.getGblEnv
666 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
667 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
669 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
670 checkWellStagedDFun pred dfun_id loc
671 = wrapTcS $ TcM.setCtLoc loc $
672 do { use_stage <- TcM.getStage
673 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
675 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
676 bind_lvl = TcM.topIdLvl dfun_id
678 pprEq :: TcType -> TcType -> SDoc
679 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
681 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
682 isTouchableMetaTyVar tv
683 = do { untch <- getUntouchables
684 ; return $ isTouchableMetaTyVar_InRange untch tv }
686 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
687 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
688 = case tcTyVarDetails tv of
689 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
690 -- See Note [Touchable meta type variables]
691 MetaTv {} -> inTouchableRange untch tv
698 Note [Touchable meta type variables]
699 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
700 Meta type variables allocated *by the constraint solver itself* are always
702 instance C a b => D [a] where...
703 if we use this instance declaration we "make up" a fresh meta type
704 variable for 'b', which we must later guess. (Perhaps C has a
705 functional dependency.) But since we aren't in the constraint *generator*
706 we can't allocate a Unique in the touchable range for this implication
707 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
712 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
714 newFlattenSkolemTy :: TcType -> TcS TcType
715 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
717 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
718 newFlattenSkolemTyVar ty
719 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
720 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
721 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
722 ; traceTcS "New Flatten Skolem Born" $
723 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
727 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
729 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
730 instDFunTypes mb_inst_tys
731 = mapM inst_tv mb_inst_tys
733 inst_tv :: Either TyVar TcType -> TcS Type
734 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
735 inst_tv (Right ty) = return ty
737 instDFunConstraints :: TcThetaType -> TcS [EvVar]
738 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
741 instFlexiTcS :: TyVar -> TcS TcTyVar
742 -- Like TcM.instMetaTyVar but the variable that is created is always
743 -- touchable; we are supposed to guess its instantiation.
744 -- See Note [Touchable meta type variables]
745 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
747 newFlexiTcSTy :: Kind -> TcS TcType
750 do { uniq <- TcM.newUnique
751 ; ref <- TcM.newMutVar Flexi
752 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
753 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
755 isFlexiTcsTv :: TyVar -> Bool
757 | not (isTcTyVar tv) = False
758 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
761 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
762 -- Create new wanted CoVar that constrains the type to have the specified kind.
763 newKindConstraint tv knd
764 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
765 ; let ty_k = mkTyVarTy tv_k
766 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
769 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
770 instFlexiTcSHelper tvname tvkind
772 do { uniq <- TcM.newUnique
773 ; ref <- TcM.newMutVar Flexi
774 ; let name = setNameUnique tvname uniq
776 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
778 -- Superclasses and recursive dictionaries
779 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
781 newEvVar :: TcPredType -> TcS EvVar
782 newEvVar pty = wrapTcS $ TcM.newEvVar pty
784 newDerivedId :: TcPredType -> TcS EvVar
785 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
787 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
788 -- Note we create immutable variables for given or derived, since we
789 -- must bind them to TcEvBinds (because their evidence may involve
790 -- superclasses). However we should be able to override existing
791 -- 'derived' evidence, even in TcEvBinds
792 newGivenCoVar ty1 ty2 co
793 = do { cv <- newCoVar ty1 ty2
794 ; setEvBind cv (EvCoercion co)
797 newCoVar :: TcType -> TcType -> TcS EvVar
798 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
800 newIPVar :: IPName Name -> TcType -> TcS EvVar
801 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
803 newDictVar :: Class -> [TcType] -> TcS EvVar
804 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
809 -- Matching and looking up classes and family instances
810 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
812 data MatchInstResult mi
813 = MatchInstNo -- No matching instance
814 | MatchInstSingle mi -- Single matching instance
815 | MatchInstMany -- Multiple matching instances
818 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
819 -- Look up a class constraint in the instance environment
821 = do { let pred = mkClassPred clas tys
822 ; instEnvs <- getInstEnvs
823 ; case lookupInstEnv instEnvs clas tys of {
824 ([], unifs) -- Nothing matches
825 -> do { traceTcS "matchClass not matching"
826 (vcat [ text "dict" <+> ppr pred,
827 text "unifs" <+> ppr unifs ])
830 ([(ispec, inst_tys)], []) -- A single match
831 -> do { let dfun_id = is_dfun ispec
832 ; traceTcS "matchClass success"
833 (vcat [text "dict" <+> ppr pred,
834 text "witness" <+> ppr dfun_id
835 <+> ppr (idType dfun_id) ])
836 -- Record that this dfun is needed
837 ; return $ MatchInstSingle (dfun_id, inst_tys)
839 (matches, unifs) -- More than one matches
840 -> do { traceTcS "matchClass multiple matches, deferring choice"
841 (vcat [text "dict" <+> ppr pred,
842 text "matches" <+> ppr matches,
843 text "unifs" <+> ppr unifs])
844 ; return MatchInstMany
851 -> TcS (MatchInstResult (TyCon, [Type]))
853 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
855 Nothing -> return MatchInstNo
856 Just res -> return $ MatchInstSingle res
857 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
858 -- multiple matches. Check.