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,
15 isWanted, isGiven, isDerived,
16 isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
21 combineCtLoc, mkGivenFlavor, mkWantedFlavor,
24 TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
25 tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
26 SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
28 -- Creation of evidence variables
29 newEvVar, newCoVar, newWantedCoVar, newGivenCoVar,
31 newIPVar, newDictVar, newKindConstraint,
33 -- Setting evidence variables
35 setIPBind, setDictBind, setEvBind,
39 getInstEnvs, getFamInstEnvs, -- Getting the environments
40 getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
41 getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
43 newFlattenSkolemTy, -- Flatten skolems
46 instDFunTypes, -- Instantiation
54 isTouchableMetaTyVar_InRange,
56 getDefaultInfo, getDynFlags,
58 matchClass, matchFam, MatchInstResult (..),
61 pprEq, -- Smaller utils, re-exported from TcM
62 -- TODO (DV): these are only really used in the
63 -- instance matcher in TcSimplify. I am wondering
64 -- if the whole instance matcher simply belongs
68 mkDerivedFunDepEqns -- Instantiation of 'Equations' from FunDeps
72 #include "HsVersions.h"
82 import qualified TcRnMonad as TcM
83 import qualified TcMType as TcM
84 import qualified TcEnv as TcM
85 ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
103 import HsBinds -- for TcEvBinds stuff
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 makeSolvedByInst :: CanonicalCt -> CanonicalCt
185 -- Record that a constraint is now solved
187 -- Given, Derived -> no-op
189 | Wanted loc <- cc_flavor ct = ct { cc_flavor = mkGivenFlavor (Wanted loc) UnkSkol }
192 deCanonicalise :: CanonicalCt -> FlavoredEvVar
193 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
195 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
196 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
197 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
198 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
199 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
200 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
202 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
203 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
204 tyVarsOfCDict _ct = emptyVarSet
206 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
207 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
209 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
210 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
212 instance Outputable CanonicalCt where
213 ppr (CDictCan d fl cls tys)
214 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
215 ppr (CIPCan ip fl ip_nm ty)
216 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
217 ppr (CTyEqCan co fl tv ty)
218 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
219 ppr (CFunEqCan co fl tc tys ty)
220 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
221 ppr (CFrozenErr co fl)
222 = ppr fl <+> pprEvVarWithType co
225 Note [Canonical implicit parameter constraints]
226 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
227 The type in a canonical implicit parameter constraint doesn't need to
228 be a xi (type-function-free type) since we can defer the flattening
229 until checking this type for equality with another type. If we
230 encounter two IP constraints with the same name, they MUST have the
231 same type, and at that point we can generate a flattened equality
232 constraint between the types. (On the other hand, the types in two
233 class constraints for the same class MAY be equal, so they need to be
234 flattened in the first place to facilitate comparing them.)
237 singleCCan :: CanonicalCt -> CanonicalCts
240 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
243 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
244 extendCCans = snocBag
246 andCCans :: [CanonicalCts] -> CanonicalCts
247 andCCans = unionManyBags
249 emptyCCan :: CanonicalCts
252 isEmptyCCan :: CanonicalCts -> Bool
253 isEmptyCCan = isEmptyBag
255 isCTyEqCan :: CanonicalCt -> Bool
256 isCTyEqCan (CTyEqCan {}) = True
257 isCTyEqCan (CFunEqCan {}) = False
260 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
261 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
262 isCDictCan_Maybe _ = Nothing
264 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
265 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
266 isCIPCan_Maybe _ = Nothing
268 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
269 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
270 isCFunEqCan_Maybe _ = Nothing
272 isCFrozenErr :: CanonicalCt -> Bool
273 isCFrozenErr (CFrozenErr {}) = True
274 isCFrozenErr _ = False
277 %************************************************************************
280 The "flavor" of a canonical constraint
282 %************************************************************************
285 getWantedLoc :: CanonicalCt -> WantedLoc
287 = ASSERT (isWanted (cc_flavor ct))
290 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
292 isWantedCt :: CanonicalCt -> Bool
293 isWantedCt ct = isWanted (cc_flavor ct)
294 isGivenCt :: CanonicalCt -> Bool
295 isGivenCt ct = isGiven (cc_flavor ct)
296 isDerivedCt :: CanonicalCt -> Bool
297 isDerivedCt ct = isDerived (cc_flavor ct)
299 canSolve :: CtFlavor -> CtFlavor -> Bool
300 -- canSolve ctid1 ctid2
301 -- The constraint ctid1 can be used to solve ctid2
302 -- "to solve" means a reaction where the active parts of the two constraints match.
303 -- active(F xis ~ xi) = F xis
304 -- active(tv ~ xi) = tv
305 -- active(D xis) = D xis
306 -- active(IP nm ty) = nm
307 -----------------------------------------
308 canSolve (Given {}) _ = True
309 canSolve (Derived {}) (Wanted {}) = False -- DV: changing the semantics
310 canSolve (Derived {}) (Derived {}) = True -- DV: changing the semantics of derived
311 canSolve (Wanted {}) (Wanted {}) = True
314 canRewrite :: CtFlavor -> CtFlavor -> Bool
315 -- canRewrite ctid1 ctid2
316 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
317 canRewrite = canSolve
319 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
320 -- Precondition: At least one of them should be wanted
321 combineCtLoc (Wanted loc) _ = loc
322 combineCtLoc _ (Wanted loc) = loc
323 combineCtLoc (Derived loc ) _ = loc
324 combineCtLoc _ (Derived loc ) = loc
325 combineCtLoc _ _ = panic "combineCtLoc: both given"
327 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
328 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
329 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
330 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
332 mkWantedFlavor :: CtFlavor -> CtFlavor
333 mkWantedFlavor (Wanted loc) = Wanted loc
334 mkWantedFlavor (Derived loc) = Wanted loc
335 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
338 %************************************************************************
340 %* The TcS solver monad *
342 %************************************************************************
346 The TcS monad is a weak form of the main Tc monad
350 * allocate new variables
351 * fill in evidence variables
353 Filling in a dictionary evidence variable means to create a binding
354 for it, so TcS carries a mutable location where the binding can be
355 added. This is initialised from the innermost implication constraint.
360 tcs_ev_binds :: EvBindsVar,
363 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
364 -- Global type bindings
366 tcs_context :: SimplContext,
368 tcs_untch :: TcsUntouchables
371 type TcsUntouchables = (Untouchables,TcTyVarSet)
372 -- Like the TcM Untouchables,
373 -- but records extra TcsTv variables generated during simplification
374 -- See Note [Extra TcsTv untouchables] in TcSimplify
379 = SimplInfer -- Inferring type of a let-bound thing
380 | SimplRuleLhs -- Inferring type of a RULE lhs
381 | SimplInteractive -- Inferring type at GHCi prompt
382 | SimplCheck -- Checking a type signature or RULE rhs
385 instance Outputable SimplContext where
386 ppr SimplInfer = ptext (sLit "SimplInfer")
387 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
388 ppr SimplInteractive = ptext (sLit "SimplInteractive")
389 ppr SimplCheck = ptext (sLit "SimplCheck")
391 isInteractive :: SimplContext -> Bool
392 isInteractive SimplInteractive = True
393 isInteractive _ = False
395 simplEqsOnly :: SimplContext -> Bool
396 -- Simplify equalities only, not dictionaries
397 -- This is used for the LHS of rules; ee
398 -- Note [Simplifying RULE lhs constraints] in TcSimplify
399 simplEqsOnly SimplRuleLhs = True
400 simplEqsOnly _ = False
402 performDefaulting :: SimplContext -> Bool
403 performDefaulting SimplInfer = False
404 performDefaulting SimplRuleLhs = False
405 performDefaulting SimplInteractive = True
406 performDefaulting SimplCheck = True
409 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
411 instance Functor TcS where
412 fmap f m = TcS $ fmap f . unTcS m
414 instance Monad TcS where
415 return x = TcS (\_ -> return x)
416 fail err = TcS (\_ -> fail err)
417 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
419 -- Basic functionality
420 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
421 wrapTcS :: TcM a -> TcS a
422 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
423 -- and TcS is supposed to have limited functionality
424 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
426 wrapErrTcS :: TcM a -> TcS a
427 -- The thing wrapped should just fail
428 -- There's no static check; it's up to the user
429 -- Having a variant for each error message is too painful
432 wrapWarnTcS :: TcM a -> TcS a
433 -- The thing wrapped should just add a warning, or no-op
434 -- There's no static check; it's up to the user
435 wrapWarnTcS = wrapTcS
437 failTcS, panicTcS :: SDoc -> TcS a
438 failTcS = wrapTcS . TcM.failWith
439 panicTcS doc = pprPanic "TcCanonical" doc
441 traceTcS :: String -> SDoc -> TcS ()
442 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
444 traceTcS0 :: String -> SDoc -> TcS ()
445 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
447 runTcS :: SimplContext
448 -> Untouchables -- Untouchables
449 -> TcS a -- What to run
450 -> TcM (a, Bag EvBind)
451 runTcS context untouch tcs
452 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
453 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
454 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
455 , tcs_ty_binds = ty_binds_var
456 , tcs_context = context
457 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
460 -- Run the computation
461 ; res <- unTcS tcs env
462 -- Perform the type unifications required
463 ; ty_binds <- TcM.readTcRef ty_binds_var
464 ; mapM_ do_unification (varEnvElts ty_binds)
467 ; ev_binds <- TcM.readTcRef evb_ref
468 ; return (res, evBindMapBinds ev_binds) }
470 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
472 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
473 nestImplicTcS ref untch (TcS thing_inside)
474 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
475 tcs_context = ctxt } ->
477 nest_env = TcSEnv { tcs_ev_binds = ref
478 , tcs_ty_binds = ty_binds
480 , tcs_context = ctxtUnderImplic ctxt }
482 thing_inside nest_env
484 recoverTcS :: TcS a -> TcS a -> TcS a
485 recoverTcS (TcS recovery_code) (TcS thing_inside)
487 TcM.recoverM (recovery_code env) (thing_inside env)
489 ctxtUnderImplic :: SimplContext -> SimplContext
490 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
491 ctxtUnderImplic SimplRuleLhs = SimplCheck
492 ctxtUnderImplic ctxt = ctxt
494 tryTcS :: TcS a -> TcS a
495 -- Like runTcS, but from within the TcS monad
496 -- Ignore all the evidence generated, and do not affect caller's evidence!
498 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
499 ; ev_binds_var <- TcM.newTcEvBinds
500 ; let env1 = env { tcs_ev_binds = ev_binds_var
501 , tcs_ty_binds = ty_binds_var }
505 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
507 getDynFlags :: TcS DynFlags
508 getDynFlags = wrapTcS TcM.getDOpts
510 getTcSContext :: TcS SimplContext
511 getTcSContext = TcS (return . tcs_context)
513 getTcEvBinds :: TcS EvBindsVar
514 getTcEvBinds = TcS (return . tcs_ev_binds)
516 getUntouchables :: TcS TcsUntouchables
517 getUntouchables = TcS (return . tcs_untch)
519 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
520 getTcSTyBinds = TcS (return . tcs_ty_binds)
522 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
523 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
526 getTcEvBindsBag :: TcS EvBindMap
528 = do { EvBindsVar ev_ref _ <- getTcEvBinds
529 ; wrapTcS $ TcM.readTcRef ev_ref }
531 setWantedCoBind :: CoVar -> Coercion -> TcS ()
532 setWantedCoBind cv co
533 = setEvBind cv (EvCoercion co)
534 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
536 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
537 -- Add a type binding
538 -- We never do this twice!
539 setWantedTyBind tv ty
540 = do { ref <- getTcSTyBinds
542 do { ty_binds <- TcM.readTcRef ref
544 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
545 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
546 , ppr tv <+> text ":=" <+> ppr ty
547 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
549 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
551 setIPBind :: EvVar -> EvTerm -> TcS ()
552 setIPBind = setEvBind
554 setDictBind :: EvVar -> EvTerm -> TcS ()
555 setDictBind = setEvBind
557 setEvBind :: EvVar -> EvTerm -> TcS ()
560 = do { tc_evbinds <- getTcEvBinds
561 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
563 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
564 warnTcS loc warn_if doc
565 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
566 | otherwise = return ()
568 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
570 = do { ctxt <- getTcSContext
571 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
572 ; return (ctxt, tys, flags) }
574 -- Just get some environments needed for instance looking up and matching
575 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
577 getInstEnvs :: TcS (InstEnv, InstEnv)
578 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
580 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
581 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
583 getTopEnv :: TcS HscEnv
584 getTopEnv = wrapTcS $ TcM.getTopEnv
586 getGblEnv :: TcS TcGblEnv
587 getGblEnv = wrapTcS $ TcM.getGblEnv
589 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
590 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
592 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
593 checkWellStagedDFun pred dfun_id loc
594 = wrapTcS $ TcM.setCtLoc loc $
595 do { use_stage <- TcM.getStage
596 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
598 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
599 bind_lvl = TcM.topIdLvl dfun_id
601 pprEq :: TcType -> TcType -> SDoc
602 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
604 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
605 isTouchableMetaTyVar tv
606 = do { untch <- getUntouchables
607 ; return $ isTouchableMetaTyVar_InRange untch tv }
609 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
610 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
611 = case tcTyVarDetails tv of
612 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
613 -- See Note [Touchable meta type variables]
614 MetaTv {} -> inTouchableRange untch tv
621 Note [Touchable meta type variables]
622 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
623 Meta type variables allocated *by the constraint solver itself* are always
625 instance C a b => D [a] where...
626 if we use this instance declaration we "make up" a fresh meta type
627 variable for 'b', which we must later guess. (Perhaps C has a
628 functional dependency.) But since we aren't in the constraint *generator*
629 we can't allocate a Unique in the touchable range for this implication
630 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
635 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
637 newFlattenSkolemTy :: TcType -> TcS TcType
638 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
640 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
641 newFlattenSkolemTyVar ty
642 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
643 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
644 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
645 ; traceTcS "New Flatten Skolem Born" $
646 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
650 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
652 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
653 instDFunTypes mb_inst_tys
654 = mapM inst_tv mb_inst_tys
656 inst_tv :: Either TyVar TcType -> TcS Type
657 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
658 inst_tv (Right ty) = return ty
660 instDFunConstraints :: TcThetaType -> TcS [EvVar]
661 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
664 instFlexiTcS :: TyVar -> TcS TcTyVar
665 -- Like TcM.instMetaTyVar but the variable that is created is always
666 -- touchable; we are supposed to guess its instantiation.
667 -- See Note [Touchable meta type variables]
668 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
670 newFlexiTcSTy :: Kind -> TcS TcType
673 do { uniq <- TcM.newUnique
674 ; ref <- TcM.newMutVar Flexi
675 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
676 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
678 isFlexiTcsTv :: TyVar -> Bool
680 | not (isTcTyVar tv) = False
681 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
684 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
685 -- Create new wanted CoVar that constrains the type to have the specified kind.
686 newKindConstraint tv knd
687 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
688 ; let ty_k = mkTyVarTy tv_k
689 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
692 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
693 instFlexiTcSHelper tvname tvkind
695 do { uniq <- TcM.newUnique
696 ; ref <- TcM.newMutVar Flexi
697 ; let name = setNameUnique tvname uniq
699 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
701 -- Superclasses and recursive dictionaries
702 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
704 newEvVar :: TcPredType -> TcS EvVar
705 newEvVar pty = wrapTcS $ TcM.newEvVar pty
707 newDerivedId :: TcPredType -> TcS EvVar
708 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
710 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
711 -- Note we create immutable variables for given or derived, since we
712 -- must bind them to TcEvBinds (because their evidence may involve
713 -- superclasses). However we should be able to override existing
714 -- 'derived' evidence, even in TcEvBinds
715 newGivenCoVar ty1 ty2 co
716 = do { cv <- newCoVar ty1 ty2
717 ; setEvBind cv (EvCoercion co)
720 newWantedCoVar :: TcType -> TcType -> TcS EvVar
721 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
723 newCoVar :: TcType -> TcType -> TcS EvVar
724 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
726 newIPVar :: IPName Name -> TcType -> TcS EvVar
727 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
729 newDictVar :: Class -> [TcType] -> TcS EvVar
730 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
735 -- Matching and looking up classes and family instances
736 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
738 data MatchInstResult mi
739 = MatchInstNo -- No matching instance
740 | MatchInstSingle mi -- Single matching instance
741 | MatchInstMany -- Multiple matching instances
744 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
745 -- Look up a class constraint in the instance environment
747 = do { let pred = mkClassPred clas tys
748 ; instEnvs <- getInstEnvs
749 ; case lookupInstEnv instEnvs clas tys of {
750 ([], unifs) -- Nothing matches
751 -> do { traceTcS "matchClass not matching"
752 (vcat [ text "dict" <+> ppr pred,
753 text "unifs" <+> ppr unifs ])
756 ([(ispec, inst_tys)], []) -- A single match
757 -> do { let dfun_id = is_dfun ispec
758 ; traceTcS "matchClass success"
759 (vcat [text "dict" <+> ppr pred,
760 text "witness" <+> ppr dfun_id
761 <+> ppr (idType dfun_id) ])
762 -- Record that this dfun is needed
763 ; return $ MatchInstSingle (dfun_id, inst_tys)
765 (matches, unifs) -- More than one matches
766 -> do { traceTcS "matchClass multiple matches, deferring choice"
767 (vcat [text "dict" <+> ppr pred,
768 text "matches" <+> ppr matches,
769 text "unifs" <+> ppr unifs])
770 ; return MatchInstMany
777 -> TcS (MatchInstResult (TyCon, [Type]))
779 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
781 Nothing -> return MatchInstNo
782 Just res -> return $ MatchInstSingle res
783 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
784 -- multiple matches. Check.
788 -- Functional dependencies, instantiation of equations
789 -------------------------------------------------------
791 mkDerivedFunDepEqns :: WantedLoc
792 -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
793 -> TcS [FlavoredEvVar] -- All Derived
794 mkDerivedFunDepEqns _ [] = return []
795 mkDerivedFunDepEqns loc eqns
796 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
797 ; evvars <- mapM to_work_item eqns
798 ; return $ concat evvars }
800 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
801 to_work_item ((qtvs, pairs), d1, d2)
802 = do { let tvs = varSetElems qtvs
803 ; tvs' <- mapM instFlexiTcS tvs
804 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
805 loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
807 ; mapM (do_one subst flav) pairs }
809 do_one subst flav (ty1, ty2)
810 = do { let sty1 = substTy subst ty1
811 sty2 = substTy subst ty2
812 ; ev <- newCoVar sty1 sty2
813 ; return (mkEvVarX ev flav) }
815 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
816 pprEquationDoc (eqn, (p1, _), (p2, _))
817 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
819 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
820 -> TcM (TidyEnv, SDoc)
821 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
822 = do { pred1' <- TcM.zonkTcPredType pred1
823 ; pred2' <- TcM.zonkTcPredType pred2
824 ; let { pred1'' = tidyPred tidy_env pred1'
825 ; pred2'' = tidyPred tidy_env pred2' }
826 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
827 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
828 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
829 ; return (tidy_env, msg) }