{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE MultiWayIf #-} -- | Solving Class constraints CDictCan module GHC.Tc.Solver.Dict ( solveDict, solveDictNC, solveCallStack, checkInstanceOK, matchLocalInst, chooseInstance, makeSuperClasses, mkStrictSuperClasses, ) where import GHC.Prelude import {-# SOURCE #-} GHC.Tc.Solver.Solve( solveSimpleWanteds ) import GHC.Tc.Errors.Types import GHC.Tc.Instance.FunDeps import GHC.Tc.Instance.Class( matchEqualityInst ) import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint import GHC.Tc.Types.CtLoc import GHC.Tc.Types.Origin import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Monad import GHC.Tc.Solver.Types import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Unify( uType, mightEqualLater ) import GHC.Hs.Type( HsIPName(..) ) import GHC.Core import GHC.Core.Make import GHC.Core.Type import GHC.Core.InstEnv ( DFunInstType, ClsInst(..) ) import GHC.Core.Class import GHC.Core.Predicate import GHC.Core.Multiplicity ( scaledThing ) import GHC.Core.Unify ( ruleMatchTyKiX ) import GHC.Types.TyThing( lookupDataCon, lookupId ) import GHC.Types.Name import GHC.Types.Name.Set import GHC.Types.Var import GHC.Types.Id( mkTemplateLocals ) import GHC.Types.Var.Set import GHC.Types.Var.Env import GHC.Types.SrcLoc import GHC.Builtin.Names( srcLocDataConName, pushCallStackName, emptyCallStackName ) import GHC.Utils.Monad ( concatMapM, foldlM ) import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Misc import GHC.Unit.Module import GHC.Data.Bag import GHC.Driver.DynFlags import qualified GHC.LanguageExtensions as LangExt import Data.Maybe ( listToMaybe, mapMaybe, isJust ) import Data.Void( Void ) import Control.Monad {- ********************************************************************* * * * Class Canonicalization * * ********************************************************************* -} solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void -- NC: this comes from CNonCanonical or CIrredCan -- Precondition: already rewritten by inert set solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void solveDictNC CtEvidence ev Class cls [Type] tys = do { TcS () -> SolverStage () forall a. TcS a -> SolverStage a simpleStage (TcS () -> SolverStage ()) -> TcS () -> SolverStage () forall a b. (a -> b) -> a -> b $ String -> SDoc -> TcS () traceTcS String "solveDictNC" (Type -> SDoc forall a. Outputable a => a -> SDoc ppr (Class -> [Type] -> Type mkClassPred Class cls [Type] tys) SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence ev) ; dict_ct <- CtEvidence -> Class -> [Type] -> SolverStage DictCt canDictCt CtEvidence ev Class cls [Type] tys ; solveDict dict_ct } solveDict :: DictCt -> SolverStage Void -- Preconditions: `tys` are already rewritten by the inert set solveDict :: DictCt -> SolverStage Void solveDict dict_ct :: DictCt dict_ct@(DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev, di_cls :: DictCt -> Class di_cls = Class cls, di_tys :: DictCt -> [Type] di_tys = [Type] tys }) | Class -> Bool isEqualityClass Class cls = CtEvidence -> Class -> [Type] -> SolverStage Void solveEqualityDict CtEvidence ev Class cls [Type] tys | Bool otherwise = Bool -> SDoc -> SolverStage Void -> SolverStage Void forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr (HasDebugCallStack => CtEvidence -> Role CtEvidence -> Role ctEvRewriteRole CtEvidence ev Role -> Role -> Bool forall a. Eq a => a -> a -> Bool == Role Nominal) (CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence ev SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ Class -> SDoc forall a. Outputable a => a -> SDoc ppr Class cls SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys) (SolverStage Void -> SolverStage Void) -> SolverStage Void -> SolverStage Void forall a b. (a -> b) -> a -> b $ do { TcS () -> SolverStage () forall a. TcS a -> SolverStage a simpleStage (TcS () -> SolverStage ()) -> TcS () -> SolverStage () forall a b. (a -> b) -> a -> b $ String -> SDoc -> TcS () traceTcS String "solveDict" (DictCt -> SDoc forall a. Outputable a => a -> SDoc ppr DictCt dict_ct) ; DictCt -> SolverStage () tryInertDicts DictCt dict_ct ; DictCt -> SolverStage () tryInstances DictCt dict_ct -- Try fundeps /after/ tryInstances: -- see (DFL2) in Note [Do fundeps last] ; DictCt -> SolverStage () doLocalFunDepImprovement DictCt dict_ct -- doLocalFunDepImprovement does StartAgain if there -- are any fundeps: see (DFL1) in Note [Do fundeps last] ; DictCt -> SolverStage () doTopFunDepImprovement DictCt dict_ct ; TcS () -> SolverStage () forall a. TcS a -> SolverStage a simpleStage (DictCt -> TcS () updInertDicts DictCt dict_ct) ; CtEvidence -> String -> SolverStage Void forall a. CtEvidence -> String -> SolverStage a stopWithStage (DictCt -> CtEvidence dictCtEvidence DictCt dict_ct) String "Kept inert DictCt" } canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt -- Once-only processing of Dict constraints: -- * expand superclasses -- * deal with CallStack canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt canDictCt CtEvidence ev Class cls [Type] tys | CtEvidence -> Bool isGiven CtEvidence ev -- See Note [Eagerly expand given superclasses] = TcS (StopOrContinue DictCt) -> SolverStage DictCt forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt) -> TcS (StopOrContinue DictCt) -> SolverStage DictCt forall a b. (a -> b) -> a -> b $ do { dflags <- TcS DynFlags forall (m :: * -> *). HasDynFlags m => m DynFlags getDynFlags ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] ; emitWork (listToBag sc_cts) ; continueWith (DictCt { di_ev = ev, di_cls = cls , di_tys = tys, di_pend_sc = doNotExpand }) } -- doNotExpand: We have already expanded superclasses for /this/ dict -- so set the fuel to doNotExpand to avoid repeating expansion | CtWanted (WantedCt { ctev_rewriters :: WantedCtEvidence -> RewriterSet ctev_rewriters = RewriterSet rws }) <- CtEvidence ev , Just FastString ip_name <- Class -> [Type] -> Maybe FastString isCallStackPred Class cls [Type] tys , Just FastString fun_fs <- CtOrigin -> Maybe FastString isPushCallStackOrigin_maybe CtOrigin orig -- If we're given a CallStack constraint that arose from a function -- call, we need to push the current call-site onto the stack instead -- of solving it directly from a given. -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence -- and Note [Solving CallStack constraints] = TcS (StopOrContinue DictCt) -> SolverStage DictCt forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt) -> TcS (StopOrContinue DictCt) -> SolverStage DictCt forall a b. (a -> b) -> a -> b $ do { -- First we emit a new constraint that will capture the -- given CallStack. let new_loc :: CtLoc new_loc = CtLoc -> CtOrigin -> CtLoc setCtLocOrigin CtLoc loc (HsIPName -> CtOrigin IPOccOrigin (FastString -> HsIPName HsIPName FastString ip_name)) -- We change the origin to IPOccOrigin so -- this rule does not fire again. -- See Note [Overview of implicit CallStacks] -- in GHC.Tc.Types.Evidence ; new_ev <- WantedCtEvidence -> CtEvidence CtWanted (WantedCtEvidence -> CtEvidence) -> TcS WantedCtEvidence -> TcS CtEvidence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> CtLoc -> RewriterSet -> Type -> TcS WantedCtEvidence newWantedEvVarNC CtLoc new_loc RewriterSet rws Type pred -- Then we solve the wanted by pushing the call-site -- onto the newly emitted CallStack ; let ev_cs = FastString -> RealSrcSpan -> EvExpr -> EvCallStack EvCsPushCall FastString fun_fs (CtLoc -> RealSrcSpan ctLocSpan CtLoc loc) (HasDebugCallStack => CtEvidence -> EvExpr CtEvidence -> EvExpr ctEvExpr CtEvidence new_ev) ; solveCallStack ev ev_cs ; continueWith (DictCt { di_ev = new_ev, di_cls = cls , di_tys = tys, di_pend_sc = doNotExpand }) } -- doNotExpand: No superclasses for class CallStack -- See invariants in CDictCan.cc_pend_sc | Bool otherwise = TcS (StopOrContinue DictCt) -> SolverStage DictCt forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt) -> TcS (StopOrContinue DictCt) -> SolverStage DictCt forall a b. (a -> b) -> a -> b $ do { dflags <- TcS DynFlags forall (m :: * -> *). HasDynFlags m => m DynFlags getDynFlags ; let fuel | Class -> Bool classHasSCs Class cls = DynFlags -> ScDepth wantedsFuel DynFlags dflags | Bool otherwise = ScDepth doNotExpand -- See Invariants in `CCDictCan.cc_pend_sc` ; continueWith (DictCt { di_ev = ev, di_cls = cls , di_tys = tys, di_pend_sc = fuel }) } where loc :: CtLoc loc = CtEvidence -> CtLoc ctEvLoc CtEvidence ev orig :: CtOrigin orig = CtLoc -> CtOrigin ctLocOrigin CtLoc loc pred :: Type pred = CtEvidence -> Type ctEvPred CtEvidence ev {- ********************************************************************* * * * Implicit parameters and call stacks * * ********************************************************************* -} solveCallStack :: CtEvidence -> EvCallStack -> TcS () -- Also called from GHC.Tc.Solver when defaulting call stacks solveCallStack :: CtEvidence -> EvCallStack -> TcS () solveCallStack CtEvidence ev EvCallStack ev_cs -- We're given ev_cs :: CallStack, but the evidence term should be a -- dictionary, so we have to coerce ev_cs to a dictionary for -- `IP ip CallStack`. See Note [Overview of implicit CallStacks] = do { inner_stk <- Type -> EvCallStack -> TcS EvExpr evCallStack Type pred EvCallStack ev_cs ; let ev_tm = EvExpr -> EvTerm EvExpr (Type -> EvExpr -> EvExpr evWrapIPE Type pred EvExpr inner_stk) ; setEvBindIfWanted ev EvCanonical ev_tm } -- EvCanonical: see Note [CallStack and ExceptionContext hack] where pred :: Type pred = CtEvidence -> Type ctEvPred CtEvidence ev -- Dictionary for CallStack implicit parameters evCallStack :: TcPredType -> EvCallStack -> TcS EvExpr -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence evCallStack :: Type -> EvCallStack -> TcS EvExpr evCallStack Type _ EvCallStack EvCsEmpty = EvVar -> EvExpr forall b. EvVar -> Expr b Var (EvVar -> EvExpr) -> TcS EvVar -> TcS EvExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Name -> TcS EvVar forall (m :: * -> *). MonadThings m => Name -> m EvVar lookupId Name emptyCallStackName evCallStack Type pred (EvCsPushCall FastString fs RealSrcSpan loc EvExpr tm) = do { df <- TcS DynFlags forall (m :: * -> *). HasDynFlags m => m DynFlags getDynFlags ; m <- getModule ; srcLocDataCon <- lookupDataCon srcLocDataConName ; let platform = DynFlags -> Platform targetPlatform DynFlags df mkSrcLoc RealSrcSpan l = DataCon -> [EvExpr] -> EvExpr mkCoreConWrapApps DataCon srcLocDataCon ([EvExpr] -> EvExpr) -> TcS [EvExpr] -> TcS EvExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [TcS EvExpr] -> TcS [EvExpr] forall (t :: * -> *) (m :: * -> *) a. (Traversable t, Monad m) => t (m a) -> m (t a) forall (m :: * -> *) a. Monad m => [m a] -> m [a] sequence [ FastString -> TcS EvExpr forall (m :: * -> *). MonadThings m => FastString -> m EvExpr mkStringExprFS (Unit -> FastString forall u. IsUnitId u => u -> FastString unitFS (Unit -> FastString) -> Unit -> FastString forall a b. (a -> b) -> a -> b $ Module -> Unit forall unit. GenModule unit -> unit moduleUnit Module m) , FastString -> TcS EvExpr forall (m :: * -> *). MonadThings m => FastString -> m EvExpr mkStringExprFS (ModuleName -> FastString moduleNameFS (ModuleName -> FastString) -> ModuleName -> FastString forall a b. (a -> b) -> a -> b $ Module -> ModuleName forall unit. GenModule unit -> ModuleName moduleName Module m) , FastString -> TcS EvExpr forall (m :: * -> *). MonadThings m => FastString -> m EvExpr mkStringExprFS (RealSrcSpan -> FastString srcSpanFile RealSrcSpan l) , EvExpr -> TcS EvExpr forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return (EvExpr -> TcS EvExpr) -> EvExpr -> TcS EvExpr forall a b. (a -> b) -> a -> b $ Platform -> ScDepth -> EvExpr mkIntExprInt Platform platform (RealSrcSpan -> ScDepth srcSpanStartLine RealSrcSpan l) , EvExpr -> TcS EvExpr forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return (EvExpr -> TcS EvExpr) -> EvExpr -> TcS EvExpr forall a b. (a -> b) -> a -> b $ Platform -> ScDepth -> EvExpr mkIntExprInt Platform platform (RealSrcSpan -> ScDepth srcSpanStartCol RealSrcSpan l) , EvExpr -> TcS EvExpr forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return (EvExpr -> TcS EvExpr) -> EvExpr -> TcS EvExpr forall a b. (a -> b) -> a -> b $ Platform -> ScDepth -> EvExpr mkIntExprInt Platform platform (RealSrcSpan -> ScDepth srcSpanEndLine RealSrcSpan l) , EvExpr -> TcS EvExpr forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return (EvExpr -> TcS EvExpr) -> EvExpr -> TcS EvExpr forall a b. (a -> b) -> a -> b $ Platform -> ScDepth -> EvExpr mkIntExprInt Platform platform (RealSrcSpan -> ScDepth srcSpanEndCol RealSrcSpan l) ] ; push_cs_id <- lookupId pushCallStackName ; name_expr <- mkStringExprFS fs ; loc_expr <- mkSrcLoc loc -- At this point tm :: IP sym CallStack -- but we need the actual CallStack to pass to pushCS, -- so we use evUwrapIP to strip the dictionary wrapper -- See Note [Overview of implicit CallStacks] ; let outer_stk = Type -> EvExpr -> EvExpr evUnwrapIPE Type pred EvExpr tm ; return (mkCoreApps (Var push_cs_id) [mkCoreTup [name_expr, loc_expr], outer_stk]) } {- Note [Solving CallStack constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence. Suppose f :: HasCallStack => blah. Then * Each call to 'f' gives rise to [W] s1 :: IP "callStack" CallStack -- CtOrigin = OccurrenceOf f with a CtOrigin that says "OccurrenceOf f". Remember that HasCallStack is just shorthand for IP "callStack" CallStack See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence * We canonicalise such constraints, in GHC.Tc.Solver.Dict.canDictNC, by pushing the call-site info on the stack, and changing the CtOrigin to record that has been done. Bind: s1 = pushCallStack <site-info> s2 [W] s2 :: IP "callStack" CallStack -- CtOrigin = IPOccOrigin * Then, and only then, we can solve the constraint from an enclosing Given. So we must be careful /not/ to solve 's1' from the Givens. We guarantee this by canonicalising before looking up in the inert set. Note [CallStack and ExceptionContext hack] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It isn't really right that we treat CallStack and ExceptionContext dictionaries as canonical, in the sense of Note [Coherence and specialisation: overview]. They definitely are not! But if we use EvNonCanonical here we get lots of nospec (error @Int) dict string (since `error` takes a HasCallStack dict), and that isn't bottoming (at least not without extra work) So, hackily, we just say that HasCallStack and ExceptionContext are canonical, even though they aren't really. Note [Shadowing of implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we add a new /given/ implicit parameter to the inert set, it /replaces/ any existing givens for the same implicit parameter. This makes a difference in two places: * In `GHC.Tc.Solver.InertSet.solveOneFromTheOther`, be careful when we have (?x :: ty) in the inert set and an identical (?x :: ty) as the work item. * In `updInertDicts`, in this module, when adding [G] (?x :: ty), remove any existing [G] (?x :: ty'), regardless of ty'. * Wrinkle (SIP1): we must be careful of superclasses. Consider f,g :: (?x::Int, C a) => a -> a f v = let ?x = 4 in g v The call to 'g' gives rise to a Wanted constraint (?x::Int, C a). We must /not/ solve this from the Given (?x::Int, C a), because of the intervening binding for (?x::Int). #14218. We deal with this by arranging that when we add [G] (?x::ty) we delete * from the inert_cans, and * from the inert_solved_dicts any existing [G] (?x::ty) /and/ any [G] D tys, where (D tys) has a superclass with (?x::ty). See Note [Local implicit parameters] in GHC.Core.Predicate. An important special case is constraint tuples like [G] (% ?x::ty, Eq a %). But it could happen for `class xx => D xx where ...` and the constraint D (?x :: int). This corner (constraint-kinded variables instantiated with implicit parameter constraints) is not well explored. Example in #14218, and #23761 The code that accounts for (SIP1) is in updInertDicts; in particular the call to GHC.Core.Predicate.mentionsIP. * Wrinkle (SIP2): we must apply this update semantics for `inert_solved_dicts` as well as `inert_cans`. You might think that wouldn't be necessary, because an element of `inert_solved_dicts` is never an implicit parameter (see Note [Solved dictionaries] in GHC.Tc.Solver.InertSet). While that is true, dictionaries in `inert_solved_dicts` may still have implicit parameters as a /superclass/! For example: class c => C c where ... f :: C (?x::Int) => blah Now (C (?x::Int)) has a superclass (?x::Int). This may look exotic, but it happens particularly for constraint tuples, like `(% ?x::Int, Eq a %)`. Example 1: Suppose we have (typecheck/should_compile/ImplicitParamFDs) flub :: (?x :: Int) => (Int, Integer) flub = (?x, let ?x = 5 in ?x) When we are checking the last ?x occurrence, we guess its type to be a fresh unification variable alpha and emit an (IP "x" alpha) constraint. But the given (?x :: Int) has been translated to an IP "x" Int constraint, which has a functional dependency from the name to the type. So if that (?x::Int) is still in the inert set, we'd get a fundep interaction that tells us that alpha ~ Int, and we get a type error. This is bad. The "replacement" semantics stops this happening. Example 2: f :: (?x :: Char) => Char f = let ?x = 'a' in ?x The "let ?x = ..." generates an implication constraint of the form: ?x :: Char => ?x :: Char Furthermore, the signature for `f` also generates an implication constraint, so we end up with the following nested implication: ?x :: Char => (?x :: Char => ?x :: Char) Note that the wanted (?x :: Char) constraint may be solved in two incompatible ways: either by using the parameter from the signature, or by using the local definition. Our intention is that the local definition should "shadow" the parameter of the signature. The "replacement" semantics for implicit parameters does this. Example 3: Similarly, consider f :: (?x::a) => Bool -> a g v = let ?x::Int = 3 in (f v, let ?x::Bool = True in f v) This should probably be well typed, with g :: Bool -> (Int, Bool) So the inner binding for ?x::Bool *overrides* the outer one. See ticket #17104 for a rather tricky example of this overriding behaviour. All this works for the normal cases but it has an odd side effect in some pathological programs like this: -- This is accepted, the second parameter shadows f1 :: (?x :: Int, ?x :: Char) => Char f1 = ?x -- This is rejected, the second parameter shadows f2 :: (?x :: Int, ?x :: Char) => Int f2 = ?x Both of these are actually wrong: when we try to use either one, we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char), which would lead to an error. I can think of two ways to fix this: 1. Simply disallow multiple constraints for the same implicit parameter---this is never useful, and it can be detected completely syntactically. 2. Move the shadowing machinery to the location where we nest implications, and add some code here that will produce an error if we get multiple givens for the same implicit parameter. -} {- ****************************************************************************** * * solveEqualityDict * * ****************************************************************************** -} {- Note [Solving equality classes] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider (~), which behaves as if it was defined like this: class a ~# b => a ~ b instance a ~# b => a ~ b There are two more similar "equality classes" like this. The full list is * (~) eqTyCon * (~~) heqTyCon * Coercible coercibleTyCon (See Note [The equality types story] in GHC.Builtin.Types.Prim.) (EQC1) For Givens, when expanding the superclasses of a equality class, we can /replace/ the constraint with its superclasses (which, remember, are equally powerful) rather than /adding/ them. This can make a huge difference. Consider T17836, which has a constraint like forall b,c. a ~ (b,c) => forall d,e. c ~ (d,e) => ...etc... If we just /add/ the superclasses of [G] g1:a ~ (b,c), we'll put [G] g1:(a~(b,c)) in the inert set and emit [G] g2:a ~# (b,c). That will kick out g1, and it'll be re-inserted as [G] g1':(b,c)~(b,c) which does no good to anyone. When the implication is deeply nested, this has quadratic cost, and no benefit. Just replace! (This can have a /big/ effect: test T17836 involves deeply-nested GADT pattern matching. Its compile-time allocation decreased by 40% when I added the "replace" rather than "add" semantics.) We achieve this by (a) not expanding superclasses for equality classes at all; see the `isEqualityClass` test in `mk_strict_superclasses` (b) special logic to solve (t1 ~ t2) in `solveEqualityDict`. (EQC2) Faced with [W] t1 ~ t2, it's always OK to reduce it to [W] t1 ~# t2, without worrying about Note [Instance and Given overlap]. Why? Because if we had [G] s1 ~ s2, then we'd get the superclass [G] s1 ~# s2, and so the reduction of the [W] constraint does not risk losing any solutions. On the other hand, it can be fatal to /fail/ to reduce such equalities on the grounds of Note [Instance and Given overlap], because many good things flow from [W] t1 ~# t2. Conclusion: we have a special solver pipeline for equality-class constraints, `solveEqualityDict`. It aggressively decomposes the boxed equality constraint into an unboxed coercion, both for Givens and Wanteds, and /replaces/ the boxed equality constraint with the unboxed one, so that the inert set never contains the boxed one. Note [Solving tuple constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ I tried treating tuple constraints, such as (% Eq a, Show a %), rather like equality-class constraints (see Note [Solving equality classes]). That is, by eagerly decomposing tuple-constraints into their component (Eq a) and (Show a). But discarding the tuple Given (which "replacing" does) means that we may have to reconstruct it for a recursive call. For example f :: (% Eq a, Show a %) => blah f x = ....(f x').... If we decomposed eagerly we'd get f = \(d : (% Eq a, Show a %)). let de = fst d ds = snd d in ....(f (% de, ds %))... and the optimiser may not be clever enough to transform (f (% de, ds %)) into (f d). See #10359 and its test case, and #23398. (This issue is less pressing for equality classes because they have to be unpacked strictly, so CSE-ing away the reconstruction works fine. So at the moment we don't decompose tuple constraints eagerly; instead we mostly just treat them like other constraints. * Given tuples are decomposed via their superclasses, in `canDictCt`. So [G] (% Eq a, Show a %) has superclasses [G] Eq a, [G] Show a * Wanted tuples are decomposed via a built-in "instance". See `GHC.Tc.Instance.Class.matchCTuple` There is a bit of special treatment: search for isCTupleClass. -} solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void -- See Note [Solving equality classes] -- Precondition: (isEqualityClass cls) True, so cls is (~), (~~), or Coercible solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void solveEqualityDict CtEvidence ev Class cls [Type] tys | CtWanted (WantedCt { ctev_dest :: WantedCtEvidence -> TcEvDest ctev_dest = TcEvDest dest }) <- CtEvidence ev = TcS (StopOrContinue Void) -> SolverStage Void forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue Void) -> SolverStage Void) -> TcS (StopOrContinue Void) -> SolverStage Void forall a b. (a -> b) -> a -> b $ do { let (Role role, Type t1, Type t2) = Class -> [Type] -> (Role, Type, Type) matchEqualityInst Class cls [Type] tys -- Unify t1~t2, putting anything that can't be solved -- immediately into the work list ; (co, _, _) <- CtEvidence -> Role -> (UnifyEnv -> TcM CoercionN) -> TcS (CoercionN, Cts, [EvVar]) forall a. CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [EvVar]) wrapUnifierTcS CtEvidence ev Role role ((UnifyEnv -> TcM CoercionN) -> TcS (CoercionN, Cts, [EvVar])) -> (UnifyEnv -> TcM CoercionN) -> TcS (CoercionN, Cts, [EvVar]) forall a b. (a -> b) -> a -> b $ \UnifyEnv uenv -> UnifyEnv -> Type -> Type -> TcM CoercionN uType UnifyEnv uenv Type t1 Type t2 -- Set d :: (t1~t2) = Eq# co ; setWantedEvTerm dest EvCanonical $ evDictApp cls tys [Coercion co] ; stopWith ev "Solved wanted lifted equality" } | CtGiven (GivenCt { ctev_evar :: GivenCtEvidence -> EvVar ctev_evar = EvVar ev_id }) <- CtEvidence ev , [EvVar sel_id] <- Class -> [EvVar] classSCSelIds Class cls -- Equality classes have just one superclass = TcS (StopOrContinue Void) -> SolverStage Void forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue Void) -> SolverStage Void) -> TcS (StopOrContinue Void) -> SolverStage Void forall a b. (a -> b) -> a -> b $ do { let loc :: CtLoc loc = CtEvidence -> CtLoc ctEvLoc CtEvidence ev sc_pred :: Type sc_pred = EvVar -> [Type] -> Type classMethodInstTy EvVar sel_id [Type] tys ev_expr :: EvTerm ev_expr = EvExpr -> EvTerm EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm forall a b. (a -> b) -> a -> b $ EvVar -> EvExpr forall b. EvVar -> Expr b Var EvVar sel_id EvExpr -> [Type] -> EvExpr forall b. Expr b -> [Type] -> Expr b `mkTyApps` [Type] tys EvExpr -> EvExpr -> EvExpr forall b. Expr b -> Expr b -> Expr b `App` EvVar -> EvExpr evId EvVar ev_id ; given_ev <- CtLoc -> (Type, EvTerm) -> TcS GivenCtEvidence newGivenEvVar CtLoc loc (Type sc_pred, EvTerm ev_expr) ; startAgainWith (mkNonCanonical $ CtGiven given_ev) } | Bool otherwise = String -> SDoc -> SolverStage Void forall a. HasCallStack => String -> SDoc -> a pprPanic String "solveEqualityDict" (Class -> SDoc forall a. Outputable a => a -> SDoc ppr Class cls) {- ****************************************************************************** * * interactDict * * ********************************************************************************* Note [Shortcut solving] ~~~~~~~~~~~~~~~~~~~~~~~ When we interact a [W] constraint with a [G] constraint that solves it, there is a possibility that we could produce better code if instead we solved from a top-level instance declaration (See #12791, #5835). For example: class M a b where m :: a -> b type C a b = (Num a, M a b) f :: C Int b => b -> Int -> Int f _ x = x + 1 The body of `f` requires a [W] `Num Int` instance. We could solve this constraint from the givens because we have `C Int b` and that provides us a solution for `Num Int`. This would let us produce core like the following (with -O2): f :: forall b. C Int b => b -> Int -> Int f = \ (@ b) ($d(%,%) :: C Int b) _ (eta1 :: Int) -> + @ Int (GHC.Classes.$p1(%,%) @ (Num Int) @ (M Int b) $d(%,%)) eta1 A.f1 This is bad! We could do /much/ better if we solved [W] `Num Int` directly from the instance that we have in scope: f :: forall b. C Int b => b -> Int -> Int f = \ (@ b) _ _ (x :: Int) -> case x of { GHC.Types.I# x1 -> GHC.Types.I# (GHC.Prim.+# x1 1#) } ** NB: It is important to emphasize that all this is purely an optimization: ** exactly the same programs should typecheck with or without this procedure. Consider f :: Ord [a] => ... f x = ..Need Eq [a]... We could use the Eq [a] superclass of the Ord [a], or we could use the top-level instance `Eq a => Eq [a]`. But if we did the latter we'd be stuck with an insoluble constraint (Eq a). ----------------------------------- So the ShortCutSolving plan is this: If we could solve a constraint from a local Given, try first to /completely/ solve the constraint using only top-level instances, /without/ using any local Givens. - If that succeeds, use it - If not, use the local Given ----------------------------------- An example that succeeds: class Eq a => C a b | b -> a where m :: b -> a f :: C [Int] b => b -> Bool f x = m x == [] We solve for `Eq [Int]`, which requires `Eq Int`, which we also have. This produces the following core: f :: forall b. C [Int] b => b -> Bool f = \ (@ b) ($dC :: C [Int] b) (x :: b) -> GHC.Classes.$fEq[]_$s$c== (m @ [Int] @ b $dC x) (GHC.Types.[] @ Int) An example that fails: class Eq a => C a b | b -> a where m :: b -> a f :: C [a] b => b -> Bool f x = m x == [] Which, because solving `Eq [a]` demands `Eq a` which we cannot solve. so short-cut solving fails and we use the superclass of C: f :: forall a b. C [a] b => b -> Bool f = \ (@ a) (@ b) ($dC :: C [a] b) (eta :: b) -> == @ [a] (A.$p1C @ [a] @ b $dC) (m @ [a] @ b $dC eta) (GHC.Types.[] @ a) The moving parts are relatively simple: * To attempt to solve the constraint completely, we just recursively call the constraint solver. See the use of `tryTcS` in `tcShortCutSolver`. * When this attempted recursive solving, we set a special mode `TcSShortCut`, which signals that we are trying to solve using only top-level instances. We switch on `TcSShortCut` mode in `tryShortCutSolver`. * When in TcSShortCut mode, we behave specially in a few places: - `tryInertDicts`, where we would otherwise look for a Given to solve our Wanted - `GHC.Tc.Solver.Monad.lookupInertDict` similarly - `noMatchableGivenDicts`, which also consults the Givens - `matchLocalInst`, which would otherwise consult Given quantified constraints - `GHC.Tc.Solver.Instance.Class.matchInstEnv`: when short-cut solving, don't pick overlappable top-level instances - `GHC.Tc.Solver.Solve.runTcPluginsWanted`: don't pass any Givens to the plugin Some wrinkles: (SCS1) Note [Shortcut solving: incoherence] (SCS2) The short-cut solver just uses the solver recursively, so we get its full power: * We need to be able to handle recursive super classes. The solved_dicts state ensures that we remember what we have already tried to solve to avoid looping. * As #15164 showed, it can be important to exploit sharing between goals. E.g. To solve G we may need G1 and G2. To solve G1 we may need H; and to solve G2 we may need H. If we don't spot this sharing we may solve H twice; and if this pattern repeats we may get exponentially bad behaviour. * Suppose we have (#13943) class Take (n :: Nat) where ... instance {-# OVERLAPPING #-} Take 0 where .. instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where .. And we have [W] Take 3. That only matches one instance so we get [W] Take (3-1). Then we should reduce the (3-1) to 2, and continue. (SCS3) When doing short-cut solving we can (and should) inherit the `solved_dicts` of the caller (#15164). You might worry about having a solved-dict that uses a Given -- but that too will have been subject to short-cut solving so it's fine. Note [Shortcut solving: incoherence] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This optimization relies on coherence of dictionaries to be correct. When we cannot assume coherence because of IncoherentInstances then this optimization can change the behavior of the user's code. The following four modules produce a program whose output would change depending on whether we apply this optimization when IncoherentInstances is in effect: ========= {-# LANGUAGE MultiParamTypeClasses #-} module A where class A a where int :: a -> Int class A a => C a b where m :: b -> a -> a ========= {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} module B where import A instance A a where int _ = 1 instance C a [b] where m _ = id ========= {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE IncoherentInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} module C where import A instance A Int where int _ = 2 instance C Int [Int] where m _ = id intC :: C Int a => a -> Int -> Int intC _ x = int x ========= module Main where import A import B import C main :: IO () main = print (intC [] (0::Int)) The output of `main` if we avoid the optimization under the effect of IncoherentInstances is `1`. If we were to do the optimization, the output of `main` would be `2`. Note [No Given/Given fundeps] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We do not create constraints from: * Given/Given interactions via functional dependencies or type family injectivity annotations. * Given/instance fundep interactions via functional dependencies or type family injectivity annotations. In this Note, all these interactions are called just "fundeps". We ingore such fundeps for several reasons: 1. These fundeps will never serve a purpose in accepting more programs: Given constraints do not contain metavariables that could be unified via exploring fundeps. They *could* be useful in discovering inaccessible code. However, the constraints will be Wanteds, and as such will cause errors (not just warnings) if they go unsolved. Maybe there is a clever way to get the right inaccessible code warnings, but the path forward is far from clear. #12466 has further commentary. 2. Furthermore, here is a case where a Given/instance interaction is actively harmful (from dependent/should_compile/RaeJobTalk): type family a == b :: Bool type family Not a = r | r -> a where Not False = True Not True = False [G] Not (a == b) ~ True Reacting this Given with the equations for Not produces [W] a == b ~ False This is indeed a true consequence, and would make sense as a fresh Given. But we don't have a way to produce evidence for fundeps, as a Wanted it is /harmful/: we can't prove it, and so we'll report an error and reject the program. (Previously fundeps gave rise to Deriveds, which carried no evidence, so it didn't matter that they could not be proved.) 3. #20922 showed a subtle different problem with Given/instance fundeps. type family ZipCons (as :: [k]) (bssx :: [[k]]) = (r :: [[k]]) | r -> as bssx where ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss ... tclevel = 4 [G] ZipCons is1 iss ~ (i : is2) : jss (The tclevel=4 means that this Given is at level 4.) The fundep tells us that 'iss' must be of form (is2 : beta[4]) where beta[4] is a fresh unification variable; we don't know what type it stands for. So we would emit [W] iss ~ is2 : beta Again we can't prove that equality; and worse we'll rewrite iss to (is2:beta) in deeply nested constraints inside this implication, where beta is untouchable (under other equality constraints), leading to other insoluble constraints. The bottom line: since we have no evidence for them, we should ignore Given/Given and Given/instance fundeps entirely. -} tryInertDicts :: DictCt -> SolverStage () tryInertDicts :: DictCt -> SolverStage () tryInertDicts DictCt dict_ct = TcS (StopOrContinue ()) -> SolverStage () forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue ()) -> SolverStage ()) -> TcS (StopOrContinue ()) -> SolverStage () forall a b. (a -> b) -> a -> b $ do { inerts <- TcS InertCans getInertCans ; mode <- getTcSMode ; try_inert_dicts mode inerts dict_ct } try_inert_dicts :: TcSMode -> InertCans -> DictCt -> TcS (StopOrContinue ()) try_inert_dicts :: TcSMode -> InertCans -> DictCt -> TcS (StopOrContinue ()) try_inert_dicts TcSMode mode InertCans inerts dict_w :: DictCt dict_w@(DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev_w, di_cls :: DictCt -> Class di_cls = Class cls, di_tys :: DictCt -> [Type] di_tys = [Type] tys }) | Bool -> Bool not (TcSMode mode TcSMode -> TcSMode -> Bool forall a. Eq a => a -> a -> Bool == TcSMode TcSShortCut) -- Ignore the inerts (esp Givens) in short-cut mode -- See Note [Shortcut solving] , Just DictCt dict_i <- InertCans -> Class -> [Type] -> Maybe DictCt lookupInertDict InertCans inerts Class cls [Type] tys , let ev_i :: CtEvidence ev_i = DictCt -> CtEvidence dictCtEvidence DictCt dict_i loc_i :: CtLoc loc_i = CtEvidence -> CtLoc ctEvLoc CtEvidence ev_i loc_w :: CtLoc loc_w = CtEvidence -> CtLoc ctEvLoc CtEvidence ev_w = -- There is a matching dictionary in the inert set do { -- First to try to solve it /completely/ from top level instances -- See Note [Shortcut solving] ; short_cut_worked <- Bool -> DictCt -> TcS Bool tryShortCutSolver (CtEvidence -> Bool isGiven CtEvidence ev_i) DictCt dict_w ; if | short_cut_worked -> stopWith ev_w "shortCutSolver worked(1)" -- Next see if we are in "loopy-superclass" land. If so, -- we don't want to replace the (Given) inert with the -- (Wanted) work-item, or vice versa; we want to hang on -- to both, and try to solve the work-item via an instance. -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance | prohibitedSuperClassSolve loc_i loc_w -> continueWith () | otherwise -- We can either solve the inert from the work-item or vice-versa. -> case solveOneFromTheOther (CDictCan dict_i) (CDictCan dict_w) of InteractResult KeepInert -> do { String -> SDoc -> TcS () traceTcS String "lookupInertDict:KeepInert" (DictCt -> SDoc forall a. Outputable a => a -> SDoc ppr DictCt dict_w) ; CtEvidence -> CanonicalEvidence -> EvTerm -> TcS () setEvBindIfWanted CtEvidence ev_w CanonicalEvidence EvCanonical (CtEvidence -> EvTerm ctEvTerm CtEvidence ev_i) ; StopOrContinue () -> TcS (StopOrContinue ()) forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return (StopOrContinue () -> TcS (StopOrContinue ())) -> StopOrContinue () -> TcS (StopOrContinue ()) forall a b. (a -> b) -> a -> b $ CtEvidence -> SDoc -> StopOrContinue () forall a. CtEvidence -> SDoc -> StopOrContinue a Stop CtEvidence ev_w (String -> SDoc forall doc. IsLine doc => String -> doc text String "Dict equal" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> DictCt -> SDoc forall a. Outputable a => a -> SDoc ppr DictCt dict_w) } InteractResult KeepWork -> do { String -> SDoc -> TcS () traceTcS String "lookupInertDict:KeepWork" (DictCt -> SDoc forall a. Outputable a => a -> SDoc ppr DictCt dict_w) ; CtEvidence -> CanonicalEvidence -> EvTerm -> TcS () setEvBindIfWanted CtEvidence ev_i CanonicalEvidence EvCanonical (CtEvidence -> EvTerm ctEvTerm CtEvidence ev_w) ; (InertCans -> InertCans) -> TcS () updInertCans ((DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans updDicts ((DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans) -> (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans forall a b. (a -> b) -> a -> b $ DictCt -> DictMap DictCt -> DictMap DictCt forall a. DictCt -> DictMap a -> DictMap a delDict DictCt dict_w) ; () -> TcS (StopOrContinue ()) forall a. a -> TcS (StopOrContinue a) continueWith () } } | Bool otherwise = do { String -> SDoc -> TcS () traceTcS String "tryInertDicts:no" (DictCt -> SDoc forall a. Outputable a => a -> SDoc ppr DictCt dict_w SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ Class -> SDoc forall a. Outputable a => a -> SDoc ppr Class cls SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys) ; () -> TcS (StopOrContinue ()) forall a. a -> TcS (StopOrContinue a) continueWith () } -- See Note [Shortcut solving] tryShortCutSolver :: Bool -- True <=> try the short-cut solver; False <=> don't -> DictCt -- Work item -> TcS Bool -- True <=> success -- We are about to solve a [W] constraint from a [G] constraint. We take -- a moment to see if we can get a better solution using an instance. -- Note that we only do this for the sake of performance. Exactly the same -- programs should typecheck regardless of whether we take this step or -- not. See Note [Shortcut solving] tryShortCutSolver :: Bool -> DictCt -> TcS Bool tryShortCutSolver Bool try_short_cut dict_w :: DictCt dict_w@(DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev_w }) | Bool -> Bool not Bool try_short_cut = Bool -> TcS Bool forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return Bool False | Bool otherwise = do { dflags <- TcS DynFlags forall (m :: * -> *). HasDynFlags m => m DynFlags getDynFlags ; if | CtWanted (WantedCt { ctev_pred = pred_w }) <- ev_w , not (couldBeIPLike pred_w) -- Not for implicit parameters (#18627) , not (xopt LangExt.IncoherentInstances dflags) -- If IncoherentInstances is on then we cannot rely on coherence of proofs -- in order to justify this optimization: The proof provided by the -- [G] constraint's superclass may be different from the top-level proof. -- See Note [Shortcut solving: incoherence] , gopt Opt_SolveConstantDicts dflags -- Enabled by the -fsolve-constant-dicts flag -> tryTcS $ -- tryTcS tries to completely solve some contraints -- Inherit the current solved_dicts, so that one invocation of -- tryShortCutSolver can benefit from the work of earlier invocations -- See wrinkle (SCS3) of Note [Shortcut solving] setTcSMode TcSShortCut $ do { residual <- solveSimpleWanteds (unitBag (CDictCan dict_w)) ; return (isEmptyBag residual) } | otherwise -> return False } {- ******************************************************************* * * Top-level reaction for class constraints (CDictCan) * * **********************************************************************-} tryInstances :: DictCt -> SolverStage () tryInstances :: DictCt -> SolverStage () tryInstances DictCt dict_ct = TcS (StopOrContinue ()) -> SolverStage () forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue ()) -> SolverStage ()) -> TcS (StopOrContinue ()) -> SolverStage () forall a b. (a -> b) -> a -> b $ do { inerts <- TcS InertSet getInertSet ; try_instances inerts dict_ct } try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ()) -- Try to use type-class instance declarations to simplify the constraint try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ()) try_instances InertSet inerts work_item :: DictCt work_item@(DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev, di_cls :: DictCt -> Class di_cls = Class cls , di_tys :: DictCt -> [Type] di_tys = [Type] xis }) | CtEvidence -> Bool isGiven CtEvidence ev -- Never use instances for Given constraints = () -> TcS (StopOrContinue ()) forall a. a -> TcS (StopOrContinue a) continueWith () -- See Note [No Given/Given fundeps] | Just CtEvidence solved_ev <- InertSet -> Class -> [Type] -> Maybe CtEvidence lookupSolvedDict InertSet inerts Class cls [Type] xis -- Cached = do { CtEvidence -> CanonicalEvidence -> EvTerm -> TcS () setEvBindIfWanted CtEvidence ev CanonicalEvidence EvCanonical (CtEvidence -> EvTerm ctEvTerm CtEvidence solved_ev) ; CtEvidence -> String -> TcS (StopOrContinue ()) forall a. CtEvidence -> String -> TcS (StopOrContinue a) stopWith CtEvidence ev String "Dict/Top (cached)" } | Bool otherwise -- Wanted, but not cached = do { dflags <- TcS DynFlags forall (m :: * -> *). HasDynFlags m => m DynFlags getDynFlags ; mode <- getTcSMode ; lkup_res <- matchClassInst dflags mode inerts cls xis dict_loc ; case lkup_res of OneInst { cir_what :: ClsInstResult -> InstanceWhat cir_what = InstanceWhat what } -> do { let is_local_given :: Bool is_local_given = case InstanceWhat what of { InstanceWhat LocalInstance -> Bool True; InstanceWhat _ -> Bool False } ; take_shortcut <- Bool -> DictCt -> TcS Bool tryShortCutSolver Bool is_local_given DictCt work_item ; if take_shortcut then stopWith ev "shortCutSolver worked(2)" else do { insertSafeOverlapFailureTcS what work_item ; updSolvedDicts what work_item ; chooseInstance ev lkup_res } } ClsInstResult _ -> -- NoInstance or NotSure: we didn't solve it () -> TcS (StopOrContinue ()) forall a. a -> TcS (StopOrContinue a) continueWith () } where dict_loc :: CtLoc dict_loc = CtEvidence -> CtLoc ctEvLoc CtEvidence ev chooseInstance :: CtEvidence -> ClsInstResult -> TcS (StopOrContinue a) chooseInstance :: forall a. CtEvidence -> ClsInstResult -> TcS (StopOrContinue a) chooseInstance CtEvidence work_item (OneInst { cir_new_theta :: ClsInstResult -> [Type] cir_new_theta = [Type] theta , cir_what :: ClsInstResult -> InstanceWhat cir_what = InstanceWhat what , cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm cir_mk_ev = [EvExpr] -> EvTerm mk_ev , cir_canonical :: ClsInstResult -> CanonicalEvidence cir_canonical = CanonicalEvidence canonical }) = do { String -> SDoc -> TcS () traceTcS String "doTopReact/found instance for" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence work_item ; deeper_loc <- CtLoc -> InstanceWhat -> Type -> TcS CtLoc checkInstanceOK CtLoc loc InstanceWhat what Type pred ; checkReductionDepth deeper_loc pred ; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar) (ppr work_item) ; evc_vars <- mapM (newWanted deeper_loc (ctEvRewriters work_item)) theta ; setEvBindIfWanted work_item canonical (mk_ev (map getEvExpr evc_vars)) ; emitWorkNC (map CtWanted $ freshGoals evc_vars) ; stopWith work_item "Dict/Top (solved wanted)" } where pred :: Type pred = CtEvidence -> Type ctEvPred CtEvidence work_item loc :: CtLoc loc = CtEvidence -> CtLoc ctEvLoc CtEvidence work_item chooseInstance CtEvidence work_item ClsInstResult lookup_res = String -> SDoc -> TcS (StopOrContinue a) forall a. HasCallStack => String -> SDoc -> a pprPanic String "chooseInstance" (CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence work_item SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ ClsInstResult -> SDoc forall a. Outputable a => a -> SDoc ppr ClsInstResult lookup_res) checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc -- Check that it's OK to use this instance: -- (a) the use is well staged in the Template Haskell sense -- Returns the CtLoc to used for sub-goals -- Probably also want to call checkReductionDepth checkInstanceOK :: CtLoc -> InstanceWhat -> Type -> TcS CtLoc checkInstanceOK CtLoc loc InstanceWhat what Type pred = do { CtLoc -> InstanceWhat -> Type -> TcS () checkWellLevelledDFun CtLoc loc InstanceWhat what Type pred ; CtLoc -> TcS CtLoc forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return CtLoc deeper_loc } where deeper_loc :: CtLoc deeper_loc = CtLoc -> CtLoc zap_origin (CtLoc -> CtLoc bumpCtLocDepth CtLoc loc) origin :: CtOrigin origin = CtLoc -> CtOrigin ctLocOrigin CtLoc loc zap_origin :: CtLoc -> CtLoc zap_origin CtLoc loc -- After applying an instance we can set ScOrigin to -- NotNakedSc, so that prohibitedSuperClassSolve never fires -- See Note [Solving superclass constraints] in -- GHC.Tc.TyCl.Instance, (sc1). | ScOrigin ClsInstOrQC what NakedScFlag _ <- CtOrigin origin = CtLoc -> CtOrigin -> CtLoc setCtLocOrigin CtLoc loc (ClsInstOrQC -> NakedScFlag -> CtOrigin ScOrigin ClsInstOrQC what NakedScFlag NotNakedSc) | Bool otherwise = CtLoc loc matchClassInst :: DynFlags -> TcSMode -> InertSet -> Class -> [Type] -> CtLoc -> TcS ClsInstResult matchClassInst :: DynFlags -> TcSMode -> InertSet -> Class -> [Type] -> CtLoc -> TcS ClsInstResult matchClassInst DynFlags dflags TcSMode mode InertSet inerts Class clas [Type] tys CtLoc loc -- First check whether there is an in-scope Given that could -- match this constraint. In that case, do not use any instance -- whether top level, or local quantified constraints. -- See Note [Instance and Given overlap] and see -- (IL0) in Note [Rules for instance lookup] in GHC.Core.InstEnv | Bool -> Bool not (Extension -> DynFlags -> Bool xopt Extension LangExt.IncoherentInstances DynFlags dflags) , Bool -> Bool not (Class -> Bool isCTupleClass Class clas) -- It is always safe to unpack constraint tuples -- And if we don't do so, we may never solve it at all -- See Note [Solving tuple constraints] , Bool -> Bool not (TcSMode -> InertSet -> CtLoc -> Class -> [Type] -> Bool noMatchableGivenDicts TcSMode mode InertSet inerts CtLoc loc Class clas [Type] tys) = do { String -> SDoc -> TcS () traceTcS String "Delaying instance application" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ String -> SDoc forall doc. IsLine doc => String -> doc text String "Work item:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Class -> [Type] -> SDoc pprClassPred Class clas [Type] tys ] ; ClsInstResult -> TcS ClsInstResult forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return ClsInstResult NotSure } | Bool otherwise = do { String -> SDoc -> TcS () traceTcS String "matchClassInst" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "pred =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type pred SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Char -> SDoc forall doc. IsLine doc => Char -> doc char Char '{' ; local_res <- Type -> CtLoc -> TcS ClsInstResult matchLocalInst Type pred CtLoc loc ; case local_res of OneInst {} -> -- See Note [Local instances and incoherence] do { String -> SDoc -> TcS () traceTcS String "} matchClassInst local match" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ ClsInstResult -> SDoc forall a. Outputable a => a -> SDoc ppr ClsInstResult local_res ; ClsInstResult -> TcS ClsInstResult forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return ClsInstResult local_res } ClsInstResult NotSure -> -- In the NotSure case for local instances -- we don't want to try global instances do { String -> SDoc -> TcS () traceTcS String "} matchClassInst local not sure" SDoc forall doc. IsOutput doc => doc empty ; ClsInstResult -> TcS ClsInstResult forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return ClsInstResult local_res } ClsInstResult NoInstance -- No local instances, so try global ones -> do { global_res <- DynFlags -> Class -> [Type] -> CtLoc -> TcS ClsInstResult matchGlobalInst DynFlags dflags Class clas [Type] tys CtLoc loc ; warn_custom_warn_instance global_res loc -- See Note [Implementation of deprecated instances] ; traceTcS "} matchClassInst global result" $ ppr global_res ; return global_res } } where pred :: Type pred = Class -> [Type] -> Type mkClassPred Class clas [Type] tys -- | Returns True iff there are no Given constraints that might, -- potentially, match the given class constraint. This is used when checking to see if a -- Given might overlap with an instance. See Note [Instance and Given overlap] -- in GHC.Tc.Solver.Dict noMatchableGivenDicts :: TcSMode -> InertSet -> CtLoc -> Class -> [TcType] -> Bool noMatchableGivenDicts :: TcSMode -> InertSet -> CtLoc -> Class -> [Type] -> Bool noMatchableGivenDicts TcSMode mode inerts :: InertSet inerts@(IS { inert_cans :: InertSet -> InertCans inert_cans = InertCans inert_cans }) CtLoc loc_w Class clas [Type] tys | TcSMode TcSShortCut <- TcSMode mode = Bool True -- In TcSShortCut mode we behave as if there were no Givens at all | Bool otherwise = Bool -> Bool not (Bool -> Bool) -> Bool -> Bool forall a b. (a -> b) -> a -> b $ (DictCt -> Bool) -> Bag DictCt -> Bool forall a. (a -> Bool) -> Bag a -> Bool anyBag DictCt -> Bool matchable_given (Bag DictCt -> Bool) -> Bag DictCt -> Bool forall a b. (a -> b) -> a -> b $ DictMap DictCt -> Class -> Bag DictCt forall a. DictMap a -> Class -> Bag a findDictsByClass (InertCans -> DictMap DictCt inert_dicts InertCans inert_cans) Class clas where pred_w :: Type pred_w = Class -> [Type] -> Type mkClassPred Class clas [Type] tys matchable_given :: DictCt -> Bool matchable_given :: DictCt -> Bool matchable_given (DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev }) | CtGiven (GivenCt { ctev_loc :: GivenCtEvidence -> CtLoc ctev_loc = CtLoc loc_g, ctev_pred :: GivenCtEvidence -> Type ctev_pred = Type pred_g }) <- CtEvidence ev = Maybe Subst -> Bool forall a. Maybe a -> Bool isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool forall a b. (a -> b) -> a -> b $ InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst mightEqualLater InertSet inerts Type pred_g CtLoc loc_g Type pred_w CtLoc loc_w | Bool otherwise = Bool False {- Note [Implementation of deprecated instances] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This note describes the implementation of the deprecated instances GHC proposal https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0575-deprecated-instances.rst In the parser, we parse deprecations/warnings attached to instances: instance {-# DEPRECATED "msg" #-} Show X deriving instance {-# WARNING "msg2" #-} Eq Y (Note that non-standalone deriving instance declarations do not support this mechanism.) (Note that the DEPRECATED and WARNING pragmas can be used here interchangeably.) We store the resulting warning message in the extension field of `ClsInstDecl` (respectively, `DerivDecl`; See Note [Trees That Grow]). In `GHC.Tc.TyCl.Instance.tcClsInstDecl` (respectively, `GHC.Tc.Deriv.Utils.newDerivClsInst`), we pass on that information to `ClsInst` (and eventually store it in `IfaceClsInst` too). Next, if we solve a constraint using such an instance, in `GHC.Tc.Instance.Class.matchInstEnv`, we pass it further into the `Ghc.Tc.Types.Origin.InstanceWhat`. Finally, if the instance solving function `GHC.Tc.Solver.Monad.matchGlobalInst` returns a `Ghc.Tc.Instance.Class.ClsInstResult` with `Ghc.Tc.Types.Origin.InstanceWhat` containing a warning, when called from either `matchClassInst` or `shortCutSolver`, we call `warn_custom_warn_instance` that ultimately emits the warning if needed. Note that we only emit a warning when the instance is used in a different module than it is defined, which keeps the behaviour in line with the deprecation of top-level identifiers. -} -- | Emits the custom warning for a deprecated instance -- -- See Note [Implementation of deprecated instances] warn_custom_warn_instance :: ClsInstResult -> CtLoc -> TcS () warn_custom_warn_instance :: ClsInstResult -> CtLoc -> TcS () warn_custom_warn_instance (OneInst{ cir_what :: ClsInstResult -> InstanceWhat cir_what = InstanceWhat what }) CtLoc ct_loc | TopLevInstance{ iw_dfun_id :: InstanceWhat -> EvVar iw_dfun_id = EvVar dfun, iw_warn :: InstanceWhat -> Maybe (WarningTxt GhcRn) iw_warn = Just WarningTxt GhcRn warn } <- InstanceWhat what = do let mod :: Module mod = HasDebugCallStack => Name -> Module Name -> Module nameModule (Name -> Module) -> Name -> Module forall a b. (a -> b) -> a -> b $ EvVar -> Name forall a. NamedThing a => a -> Name getName EvVar dfun this_mod <- TcS Module forall (m :: * -> *). HasModule m => m Module getModule when (this_mod /= mod) -- We don't emit warnings for usages inside of the same module -- to prevent it being triggered for instance child declarations $ ctLocWarnTcS ct_loc $ TcRnPragmaWarning { pragma_warning_info = PragmaWarningInstance dfun (ctl_origin ct_loc) , pragma_warning_msg = warn } warn_custom_warn_instance ClsInstResult _ CtLoc _ = () -> TcS () forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return () {- Note [Instance and Given overlap] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Example, from the OutsideIn(X) paper: instance P x => Q [x] instance (x ~ y) => R y [x] wob :: forall a b. (Q [b], R b a) => a -> Int g :: forall a. Q [a] => [a] -> Int g x = wob x From 'g' we get the implication constraint: forall a. Q [a] => (Q [beta], R beta [a]) If we react (Q [beta]) with its top-level axiom, we end up with a (P beta), which we have no way of discharging. On the other hand, if we react R beta [a] with the top-level we get (beta ~ a), which is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is now solvable by the given Q [a]. The partial solution is that: In matchClassInst (and thus in topReact), we return a matching instance only when there is no Given in the inerts which is unifiable to this particular dictionary. We treat any meta-tyvar as "unifiable" for this purpose, *including* untouchable ones. But not skolems like 'a' in the implication constraint above. The end effect is that, much as we do for overlapping instances, we delay choosing a class instance if there is a possibility of another instance OR a given to match our constraint later on. This fixes tickets #4981 and #5002. Other notes: * The check is done *first*, so that it also covers classes with built-in instance solving, such as - constraint tuples - natural numbers - Typeable * See also Note [What might equal later?] in GHC.Tc.Utils.Unify * The given-overlap problem is arguably not easy to appear in practice due to our aggressive prioritization of equality solving over other constraints, but it is possible. I've added a test case in typecheck/should-compile/GivenOverlapping.hs * Another "live" example is #10195; another is #10177. * We ignore the overlap problem if -XIncoherentInstances is in force: see #6002 for a worked-out example where this makes a difference. * Moreover notice that our goals here are different than the goals of the top-level overlapping checks. There we are interested in validating the following principle: If we inline a function f at a site where the same global instance environment is available as the instance environment at the definition site of f then we should get the same behaviour. But for the Given Overlap check our goal is just related to completeness of constraint solving. * The solution is only a partial one. Consider the above example with g :: forall a. Q [a] => [a] -> Int g x = let v = wob x in v and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most general type for 'v'. When generalising v's type we'll simplify its Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we will use the instance declaration after all. #11948 was a case in point. All of this is disgustingly delicate, so to discourage people from writing simplifiable class givens, we warn about signatures that contain them; see GHC.Tc.Validity Note [Simplifiable given constraints]. Note [Local instances and incoherence] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider f :: forall b c. (Eq b, forall a. Eq a => Eq (c a)) => c b -> Bool f x = x==x We get [W] Eq (c b), and we must use the local instance to solve it. BUT that wanted also unifies with the top-level Eq [a] instance, and Eq (Maybe a) etc. We want the local instance to "win", otherwise we can't solve the wanted at all. So we mark it as Incohherent. According to Note [Rules for instance lookup] in GHC.Core.InstEnv, that'll make it win even if there are other instances that unify. Moreover this is not a hack! The evidence for this local instance will be constructed by GHC at a call site... from the very instances that unify with it here. It is not like an incoherent user-written instance which might have utterly different behaviour. Consider f :: Eq a => blah. If we have [W] Eq a, we certainly get it from the Eq a context, without worrying that there are lots of top-level instances that unify with [W] Eq a! We'll use those instances to build evidence to pass to f. That's just the nullary case of what's happening here. -} matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult -- Look up the predicate in Given quantified constraints, -- which are effectively just local instance declarations. matchLocalInst :: Type -> CtLoc -> TcS ClsInstResult matchLocalInst Type body_pred CtLoc loc = do { -- In TcSShortCut mode we do not look at Givens; -- c.f. tryInertDicts mode <- TcS TcSMode getTcSMode ; case mode of { TcSMode TcSShortCut -> do { String -> SDoc -> TcS () traceTcS String "matchLocalInst:TcSShortCut" (Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type body_pred) ; ClsInstResult -> TcS ClsInstResult forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return ClsInstResult NoInstance } ; TcSMode _other -> do { -- Look in the inert set for a matching Given quantified constraint inerts@(IS { inert_cans = ics }) <- TcS InertSet getInertSet ; case match_local_inst inerts (inert_insts ics) of { ([], []) -> do { String -> SDoc -> TcS () traceTcS String "No local instance for" (Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type body_pred) ; ClsInstResult -> TcS ClsInstResult forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return ClsInstResult NoInstance } ; ([(CtEvidence, [DFunInstType])] matches, [(CtEvidence, [DFunInstType])] unifs) -> do { -- Find the best match -- See Note [Use only the best matching quantified constraint] matches <- ((CtEvidence, [DFunInstType]) -> TcS InstDFun) -> [(CtEvidence, [DFunInstType])] -> TcS [InstDFun] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b] mapM (CtEvidence, [DFunInstType]) -> TcS InstDFun mk_instDFun [(CtEvidence, [DFunInstType])] matches ; unifs <- mapM mk_instDFun unifs ; case dominatingMatch matches of { Just (EvVar dfun_id, [Type] tys, [Type] theta) | (InstDFun -> Bool) -> [InstDFun] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all (([Type] theta [Type] -> [Type] -> Bool `impliedBySCs`) ([Type] -> Bool) -> (InstDFun -> [Type]) -> InstDFun -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . InstDFun -> [Type] forall a b c. (a, b, c) -> c thdOf3) [InstDFun] unifs -> do { let result :: ClsInstResult result = OneInst { cir_new_theta :: [Type] cir_new_theta = [Type] theta , cir_mk_ev :: [EvExpr] -> EvTerm cir_mk_ev = EvVar -> [Type] -> [EvExpr] -> EvTerm evDFunApp EvVar dfun_id [Type] tys , cir_canonical :: CanonicalEvidence cir_canonical = CanonicalEvidence EvCanonical , cir_what :: InstanceWhat cir_what = InstanceWhat LocalInstance } ; String -> SDoc -> TcS () traceTcS String "Best local instance found:" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ String -> SDoc forall doc. IsLine doc => String -> doc text String "body_pred:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type body_pred , String -> SDoc forall doc. IsLine doc => String -> doc text String "result:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> ClsInstResult -> SDoc forall a. Outputable a => a -> SDoc ppr ClsInstResult result , String -> SDoc forall doc. IsLine doc => String -> doc text String "matches:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [InstDFun] -> SDoc forall a. Outputable a => a -> SDoc ppr [InstDFun] matches , String -> SDoc forall doc. IsLine doc => String -> doc text String "unifs:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [InstDFun] -> SDoc forall a. Outputable a => a -> SDoc ppr [InstDFun] unifs ] ; ClsInstResult -> TcS ClsInstResult forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return ClsInstResult result } ; Maybe InstDFun mb_best -> do { String -> SDoc -> TcS () traceTcS String "Multiple local instances; not committing to any" (SDoc -> TcS ()) -> SDoc -> TcS () forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ String -> SDoc forall doc. IsLine doc => String -> doc text String "body_pred:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type body_pred , String -> SDoc forall doc. IsLine doc => String -> doc text String "matches:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [InstDFun] -> SDoc forall a. Outputable a => a -> SDoc ppr [InstDFun] matches , String -> SDoc forall doc. IsLine doc => String -> doc text String "unifs:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [InstDFun] -> SDoc forall a. Outputable a => a -> SDoc ppr [InstDFun] unifs , String -> SDoc forall doc. IsLine doc => String -> doc text String "best_match:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Maybe InstDFun -> SDoc forall a. Outputable a => a -> SDoc ppr Maybe InstDFun mb_best ] ; ClsInstResult -> TcS ClsInstResult forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return ClsInstResult NotSure }}}}}}} where body_pred_tv_set :: TyCoVarSet body_pred_tv_set = Type -> TyCoVarSet tyCoVarsOfType Type body_pred mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun mk_instDFun (CtEvidence ev, [DFunInstType] tys) = let dfun_id :: EvVar dfun_id = CtEvidence -> EvVar ctEvEvId CtEvidence ev in do { (tys, theta) <- EvVar -> [DFunInstType] -> TcS ([Type], [Type]) instDFunType (CtEvidence -> EvVar ctEvEvId CtEvidence ev) [DFunInstType] tys ; return (dfun_id, tys, theta) } -- Compute matching and unifying local instances match_local_inst :: InertSet -> [QCInst] -> ( [(CtEvidence, [DFunInstType])] , [(CtEvidence, [DFunInstType])] ) match_local_inst :: InertSet -> [QCInst] -> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])]) match_local_inst InertSet _inerts [] = ([], []) match_local_inst InertSet inerts (qci :: QCInst qci@(QCI { qci_tvs :: QCInst -> [EvVar] qci_tvs = [EvVar] qtvs , qci_body :: QCInst -> Type qci_body = Type qbody , qci_ev :: QCInst -> CtEvidence qci_ev = CtEvidence qev }) : [QCInst] qcis) | CtEvidence -> Bool isWanted CtEvidence qev -- Skip Wanteds = InertSet -> [QCInst] -> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])]) match_local_inst InertSet inerts [QCInst] qcis | let in_scope :: InScopeSet in_scope = TyCoVarSet -> InScopeSet mkInScopeSet (TyCoVarSet qtv_set TyCoVarSet -> TyCoVarSet -> TyCoVarSet `unionVarSet` TyCoVarSet body_pred_tv_set) , Just TvSubstEnv tv_subst <- TyCoVarSet -> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv ruleMatchTyKiX TyCoVarSet qtv_set (InScopeSet -> RnEnv2 mkRnEnv2 InScopeSet in_scope) TvSubstEnv emptyTvSubstEnv Type qbody Type body_pred , let match :: (CtEvidence, [DFunInstType]) match = (CtEvidence qev, (EvVar -> DFunInstType) -> [EvVar] -> [DFunInstType] forall a b. (a -> b) -> [a] -> [b] map (TvSubstEnv -> EvVar -> DFunInstType forall a. VarEnv a -> EvVar -> Maybe a lookupVarEnv TvSubstEnv tv_subst) [EvVar] qtvs) = ((CtEvidence, [DFunInstType]) match(CtEvidence, [DFunInstType]) -> [(CtEvidence, [DFunInstType])] -> [(CtEvidence, [DFunInstType])] forall a. a -> [a] -> [a] :[(CtEvidence, [DFunInstType])] matches, [(CtEvidence, [DFunInstType])] unifs) | Bool otherwise = Bool -> SDoc -> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])]) -> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])]) forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr (TyCoVarSet -> TyCoVarSet -> Bool disjointVarSet TyCoVarSet qtv_set (Type -> TyCoVarSet tyCoVarsOfType Type body_pred)) (QCInst -> SDoc forall a. Outputable a => a -> SDoc ppr QCInst qci SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type body_pred) -- ASSERT: unification relies on the -- quantified variables being fresh ([(CtEvidence, [DFunInstType])] matches, Maybe (CtEvidence, [DFunInstType]) this_unif Maybe (CtEvidence, [DFunInstType]) -> [(CtEvidence, [DFunInstType])] -> [(CtEvidence, [DFunInstType])] forall {a}. Maybe a -> [a] -> [a] `combine` [(CtEvidence, [DFunInstType])] unifs) where qloc :: CtLoc qloc = CtEvidence -> CtLoc ctEvLoc CtEvidence qev qtv_set :: TyCoVarSet qtv_set = [EvVar] -> TyCoVarSet mkVarSet [EvVar] qtvs ([(CtEvidence, [DFunInstType])] matches, [(CtEvidence, [DFunInstType])] unifs) = InertSet -> [QCInst] -> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])]) match_local_inst InertSet inerts [QCInst] qcis this_unif :: Maybe (CtEvidence, [DFunInstType]) this_unif | Just Subst subst <- InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst mightEqualLater InertSet inerts Type qbody CtLoc qloc Type body_pred CtLoc loc = (CtEvidence, [DFunInstType]) -> Maybe (CtEvidence, [DFunInstType]) forall a. a -> Maybe a Just (CtEvidence qev, (EvVar -> DFunInstType) -> [EvVar] -> [DFunInstType] forall a b. (a -> b) -> [a] -> [b] map (Subst -> EvVar -> DFunInstType lookupTyVar Subst subst) [EvVar] qtvs) | Bool otherwise = Maybe (CtEvidence, [DFunInstType]) forall a. Maybe a Nothing combine :: Maybe a -> [a] -> [a] combine Maybe a Nothing [a] us = [a] us combine (Just a u) [a] us = a u a -> [a] -> [a] forall a. a -> [a] -> [a] : [a] us -- | Instance dictionary function and type. type InstDFun = (DFunId, [TcType], TcThetaType) -- | Try to find a local quantified instance that dominates all others, -- i.e. which has a weaker instance context than all the others. -- -- See Note [Use only the best matching quantified constraint]. dominatingMatch :: [InstDFun] -> Maybe InstDFun dominatingMatch :: [InstDFun] -> Maybe InstDFun dominatingMatch [InstDFun] matches = [InstDFun] -> Maybe InstDFun forall a. [a] -> Maybe a listToMaybe ([InstDFun] -> Maybe InstDFun) -> [InstDFun] -> Maybe InstDFun forall a b. (a -> b) -> a -> b $ ((InstDFun, [InstDFun]) -> Maybe InstDFun) -> [(InstDFun, [InstDFun])] -> [InstDFun] forall a b. (a -> Maybe b) -> [a] -> [b] mapMaybe ((InstDFun -> [InstDFun] -> Maybe InstDFun) -> (InstDFun, [InstDFun]) -> Maybe InstDFun forall a b c. (a -> b -> c) -> (a, b) -> c uncurry InstDFun -> [InstDFun] -> Maybe InstDFun go) ([InstDFun] -> [(InstDFun, [InstDFun])] forall a. [a] -> [(a, [a])] holes [InstDFun] matches) -- listToMaybe: arbitrarily pick any one context that is weaker than -- all others, e.g. so that we can handle [Eq a, Num a] vs [Num a, Eq a] -- (see test case T22223). where go :: InstDFun -> [InstDFun] -> Maybe InstDFun go :: InstDFun -> [InstDFun] -> Maybe InstDFun go InstDFun this [] = InstDFun -> Maybe InstDFun forall a. a -> Maybe a Just InstDFun this go this :: InstDFun this@(EvVar _,[Type] _,[Type] this_theta) ((EvVar _,[Type] _,[Type] other_theta):[InstDFun] others) | [Type] this_theta [Type] -> [Type] -> Bool `impliedBySCs` [Type] other_theta = InstDFun -> [InstDFun] -> Maybe InstDFun go InstDFun this [InstDFun] others | Bool otherwise = Maybe InstDFun forall a. Maybe a Nothing -- | Whether a collection of constraints is implied by another collection, -- according to a simple superclass check. -- -- See Note [When does a quantified instance dominate another?]. impliedBySCs :: TcThetaType -> TcThetaType -> Bool impliedBySCs :: [Type] -> [Type] -> Bool impliedBySCs [Type] c1 [Type] c2 = (Type -> Bool) -> [Type] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all Type -> Bool in_c2 [Type] c1 where in_c2 :: TcPredType -> Bool in_c2 :: Type -> Bool in_c2 Type pred = (Type -> Bool) -> [Type] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool any (Type pred HasDebugCallStack => Type -> Type -> Bool Type -> Type -> Bool `tcEqType`) [Type] c2_expanded c2_expanded :: [TcPredType] -- Includes all superclasses c2_expanded :: [Type] c2_expanded = [ Type q | Type p <- [Type] c2, Type q <- Type p Type -> [Type] -> [Type] forall a. a -> [a] -> [a] : Type -> [Type] transSuperClasses Type p ] {- Note [When does a quantified instance dominate another?] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When matching local quantified instances, it's useful to be able to pick the one with the weakest precondition, e.g. if one has both [G] d1: forall a b. ( Eq a, Num b, C a b ) => D a b [G] d2: forall a . C a Int => D a Int [W] {w}: D a Int Then it makes sense to use d2 to solve w, as doing so we end up with a strictly weaker proof obligation of `C a Int`, compared to `(Eq a, Num Int, C a Int)` were we to use d1. In theory, to compute whether one context implies another, we would need to recursively invoke the constraint solver. This is expensive, so we instead do a simple check using superclasses, implemented in impliedBySCs. Examples: - [Eq a] is implied by [Ord a] - [Ord a] is not implied by [Eq a], - any context is implied by itself, - the empty context is implied by any context. Note [Use only the best matching quantified constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider (#20582) the ambiguity check for (forall a. Ord (m a), forall a. Semigroup a => Eq (m a)) => m Int Because of eager expansion of given superclasses, we get [G] d1: forall a. Ord (m a) [G] d2: forall a. Eq (m a) [G] d3: forall a. Semigroup a => Eq (m a) [W] {w1}: forall a. Ord (m a) [W] {w2}: forall a. Semigroup a => Eq (m a) The first wanted is solved straightforwardly. But the second wanted matches *two* local instances: d2 and d3. Our general rule around multiple local instances is that we refuse to commit to any of them. However, that means that our type fails the ambiguity check. That's bad: the type is perfectly fine. (This actually came up in the wild, in the streamly library.) The solution is to prefer local instances which are easier to prove, meaning that they have a weaker precondition. In this case, the empty context of d2 is a weaker constraint than the "Semigroup a" context of d3, so we prefer using it when proving w2. This allows us to pass the ambiguity check here. Our criterion for solving a Wanted by matching local quantified instances is thus as follows: - There is a matching local quantified instance that dominates all others matches, in the sense of [When does a quantified instance dominate another?]. Any such match do, we pick it arbitrarily (the T22223 example below says why). - This local quantified instance also dominates all the unifiers, as we wouldn't want to commit to a single match when we might have multiple, genuinely different matches after further unification takes place. Some other examples: #15244: f :: (C g, D g) => .... class S g => C g where ... class S g => D g where ... class (forall a. Eq a => Eq (g a)) => S g where ... Here, in f's RHS, there are two identical quantified constraints available, one via the superclasses of C and one via the superclasses of D. Given that each implies the other, we pick one arbitrarily. #22216: class Eq a class Eq a => Ord a class (forall b. Eq b => Eq (f b)) => Eq1 f class (Eq1 f, forall b. Ord b => Ord (f b)) => Ord1 f Suppose we have [G] d1: Ord1 f [G] d2: Eq a [W] {w}: Eq (f a) Superclass expansion of d1 gives us: [G] d3 : Eq1 f [G] d4 : forall b. Ord b => Ord (f b) expanding d4 and d5 gives us, respectively: [G] d5 : forall b. Eq b => Eq (f b) [G] d6 : forall b. Ord b => Eq (f b) Now we have two matching local instances that we could use when solving the Wanted. However, it's obviously silly to use d6, given that d5 provides us with as much information, with a strictly weaker precondition. So we pick d5 to solve w. If we chose d6, we would get [W] Ord a, which in this case we can't solve. #22223: [G] forall a b. (Eq a, Ord b) => C a b [G] forall a b. (Ord b, Eq a) => C a b [W] C x y Here we should be free to pick either quantified constraint, as they are equivalent up to re-ordering of the constraints in the context. See also Note [Do not add duplicate quantified instances] in GHC.Tc.Solver.Monad. Test cases: typecheck/should_compile/T20582 quantified-constraints/T15244 quantified-constraints/T22216{a,b,c,d,e} quantified-constraints/T22223 Historical note: a previous solution was to instead pick the local instance with the least superclass depth (see Note [Replacement vs keeping]), but that doesn't work for the example from #22216. -} {- ********************************************************************* * * * Functional dependencies, instantiation of equations * * ************************************************************************ When we spot an equality arising from a functional dependency, we now use that equality (a "wanted") to rewrite the work-item constraint right away. This avoids two dangers Danger 1: If we send the original constraint on down the pipeline it may react with an instance declaration, and in delicate situations (when a Given overlaps with an instance) that may produce new insoluble goals: see #4952 Danger 2: If we don't rewrite the constraint, it may re-react with the same thing later, and produce the same equality again --> termination worries. To achieve this required some refactoring of GHC.Tc.Instance.FunDeps (nicer now!). Note [FunDep and implicit parameter reactions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Currently, our story of interacting two dictionaries (or a dictionary and top-level instances) for functional dependencies, and implicit parameters, is that we simply produce new Wanted equalities. So for example class D a b | a -> b where ... Inert: [G] d1 : D Int Bool WorkItem: [W] d2 : D Int alpha We generate the extra work item [W] cv : alpha ~ Bool where 'cv' is currently unused. However, this new item can perhaps be spontaneously solved to become given and react with d2, discharging it in favour of a new constraint d2' thus: [W] d2' : D Int Bool d2 := d2' |> D Int cv Now d2' can be discharged from d1 We could be more aggressive and try to *immediately* solve the dictionary using those extra equalities. If that were the case with the same inert set and work item we might discard d2 directly: [W] cv : alpha ~ Bool d2 := d1 |> D Int cv But in general it's a bit painful to figure out the necessary coercion, so we just take the first approach. Here is a better example. Consider: class C a b c | a -> b And: [G] d1 : C T Int Char [W] d2 : C T beta Int In this case, it's *not even possible* to solve the wanted immediately. So we should simply output the functional dependency and add this guy [but NOT its superclasses] back in the worklist. Even worse: [G] d1 : C T Int beta [W] d2: C T beta Int Then it is solvable, but its very hard to detect this on the spot. It's exactly the same with implicit parameters, except that the "aggressive" approach would be much easier to implement. Note [Fundeps with instances, and equality orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This Note describes a delicate interaction that constrains the orientation of equalities. This one is about fundeps, but the /exact/ same thing arises for type-family injectivity constraints: see Note [Improvement orientation]. doTopFunDepImprovement compares the constraint with all the instance declarations, to see if we can produce any equalities. E.g class C2 a b | a -> b instance C Int Bool Then the constraint (C Int ty) generates the equality [W] ty ~ Bool. There is a nasty corner in #19415 which led to the typechecker looping: class C s t b | s -> t instance ... => C (T kx x) (T ky y) Int T :: forall k. k -> Type work_item: dwrk :: C (T @ka (a::ka)) (T @kb0 (b0::kb0)) Char where kb0, b0 are unification vars ==> {doTopFunDepImprovement: compare work_item with instance, generate /fresh/ unification variables kfresh0, yfresh0, emit a new Wanted, and add dwrk to inert set} Suppose we emit this new Wanted from the fundep: [W] T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0) ==> {solve that equality kb0 := kfresh0, b0 := yfresh0} Now kick out dwrk, since it mentions kb0 But now we are back to the start! Loop! NB1: This example relies on an instance that does not satisfy the coverage condition (although it may satisfy the weak coverage condition), and hence whose fundeps generate fresh unification variables. Not satisfying the coverage condition is known to lead to termination trouble, but in this case it's plain silly. NB2: In this example, the third parameter to C ensures that the instance doesn't actually match the Wanted, so we can't use it to solve the Wanted We solve the problem by (#21703): carefully orienting the new Wanted so that all the freshly-generated unification variables are on the LHS. Thus we call unifyWanteds on T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0) and /NOT/ T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0) Now we'll unify kfresh0:=kb0, yfresh0:=b0, and all is well. The general idea is that we want to preferentially eliminate those freshly-generated unification variables, rather than unifying older variables, which causes kick-out etc. Keeping younger variables on the left also gives very minor improvement in the compiler performance by having less kick-outs and allocations (-0.1% on average). Indeed Historical Note [Eliminate younger unification variables] in GHC.Tc.Utils.Unify describes an earlier attempt to do so systematically, apparently now in abeyance. But this is is a delicate solution. We must take care to /preserve/ orientation during solving. Wrinkles: (W1) We start with [W] T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0) Decompose to [W] kfresh0 ~ kb0 [W] (yfresh0::kfresh0) ~ (b0::kb0) Preserve orientation when decomposing!! (W2) Suppose we happen to tackle the second Wanted from (W1) first. Then in canEqCanLHSHetero we emit a /kind/ equality, as well as a now-homogeneous type equality [W] kco : kfresh0 ~ kb0 [W] (yfresh0::kfresh0) ~ (b0::kb0) |> (sym kco) Preserve orientation in canEqCanLHSHetero!! (Failing to preserve orientation here was the immediate cause of #21703.) (W3) There is a potential interaction with the swapping done by GHC.Tc.Utils.Unify.swapOverTyVars. We think it's fine, but it's a slight worry. See especially Note [TyVar/TyVar orientation] in that module. The trouble is that "preserving orientation" is a rather global invariant, and sometimes we definitely do want to swap (e.g. Int ~ alpha), so we don't even have a precise statement of what the invariant is. The advantage of the preserve-orientation plan is that it is extremely cheap to implement, and apparently works beautifully. --- Alternative plan (1) --- Rather than have an ill-defined invariant, another possiblity is to elminate those fresh unification variables at birth, when generating the new fundep-inspired equalities. The key idea is to call `instFlexiX` in `emitFunDepWanteds` on only those type variables that are guaranteed to give us some progress. This means we have to locally (without calling emitWanteds) identify the type variables that do not give us any progress. In the above example, we _know_ that emitting the two wanteds `kco` and `co` is fruitless. Q: How do we identify such no-ops? 1. Generate a matching substitution from LHS to RHS ɸ = [kb0 :-> k0, b0 :-> y0] 2. Call `instFlexiX` on only those type variables that do not appear in the domain of ɸ ɸ' = instFlexiX ɸ (tvs - domain ɸ) 3. Apply ɸ' on LHS and then call emitWanteds unifyWanteds ... (subst ɸ' LHS) RHS Why will this work? The matching substitution ɸ will be a best effort substitution that gives us all the easy solutions. It can be generated with modified version of `Core/Unify.unify_tys` where we run it in a matching mode and never generate `SurelyApart` and always return a `MaybeApart Subst` instead. The same alternative plan would work for type-family injectivity constraints: see Note [Improvement orientation] in GHC.Tc.Solver.Equality. --- End of Alternative plan (1) --- --- Alternative plan (2) --- We could have a new flavour of TcTyVar (like `TauTv`, `TyVarTv` etc; see GHC.Tc.Utils.TcType.MetaInfo) for the fresh unification variables introduced by functional dependencies. Say `FunDepTv`. Then in GHC.Tc.Utils.Unify.swapOverTyVars we could arrange to keep a `FunDepTv` on the left if possible. Looks possible, but it's one more complication. --- End of Alternative plan (2) --- --- Historical note: Failed Alternative Plan (3) --- Previously we used a flag `cc_fundeps` in `CDictCan`. It would flip to False once we used a fun dep to hint the solver to break and to stop emitting more wanteds. This solution was not complete, and caused a failures while trying to solve for transitive functional dependencies (test case: T21703) -- End of Historical note: Failed Alternative Plan (3) -- Note [Do fundeps last] ~~~~~~~~~~~~~~~~~~~~~~ Consider T4254b: class FD a b | a -> b where { op :: a -> b } instance FD Int Bool foo :: forall a b. (a~Int,FD a b) => a -> Bool foo = op (DFL1) Try local fundeps first. From the ambiguity check on the type signature we get [G] FD Int b [W] FD Int beta Interacting these gives beta:=b; then we start again and solve without trying fundeps between the new [W] FD Int b and the top-level instance. If we did, we'd generate [W] b ~ Bool, which fails. (DFL2) Try solving from top-level instances before fundeps From the definition `foo = op` we get [G] FD Int b [W] FD Int Bool We solve this from the top level instance before even trying fundeps. If we did try fundeps, we'd generate [W] b ~ Bool, which fails. Note [Weird fundeps] ~~~~~~~~~~~~~~~~~~~~ Consider class Het a b | a -> b where het :: m (f c) -> a -> m b class GHet (a :: * -> *) (b :: * -> *) | a -> b instance GHet (K a) (K [a]) instance Het a b => GHet (K a) (K b) The two instances don't actually conflict on their fundeps, although it's pretty strange. So they are both accepted. Now try [W] GHet (K Int) (K Bool) This triggers fundeps from both instance decls; [W] K Bool ~ K [a] [W] K Bool ~ K beta And there's a risk of complaining about Bool ~ [a]. But in fact the Wanted matches the second instance, so we never get as far as the fundeps. #7875 is a case in point. -} doLocalFunDepImprovement :: DictCt -> SolverStage () -- Add wanted constraints from type-class functional dependencies. doLocalFunDepImprovement :: DictCt -> SolverStage () doLocalFunDepImprovement dict_ct :: DictCt dict_ct@(DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence work_ev, di_cls :: DictCt -> Class di_cls = Class cls }) = TcS (StopOrContinue ()) -> SolverStage () forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue ()) -> SolverStage ()) -> TcS (StopOrContinue ()) -> SolverStage () forall a b. (a -> b) -> a -> b $ do { inerts <- TcS InertCans getInertCans ; imp <- foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls) ; if imp then startAgainWith (CDictCan dict_ct) else continueWith () } where work_pred :: Type work_pred = CtEvidence -> Type ctEvPred CtEvidence work_ev work_loc :: CtLoc work_loc = CtEvidence -> CtLoc ctEvLoc CtEvidence work_ev add_fds :: Bool -> DictCt -> TcS Bool add_fds :: Bool -> DictCt -> TcS Bool add_fds Bool so_far (DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence inert_ev }) | CtEvidence -> Bool isGiven CtEvidence work_ev Bool -> Bool -> Bool && CtEvidence -> Bool isGiven CtEvidence inert_ev -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps] = Bool -> TcS Bool forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return Bool so_far | Bool otherwise = do { String -> SDoc -> TcS () traceTcS String "doLocalFunDepImprovement" ([SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence work_ev , CtLoc -> SDoc pprCtLoc CtLoc work_loc, Bool -> SDoc forall a. Outputable a => a -> SDoc ppr (CtLoc -> Bool isGivenLoc CtLoc work_loc) , CtLoc -> SDoc pprCtLoc CtLoc inert_loc, Bool -> SDoc forall a. Outputable a => a -> SDoc ppr (CtLoc -> Bool isGivenLoc CtLoc inert_loc) , CtLoc -> SDoc pprCtLoc CtLoc derived_loc, Bool -> SDoc forall a. Outputable a => a -> SDoc ppr (CtLoc -> Bool isGivenLoc CtLoc derived_loc) ]) ; unifs <- CtEvidence -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool emitFunDepWanteds CtEvidence work_ev ([FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool) -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool forall a b. (a -> b) -> a -> b $ (CtLoc, RewriterSet) -> Type -> Type -> [FunDepEqn (CtLoc, RewriterSet)] forall loc. loc -> Type -> Type -> [FunDepEqn loc] improveFromAnother (CtLoc derived_loc, RewriterSet inert_rewriters) Type inert_pred Type work_pred ; return (so_far || unifs) } where inert_pred :: Type inert_pred = CtEvidence -> Type ctEvPred CtEvidence inert_ev inert_loc :: CtLoc inert_loc = CtEvidence -> CtLoc ctEvLoc CtEvidence inert_ev inert_rewriters :: RewriterSet inert_rewriters = CtEvidence -> RewriterSet ctEvRewriters CtEvidence inert_ev derived_loc :: CtLoc derived_loc = CtLoc work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth` ctl_depth inert_loc , ctl_origin = FunDepOrigin1 work_pred (ctLocOrigin work_loc) (ctLocSpan work_loc) inert_pred (ctLocOrigin inert_loc) (ctLocSpan inert_loc) } doTopFunDepImprovement :: DictCt -> SolverStage () -- Try to functional-dependency improvement between the constraint -- and the top-level instance declarations -- See Note [Fundeps with instances, and equality orientation] -- See also Note [Weird fundeps] doTopFunDepImprovement :: DictCt -> SolverStage () doTopFunDepImprovement dict_ct :: DictCt dict_ct@(DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev, di_cls :: DictCt -> Class di_cls = Class cls, di_tys :: DictCt -> [Type] di_tys = [Type] xis }) | CtEvidence -> Bool isGiven CtEvidence ev -- No improvement for Givens = TcS (StopOrContinue ()) -> SolverStage () forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue ()) -> SolverStage ()) -> TcS (StopOrContinue ()) -> SolverStage () forall a b. (a -> b) -> a -> b $ () -> TcS (StopOrContinue ()) forall a. a -> TcS (StopOrContinue a) continueWith () | Bool otherwise = TcS (StopOrContinue ()) -> SolverStage () forall a. TcS (StopOrContinue a) -> SolverStage a Stage (TcS (StopOrContinue ()) -> SolverStage ()) -> TcS (StopOrContinue ()) -> SolverStage () forall a b. (a -> b) -> a -> b $ do { String -> SDoc -> TcS () traceTcS String "try_fundeps" (DictCt -> SDoc forall a. Outputable a => a -> SDoc ppr DictCt dict_ct) ; instEnvs <- TcS InstEnvs getInstEnvs ; let fundep_eqns = InstEnvs -> (ClsInst -> (CtLoc, RewriterSet)) -> Class -> [Type] -> [FunDepEqn (CtLoc, RewriterSet)] forall loc. InstEnvs -> (ClsInst -> loc) -> Class -> [Type] -> [FunDepEqn loc] improveFromInstEnv InstEnvs instEnvs ClsInst -> (CtLoc, RewriterSet) mk_ct_loc Class cls [Type] xis ; imp <- emitFunDepWanteds ev fundep_eqns ; if imp then startAgainWith (CDictCan dict_ct) else continueWith () } where dict_pred :: Type dict_pred = Class -> [Type] -> Type mkClassPred Class cls [Type] xis dict_loc :: CtLoc dict_loc = CtEvidence -> CtLoc ctEvLoc CtEvidence ev dict_origin :: CtOrigin dict_origin = CtLoc -> CtOrigin ctLocOrigin CtLoc dict_loc mk_ct_loc :: ClsInst -- The instance decl -> (CtLoc, RewriterSet) mk_ct_loc :: ClsInst -> (CtLoc, RewriterSet) mk_ct_loc ClsInst ispec = ( CtLoc dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin inst_pred inst_loc } , RewriterSet emptyRewriterSet ) where inst_pred :: Type inst_pred = Class -> [Type] -> Type mkClassPred Class cls (ClsInst -> [Type] is_tys ClsInst ispec) inst_loc :: SrcSpan inst_loc = EvVar -> SrcSpan forall a. NamedThing a => a -> SrcSpan getSrcSpan (ClsInst -> EvVar is_dfun ClsInst ispec) {- ********************************************************************* * * * Superclasses * * ********************************************************************* -} {- Note [The superclass story] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We need to add superclass constraints for two reasons: * For givens [G], they give us a route to proof. E.g. f :: Ord a => a -> Bool f x = x == x We get a Wanted (Eq a), which can only be solved from the superclass of the Given (Ord a). * For wanteds [W], they may give useful functional dependencies. E.g. class C a b | a -> b where ... class C a b => D a b where ... Now a [W] constraint (D Int beta) has (C Int beta) as a superclass and that might tell us about beta, via C's fundeps. We can get this by generating a [W] (C Int beta) constraint. We won't use the evidence, but it may lead to unification. See Note [Why adding superclasses can help]. For these reasons we want to generate superclass constraints for both Givens and Wanteds. But: * (Minor) they are often not needed, so generating them aggressively is a waste of time. * (Major) if we want recursive superclasses, there would be an infinite number of them. Here is a real-life example (#10318); class (Frac (Frac a) ~ Frac a, Fractional (Frac a), IntegralDomain (Frac a)) => IntegralDomain a where type Frac a :: * Notice that IntegralDomain has an associated type Frac, and one of IntegralDomain's superclasses is another IntegralDomain constraint. So here's the plan: 1. Eagerly generate superclasses for given (but not wanted) constraints; see Note [Eagerly expand given superclasses]. This is done using mkStrictSuperClasses in canDictCt, when we take a non-canonical Given constraint and cannonicalise it. However stop if you encounter the same class twice. That is, mkStrictSuperClasses expands eagerly, but has a conservative termination condition: see Note [Expanding superclasses] in GHC.Tc.Utils.TcType. 2. Solve the wanteds as usual, but do no further expansion of superclasses for canonical CDictCans in solveSimpleGivens or solveSimpleWanteds; Note [Danger of adding superclasses during solving] However, /do/ continue to eagerly expand superclasses for new /given/ /non-canonical/ constraints (canDictCt does this). As #12175 showed, a type-family application can expand to a class constraint, and we want to see its superclasses for just the same reason as Note [Eagerly expand given superclasses]. 3. If we have any remaining unsolved wanteds (see Note [When superclasses help] in GHC.Tc.Types.Constraint) try harder: take both the Givens and Wanteds, and expand superclasses again. See the calls to expandSuperClasses in GHC.Tc.Solver.simpl_loop and solveWanteds. This may succeed in generating (a finite number of) extra Givens, and extra Wanteds. Both may help the proof. 3a An important wrinkle: only expand Givens from the current level. Two reasons: - We only want to expand it once, and that is best done at the level it is bound, rather than repeatedly at the leaves of the implication tree - We may be inside a type where we can't create term-level evidence anyway, so we can't superclass-expand, say, (a ~ b) to get (a ~# b). This happened in #15290. 4. Go round to (2) again. This loop (2,3,4) is implemented in GHC.Tc.Solver.simpl_loop. The cc_pend_sc field in a CDictCan records whether the superclasses of this constraint have been expanded. Specifically, in Step 3 we only expand superclasses for constraints with cc_pend_sc > 0 (i.e. isPendingScDict holds). See Note [Expanding Recursive Superclasses and ExpansionFuel] Why do we do this? Two reasons: * To avoid repeated work, by repeatedly expanding the superclasses of same constraint, * To terminate the above loop, at least in the -XNoUndecidableSuperClasses case. If there are recursive superclasses we could, in principle, expand forever, always encountering new constraints. When we take a CNonCanonical or CIrredCan, but end up classifying it as a CDictCan, we set the cc_pend_sc flag to False. Note [Superclass loops] ~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have class C a => D a class D a => C a Then, when we expand superclasses, we'll get back to the self-same predicate, so we have reached a fixpoint in expansion and there is no point in fruitlessly expanding further. This case just falls out from our strategy. Consider f :: C a => a -> Bool f x = x==x Then canDictCt gets the [G] d1: C a constraint, and eager emits superclasses G] d2: D a, [G] d3: C a (psc). (The "psc" means it has its cc_pend_sc has pending expansion fuel.) When processing d3 we find a match with d1 in the inert set, and we always keep the inert item (d1) if possible: see Note [Replacement vs keeping] in GHC.Tc.Solver.InertSet. So d3 dies a quick, happy death. Note [Eagerly expand given superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In step (1) of Note [The superclass story], why do we eagerly expand Given superclasses by one layer? (By "one layer" we mean expand transitively until you meet the same class again -- the conservative criterion embodied in expandSuperClasses. So a "layer" might be a whole stack of superclasses.) We do this eagerly for Givens mainly because of some very obscure cases like this: instance Bad a => Eq (T a) f :: (Ord (T a)) => blah f x = ....needs Eq (T a), Ord (T a).... Here if we can't satisfy (Eq (T a)) from the givens we'll use the instance declaration; but then we are stuck with (Bad a). Sigh. This is really a case of non-confluent proofs, but to stop our users complaining we expand one layer in advance. See Note [Instance and Given overlap]. We also want to do this if we have f :: F (T a) => blah where type instance F (T a) = Ord (T a) So we may need to do a little work on the givens to expose the class that has the superclasses. That's why the superclass expansion for Givens happens in canDictCt. This same scenario happens with quantified constraints, whose superclasses are also eagerly expanded. Test case: typecheck/should_compile/T16502b These are handled in canForAllNC, analogously to canDictCt. Note [Why adding superclasses can help] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Examples of how adding superclasses can help: --- Example 1 class C a b | a -> b Suppose we want to solve [G] C a b [W] C a beta Then adding [W] beta~b will let us solve it. -- Example 2 (similar but using a type-equality superclass) class (F a ~ b) => C a b And try to sllve: [G] C a b [W] C a beta Follow the superclass rules to add [G] F a ~ b [W] F a ~ beta Now we get [W] beta ~ b, and can solve that. -- Example (tcfail138) class L a b | a -> b class (G a, L a b) => C a b instance C a b' => G (Maybe a) instance C a b => C (Maybe a) a instance L (Maybe a) a When solving the superclasses of the (C (Maybe a) a) instance, we get [G] C a b, and hence by superclasses, [G] G a, [G] L a b [W] G (Maybe a) Use the instance decl to get [W] C a beta Generate its superclass [W] L a beta. Now using fundeps, combine with [G] L a b to get [W] beta ~ b which is what we want. Note [Danger of adding superclasses during solving] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Here's a serious, but now out-dated example, from #4497: class Num (RealOf t) => Normed t type family RealOf x Assume the generated wanted constraint is: [W] RealOf e ~ e [W] Normed e If we were to be adding the superclasses during simplification we'd get: [W] RealOf e ~ e [W] Normed e [W] RealOf e ~ fuv [W] Num fuv ==> e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv While looks exactly like our original constraint. If we add the superclass of (Normed fuv) again we'd loop. By adding superclasses definitely only once, during canonicalisation, this situation can't happen. Note [Nested quantified constraint superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider (typecheck/should_compile/T17202) class C1 a class (forall c. C1 c) => C2 a class (forall b. (b ~ F a) => C2 a) => C3 a Elsewhere in the code, we get a [G] g1 :: C3 a. We expand its superclass to get [G] g2 :: (forall b. (b ~ F a) => C2 a). This constraint has a superclass, as well. But we now must be careful: we cannot just add (forall c. C1 c) as a Given, because we need to remember g2's context. That new constraint is Given only when forall b. (b ~ F a) is true. It's tempting to make the new Given be (forall b. (b ~ F a) => forall c. C1 c), but that's problematic, because it's nested, and ForAllPred is not capable of representing a nested quantified constraint. (We could change ForAllPred to allow this, but the solution in this Note is much more local and simpler.) So, we swizzle it around to get (forall b c. (b ~ F a) => C1 c). More generally, if we are expanding the superclasses of g0 :: forall tvs. theta => cls tys and find a superclass constraint (itself perhaps a quantified constraint) forall sc_tvs. sc_theta => sc_inner_pred we must have a selector sel_id :: forall cls_tvs. cls cls_tvs => forall sc_tvs. sc_theta => sc_inner_pred and thus build g_sc :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred g_sc = /\ tvs. /\ sc_tvs. \ theta_ids. \ sc_theta_ids. sel_id tys (g0 tvs theta_ids) sc_tvs sc_theta_ids Actually, we cheat a bit by eta-reducing: note that sc_theta_ids are both the last bound variables and the last arguments. This avoids the need to produce the sc_theta_ids at all. So our final construction is g_sc = /\ tvs. /\ sc_tvs. \ theta_ids. sel_id tys (g0 tvs theta_ids) sc_tvs (NQCS1) Common case. If theta_ids[] we get just g_sc = /\ tvs. /\sc_tvs. sel_id tys (g0 tvs) sc_tvs and can eta-reduce even more to g_sc = /\ tvs. sel_id tys (g0 tvs) and if tvs=[] we get the straight superclass selection g_sc = sel_id tys g0 -} makeSuperClasses :: [Ct] -> TcS [Ct] -- Returns strict superclasses, transitively, see Note [The superclass story] -- The loop-breaking here follows Note [Expanding superclasses] in GHC.Tc.Utils.TcType -- Specifically, for an incoming (C t) constraint, we return all of (C t)'s -- superclasses, up to /and including/ the first repetition of C -- -- Example: class D a => C a -- class C [a] => D a -- makeSuperClasses (C x) will return (D x, C [x]) -- -- NB: the incoming constraint's superclass will consume a unit of fuel -- Preconditions on `cts`: 1. They are either `CDictCan` or `CQuantCan` -- 2. Their fuel (stored in cc_pend_sc or qci_pend_sc) is > 0 makeSuperClasses :: [Ct] -> TcS [Ct] makeSuperClasses [Ct] cts = (Ct -> TcS [Ct]) -> [Ct] -> TcS [Ct] forall (m :: * -> *) (f :: * -> *) a b. (Monad m, Traversable f) => (a -> m [b]) -> f a -> m [b] concatMapM Ct -> TcS [Ct] go [Ct] cts where go :: Ct -> TcS [Ct] go (CDictCan (DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev, di_cls :: DictCt -> Class di_cls = Class cls, di_tys :: DictCt -> [Type] di_tys = [Type] tys, di_pend_sc :: DictCt -> ScDepth di_pend_sc = ScDepth fuel })) = ScDepth -> TcS [Ct] -> TcS [Ct] forall a. ScDepth -> a -> a assertFuelPreconditionStrict ScDepth fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct] forall a b. (a -> b) -> a -> b $ -- fuel needs to be more than 0 always ScDepth -> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct] mkStrictSuperClasses ScDepth fuel CtEvidence ev [] [] Class cls [Type] tys go (CQuantCan (QCI { qci_body :: QCInst -> Type qci_body = Type body_pred, qci_ev :: QCInst -> CtEvidence qci_ev = CtEvidence ev, qci_pend_sc :: QCInst -> ScDepth qci_pend_sc = ScDepth fuel })) = Bool -> SDoc -> TcS [Ct] -> TcS [Ct] forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr (Type -> Bool isClassPred Type body_pred) (Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type body_pred) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct] forall a b. (a -> b) -> a -> b $ -- The cts should all have class pred heads ScDepth -> TcS [Ct] -> TcS [Ct] forall a. ScDepth -> a -> a assertFuelPreconditionStrict ScDepth fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct] forall a b. (a -> b) -> a -> b $ -- fuel needs to be more than 0, always ScDepth -> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct] mkStrictSuperClasses ScDepth fuel CtEvidence ev [EvVar] tvs [Type] theta Class cls [Type] tys where ([EvVar] tvs, [Type] theta, Class cls, [Type] tys) = Type -> ([EvVar], [Type], Class, [Type]) tcSplitDFunTy (CtEvidence -> Type ctEvPred CtEvidence ev) go Ct ct = String -> SDoc -> TcS [Ct] forall a. HasCallStack => String -> SDoc -> a pprPanic String "makeSuperClasses" (Ct -> SDoc forall a. Outputable a => a -> SDoc ppr Ct ct) mkStrictSuperClasses :: ExpansionFuel -> CtEvidence -> [TyVar] -> ThetaType -- These two args are non-empty only when taking -- superclasses of a /quantified/ constraint -> Class -> [Type] -> TcS [Ct] -- Return constraints for the strict superclasses of -- ev :: forall as. theta => cls tys -- Precondition: fuel > 0 -- Postcondition: fuel for recursive superclass ct is one unit less than cls fuel mkStrictSuperClasses :: ScDepth -> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct] mkStrictSuperClasses ScDepth fuel CtEvidence ev [EvVar] tvs [Type] theta Class cls [Type] tys = ScDepth -> NameSet -> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct] mk_strict_superclasses (ScDepth -> ScDepth consumeFuel ScDepth fuel) (Name -> NameSet unitNameSet (Class -> Name className Class cls)) CtEvidence ev [EvVar] tvs [Type] theta Class cls [Type] tys mk_strict_superclasses :: ExpansionFuel -> NameSet -> CtEvidence -> [TyVar] -> ThetaType -> Class -> [Type] -> TcS [Ct] -- Always return the immediate superclasses of (cls tys); -- and expand their superclasses, provided none of them are in rec_clss -- nor are repeated -- The caller of this function is supposed to perform fuel book keeping -- Precondition: fuel >= 0 mk_strict_superclasses :: ScDepth -> NameSet -> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct] mk_strict_superclasses ScDepth _ NameSet _ CtEvidence _ [EvVar] _ [Type] _ Class cls [Type] _ | Class -> Bool isEqualityClass Class cls -- See (EQC1) in Note [Solving equality classes] = [Ct] -> TcS [Ct] forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return [] mk_strict_superclasses ScDepth fuel NameSet rec_clss ev :: CtEvidence ev@(CtGiven (GivenCt { ctev_evar :: GivenCtEvidence -> EvVar ctev_evar = EvVar evar })) [EvVar] tvs [Type] theta Class cls [Type] tys = -- Given case do { String -> SDoc -> TcS () traceTcS String "mk_strict" (CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence ev SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ CtOrigin -> SDoc forall a. Outputable a => a -> SDoc ppr (CtLoc -> CtOrigin ctLocOrigin CtLoc loc)) ; (EvVar -> TcS [Ct]) -> [EvVar] -> TcS [Ct] forall (m :: * -> *) (f :: * -> *) a b. (Monad m, Traversable f) => (a -> m [b]) -> f a -> m [b] concatMapM EvVar -> TcS [Ct] do_one_given (Class -> [EvVar] classSCSelIds Class cls) } where loc :: CtLoc loc = CtEvidence -> CtLoc ctEvLoc CtEvidence ev dict_ids :: [EvVar] dict_ids = [Type] -> [EvVar] mkTemplateLocals [Type] theta this_size :: PatersonSize this_size = Class -> [Type] -> PatersonSize pSizeClassPred Class cls [Type] tys do_one_given :: EvVar -> TcS [Ct] do_one_given EvVar sel_id | HasDebugCallStack => Type -> Bool Type -> Bool isUnliftedType Type sc_pred -- NB: class superclasses are never representation-polymorphic, -- so isUnliftedType is OK here. , Bool -> Bool not ([EvVar] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [EvVar] tvs Bool -> Bool -> Bool && [Type] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Type] theta) = -- See Note [Equality superclasses in quantified constraints] [Ct] -> TcS [Ct] forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return [] | Bool otherwise = do { given_ev <- CtLoc -> (Type, EvTerm) -> TcS GivenCtEvidence newGivenEvVar CtLoc sc_loc ((Type, EvTerm) -> TcS GivenCtEvidence) -> (Type, EvTerm) -> TcS GivenCtEvidence forall a b. (a -> b) -> a -> b $ EvVar -> Type -> (Type, EvTerm) mk_given_desc EvVar sel_id Type sc_pred ; assertFuelPrecondition fuel $ mk_superclasses fuel rec_clss (CtGiven given_ev) tvs theta sc_pred } where sc_pred :: Type sc_pred = EvVar -> [Type] -> Type classMethodInstTy EvVar sel_id [Type] tys -- See Note [Nested quantified constraint superclasses] mk_given_desc :: Id -> PredType -> (PredType, EvTerm) mk_given_desc :: EvVar -> Type -> (Type, EvTerm) mk_given_desc EvVar sel_id Type sc_pred = (Type swizzled_pred, EvExpr -> EvTerm EvExpr EvExpr swizzled_evterm) where ([EvVar] sc_tvs, Type sc_rho) = Type -> ([EvVar], Type) splitForAllTyCoVars Type sc_pred ([Scaled Type] sc_theta, Type sc_inner_pred) = Type -> ([Scaled Type], Type) splitFunTys Type sc_rho all_tvs :: [EvVar] all_tvs = [EvVar] tvs [EvVar] -> [EvVar] -> [EvVar] forall a. [a] -> [a] -> [a] `chkAppend` [EvVar] sc_tvs all_theta :: [Type] all_theta = [Type] theta [Type] -> [Type] -> [Type] forall a. [a] -> [a] -> [a] `chkAppend` ((Scaled Type -> Type) -> [Scaled Type] -> [Type] forall a b. (a -> b) -> [a] -> [b] map Scaled Type -> Type forall a. Scaled a -> a scaledThing [Scaled Type] sc_theta) swizzled_pred :: Type swizzled_pred = [EvVar] -> [Type] -> Type -> Type HasDebugCallStack => [EvVar] -> [Type] -> Type -> Type mkInfSigmaTy [EvVar] all_tvs [Type] all_theta Type sc_inner_pred -- evar :: forall tvs. theta => cls tys -- sel_id :: forall cls_tvs. cls cls_tvs -- => forall sc_tvs. sc_theta => sc_inner_pred -- swizzled_evterm :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred swizzled_evterm :: EvExpr swizzled_evterm | [EvVar] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [EvVar] tvs, [Type] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Type] theta -- See wrinkle (NQCS1) = EvVar -> EvExpr forall b. EvVar -> Expr b Var EvVar sel_id EvExpr -> [Type] -> EvExpr forall b. Expr b -> [Type] -> Expr b `mkTyApps` [Type] tys EvExpr -> EvExpr -> EvExpr forall b. Expr b -> Expr b -> Expr b `App` EvVar -> EvExpr evId EvVar evar | Bool otherwise = [EvVar] -> EvExpr -> EvExpr forall b. [b] -> Expr b -> Expr b mkLams [EvVar] all_tvs (EvExpr -> EvExpr) -> EvExpr -> EvExpr forall a b. (a -> b) -> a -> b $ [EvVar] -> EvExpr -> EvExpr forall b. [b] -> Expr b -> Expr b mkLams [EvVar] dict_ids (EvExpr -> EvExpr) -> EvExpr -> EvExpr forall a b. (a -> b) -> a -> b $ EvVar -> EvExpr forall b. EvVar -> Expr b Var EvVar sel_id EvExpr -> [Type] -> EvExpr forall b. Expr b -> [Type] -> Expr b `mkTyApps` [Type] tys EvExpr -> EvExpr -> EvExpr forall b. Expr b -> Expr b -> Expr b `App` (EvVar -> EvExpr evId EvVar evar EvExpr -> [EvVar] -> EvExpr forall b. Expr b -> [EvVar] -> Expr b `mkVarApps` ([EvVar] tvs [EvVar] -> [EvVar] -> [EvVar] forall a. [a] -> [a] -> [a] ++ [EvVar] dict_ids)) EvExpr -> [EvVar] -> EvExpr forall b. Expr b -> [EvVar] -> Expr b `mkVarApps` [EvVar] sc_tvs sc_loc :: CtLoc sc_loc | Class -> Bool isCTupleClass Class cls = CtLoc loc | Bool otherwise = CtLoc loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) } -- isCTupleClass: we don't want tuples to mess up the size calculations -- of Note [Solving superclass constraints]. For tuple predicates, this -- matters, because their size can be large, and we don't want to add a -- big class to the size of the dictionaries in the chain. When we get -- down to a base predicate, we'll include its size. See #10335. -- See Note [Solving tuple constraints] -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance -- for explanation of GivenSCOrigin and Note [Replacement vs keeping] in -- GHC.Tc.Solver.InertSet for why we need depths mk_sc_origin :: CtOrigin -> CtOrigin mk_sc_origin :: CtOrigin -> CtOrigin mk_sc_origin (GivenSCOrigin SkolemInfoAnon skol_info ScDepth sc_depth Bool already_blocked) = SkolemInfoAnon -> ScDepth -> Bool -> CtOrigin GivenSCOrigin SkolemInfoAnon skol_info (ScDepth sc_depth ScDepth -> ScDepth -> ScDepth forall a. Num a => a -> a -> a + ScDepth 1) (Bool already_blocked Bool -> Bool -> Bool || SkolemInfoAnon -> Bool newly_blocked SkolemInfoAnon skol_info) mk_sc_origin (GivenOrigin SkolemInfoAnon skol_info) = -- These cases do not already have a superclass constraint: depth starts at 1 SkolemInfoAnon -> ScDepth -> Bool -> CtOrigin GivenSCOrigin SkolemInfoAnon skol_info ScDepth 1 (SkolemInfoAnon -> Bool newly_blocked SkolemInfoAnon skol_info) mk_sc_origin CtOrigin other_orig = String -> SDoc -> CtOrigin forall a. HasCallStack => String -> SDoc -> a pprPanic String "Given constraint without given origin" (SDoc -> CtOrigin) -> SDoc -> CtOrigin forall a b. (a -> b) -> a -> b $ EvVar -> SDoc forall a. Outputable a => a -> SDoc ppr EvVar evar SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ CtOrigin -> SDoc forall a. Outputable a => a -> SDoc ppr CtOrigin other_orig newly_blocked :: SkolemInfoAnon -> Bool newly_blocked (InstSkol ClsInstOrQC _ PatersonSize head_size) = Maybe PatersonCondFailure -> Bool forall a. Maybe a -> Bool isJust (PatersonSize this_size PatersonSize -> PatersonSize -> Maybe PatersonCondFailure `ltPatersonSize` PatersonSize head_size) newly_blocked SkolemInfoAnon _ = Bool False -- Wanted case mk_strict_superclasses ScDepth fuel NameSet rec_clss (CtWanted (WantedCt { ctev_pred :: WantedCtEvidence -> Type ctev_pred = Type pty, ctev_loc :: WantedCtEvidence -> CtLoc ctev_loc = CtLoc loc0, ctev_rewriters :: WantedCtEvidence -> RewriterSet ctev_rewriters = RewriterSet rws })) [EvVar] tvs [Type] theta Class cls [Type] tys | (Type -> Bool) -> [Type] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all Type -> Bool noFreeVarsOfType [Type] tys = [Ct] -> TcS [Ct] forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return [] -- Wanteds with no variables yield no superclass constraints. -- See Note [Improvement from Ground Wanteds] | Bool otherwise -- Wanted case, just add Wanted superclasses -- that can lead to improvement. = Bool -> SDoc -> TcS [Ct] -> TcS [Ct] forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr ([EvVar] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [EvVar] tvs Bool -> Bool -> Bool && [Type] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Type] theta) ([EvVar] -> SDoc forall a. Outputable a => a -> SDoc ppr [EvVar] tvs SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] theta) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct] forall a b. (a -> b) -> a -> b $ (Type -> TcS [Ct]) -> [Type] -> TcS [Ct] forall (m :: * -> *) (f :: * -> *) a b. (Monad m, Traversable f) => (a -> m [b]) -> f a -> m [b] concatMapM Type -> TcS [Ct] do_one (Class -> [Type] -> [Type] immSuperClasses Class cls [Type] tys) where loc :: CtLoc loc = CtLoc loc0 CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc `updateCtLocOrigin` Type -> CtOrigin -> CtOrigin WantedSuperclassOrigin Type pty do_one :: Type -> TcS [Ct] do_one Type sc_pred = do { String -> SDoc -> TcS () traceTcS String "mk_strict_superclasses Wanted" (Type -> SDoc forall a. Outputable a => a -> SDoc ppr (Class -> [Type] -> Type mkClassPred Class cls [Type] tys) SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type sc_pred) ; sc_ev <- CtLoc -> RewriterSet -> Type -> TcS WantedCtEvidence newWantedNC CtLoc loc RewriterSet rws Type sc_pred ; mk_superclasses fuel rec_clss (CtWanted sc_ev) [] [] sc_pred } {- Note [Improvement from Ground Wanteds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose class C b a => D a b and consider [W] D Int Bool Is there any point in emitting [W] C Bool Int? No! The only point of emitting superclass constraints for W constraints is to get improvement, extra unifications that result from functional dependencies. See Note [Why adding superclasses can help] above. But no variables means no improvement; case closed. -} mk_superclasses :: ExpansionFuel -> NameSet -> CtEvidence -> [TyVar] -> ThetaType -> PredType -> TcS [Ct] -- Return this constraint, plus its superclasses, if any -- Precondition: fuel >= 0 mk_superclasses :: ScDepth -> NameSet -> CtEvidence -> [EvVar] -> [Type] -> Type -> TcS [Ct] mk_superclasses ScDepth fuel NameSet rec_clss CtEvidence ev [EvVar] tvs [Type] theta Type pred | ClassPred Class cls [Type] tys <- HasDebugCallStack => Type -> Pred Type -> Pred classifyPredType Type pred = ScDepth -> TcS [Ct] -> TcS [Ct] forall a. ScDepth -> a -> a assertFuelPrecondition ScDepth fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct] forall a b. (a -> b) -> a -> b $ ScDepth -> NameSet -> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct] mk_superclasses_of ScDepth fuel NameSet rec_clss CtEvidence ev [EvVar] tvs [Type] theta Class cls [Type] tys | Bool otherwise -- Superclass is not a class predicate = [Ct] -> TcS [Ct] forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return [CtEvidence -> Ct mkNonCanonical CtEvidence ev] mk_superclasses_of :: ExpansionFuel -> NameSet -> CtEvidence -> [TyVar] -> ThetaType -> Class -> [Type] -> TcS [Ct] -- Always return this class constraint, -- and expand its superclasses -- Precondition: fuel >= 0 mk_superclasses_of :: ScDepth -> NameSet -> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct] mk_superclasses_of ScDepth fuel NameSet rec_clss CtEvidence ev [EvVar] tvs [Type] theta Class cls [Type] tys | Bool loop_found = do { String -> SDoc -> TcS () traceTcS String "mk_superclasses_of: loop" (Class -> SDoc forall a. Outputable a => a -> SDoc ppr Class cls SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys) ; ScDepth -> TcS [Ct] -> TcS [Ct] forall a. ScDepth -> a -> a assertFuelPrecondition ScDepth fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct] forall a b. (a -> b) -> a -> b $ [Ct] -> TcS [Ct] forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return [ScDepth -> Ct mk_this_ct ScDepth fuel] } -- cc_pend_sc of returning ct = fuel | Bool otherwise = do { String -> SDoc -> TcS () traceTcS String "mk_superclasses_of" ([SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ Class -> SDoc forall a. Outputable a => a -> SDoc ppr Class cls SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys , Bool -> SDoc forall a. Outputable a => a -> SDoc ppr (Class -> Bool isCTupleClass Class cls) , NameSet -> SDoc forall a. Outputable a => a -> SDoc ppr NameSet rec_clss ]) ; sc_cts <- ScDepth -> TcS [Ct] -> TcS [Ct] forall a. ScDepth -> a -> a assertFuelPrecondition ScDepth fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct] forall a b. (a -> b) -> a -> b $ ScDepth -> NameSet -> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct] mk_strict_superclasses ScDepth fuel NameSet rec_clss' CtEvidence ev [EvVar] tvs [Type] theta Class cls [Type] tys ; return (mk_this_ct doNotExpand : sc_cts) } -- doNotExpand: we have expanded this cls's superclasses, so -- exhaust the associated constraint's fuel, -- to avoid duplicate work where cls_nm :: Name cls_nm = Class -> Name className Class cls loop_found :: Bool loop_found = Bool -> Bool not (Class -> Bool isCTupleClass Class cls) Bool -> Bool -> Bool && Name cls_nm Name -> NameSet -> Bool `elemNameSet` NameSet rec_clss -- Tuples never contribute to recursion, and can be nested rec_clss' :: NameSet rec_clss' = NameSet rec_clss NameSet -> Name -> NameSet `extendNameSet` Name cls_nm mk_this_ct :: ExpansionFuel -> Ct -- We can't use CNonCanonical here because we need to tradk the fuel mk_this_ct :: ScDepth -> Ct mk_this_ct ScDepth fuel | [EvVar] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [EvVar] tvs, [Type] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Type] theta = DictCt -> Ct CDictCan (DictCt { di_ev :: CtEvidence di_ev = CtEvidence ev, di_cls :: Class di_cls = Class cls , di_tys :: [Type] di_tys = [Type] tys, di_pend_sc :: ScDepth di_pend_sc = ScDepth fuel }) -- NB: If there is a loop, we cut off, so we have not -- added the superclasses, hence cc_pend_sc = fuel | Bool otherwise = QCInst -> Ct CQuantCan (QCI { qci_tvs :: [EvVar] qci_tvs = [EvVar] tvs, qci_theta :: [Type] qci_theta = [Type] theta , qci_body :: Type qci_body = Class -> [Type] -> Type mkClassPred Class cls [Type] tys , qci_ev :: CtEvidence qci_ev = CtEvidence ev, qci_pend_sc :: ScDepth qci_pend_sc = ScDepth fuel }) {- Note [Equality superclasses in quantified constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider (#15359, #15593, #15625) f :: (forall a. theta => a ~ b) => stuff It's a bit odd to have a local, quantified constraint for `(a~b)`, but some people want such a thing (see the tickets). And for Coercible it is definitely useful f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q))) => stuff Moreover it's not hard to arrange; we just need to look up /equality/ constraints in the quantified-constraint environment, which we do in GHC.Tc.Solver.Equality.tryQCsEqCt. There is a wrinkle though, in the case where 'theta' is empty, so we have f :: (forall a. a~b) => stuff Now, potentially, the superclass machinery kicks in, in makeSuperClasses, giving us a a second quantified constraint (forall a. a ~# b) BUT this is an unboxed value! And nothing has prepared us for dictionary "functions" that are unboxed. Actually it does just about work, but the simplifier ends up with stuff like case (/\a. eq_sel d) of df -> ...(df @Int)... and fails to simplify that any further. So for now we simply decline to take superclasses in the quantified case. Instead we have a special case in GHC.Tc.Solver.Equality.tryQCsEqCt which looks for primitive equalities specially in the quantified constraints. See also Note [Evidence for quantified constraints] in GHC.Core.Predicate. -}