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
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 makeSolvedByInst :: CanonicalCt -> CanonicalCt
184 -- Record that a constraint is now solved
186 -- Given, Derived -> no-op
188 | Wanted loc <- cc_flavor ct
189 = ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) }
190 | otherwise -- Only called on wanteds
191 = pprPanic "makeSolvedByInst" (ppr ct)
193 deCanonicalise :: CanonicalCt -> FlavoredEvVar
194 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
196 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
197 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
198 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
199 tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
200 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
201 tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev
203 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
204 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
205 tyVarsOfCDict _ct = emptyVarSet
207 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
208 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
210 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
211 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
213 instance Outputable CanonicalCt where
214 ppr (CDictCan d fl cls tys)
215 = ppr fl <+> ppr d <+> dcolon <+> pprClassPred cls tys
216 ppr (CIPCan ip fl ip_nm ty)
217 = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
218 ppr (CTyEqCan co fl tv ty)
219 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
220 ppr (CFunEqCan co fl tc tys ty)
221 = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
222 ppr (CFrozenErr co fl)
223 = ppr fl <+> pprEvVarWithType co
226 Note [Canonical implicit parameter constraints]
227 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
228 The type in a canonical implicit parameter constraint doesn't need to
229 be a xi (type-function-free type) since we can defer the flattening
230 until checking this type for equality with another type. If we
231 encounter two IP constraints with the same name, they MUST have the
232 same type, and at that point we can generate a flattened equality
233 constraint between the types. (On the other hand, the types in two
234 class constraints for the same class MAY be equal, so they need to be
235 flattened in the first place to facilitate comparing them.)
238 singleCCan :: CanonicalCt -> CanonicalCts
241 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
244 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
245 extendCCans = snocBag
247 andCCans :: [CanonicalCts] -> CanonicalCts
248 andCCans = unionManyBags
250 emptyCCan :: CanonicalCts
253 isEmptyCCan :: CanonicalCts -> Bool
254 isEmptyCCan = isEmptyBag
256 isCTyEqCan :: CanonicalCt -> Bool
257 isCTyEqCan (CTyEqCan {}) = True
258 isCTyEqCan (CFunEqCan {}) = False
261 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
262 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
263 isCDictCan_Maybe _ = Nothing
265 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
266 isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
267 isCIPCan_Maybe _ = Nothing
269 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
270 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
271 isCFunEqCan_Maybe _ = Nothing
273 isCFrozenErr :: CanonicalCt -> Bool
274 isCFrozenErr (CFrozenErr {}) = True
275 isCFrozenErr _ = False
278 %************************************************************************
281 The "flavor" of a canonical constraint
283 %************************************************************************
286 getWantedLoc :: CanonicalCt -> WantedLoc
288 = ASSERT (isWanted (cc_flavor ct))
291 _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
293 isWantedCt :: CanonicalCt -> Bool
294 isWantedCt ct = isWanted (cc_flavor ct)
295 isGivenCt :: CanonicalCt -> Bool
296 isGivenCt ct = isGiven (cc_flavor ct)
297 isDerivedCt :: CanonicalCt -> Bool
298 isDerivedCt ct = isDerived (cc_flavor ct)
300 canSolve :: CtFlavor -> CtFlavor -> Bool
301 -- canSolve ctid1 ctid2
302 -- The constraint ctid1 can be used to solve ctid2
303 -- "to solve" means a reaction where the active parts of the two constraints match.
304 -- active(F xis ~ xi) = F xis
305 -- active(tv ~ xi) = tv
306 -- active(D xis) = D xis
307 -- active(IP nm ty) = nm
308 -----------------------------------------
309 canSolve (Given {}) _ = True
310 canSolve (Derived {}) (Wanted {}) = False -- DV: changing the semantics
311 canSolve (Derived {}) (Derived {}) = True -- DV: changing the semantics of derived
312 canSolve (Wanted {}) (Wanted {}) = True
315 canRewrite :: CtFlavor -> CtFlavor -> Bool
316 -- canRewrite ctid1 ctid2
317 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
318 canRewrite = canSolve
320 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
321 -- Precondition: At least one of them should be wanted
322 combineCtLoc (Wanted loc) _ = loc
323 combineCtLoc _ (Wanted loc) = loc
324 combineCtLoc (Derived loc ) _ = loc
325 combineCtLoc _ (Derived loc ) = loc
326 combineCtLoc _ _ = panic "combineCtLoc: both given"
328 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
329 mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
330 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
331 mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
334 mkWantedFlavor :: CtFlavor -> CtFlavor
335 mkWantedFlavor (Wanted loc) = Wanted loc
336 mkWantedFlavor (Derived loc) = Wanted loc
337 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
340 %************************************************************************
342 %* The TcS solver monad *
344 %************************************************************************
348 The TcS monad is a weak form of the main Tc monad
352 * allocate new variables
353 * fill in evidence variables
355 Filling in a dictionary evidence variable means to create a binding
356 for it, so TcS carries a mutable location where the binding can be
357 added. This is initialised from the innermost implication constraint.
362 tcs_ev_binds :: EvBindsVar,
365 tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
366 -- Global type bindings
368 tcs_context :: SimplContext,
370 tcs_untch :: TcsUntouchables
373 type TcsUntouchables = (Untouchables,TcTyVarSet)
374 -- Like the TcM Untouchables,
375 -- but records extra TcsTv variables generated during simplification
376 -- See Note [Extra TcsTv untouchables] in TcSimplify
381 = SimplInfer -- Inferring type of a let-bound thing
382 | SimplRuleLhs -- Inferring type of a RULE lhs
383 | SimplInteractive -- Inferring type at GHCi prompt
384 | SimplCheck -- Checking a type signature or RULE rhs
387 instance Outputable SimplContext where
388 ppr SimplInfer = ptext (sLit "SimplInfer")
389 ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
390 ppr SimplInteractive = ptext (sLit "SimplInteractive")
391 ppr SimplCheck = ptext (sLit "SimplCheck")
393 isInteractive :: SimplContext -> Bool
394 isInteractive SimplInteractive = True
395 isInteractive _ = False
397 simplEqsOnly :: SimplContext -> Bool
398 -- Simplify equalities only, not dictionaries
399 -- This is used for the LHS of rules; ee
400 -- Note [Simplifying RULE lhs constraints] in TcSimplify
401 simplEqsOnly SimplRuleLhs = True
402 simplEqsOnly _ = False
404 performDefaulting :: SimplContext -> Bool
405 performDefaulting SimplInfer = False
406 performDefaulting SimplRuleLhs = False
407 performDefaulting SimplInteractive = True
408 performDefaulting SimplCheck = True
411 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
413 instance Functor TcS where
414 fmap f m = TcS $ fmap f . unTcS m
416 instance Monad TcS where
417 return x = TcS (\_ -> return x)
418 fail err = TcS (\_ -> fail err)
419 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
421 -- Basic functionality
422 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
423 wrapTcS :: TcM a -> TcS a
424 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
425 -- and TcS is supposed to have limited functionality
426 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
428 wrapErrTcS :: TcM a -> TcS a
429 -- The thing wrapped should just fail
430 -- There's no static check; it's up to the user
431 -- Having a variant for each error message is too painful
434 wrapWarnTcS :: TcM a -> TcS a
435 -- The thing wrapped should just add a warning, or no-op
436 -- There's no static check; it's up to the user
437 wrapWarnTcS = wrapTcS
439 failTcS, panicTcS :: SDoc -> TcS a
440 failTcS = wrapTcS . TcM.failWith
441 panicTcS doc = pprPanic "TcCanonical" doc
443 traceTcS :: String -> SDoc -> TcS ()
444 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
446 traceTcS0 :: String -> SDoc -> TcS ()
447 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
449 runTcS :: SimplContext
450 -> Untouchables -- Untouchables
451 -> TcS a -- What to run
452 -> TcM (a, Bag EvBind)
453 runTcS context untouch tcs
454 = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
455 ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
456 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
457 , tcs_ty_binds = ty_binds_var
458 , tcs_context = context
459 , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
462 -- Run the computation
463 ; res <- unTcS tcs env
464 -- Perform the type unifications required
465 ; ty_binds <- TcM.readTcRef ty_binds_var
466 ; mapM_ do_unification (varEnvElts ty_binds)
469 ; ev_binds <- TcM.readTcRef evb_ref
470 ; return (res, evBindMapBinds ev_binds) }
472 do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
474 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
475 nestImplicTcS ref untch (TcS thing_inside)
476 = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
477 tcs_context = ctxt } ->
479 nest_env = TcSEnv { tcs_ev_binds = ref
480 , tcs_ty_binds = ty_binds
482 , tcs_context = ctxtUnderImplic ctxt }
484 thing_inside nest_env
486 recoverTcS :: TcS a -> TcS a -> TcS a
487 recoverTcS (TcS recovery_code) (TcS thing_inside)
489 TcM.recoverM (recovery_code env) (thing_inside env)
491 ctxtUnderImplic :: SimplContext -> SimplContext
492 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
493 ctxtUnderImplic SimplRuleLhs = SimplCheck
494 ctxtUnderImplic ctxt = ctxt
496 tryTcS :: TcS a -> TcS a
497 -- Like runTcS, but from within the TcS monad
498 -- Ignore all the evidence generated, and do not affect caller's evidence!
500 = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
501 ; ev_binds_var <- TcM.newTcEvBinds
502 ; let env1 = env { tcs_ev_binds = ev_binds_var
503 , tcs_ty_binds = ty_binds_var }
507 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
509 getDynFlags :: TcS DynFlags
510 getDynFlags = wrapTcS TcM.getDOpts
512 getTcSContext :: TcS SimplContext
513 getTcSContext = TcS (return . tcs_context)
515 getTcEvBinds :: TcS EvBindsVar
516 getTcEvBinds = TcS (return . tcs_ev_binds)
518 getUntouchables :: TcS TcsUntouchables
519 getUntouchables = TcS (return . tcs_untch)
521 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
522 getTcSTyBinds = TcS (return . tcs_ty_binds)
524 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
525 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
528 getTcEvBindsBag :: TcS EvBindMap
530 = do { EvBindsVar ev_ref _ <- getTcEvBinds
531 ; wrapTcS $ TcM.readTcRef ev_ref }
533 setWantedCoBind :: CoVar -> Coercion -> TcS ()
534 setWantedCoBind cv co
535 = setEvBind cv (EvCoercion co)
536 -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
538 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
539 -- Add a type binding
540 -- We never do this twice!
541 setWantedTyBind tv ty
542 = do { ref <- getTcSTyBinds
544 do { ty_binds <- TcM.readTcRef ref
546 ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
547 vcat [ text "TERRIBLE ERROR: double set of meta type variable"
548 , ppr tv <+> text ":=" <+> ppr ty
549 , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
551 ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
553 setIPBind :: EvVar -> EvTerm -> TcS ()
554 setIPBind = setEvBind
556 setDictBind :: EvVar -> EvTerm -> TcS ()
557 setDictBind = setEvBind
559 setEvBind :: EvVar -> EvTerm -> TcS ()
562 = do { tc_evbinds <- getTcEvBinds
563 ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
565 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
566 warnTcS loc warn_if doc
567 | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
568 | otherwise = return ()
570 getDefaultInfo :: TcS (SimplContext, [Type], (Bool, Bool))
572 = do { ctxt <- getTcSContext
573 ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
574 ; return (ctxt, tys, flags) }
576 -- Just get some environments needed for instance looking up and matching
577 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
579 getInstEnvs :: TcS (InstEnv, InstEnv)
580 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
582 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
583 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
585 getTopEnv :: TcS HscEnv
586 getTopEnv = wrapTcS $ TcM.getTopEnv
588 getGblEnv :: TcS TcGblEnv
589 getGblEnv = wrapTcS $ TcM.getGblEnv
591 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
594 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
595 checkWellStagedDFun pred dfun_id loc
596 = wrapTcS $ TcM.setCtLoc loc $
597 do { use_stage <- TcM.getStage
598 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
600 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
601 bind_lvl = TcM.topIdLvl dfun_id
603 pprEq :: TcType -> TcType -> SDoc
604 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
606 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
607 isTouchableMetaTyVar tv
608 = do { untch <- getUntouchables
609 ; return $ isTouchableMetaTyVar_InRange untch tv }
611 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
612 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
613 = case tcTyVarDetails tv of
614 MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
615 -- See Note [Touchable meta type variables]
616 MetaTv {} -> inTouchableRange untch tv
623 Note [Touchable meta type variables]
624 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
625 Meta type variables allocated *by the constraint solver itself* are always
627 instance C a b => D [a] where...
628 if we use this instance declaration we "make up" a fresh meta type
629 variable for 'b', which we must later guess. (Perhaps C has a
630 functional dependency.) But since we aren't in the constraint *generator*
631 we can't allocate a Unique in the touchable range for this implication
632 constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
637 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
639 newFlattenSkolemTy :: TcType -> TcS TcType
640 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
642 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
643 newFlattenSkolemTyVar ty
644 = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
645 ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
646 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
647 ; traceTcS "New Flatten Skolem Born" $
648 (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
652 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
654 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
655 instDFunTypes mb_inst_tys
656 = mapM inst_tv mb_inst_tys
658 inst_tv :: Either TyVar TcType -> TcS Type
659 inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
660 inst_tv (Right ty) = return ty
662 instDFunConstraints :: TcThetaType -> TcS [EvVar]
663 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
666 instFlexiTcS :: TyVar -> TcS TcTyVar
667 -- Like TcM.instMetaTyVar but the variable that is created is always
668 -- touchable; we are supposed to guess its instantiation.
669 -- See Note [Touchable meta type variables]
670 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
672 newFlexiTcSTy :: Kind -> TcS TcType
675 do { uniq <- TcM.newUnique
676 ; ref <- TcM.newMutVar Flexi
677 ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
678 ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
680 isFlexiTcsTv :: TyVar -> Bool
682 | not (isTcTyVar tv) = False
683 | MetaTv TcsTv _ <- tcTyVarDetails tv = True
686 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
687 -- Create new wanted CoVar that constrains the type to have the specified kind.
688 newKindConstraint tv knd
689 = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
690 ; let ty_k = mkTyVarTy tv_k
691 ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
694 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
695 instFlexiTcSHelper tvname tvkind
697 do { uniq <- TcM.newUnique
698 ; ref <- TcM.newMutVar Flexi
699 ; let name = setNameUnique tvname uniq
701 ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
703 -- Superclasses and recursive dictionaries
704 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
706 newEvVar :: TcPredType -> TcS EvVar
707 newEvVar pty = wrapTcS $ TcM.newEvVar pty
709 newDerivedId :: TcPredType -> TcS EvVar
710 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
712 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
713 -- Note we create immutable variables for given or derived, since we
714 -- must bind them to TcEvBinds (because their evidence may involve
715 -- superclasses). However we should be able to override existing
716 -- 'derived' evidence, even in TcEvBinds
717 newGivenCoVar ty1 ty2 co
718 = do { cv <- newCoVar ty1 ty2
719 ; setEvBind cv (EvCoercion co)
722 newWantedCoVar :: TcType -> TcType -> TcS EvVar
723 newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
725 newCoVar :: TcType -> TcType -> TcS EvVar
726 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
728 newIPVar :: IPName Name -> TcType -> TcS EvVar
729 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
731 newDictVar :: Class -> [TcType] -> TcS EvVar
732 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
737 -- Matching and looking up classes and family instances
738 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
740 data MatchInstResult mi
741 = MatchInstNo -- No matching instance
742 | MatchInstSingle mi -- Single matching instance
743 | MatchInstMany -- Multiple matching instances
746 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
747 -- Look up a class constraint in the instance environment
749 = do { let pred = mkClassPred clas tys
750 ; instEnvs <- getInstEnvs
751 ; case lookupInstEnv instEnvs clas tys of {
752 ([], unifs) -- Nothing matches
753 -> do { traceTcS "matchClass not matching"
754 (vcat [ text "dict" <+> ppr pred,
755 text "unifs" <+> ppr unifs ])
758 ([(ispec, inst_tys)], []) -- A single match
759 -> do { let dfun_id = is_dfun ispec
760 ; traceTcS "matchClass success"
761 (vcat [text "dict" <+> ppr pred,
762 text "witness" <+> ppr dfun_id
763 <+> ppr (idType dfun_id) ])
764 -- Record that this dfun is needed
765 ; return $ MatchInstSingle (dfun_id, inst_tys)
767 (matches, unifs) -- More than one matches
768 -> do { traceTcS "matchClass multiple matches, deferring choice"
769 (vcat [text "dict" <+> ppr pred,
770 text "matches" <+> ppr matches,
771 text "unifs" <+> ppr unifs])
772 ; return MatchInstMany
779 -> TcS (MatchInstResult (TyCon, [Type]))
781 = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
783 Nothing -> return MatchInstNo
784 Just res -> return $ MatchInstSingle res
785 -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
786 -- multiple matches. Check.
790 -- Functional dependencies, instantiation of equations
791 -------------------------------------------------------
793 mkDerivedFunDepEqns :: WantedLoc
794 -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
795 -> TcS [FlavoredEvVar] -- All Derived
796 mkDerivedFunDepEqns _ [] = return []
797 mkDerivedFunDepEqns loc eqns
798 = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
799 ; evvars <- mapM to_work_item eqns
800 ; return $ concat evvars }
802 to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
803 to_work_item ((qtvs, pairs), d1, d2)
804 = do { let tvs = varSetElems qtvs
805 ; tvs' <- mapM instFlexiTcS tvs
806 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
807 loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
809 ; mapM (do_one subst flav) pairs }
811 do_one subst flav (ty1, ty2)
812 = do { let sty1 = substTy subst ty1
813 sty2 = substTy subst ty2
814 ; ev <- newCoVar sty1 sty2
815 ; return (mkEvVarX ev flav) }
817 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
818 pprEquationDoc (eqn, (p1, _), (p2, _))
819 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
821 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
822 -> TcM (TidyEnv, SDoc)
823 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
824 = do { pred1' <- TcM.zonkTcPredType pred1
825 ; pred2' <- TcM.zonkTcPredType pred2
826 ; let { pred1'' = tidyPred tidy_env pred1'
827 ; pred2'' = tidyPred tidy_env pred2' }
828 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
829 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
830 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
831 ; return (tidy_env, msg) }