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 CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
12 deCanonicalise, mkFrozenError,
14 isWanted, isGiven, isDerived,
15 isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
20 combineCtLoc, mkGivenFlavor, mkWantedFlavor,
23 TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
24 traceFireTcS, bumpStepCountTcS,
25 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
26 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
28 -- Creation of evidence variables
29 newEvVar, newCoVar, newGivenCoVar,
31 newIPVar, newDictVar, newKindConstraint,
33 -- Setting evidence variables
34 setCoBind, setIPBind, setDictBind, setEvBind,
38 getInstEnvs, getFamInstEnvs, -- Getting the environments
39 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
40 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
42 newFlattenSkolemTy, -- Flatten skolems
45 instDFunTypes, -- Instantiation
47 newFlexiTcSTy, instFlexiTcS,
53 isTouchableMetaTyVar_InRange,
55 getDefaultInfo, getDynFlags,
57 matchClass, matchFam, MatchInstResult (..),
60 pprEq -- Smaller utils, re-exported from TcM
61 -- TODO (DV): these are only really used in the
62 -- instance matcher in TcSimplify. I am wondering
63 -- if the whole instance matcher simply belongs
67 #include "HsVersions.h"
77 import qualified TcRnMonad as TcM
78 import qualified TcMType as TcM
79 import qualified TcEnv as TcM
80 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
98 import HsBinds -- for TcEvBinds stuff
107 %************************************************************************
109 %* Canonical constraints *
111 %* These are the constraints the low-level simplifier works with *
113 %************************************************************************
116 -- Types without any type functions inside. However, note that xi
117 -- types CAN contain unexpanded type synonyms; however, the
118 -- (transitive) expansions of those type synonyms will not contain any
120 type Xi = Type -- In many comments, "xi" ranges over Xi
122 type CanonicalCts = Bag CanonicalCt
125 -- Atomic canonical constraints
126 = CDictCan { -- e.g. Num xi
128 cc_flavor :: CtFlavor,
133 | CIPCan { -- ?x::tau
134 -- See note [Canonical implicit parameter constraints].
136 cc_flavor :: CtFlavor,
137 cc_ip_nm :: IPName Name,
138 cc_ip_ty :: TcTauType
141 | CTyEqCan { -- tv ~ xi (recall xi means function free)
143 -- * tv not in tvs(xi) (occurs check)
144 -- * typeKind xi `compatKind` typeKind tv
145 -- See Note [Spontaneous solving and kind compatibility]
146 -- * We prefer unification variables on the left *JUST* for efficiency
148 cc_flavor :: CtFlavor,
153 | CFunEqCan { -- F xis ~ xi
154 -- Invariant: * isSynFamilyTyCon cc_fun
155 -- * typeKind (F xis) `compatKind` typeKind xi
157 cc_flavor :: CtFlavor,
158 cc_fun :: TyCon, -- A type function
159 cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
160 cc_rhs :: Xi -- *never* over-saturated (because if so
161 -- we should have decomposed)
165 | CFrozenErr { -- A "frozen error" does not interact with anything
166 -- See Note [Frozen Errors]
168 cc_flavor :: CtFlavor
171 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
172 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
174 compatKind :: Kind -> Kind -> Bool
175 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
177 deCanonicalise :: CanonicalCt -> FlavoredEvVar
178 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
180 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
181 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
182 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
183 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
184 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
185 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
187 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
188 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
189 tyVarsOfCDict _ct = emptyVarSet
191 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
192 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
194 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
195 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
197 instance Outputable CanonicalCt where
198 ppr (CDictCan d fl cls tys)
199 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
200 ppr (CIPCan ip fl ip_nm ty)
201 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
202 ppr (CTyEqCan co fl tv ty)
203 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
204 ppr (CFunEqCan co fl tc tys ty)
205 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
206 ppr (CFrozenErr co fl)
207 = ppr fl <+> pprEvVarWithType co
210 Note [Canonical implicit parameter constraints]
211 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
212 The type in a canonical implicit parameter constraint doesn't need to
213 be a xi (type-function-free type) since we can defer the flattening
214 until checking this type for equality with another type. If we
215 encounter two IP constraints with the same name, they MUST have the
216 same type, and at that point we can generate a flattened equality
217 constraint between the types. (On the other hand, the types in two
218 class constraints for the same class MAY be equal, so they need to be
219 flattened in the first place to facilitate comparing them.)
222 singleCCan :: CanonicalCt -> CanonicalCts
225 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
228 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
229 extendCCans = snocBag
231 andCCans :: [CanonicalCts] -> CanonicalCts
232 andCCans = unionManyBags
234 emptyCCan :: CanonicalCts
237 isEmptyCCan :: CanonicalCts -> Bool
238 isEmptyCCan = isEmptyBag
240 isCTyEqCan :: CanonicalCt -> Bool
241 isCTyEqCan (CTyEqCan {}) = True
242 isCTyEqCan (CFunEqCan {}) = False
245 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
246 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
247 isCDictCan_Maybe _ = Nothing
249 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
250 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
251 isCIPCan_Maybe _ = Nothing
253 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
254 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
255 isCFunEqCan_Maybe _ = Nothing
257 isCFrozenErr :: CanonicalCt -> Bool
258 isCFrozenErr (CFrozenErr {}) = True
259 isCFrozenErr _ = False
262 %************************************************************************
265 The "flavor" of a canonical constraint
267 %************************************************************************
270 getWantedLoc :: CanonicalCt -> WantedLoc
272 = ASSERT (isWanted (cc_flavor ct))
275 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
277 isWantedCt :: CanonicalCt -> Bool
278 isWantedCt ct = isWanted (cc_flavor ct)
279 isGivenCt :: CanonicalCt -> Bool
280 isGivenCt ct = isGiven (cc_flavor ct)
281 isDerivedCt :: CanonicalCt -> Bool
282 isDerivedCt ct = isDerived (cc_flavor ct)
284 canSolve :: CtFlavor -> CtFlavor -> Bool
285 -- canSolve ctid1 ctid2
286 -- The constraint ctid1 can be used to solve ctid2
287 -- "to solve" means a reaction where the active parts of the two constraints match.
288 -- active(F xis ~ xi) = F xis
289 -- active(tv ~ xi) = tv
290 -- active(D xis) = D xis
291 -- active(IP nm ty) = nm
293 -- NB: either (a `canSolve` b) or (b `canSolve` a) must hold
294 -----------------------------------------
295 canSolve (Given {}) _ = True
296 canSolve (Wanted {}) (Derived {}) = True
297 canSolve (Wanted {}) (Wanted {}) = True
298 canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given
299 canSolve _ _ = False -- (There is no *evidence* for a derived.)
301 canRewrite :: CtFlavor -> CtFlavor -> Bool
302 -- canRewrite ctid1 ctid2
303 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
304 canRewrite = canSolve
306 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
307 -- Precondition: At least one of them should be wanted
308 combineCtLoc (Wanted loc) _ = loc
309 combineCtLoc _ (Wanted loc) = loc
310 combineCtLoc (Derived loc ) _ = loc
311 combineCtLoc _ (Derived loc ) = loc
312 combineCtLoc _ _ = panic "combineCtLoc: both given"
314 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
315 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
316 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
317 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
320 mkWantedFlavor :: CtFlavor -> CtFlavor
321 mkWantedFlavor (Wanted loc) = Wanted loc
322 mkWantedFlavor (Derived loc) = Wanted loc
323 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
326 %************************************************************************
328 %* The TcS solver monad *
330 %************************************************************************
334 The TcS monad is a weak form of the main Tc monad
338 * allocate new variables
339 * fill in evidence variables
341 Filling in a dictionary evidence variable means to create a binding
342 for it, so TcS carries a mutable location where the binding can be
343 added. This is initialised from the innermost implication constraint.
348 tcs_ev_binds :: EvBindsVar,
351 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
352 -- Global type bindings
354 tcs_context :: SimplContext,
356 tcs_untch :: TcsUntouchables,
358 tcs_ic_depth :: Int, -- Implication nesting depth
359 tcs_count :: IORef Int -- Global step count
362 type TcsUntouchables = (Untouchables,TcTyVarSet)
363 -- Like the TcM Untouchables,
364 -- but records extra TcsTv variables generated during simplification
365 -- See Note [Extra TcsTv untouchables] in TcSimplify
370 = SimplInfer -- Inferring type of a let-bound thing
371 | SimplRuleLhs -- Inferring type of a RULE lhs
372 | SimplInteractive -- Inferring type at GHCi prompt
373 | SimplCheck -- Checking a type signature or RULE rhs
376 instance Outputable SimplContext where
377 ppr SimplInfer = ptext (sLit "SimplInfer")
378 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
379 ppr SimplInteractive = ptext (sLit "SimplInteractive")
380 ppr SimplCheck = ptext (sLit "SimplCheck")
382 isInteractive :: SimplContext -> Bool
383 isInteractive SimplInteractive = True
384 isInteractive _ = False
386 simplEqsOnly :: SimplContext -> Bool
387 -- Simplify equalities only, not dictionaries
388 -- This is used for the LHS of rules; ee
389 -- Note [Simplifying RULE lhs constraints] in TcSimplify
390 simplEqsOnly SimplRuleLhs = True
391 simplEqsOnly _ = False
393 performDefaulting :: SimplContext -> Bool
394 performDefaulting SimplInfer = False
395 performDefaulting SimplRuleLhs = False
396 performDefaulting SimplInteractive = True
397 performDefaulting SimplCheck = True
400 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
402 instance Functor TcS where
403 fmap f m = TcS $ fmap f . unTcS m
405 instance Monad TcS where
406 return x = TcS (\_ -> return x)
407 fail err = TcS (\_ -> fail err)
408 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
410 -- Basic functionality
411 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
412 wrapTcS :: TcM a -> TcS a
413 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
414 -- and TcS is supposed to have limited functionality
415 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
417 wrapErrTcS :: TcM a -> TcS a
418 -- The thing wrapped should just fail
419 -- There's no static check; it's up to the user
420 -- Having a variant for each error message is too painful
423 wrapWarnTcS :: TcM a -> TcS a
424 -- The thing wrapped should just add a warning, or no-op
425 -- There's no static check; it's up to the user
426 wrapWarnTcS = wrapTcS
428 failTcS, panicTcS :: SDoc -> TcS a
429 failTcS = wrapTcS . TcM.failWith
430 panicTcS doc = pprPanic "TcCanonical" doc
432 traceTcS :: String -> SDoc -> TcS ()
433 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
435 bumpStepCountTcS :: TcS ()
436 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
437 ; n <- TcM.readTcRef ref
438 ; TcM.writeTcRef ref (n+1) }
440 traceFireTcS :: Int -> SDoc -> TcS ()
441 -- Dump a rule-firing trace
442 traceFireTcS depth doc
444 TcM.ifDOptM Opt_D_dump_cs_trace $
445 do { n <- TcM.readTcRef (tcs_count env)
447 <> text (replicate (tcs_ic_depth env) '>')
448 <> brackets (int depth) <+> doc
451 runTcS :: SimplContext
452 -> Untouchables -- Untouchables
453 -> TcS a -- What to run
454 -> TcM (a, Bag EvBind)
455 runTcS context untouch tcs
456 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
457 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
458 ; step_count <- TcM.newTcRef 0
459 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
460 , tcs_ty_binds = ty_binds_var
461 , tcs_context = context
462 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
463 , tcs_count = step_count
467 -- Run the computation
468 ; res <- unTcS tcs env
469 -- Perform the type unifications required
470 ; ty_binds <- TcM.readTcRef ty_binds_var
471 ; mapM_ do_unification (varEnvElts ty_binds)
474 ; count <- TcM.readTcRef step_count
475 ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
478 ; ev_binds <- TcM.readTcRef evb_ref
479 ; return (res, evBindMapBinds ev_binds) }
481 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
483 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
484 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
485 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
486 , tcs_untch = (_outer_range, outer_tcs)
488 , tcs_ic_depth = idepth
489 , tcs_context = ctxt } ->
491 inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
492 -- The inner_range should be narrower than the outer one
493 -- (thus increasing the set of untouchables) but
494 -- the inner Tcs-untouchables must be unioned with the
496 nest_env = TcSEnv { tcs_ev_binds = ref
497 , tcs_ty_binds = ty_binds
498 , tcs_untch = inner_untch
500 , tcs_ic_depth = idepth+1
501 , tcs_context = ctxtUnderImplic ctxt }
503 thing_inside nest_env
505 recoverTcS :: TcS a -> TcS a -> TcS a
506 recoverTcS (TcS recovery_code) (TcS thing_inside)
508 TcM.recoverM (recovery_code env) (thing_inside env)
510 ctxtUnderImplic :: SimplContext -> SimplContext
511 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
512 ctxtUnderImplic SimplRuleLhs = SimplCheck
513 ctxtUnderImplic ctxt = ctxt
515 tryTcS :: TcS a -> TcS a
516 -- Like runTcS, but from within the TcS monad
517 -- Ignore all the evidence generated, and do not affect caller's evidence!
519 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
520 ; ev_binds_var <- TcM.newTcEvBinds
521 ; let env1 = env { tcs_ev_binds = ev_binds_var
522 , tcs_ty_binds = ty_binds_var }
526 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
528 getDynFlags :: TcS DynFlags
529 getDynFlags = wrapTcS TcM.getDOpts
531 getTcSContext :: TcS SimplContext
532 getTcSContext = TcS (return . tcs_context)
534 getTcEvBinds :: TcS EvBindsVar
535 getTcEvBinds = TcS (return . tcs_ev_binds)
537 getUntouchables :: TcS TcsUntouchables
538 getUntouchables = TcS (return . tcs_untch)
540 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
541 getTcSTyBinds = TcS (return . tcs_ty_binds)
543 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
544 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
547 getTcEvBindsBag :: TcS EvBindMap
549 = do { EvBindsVar ev_ref _ <- getTcEvBinds
550 ; wrapTcS $ TcM.readTcRef ev_ref }
552 setCoBind :: CoVar -> Coercion -> TcS ()
553 setCoBind cv co = setEvBind cv (EvCoercion co)
555 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
556 -- Add a type binding
557 -- We never do this twice!
558 setWantedTyBind tv ty
559 = do { ref <- getTcSTyBinds
561 do { ty_binds <- TcM.readTcRef ref
563 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
564 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
565 , ppr tv <+> text ":=" <+> ppr ty
566 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
568 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
570 setIPBind :: EvVar -> EvTerm -> TcS ()
571 setIPBind = setEvBind
573 setDictBind :: EvVar -> EvTerm -> TcS ()
574 setDictBind = setEvBind
576 setEvBind :: EvVar -> EvTerm -> TcS ()
579 = do { tc_evbinds <- getTcEvBinds
580 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
582 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
583 warnTcS loc warn_if doc
584 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
585 | otherwise = return ()
587 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
589 = do { ctxt <- getTcSContext
590 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
591 ; return (ctxt, tys, flags) }
593 -- Just get some environments needed for instance looking up and matching
594 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
596 getInstEnvs :: TcS (InstEnv, InstEnv)
597 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
599 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
600 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
602 getTopEnv :: TcS HscEnv
603 getTopEnv = wrapTcS $ TcM.getTopEnv
605 getGblEnv :: TcS TcGblEnv
606 getGblEnv = wrapTcS $ TcM.getGblEnv
608 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
609 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
611 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
612 checkWellStagedDFun pred dfun_id loc
613 = wrapTcS $ TcM.setCtLoc loc $
614 do { use_stage <- TcM.getStage
615 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
617 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
618 bind_lvl = TcM.topIdLvl dfun_id
620 pprEq :: TcType -> TcType -> SDoc
621 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
623 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
624 isTouchableMetaTyVar tv
625 = do { untch <- getUntouchables
626 ; return $ isTouchableMetaTyVar_InRange untch tv }
628 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
629 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
630 = case tcTyVarDetails tv of
631 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
632 -- See Note [Touchable meta type variables]
633 MetaTv {} -> inTouchableRange untch tv
640 Note [Touchable meta type variables]
641 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
642 Meta type variables allocated *by the constraint solver itself* are always
644 instance C a b => D [a] where...
645 if we use this instance declaration we "make up" a fresh meta type
646 variable for 'b', which we must later guess. (Perhaps C has a
647 functional dependency.) But since we aren't in the constraint *generator*
648 we can't allocate a Unique in the touchable range for this implication
649 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
654 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
656 newFlattenSkolemTy :: TcType -> TcS TcType
657 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
659 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
660 newFlattenSkolemTyVar ty
661 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
662 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
663 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
664 ; traceTcS "New Flatten Skolem Born" $
665 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
669 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
671 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
672 instDFunTypes mb_inst_tys
673 = mapM inst_tv mb_inst_tys
675 inst_tv :: Either TyVar TcType -> TcS Type
676 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
677 inst_tv (Right ty) = return ty
679 instDFunConstraints :: TcThetaType -> TcS [EvVar]
680 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
683 instFlexiTcS :: TyVar -> TcS TcTyVar
684 -- Like TcM.instMetaTyVar but the variable that is created is always
685 -- touchable; we are supposed to guess its instantiation.
686 -- See Note [Touchable meta type variables]
687 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
689 newFlexiTcSTy :: Kind -> TcS TcType
692 do { uniq <- TcM.newUnique
693 ; ref <- TcM.newMutVar Flexi
694 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
695 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
697 isFlexiTcsTv :: TyVar -> Bool
699 | not (isTcTyVar tv) = False
700 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
703 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
704 -- Create new wanted CoVar that constrains the type to have the specified kind.
705 newKindConstraint tv knd
706 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
707 ; let ty_k = mkTyVarTy tv_k
708 ; co_var <- newCoVar (mkTyVarTy tv) ty_k
711 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
712 instFlexiTcSHelper tvname tvkind
714 do { uniq <- TcM.newUnique
715 ; ref <- TcM.newMutVar Flexi
716 ; let name = setNameUnique tvname uniq
718 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
720 -- Superclasses and recursive dictionaries
721 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
723 newEvVar :: TcPredType -> TcS EvVar
724 newEvVar pty = wrapTcS $ TcM.newEvVar pty
726 newDerivedId :: TcPredType -> TcS EvVar
727 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
729 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
730 -- Note we create immutable variables for given or derived, since we
731 -- must bind them to TcEvBinds (because their evidence may involve
732 -- superclasses). However we should be able to override existing
733 -- 'derived' evidence, even in TcEvBinds
734 newGivenCoVar ty1 ty2 co
735 = do { cv <- newCoVar ty1 ty2
736 ; setEvBind cv (EvCoercion co)
739 newCoVar :: TcType -> TcType -> TcS EvVar
740 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
742 newIPVar :: IPName Name -> TcType -> TcS EvVar
743 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
745 newDictVar :: Class -> [TcType] -> TcS EvVar
746 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
751 -- Matching and looking up classes and family instances
752 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
754 data MatchInstResult mi
755 = MatchInstNo -- No matching instance
756 | MatchInstSingle mi -- Single matching instance
757 | MatchInstMany -- Multiple matching instances
760 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
761 -- Look up a class constraint in the instance environment
763 = do { let pred = mkClassPred clas tys
764 ; instEnvs <- getInstEnvs
765 ; case lookupInstEnv instEnvs clas tys of {
766 ([], unifs) -- Nothing matches
767 -> do { traceTcS "matchClass not matching"
768 (vcat [ text "dict" <+> ppr pred,
769 text "unifs" <+> ppr unifs ])
772 ([(ispec, inst_tys)], []) -- A single match
773 -> do { let dfun_id = is_dfun ispec
774 ; traceTcS "matchClass success"
775 (vcat [text "dict" <+> ppr pred,
776 text "witness" <+> ppr dfun_id
777 <+> ppr (idType dfun_id) ])
778 -- Record that this dfun is needed
779 ; return $ MatchInstSingle (dfun_id, inst_tys)
781 (matches, unifs) -- More than one matches
782 -> do { traceTcS "matchClass multiple matches, deferring choice"
783 (vcat [text "dict" <+> ppr pred,
784 text "matches" <+> ppr matches,
785 text "unifs" <+> ppr unifs])
786 ; return MatchInstMany
793 -> TcS (MatchInstResult (TyCon, [Type]))
795 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
797 Nothing -> return MatchInstNo
798 Just res -> return $ MatchInstSingle res
799 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
800 -- multiple matches. Check.