diff options
| author | Gergő Érdi <gergo@erdi.hu> | 2022-11-21 02:49:17 +0000 |
|---|---|---|
| committer | Gergő Érdi <gergo@erdi.hu> | 2023-02-27 13:34:22 +0000 |
| commit | b56025f448646de40446a133f140f62c8a49cabf (patch) | |
| tree | c88c02b87b312119d2ecfa751a95e30dfecdfc4a | |
| parent | 7825fef9f2096d7769baf433c6858d132af60a3a (diff) | |
| download | haskell-b56025f448646de40446a133f140f62c8a49cabf.tar.gz | |
Don't specialise incoherent instance applications
Using incoherent instances, there can be situations where two
occurrences of the same overloaded function at the same type use two
different instances (see #22448). For incoherently resolved instances,
we must mark them with `nospec` to avoid the specialiser rewriting one
to the other. This marking is done during the desugaring of the
`WpEvApp` wrapper.
Fixes #22448
Metric Increase:
T15304
24 files changed, 592 insertions, 279 deletions
diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs index 90664d46e2..7a4dcdc15f 100644 --- a/compiler/GHC/Core/InstEnv.hs +++ b/compiler/GHC/Core/InstEnv.hs @@ -11,7 +11,7 @@ The bits common to GHC.Tc.TyCl.Instance and GHC.Tc.Deriv. module GHC.Core.InstEnv ( DFunId, InstMatch, ClsInstLookupResult, - PotentialUnifiers(..), getPotentialUnifiers, nullUnifiers, + Coherence(..), PotentialUnifiers(..), getPotentialUnifiers, nullUnifiers, OverlapFlag(..), OverlapMode(..), setOverlapModeMaybe, ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprInstances, instanceHead, instanceSig, mkLocalClsInst, mkImportedClsInst, @@ -56,7 +56,7 @@ import Data.List.NonEmpty ( NonEmpty (..), nonEmpty ) import qualified Data.List.NonEmpty as NE import Data.Maybe ( isJust ) -import GHC.Utils.Outputable +import GHC.Utils.Outputable hiding ((<>)) import GHC.Utils.Panic import GHC.Utils.Panic.Plain import Data.Semigroup @@ -577,50 +577,54 @@ The willingness to be overlapped or incoherent is a property of the instance declaration itself, controlled as follows: * An instance is "incoherent" - if it has an INCOHERENT pragma, or - if it appears in a module compiled with -XIncoherentInstances. + if it has an `INCOHERENT` pragma, or + if it appears in a module compiled with `-XIncoherentInstances`. * An instance is "overlappable" - if it has an OVERLAPPABLE or OVERLAPS pragma, or - if it appears in a module compiled with -XOverlappingInstances, or + if it has an `OVERLAPPABLE` or `OVERLAPS` pragma, or + if it appears in a module compiled with `-XOverlappingInstances`, or if the instance is incoherent. * An instance is "overlapping" - if it has an OVERLAPPING or OVERLAPS pragma, or - if it appears in a module compiled with -XOverlappingInstances, or + if it has an `OVERLAPPING` or `OVERLAPS` pragma, or + if it appears in a module compiled with `-XOverlappingInstances`, or if the instance is incoherent. - compiled with -XOverlappingInstances. Now suppose that, in some client module, we are searching for an instance of the target constraint (C ty1 .. tyn). The search works like this. -* Find all instances `I` that *match* the target constraint; that is, the - target constraint is a substitution instance of `I`. These instance - declarations are the *candidates*. +(IL0) If there are any local Givens that match (potentially unifying + any metavariables, even untouchable ones) the target constraint, + the search fails. See Note [Instance and Given overlap] in + GHC.Tc.Solver.Interact. -* Eliminate any candidate `IX` for which both of the following hold: +(IL1) Find all instances `I` that *match* the target constraint; that is, the target + constraint is a substitution instance of `I`. These instance declarations are + the /candidates/. - - There is another candidate `IY` that is strictly more specific; that - is, `IY` is a substitution instance of `IX` but not vice versa. +(IL2) If there are no candidates, the search fails. - - Either `IX` is *overlappable*, or `IY` is *overlapping*. (This - "either/or" design, rather than a "both/and" design, allow a - client to deliberately override an instance from a library, - without requiring a change to the library.) +(IL3) Eliminate any candidate `IX` for which there is another candidate `IY` such + that both of the following hold: + - `IY` is strictly more specific than `IX`. That is, `IY` is a + substitution instance of `IX` but not vice versa. + - Either `IX` is *overlappable*, or `IY` is *overlapping*. (This + "either/or" design, rather than a "both/and" design, allow a + client to deliberately override an instance from a library, + without requiring a change to the library.) -- If exactly one non-incoherent candidate remains, select it. If all - remaining candidates are incoherent, select an arbitrary one. - Otherwise the search fails (i.e. when more than one surviving - candidate is not incoherent). +(IL4) If all the remaining candidates are *incoherent*, the search succeeds, + returning an arbitrary surviving candidate. -- If the selected candidate (from the previous step) is incoherent, the - search succeeds, returning that candidate. +(IL5) If more than one non-*incoherent* candidate remains, the search + fails. Otherwise there is exactly one non-*incoherent* + candidate; call it the "prime candidate". -- If not, find all instances that *unify* with the target constraint, - but do not *match* it. Such non-candidate instances might match when - the target constraint is further instantiated. If all of them are - incoherent, the search succeeds, returning the selected candidate; if - not, the search fails. +(IL6) Now find all instances that unify with the target constraint, + but do not match it. Such non-candidate instances might match + when the target constraint is further instantiated. If all of + them are *incoherent* top-level instances, the search succeeds, + returning the prime candidate. Otherwise the search fails. Notice that these rules are not influenced by flag settings in the client module, where the instances are *used*. These rules make it @@ -748,6 +752,103 @@ but neither does But still x and y might subsequently be unified so they *do* match. Simple story: unify, don't match. + +Note [Coherence and specialisation: overview] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +GHC's specialiser relies on the Coherence Assumption: that if + d1 :: C tys + d2 :: C tys +then the dictionary d1 can be used in place of d2 and vice versa; it is as if +(C tys) is a singleton type. How do we guarantee this? Let's use this +example + class C a where { op :: a -> Int } + instance C [a] where {...} -- (I1) + instance {-# OVERLAPPING #-} C [Int] where {...} -- (I2) + + instance C a => C (Maybe a) where {...} -- (I3) + instance {-# INCOHERENT #-} C (Maybe Int) where {...} -- (I4) + instance C Int where {...} -- (I5) + +* When solving (C tys) from the top-level instances, we generally insist that + there is a unique, most-specific match. (Incoherent instances change the + picture a bit: see Note [Rules for instance lookup].) Example: + [W] C [Int] -- Pick (I2) + [W] C [Char] -- Pick (I1); does not match (I2) + + Caveat: if different usage sites see different instances (which the + programmer can contrive, with some effort), all bets are off; we really + can't make any guarantees at all. + +* But what about [W] C [b], which might arise from + risky :: b -> Int + risky x = op [x] + We can't pick (I2) because `b` is not Int. But if we pick (I1), and later + the simplifier inlines a call (risky @Int) we'll get a dictionary of type + (C [Int]) built by (I1), which might be utterly different to the dictionary + of type (C [Int]) built by (I2). That breaks the Coherence Assumption. + + So GHC declines to pick either, and rejects `risky`. You have to write a + different signature + notRisky :: C [b] => b -> Int + notRisky x = op [x] + so that the dictionary is resolved at the call site. + +* The INCOHERENT pragma tells GHC to choose an instance anyway: see + Note [Rules for instance lookup] step (IL6). Suppose we have + veryRisky :: C b => b -> Int + veryRisky x = op (Just x) + So we have [W] C (Maybe b). Because (I4) is INCOHERENT, GHC is allowed to + pick (I3). Of course, this risks breaking the Coherence Assumption, as + described above. + +* What about the incoherence from step (IL4)? For example + class D a b where { opD :: a -> b -> String } + instance {-# INCOHERENT #-} D Int b where {...} -- (I7) + instance {-# INCOHERENT #-} D a Int where {...} -- (I8) + + g (x::Int) = opD x x -- [W] D Int Int + + Here both (I7) and (I8) match, GHC picks an arbitrary one. + +So INCOHERENT may break the Coherence Assumption. To avoid this +incoherence breaking the specialiser, + +* We label as "incoherent" the dictionary constructed by a + (potentially) incoherent use of an instance declaration. + +* We do not specialise a function if there is an incoherent dictionary + in the /transistive dependencies/ of its dictionary arguments. + +To see the transitive closure issue, consider + deeplyRisky :: C b => b -> Int + deeplyRisky x = op (Just (Just x)) + +From (op (Just (Just x))) we get + [W] d1 : C (Maybe (Maybe b)) +which we solve (coherently!) via (I3), giving + [W] d2 : C (Maybe b) +Now we can only solve this incoherently. So we end up with + + deeplyRisky @b (d1 :: C b) + = op @(Maybe (Maybe b)) d1 + where + d1 :: C (Maybe (Maybe b)) = $dfI3 d2 -- Coherent decision + d2 :: C (Maybe b) = $sfI3 d1 -- Incoherent decision + +So `d2` is incoherent, and hence (transitively) so is `d1`. + +Here are the moving parts: + +* GHC.Core.InstEnv.lookupInstEnv tells if any incoherent unifiers were discarded + in step (IL6) of the instance lookup. + +* That info is recorded in the `cir_is_coherent` field of `OneInst`, and thence + transferred to the `ep_is_coherent` field of the `EvBind` for the dictionary. + +* `GHC.HsToCore.Binds.dsHsWrapper` desugars the evidence application (f d) into + (nospec f d) if `d` is incoherent. It has to do a dependency analysis to + determine transitive dependencies, but we need to do that anway. + See Note [Desugaring incoherent evidence] in GHC.HsToCore.Binds. -} type DFunInstType = Maybe Type @@ -840,31 +941,54 @@ lookupUniqueInstEnv instEnv cls tys _other -> Left $ text "instance not found" <+> (ppr $ mkTyConApp (classTyCon cls) tys) -data PotentialUnifiers = NoUnifiers - | OneOrMoreUnifiers [ClsInst] +data Coherence = IsCoherent | IsIncoherent + +-- See Note [Recording coherence information in `PotentialUnifiers`] +data PotentialUnifiers = NoUnifiers Coherence + | OneOrMoreUnifiers (NonEmpty ClsInst) -- This list is lazy as we only look at all the unifiers when -- printing an error message. It can be expensive to compute all -- the unifiers because if you are matching something like C a[sk] then -- all instances will unify. +{- Note [Recording coherence information in `PotentialUnifiers`] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we have any potential unifiers, then we go down the `NotSure` route +in `matchInstEnv`. According to Note [Rules for instance lookup] +steps IL4 and IL6, we only care about non-`INCOHERENT` instances for +this purpose. + +It is only when we don't have any potential unifiers (i.e. we know +that we have a unique solution modulo `INCOHERENT` instances) that we +care about that unique solution being coherent or not (see +Note [Coherence and specialisation: overview] for why we care at all). +So we only need the `Coherent` flag in the case where the set of +potential unifiers is otherwise empty. +-} + +instance Outputable Coherence where + ppr IsCoherent = text "coherent" + ppr IsIncoherent = text "incoherent" + instance Outputable PotentialUnifiers where - ppr NoUnifiers = text "NoUnifiers" + ppr (NoUnifiers c) = text "NoUnifiers" <+> ppr c ppr xs = ppr (getPotentialUnifiers xs) -instance Semigroup PotentialUnifiers where - NoUnifiers <> u = u - u <> NoUnifiers = u - u1 <> u2 = OneOrMoreUnifiers (getPotentialUnifiers u1 ++ getPotentialUnifiers u2) +instance Semigroup Coherence where + IsCoherent <> IsCoherent = IsCoherent + _ <> _ = IsIncoherent -instance Monoid PotentialUnifiers where - mempty = NoUnifiers +instance Semigroup PotentialUnifiers where + NoUnifiers c1 <> NoUnifiers c2 = NoUnifiers (c1 <> c2) + NoUnifiers _ <> u = u + OneOrMoreUnifiers (unifier :| unifiers) <> u = OneOrMoreUnifiers (unifier :| (unifiers <> getPotentialUnifiers u)) getPotentialUnifiers :: PotentialUnifiers -> [ClsInst] -getPotentialUnifiers NoUnifiers = [] -getPotentialUnifiers (OneOrMoreUnifiers cls) = cls +getPotentialUnifiers NoUnifiers{} = [] +getPotentialUnifiers (OneOrMoreUnifiers cls) = NE.toList cls nullUnifiers :: PotentialUnifiers -> Bool -nullUnifiers NoUnifiers = True +nullUnifiers NoUnifiers{} = True nullUnifiers _ = False lookupInstEnv' :: InstEnv -- InstEnv to look in @@ -901,8 +1025,12 @@ lookupInstEnv' (InstEnv rm) vis_mods cls tys = acc + incoherently_matched :: PotentialUnifiers -> PotentialUnifiers + incoherently_matched (NoUnifiers _) = NoUnifiers IsIncoherent + incoherently_matched u = u + check_unifier :: [ClsInst] -> PotentialUnifiers - check_unifier [] = NoUnifiers + check_unifier [] = NoUnifiers IsCoherent check_unifier (item@ClsInst { is_tvs = tpl_tvs, is_tys = tpl_tys }:items) | not (instIsVisible vis_mods item) = check_unifier items -- See Note [Instance lookup and orphan instances] @@ -910,8 +1038,9 @@ lookupInstEnv' (InstEnv rm) vis_mods cls tys -- Does not match, so next check whether the things unify -- See Note [Overlapping instances] -- Ignore ones that are incoherent: Note [Incoherent instances] + -- Record that we encountered incoherent instances: Note [Coherence and specialisation: overview] | isIncoherent item - = check_unifier items + = incoherently_matched $ check_unifier items | otherwise = assertPpr (tys_tv_set `disjointVarSet` tpl_tv_set) @@ -928,7 +1057,7 @@ lookupInstEnv' (InstEnv rm) vis_mods cls tys -- See Note [Infinitary substitution in lookup] MaybeApart MARInfinite _ -> check_unifier items _ -> - OneOrMoreUnifiers (item: getPotentialUnifiers (check_unifier items)) + OneOrMoreUnifiers (item :| getPotentialUnifiers (check_unifier items)) where tpl_tv_set = mkVarSet tpl_tvs @@ -953,8 +1082,8 @@ lookupInstEnv check_overlap_safe where (home_matches, home_unifs) = lookupInstEnv' home_ie vis_mods cls tys (pkg_matches, pkg_unifs) = lookupInstEnv' pkg_ie vis_mods cls tys - all_matches = home_matches ++ pkg_matches - all_unifs = home_unifs `mappend` pkg_unifs + all_matches = home_matches <> pkg_matches + all_unifs = home_unifs <> pkg_unifs final_matches = pruneOverlappedMatches all_matches -- Even if the unifs is non-empty (an error situation) -- we still prune the matches, so that the error message isn't @@ -968,7 +1097,7 @@ lookupInstEnv check_overlap_safe -- If the selected match is incoherent, discard all unifiers final_unifs = case final_matches of - (m:_) | isIncoherent (fst m) -> NoUnifiers + (m:_) | isIncoherent (fst m) -> NoUnifiers IsCoherent _ -> all_unifs -- Note [Safe Haskell isSafeOverlap] @@ -1299,6 +1428,36 @@ not incoherent, but we still want this to compile. Hence the The implementation is in insert_overlapping, where we remove matching incoherent instances as long as there are others. +If the choice of instance *does* matter, all bets are still not off: +users can consult the detailed specification of the instance selection +algorithm in the GHC Users' Manual. However, this means we can end up +with different instances at the same types at different parts of the +program, and this difference has to be preserved. For example, if we +have + + class C a where + op :: a -> String + + instance {-# OVERLAPPABLE #-} C a where ... + instance {-# INCOHERENT #-} C () where ... + +then depending on the circumstances (see #22448 for a full setup) some +occurrences of `op :: () -> String` may be resolved to the generic +instance, and other to the specific one; so we end up in the desugared +code with occurrences of both + + op @() ($dC_a @()) + +and + + op @() $dC_() + +In particular, the specialiser needs to ignore the incoherently +selected instance in `op @() ($dC_a @())`. So during instance lookup, +we record in `PotentialUnifiers` if a given solution was arrived at +incoherently; we then use this information to inhibit specialisation +a la Note [nospecId magic] in GHC.Types.Id.Make. + ************************************************************************ diff --git a/compiler/GHC/HsToCore.hs b/compiler/GHC/HsToCore.hs index 3c6ec71079..755fe3e198 100644 --- a/compiler/GHC/HsToCore.hs +++ b/compiler/GHC/HsToCore.hs @@ -182,8 +182,8 @@ deSugar hsc_env _ -> pure $ emptyHpcInfo other_hpc_info ; (msgs, mb_res) <- initDs hsc_env tcg_env $ - do { ds_ev_binds <- dsEvBinds ev_binds - ; core_prs <- dsTopLHsBinds binds_cvr + do { dsEvBinds ev_binds $ \ ds_ev_binds -> do + { core_prs <- dsTopLHsBinds binds_cvr ; core_prs <- patchMagicDefns core_prs ; (spec_prs, spec_rules) <- dsImpSpecs imp_specs ; (ds_fords, foreign_prs) <- dsForeigns fords @@ -194,7 +194,7 @@ deSugar hsc_env ; return ( ds_ev_binds , foreign_prs `appOL` core_prs `appOL` spec_prs , spec_rules ++ ds_rules - , ds_fords `appendStubC` hpc_init) } + , ds_fords `appendStubC` hpc_init) } } ; case mb_res of { Nothing -> return (msgs, Nothing) ; diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs index 3013524a2d..cc757a94e3 100644 --- a/compiler/GHC/HsToCore/Arrows.hs +++ b/compiler/GHC/HsToCore/Arrows.hs @@ -643,8 +643,8 @@ dsCmd _ local_vars _stack_ty _res_ty (HsCmdArrForm _ op _ _ args) env_ids = do dsCmd ids local_vars stack_ty res_ty (XCmd (HsWrap wrap cmd)) env_ids = do (core_cmd, env_ids') <- dsCmd ids local_vars stack_ty res_ty cmd env_ids - core_wrap <- dsHsWrapper wrap - return (core_wrap core_cmd, env_ids') + dsHsWrapper wrap $ \core_wrap -> + return (core_wrap core_cmd, env_ids') dsCmd _ _ _ _ c@(HsCmdLam {}) _ = pprPanic "dsCmd" (ppr c) diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs index 4d594e833f..1a025e1dec 100644 --- a/compiler/GHC/HsToCore/Binds.hs +++ b/compiler/GHC/HsToCore/Binds.hs @@ -16,7 +16,7 @@ lower levels it is preserved with @let@/@letrec@s). module GHC.HsToCore.Binds ( dsTopLHsBinds, dsLHsBinds, decomposeRuleLhs, dsSpec - , dsHsWrapper, dsEvTerm, dsTcEvBinds, dsTcEvBinds_s, dsEvBinds + , dsHsWrapper, dsHsWrappers, dsEvTerm, dsTcEvBinds, dsTcEvBinds_s, dsEvBinds , dsWarnOrphanRule ) where @@ -41,6 +41,7 @@ import GHC.Hs -- lots of things import GHC.Core -- lots of things import GHC.Core.SimpleOpt ( simpleOptExpr ) import GHC.Core.Opt.OccurAnal ( occurAnalyseExpr ) +import GHC.Core.InstEnv ( Coherence(..) ) import GHC.Core.Make import GHC.Core.Utils import GHC.Core.Opt.Arity ( etaExpand ) @@ -60,6 +61,7 @@ import GHC.Builtin.Types ( naturalTy, typeSymbolKind, charTy ) import GHC.Tc.Types.Evidence import GHC.Types.Id +import GHC.Types.Id.Make ( nospecId ) import GHC.Types.Name import GHC.Types.Var.Set import GHC.Types.Var.Env @@ -72,6 +74,7 @@ import GHC.Data.Maybe import GHC.Data.OrdList import GHC.Data.Graph.Directed import GHC.Data.Bag +import qualified Data.Set as S import GHC.Utils.Constants (debugIsOn) import GHC.Utils.Misc @@ -153,7 +156,8 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun , fun_matches = matches , fun_ext = (co_fn, tick) }) - = do { (args, body) <- addTyCs FromSource (hsWrapDictBinders co_fn) $ + = do { dsHsWrapper co_fn $ \core_wrap -> do + { (args, body) <- addTyCs FromSource (hsWrapDictBinders co_fn) $ -- FromSource might not be accurate (we don't have any -- origin annotations for things in this module), but at -- worst we do superfluous calls to the pattern match @@ -163,7 +167,6 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun -- See Note [Long-distance information] in "GHC.HsToCore.Pmc" matchWrapper (mkPrefixFunRhs (L loc (idName fun))) Nothing matches - ; core_wrap <- dsHsWrapper co_fn ; let body' = mkOptTickBox tick body rhs = core_wrap (mkLams args body') core_binds@(id,_) = makeCorePair dflags fun False 0 rhs @@ -179,7 +182,7 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun ; --pprTrace "dsHsBind" (vcat [ ppr fun <+> ppr (idInlinePragma fun) -- , ppr (mg_alts matches) -- , ppr args, ppr core_binds, ppr body']) $ - return (force_var, [core_binds]) } + return (force_var, [core_binds]) } } dsHsBind dflags (PatBind { pat_lhs = pat, pat_rhs = grhss , pat_ext = (ty, (rhs_tick, var_ticks)) @@ -208,10 +211,10 @@ dsHsBind -- for inner pattern match check -- See Check, Note [Long-distance information] - ; ds_ev_binds <- dsTcEvBinds_s ev_binds + ; dsTcEvBinds_s ev_binds $ \ds_ev_binds -> do -- dsAbsBinds does the hard work - ; dsAbsBinds dflags tyvars dicts exports ds_ev_binds ds_binds has_sig } + { dsAbsBinds dflags tyvars dicts exports ds_ev_binds ds_binds has_sig } } dsHsBind _ (PatSynBind{}) = panic "dsHsBind: PatSynBind" @@ -241,9 +244,8 @@ dsAbsBinds dflags tyvars dicts exports _ -> Nothing -- If there is a variable to force, it's just the -- single variable we are binding here - = do { core_wrap <- dsHsWrapper wrap -- Usually the identity - - ; let rhs = core_wrap $ + = do { dsHsWrapper wrap $ \core_wrap -> do -- Usually the identity + { let rhs = core_wrap $ mkLams tyvars $ mkLams dicts $ mkCoreLets ds_ev_binds $ body @@ -261,7 +263,7 @@ dsAbsBinds dflags tyvars dicts exports (isDefaultMethod prags) (dictArity dicts) rhs - ; return (force_vars', main_bind : fromOL spec_binds) } + ; return (force_vars', main_bind : fromOL spec_binds) } } -- Another common case: no tyvars, no dicts -- In this case we can have a much simpler desugaring @@ -273,9 +275,9 @@ dsAbsBinds dflags tyvars dicts exports , abe_wrap = wrap }) -- No SpecPrags (no dicts) -- Can't be a default method (default methods are singletons) - = do { core_wrap <- dsHsWrapper wrap - ; return ( gbl_id `setInlinePragma` defaultInlinePragma - , core_wrap (Var lcl_id)) } + = do { dsHsWrapper wrap $ \core_wrap -> do + { return ( gbl_id `setInlinePragma` defaultInlinePragma + , core_wrap (Var lcl_id)) } } ; main_prs <- mapM mk_main exports ; return (force_vars, flattenBinds ds_ev_binds @@ -309,8 +311,8 @@ dsAbsBinds dflags tyvars dicts exports , abe_mono = local, abe_prags = spec_prags }) -- See Note [ABExport wrapper] in "GHC.Hs.Binds" = do { tup_id <- newSysLocalDs ManyTy tup_ty - ; core_wrap <- dsHsWrapper wrap - ; let rhs = core_wrap $ mkLams tyvars $ mkLams dicts $ + ; dsHsWrapper wrap $ \core_wrap -> do + { let rhs = core_wrap $ mkLams tyvars $ mkLams dicts $ mkBigTupleSelector all_locals local tup_id $ mkVarApps (Var poly_tup_id) (tyvars ++ dicts) rhs_for_spec = Let (NonRec poly_tup_id poly_tup_rhs) rhs @@ -320,7 +322,7 @@ dsAbsBinds dflags tyvars dicts exports -- Kill the INLINE pragma because it applies to -- the user written (local) function. The global -- Id is just the selector. Hmm. - ; return ((global', rhs) : fromOL spec_binds) } + ; return ((global', rhs) : fromOL spec_binds) } } ; export_binds_s <- mapM mk_bind (exports ++ extra_exports) @@ -698,9 +700,9 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl)) -- perhaps with the body of the lambda wrapped in some WpLets -- E.g. /\a \(d:Eq a). let d2 = $df d in [] (Maybe a) d2 - ; core_app <- dsHsWrapper spec_app + ; dsHsWrapper spec_app $ \core_app -> do - ; let ds_lhs = core_app (Var poly_id) + { let ds_lhs = core_app (Var poly_id) spec_ty = mkLamTypes spec_bndrs (exprType ds_lhs) ; -- pprTrace "dsRule" (vcat [ text "Id:" <+> ppr poly_id -- , text "spec_co:" <+> ppr spec_co @@ -729,7 +731,7 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl)) -- NB: do *not* use makeCorePair on (spec_id,spec_rhs), because -- makeCorePair overwrites the unfolding, which we have -- just created using specUnfolding - } } } + } } } } where is_local_id = isJust mb_poly_rhs poly_rhs | Just rhs <- mb_poly_rhs @@ -1150,75 +1152,157 @@ evidence that is used in `e`. This question arose when thinking about deep subsumption; see https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-1125419649). + +Note [Desugaring incoherent evidence] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If the evidence is coherent, we desugar WpEvApp by simply passing +core_tm directly to k: + + k core_tm + +If the evidence is not coherent, we mark the application with nospec: + + nospec @(cls => a) k core_tm + +where nospec :: forall a. a -> a ensures that the typeclass specialiser +doesn't attempt to common up this evidence term with other evidence terms +of the same type (see Note [nospecId magic] in GHC.Types.Id.Make). + +See Note [Coherence and specialisation: overview] for why we shouldn't +specialise incoherent evidence. + +We can find out if a given evidence is coherent or not during the +desugaring of its WpLet wrapper: an evidence is incoherent if its +own resolution was incoherent (see Note [Incoherent instances]), or +if its definition refers to other incoherent evidence. dsEvBinds is +the convenient place to compute this, since it already needs to do +inter-evidence dependency analysis to generate well-scoped +bindings. We then record this coherence information in the +dsl_coherence field of DsM's local environment. + -} -dsHsWrapper :: HsWrapper -> DsM (CoreExpr -> CoreExpr) -dsHsWrapper WpHole = return $ \e -> e -dsHsWrapper (WpTyApp ty) = return $ \e -> App e (Type ty) -dsHsWrapper (WpEvLam ev) = return $ Lam ev -dsHsWrapper (WpTyLam tv) = return $ Lam tv -dsHsWrapper (WpLet ev_binds) = do { bs <- dsTcEvBinds ev_binds - ; return (mkCoreLets bs) } -dsHsWrapper (WpCompose c1 c2) = do { w1 <- dsHsWrapper c1 - ; w2 <- dsHsWrapper c2 - ; return (w1 . w2) } -dsHsWrapper (WpFun c1 c2 (Scaled w t1)) -- See Note [Desugaring WpFun] - = do { x <- newSysLocalDs w t1 - ; w1 <- dsHsWrapper c1 - ; w2 <- dsHsWrapper c2 - ; let app f a = mkCoreAppDs (text "dsHsWrapper") f a - arg = w1 (Var x) - ; return (\e -> (Lam x (w2 (app e arg)))) } -dsHsWrapper (WpCast co) = assert (coercionRole co == Representational) $ - return $ \e -> mkCastDs e co -dsHsWrapper (WpEvApp tm) = do { core_tm <- dsEvTerm tm - ; return (\e -> App e core_tm) } +dsHsWrapper :: HsWrapper -> ((CoreExpr -> CoreExpr) -> DsM a) -> DsM a +dsHsWrapper WpHole k = k $ \e -> e +dsHsWrapper (WpTyApp ty) k = k $ \e -> App e (Type ty) +dsHsWrapper (WpEvLam ev) k = k $ Lam ev +dsHsWrapper (WpTyLam tv) k = k $ Lam tv +dsHsWrapper (WpLet ev_binds) k = do { dsTcEvBinds ev_binds $ \bs -> do + { k (mkCoreLets bs) } } +dsHsWrapper (WpCompose c1 c2) k = do { dsHsWrapper c1 $ \w1 -> do + { dsHsWrapper c2 $ \w2 -> do + { k (w1 . w2) } } } +dsHsWrapper (WpFun c1 c2 (Scaled w t1)) k -- See Note [Desugaring WpFun] + = do { x <- newSysLocalDs w t1 + ; dsHsWrapper c1 $ \w1 -> do + { dsHsWrapper c2 $ \w2 -> do + { let app f a = mkCoreAppDs (text "dsHsWrapper") f a + arg = w1 (Var x) + ; k (\e -> (Lam x (w2 (app e arg)))) } } } +dsHsWrapper (WpCast co) k = assert (coercionRole co == Representational) $ + k $ \e -> mkCastDs e co +dsHsWrapper (WpEvApp tm) k = do { core_tm <- dsEvTerm tm + ; incoherents <- getIncoherents + ; let vs = exprFreeVarsList core_tm + is_incoherent_var v = v `S.member` incoherents + is_coherent = all (not . is_incoherent_var) vs -- See Note [Desugaring incoherent evidence] + ; k (\e -> app_ev is_coherent e core_tm) } -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify. -dsHsWrapper (WpMultCoercion co) = do { when (not (isReflexiveCo co)) $ - diagnosticDs DsMultiplicityCoercionsNotSupported - ; return $ \e -> e } +dsHsWrapper (WpMultCoercion co) k = do { unless (isReflexiveCo co) $ + diagnosticDs DsMultiplicityCoercionsNotSupported + ; k $ \e -> e } + +app_ev :: Bool -> CoreExpr -> CoreExpr -> CoreExpr +app_ev is_coherent k core_tm + | is_coherent = k `App` core_tm + | otherwise = Var nospecId `App` Type (exprType k) `App` k `App` core_tm + +dsHsWrappers :: [HsWrapper] -> ([CoreExpr -> CoreExpr] -> DsM a) -> DsM a +dsHsWrappers (wp:wps) k = dsHsWrapper wp $ \wrap -> dsHsWrappers wps $ \wraps -> k (wrap:wraps) +dsHsWrappers [] k = k [] + -------------------------------------- -dsTcEvBinds_s :: [TcEvBinds] -> DsM [CoreBind] -dsTcEvBinds_s [] = return [] -dsTcEvBinds_s (b:rest) = assert (null rest) $ -- Zonker ensures null - dsTcEvBinds b +dsTcEvBinds_s :: [TcEvBinds] -> ([CoreBind] -> DsM a) -> DsM a +dsTcEvBinds_s [] k = k [] +dsTcEvBinds_s (b:rest) k = assert (null rest) $ -- Zonker ensures null + dsTcEvBinds b k -dsTcEvBinds :: TcEvBinds -> DsM [CoreBind] +dsTcEvBinds :: TcEvBinds -> ([CoreBind] -> DsM a) -> DsM a dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds" -- Zonker has got rid of this dsTcEvBinds (EvBinds bs) = dsEvBinds bs -dsEvBinds :: Bag EvBind -> DsM [CoreBind] -dsEvBinds bs - = do { ds_bs <- mapBagM dsEvBind bs - ; return (mk_ev_binds ds_bs) } - -mk_ev_binds :: Bag (Id,CoreExpr) -> [CoreBind] +-- * Desugars the ev_binds, sorts them into dependency order, and +-- passes the resulting [CoreBind] to thing_inside +-- * Extends the DsM (dsl_coherence field) with coherence information +-- for each binder in ev_binds, before invoking thing_inside +dsEvBinds :: Bag EvBind -> ([CoreBind] -> DsM a) -> DsM a +dsEvBinds ev_binds thing_inside + = do { ds_binds <- mapBagM dsEvBind ev_binds + ; let comps = sort_ev_binds ds_binds + ; go comps thing_inside } + where + go ::[SCC (Node EvVar (Coherence, CoreExpr))] -> ([CoreBind] -> DsM a) -> DsM a + go (comp:comps) thing_inside + = do { incoherents <- getIncoherents + ; let (core_bind, new_incoherents) = ds_component incoherents comp + ; addIncoherents new_incoherents $ go comps $ \ core_binds -> thing_inside (core_bind:core_binds) } + go [] thing_inside = thing_inside [] + + is_coherent IsCoherent = True + is_coherent IsIncoherent = False + + ds_component incoherents (AcyclicSCC node) = (NonRec v rhs, new_incoherents) + where + ((v, rhs), (this_coherence, deps)) = unpack_node node + transitively_incoherent = not (is_coherent this_coherence) || any is_incoherent deps + is_incoherent dep = dep `S.member` incoherents + new_incoherents + | transitively_incoherent = S.singleton v + | otherwise = mempty + ds_component incoherents (CyclicSCC nodes) = (Rec pairs, new_incoherents) + where + (pairs, direct_coherence) = unzip $ map unpack_node nodes + + is_incoherent_remote dep = dep `S.member` incoherents + transitively_incoherent = or [ not (is_coherent this_coherence) || any is_incoherent_remote deps | (this_coherence, deps) <- direct_coherence ] + -- Bindings from a given SCC are transitively coherent if + -- all are coherent and all their remote dependencies are + -- also coherent; see Note [Desugaring incoherent evidence] + + new_incoherents + | transitively_incoherent = S.fromList [ v | (v, _) <- pairs] + | otherwise = mempty + + unpack_node DigraphNode { node_key = v, node_payload = (coherence, rhs), node_dependencies = deps } = ((v, rhs), (coherence, deps)) + +sort_ev_binds :: Bag (Id, Coherence, CoreExpr) -> [SCC (Node EvVar (Coherence, CoreExpr))] -- We do SCC analysis of the evidence bindings, /after/ desugaring -- them. This is convenient: it means we can use the GHC.Core -- free-variable functions rather than having to do accurate free vars -- for EvTerm. -mk_ev_binds ds_binds - = map ds_scc (stronglyConnCompFromEdgedVerticesUniq edges) +sort_ev_binds ds_binds = stronglyConnCompFromEdgedVerticesUniqR edges where - edges :: [ Node EvVar (EvVar,CoreExpr) ] + edges :: [ Node EvVar (Coherence, CoreExpr) ] edges = foldr ((:) . mk_node) [] ds_binds - mk_node :: (Id, CoreExpr) -> Node EvVar (EvVar,CoreExpr) - mk_node b@(var, rhs) - = DigraphNode { node_payload = b + mk_node :: (Id, Coherence, CoreExpr) -> Node EvVar (Coherence, CoreExpr) + mk_node (var, coherence, rhs) + = DigraphNode { node_payload = (coherence, rhs) , node_key = var , node_dependencies = nonDetEltsUniqSet $ exprFreeVars rhs `unionVarSet` coVarsOfType (varType var) } - -- It's OK to use nonDetEltsUniqSet here as stronglyConnCompFromEdgedVertices + -- It's OK to use nonDetEltsUniqSet here as graphFromEdgedVerticesUniq -- is still deterministic even if the edges are in nondeterministic order -- as explained in Note [Deterministic SCC] in GHC.Data.Graph.Directed. - ds_scc (AcyclicSCC (v,r)) = NonRec v r - ds_scc (CyclicSCC prs) = Rec prs - -dsEvBind :: EvBind -> DsM (Id, CoreExpr) -dsEvBind (EvBind { eb_lhs = v, eb_rhs = r}) = liftM ((,) v) (dsEvTerm r) +dsEvBind :: EvBind -> DsM (Id, Coherence, CoreExpr) +dsEvBind (EvBind { eb_lhs = v, eb_rhs = r, eb_info = info }) = do + e <- dsEvTerm r + let coherence = case info of + EvBindGiven{} -> IsCoherent + EvBindWanted{ ebi_coherence = coherence } -> coherence + return (v, coherence, e) {-********************************************************************** @@ -1232,10 +1316,10 @@ dsEvTerm (EvExpr e) = return e dsEvTerm (EvTypeable ty ev) = dsEvTypeable ty ev dsEvTerm (EvFun { et_tvs = tvs, et_given = given , et_binds = ev_binds, et_body = wanted_id }) - = do { ds_ev_binds <- dsTcEvBinds ev_binds - ; return $ (mkLams (tvs ++ given) $ + = do { dsTcEvBinds ev_binds $ \ds_ev_binds -> do + { return $ (mkLams (tvs ++ given) $ mkCoreLets ds_ev_binds $ - Var wanted_id) } + Var wanted_id) } } {-********************************************************************** diff --git a/compiler/GHC/HsToCore/Binds.hs-boot b/compiler/GHC/HsToCore/Binds.hs-boot index fa5923ccc6..7c2015cc33 100644 --- a/compiler/GHC/HsToCore/Binds.hs-boot +++ b/compiler/GHC/HsToCore/Binds.hs-boot @@ -3,4 +3,4 @@ import GHC.HsToCore.Monad ( DsM ) import GHC.Core ( CoreExpr ) import GHC.Tc.Types.Evidence (HsWrapper) -dsHsWrapper :: HsWrapper -> DsM (CoreExpr -> CoreExpr) +dsHsWrapper :: HsWrapper -> ((CoreExpr -> CoreExpr) -> DsM a) -> DsM a diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs index d106899835..63c2cee789 100644 --- a/compiler/GHC/HsToCore/Expr.hs +++ b/compiler/GHC/HsToCore/Expr.hs @@ -92,11 +92,11 @@ dsValBinds (ValBinds {}) _ = panic "dsValBinds ValBindsIn" ------------------------- dsIPBinds :: HsIPBinds GhcTc -> CoreExpr -> DsM CoreExpr dsIPBinds (IPBinds ev_binds ip_binds) body - = do { ds_binds <- dsTcEvBinds ev_binds - ; let inner = mkCoreLets ds_binds body + = do { dsTcEvBinds ev_binds $ \ ds_binds -> do + { let inner = mkCoreLets ds_binds body -- The dict bindings may not be in -- dependency order; hence Rec - ; foldrM ds_ip_bind inner ip_binds } + ; foldrM ds_ip_bind inner ip_binds } } where ds_ip_bind :: LIPBind GhcTc -> CoreExpr -> DsM CoreExpr ds_ip_bind (L _ (IPBind n _ e)) body @@ -182,8 +182,8 @@ dsUnliftedBind (XHsBindsLR (AbsBinds { abs_tvs = [], abs_ev_vars = [] bind_export export b = bindNonRec (abe_poly export) (Var (abe_mono export)) b ; body2 <- foldlM (\body lbind -> dsUnliftedBind (unLoc lbind) body) body1 lbinds - ; ds_binds <- dsTcEvBinds_s ev_binds - ; return (mkCoreLets ds_binds body2) } + ; dsTcEvBinds_s ev_binds $ \ ds_binds -> do + { return (mkCoreLets ds_binds body2) } } dsUnliftedBind (FunBind { fun_id = L l fun , fun_matches = matches @@ -193,9 +193,9 @@ dsUnliftedBind (FunBind { fun_id = L l fun -- so must be simply unboxed = do { (args, rhs) <- matchWrapper (mkPrefixFunRhs (L l $ idName fun)) Nothing matches ; massert (null args) -- Functions aren't unlifted - ; core_wrap <- dsHsWrapper co_fn -- Can be non-identity (#21516) - ; let rhs' = core_wrap (mkOptTickBox tick rhs) - ; return (bindNonRec fun rhs' body) } + ; dsHsWrapper co_fn $ \core_wrap -> do -- Can be non-identity (#21516) + { let rhs' = core_wrap (mkOptTickBox tick rhs) + ; return (bindNonRec fun rhs' body) } } dsUnliftedBind (PatBind { pat_lhs = pat, pat_rhs = grhss , pat_ext = (ty, _) }) body @@ -550,10 +550,10 @@ dsSyntaxExpr (SyntaxExprTc { syn_expr = expr , syn_res_wrap = res_wrap }) arg_exprs = do { fun <- dsExpr expr - ; core_arg_wraps <- mapM dsHsWrapper arg_wraps - ; core_res_wrap <- dsHsWrapper res_wrap - ; let wrapped_args = zipWithEqual "dsSyntaxExpr" ($) core_arg_wraps arg_exprs - ; return $ core_res_wrap (mkCoreApps fun wrapped_args) } + ; dsHsWrappers arg_wraps $ \core_arg_wraps -> do + { dsHsWrapper res_wrap $ \core_res_wrap -> do + { let wrapped_args = zipWithEqual "dsSyntaxExpr" ($) core_arg_wraps arg_exprs + ; return $ core_res_wrap (mkCoreApps fun wrapped_args) } } } dsSyntaxExpr NoSyntaxExprTc _ = panic "dsSyntaxExpr" findField :: [LHsRecField GhcTc arg] -> Name -> [arg] @@ -872,15 +872,15 @@ dsHsWrapped orig_hs_expr = go (wrap <.> WpTyApp ty) hs_e go wrap (HsVar _ (L _ var)) - = do { wrap' <- dsHsWrapper wrap - ; let expr = wrap' (varToCoreExpr var) + = do { dsHsWrapper wrap $ \wrap' -> do + { let expr = wrap' (varToCoreExpr var) ty = exprType expr ; dflags <- getDynFlags ; warnAboutIdentities dflags var ty - ; return expr } + ; return expr } } go wrap hs_e - = do { wrap' <- dsHsWrapper wrap - ; addTyCs FromSource (hsWrapDictBinders wrap) $ + = do { dsHsWrapper wrap $ \wrap' -> do + { addTyCs FromSource (hsWrapDictBinders wrap) $ do { e <- dsExpr hs_e - ; return (wrap' e) } } + ; return (wrap' e) } } } diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs index 0cf83d378c..56fffd89a2 100644 --- a/compiler/GHC/HsToCore/Match.hs +++ b/compiler/GHC/HsToCore/Match.hs @@ -285,9 +285,9 @@ matchCoercion (var :| vars) ty (eqns@(eqn1 :| _)) ; var' <- newUniqueId var (idMult var) pat_ty' ; match_result <- match (var':vars) ty $ NEL.toList $ decomposeFirstPat getCoPat <$> eqns - ; core_wrap <- dsHsWrapper co - ; let bind = NonRec var' (core_wrap (Var var)) - ; return (mkCoLetMatchResult bind match_result) } + ; dsHsWrapper co $ \core_wrap -> do + { let bind = NonRec var' (core_wrap (Var var)) + ; return (mkCoLetMatchResult bind match_result) } } matchView :: NonEmpty MatchId -> Type -> NonEmpty EquationInfo -> DsM (MatchResult CoreExpr) -- Apply the view function to the match variable and then match that diff --git a/compiler/GHC/HsToCore/Match/Constructor.hs b/compiler/GHC/HsToCore/Match/Constructor.hs index 64dff69c1a..fc411f491b 100644 --- a/compiler/GHC/HsToCore/Match/Constructor.hs +++ b/compiler/GHC/HsToCore/Match/Constructor.hs @@ -163,13 +163,13 @@ matchOneConLike vars ty mult (eqn1 :| eqns) -- All eqns for a single construct } } : pats })) - = do ds_bind <- dsTcEvBinds bind - return ( wrapBinds (tvs `zip` tvs1) - . wrapBinds (ds `zip` dicts1) - . mkCoreLets ds_bind - , eqn { eqn_orig = Generated - , eqn_pats = conArgPats val_arg_tys args ++ pats } - ) + = do dsTcEvBinds bind $ \ds_bind -> + return ( wrapBinds (tvs `zip` tvs1) + . wrapBinds (ds `zip` dicts1) + . mkCoreLets ds_bind + , eqn { eqn_orig = Generated + , eqn_pats = conArgPats val_arg_tys args ++ pats } + ) shift (_, (EqnInfo { eqn_pats = ps })) = pprPanic "matchOneCon/shift" (ppr ps) ; let scaled_arg_tys = map (scaleScaled mult) val_arg_tys -- The 'val_arg_tys' are taken from the data type definition, they diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs index 17d9a3db94..1edcde6924 100644 --- a/compiler/GHC/HsToCore/Monad.hs +++ b/compiler/GHC/HsToCore/Monad.hs @@ -36,6 +36,9 @@ module GHC.HsToCore.Monad ( -- Getting and setting pattern match oracle states getPmNablas, updPmNablas, + -- Tracking evidence variable coherence + addIncoherents, getIncoherents, + -- Get COMPLETE sets of a TyCon dsGetCompleteMatches, @@ -91,6 +94,7 @@ import GHC.Types.Name.Reader import GHC.Types.Basic ( Origin ) import GHC.Types.SourceFile import GHC.Types.Id +import GHC.Types.Var (EvId) import GHC.Types.SrcLoc import GHC.Types.TypeEnv import GHC.Types.Unique.Supply @@ -109,6 +113,7 @@ import qualified GHC.Data.Strict as Strict import Data.IORef import GHC.Driver.Env.KnotVars +import qualified Data.Set as S {- ************************************************************************ @@ -349,9 +354,10 @@ mkDsEnvs unit_env mod rdr_env type_env fam_inst_env ptc msg_var cc_st_var , ds_cc_st = cc_st_var , ds_next_wrapper_num = next_wrapper_num } - lcl_env = DsLclEnv { dsl_meta = emptyNameEnv - , dsl_loc = real_span - , dsl_nablas = initNablas + lcl_env = DsLclEnv { dsl_meta = emptyNameEnv + , dsl_loc = real_span + , dsl_nablas = initNablas + , dsl_incoherents = mempty } in (gbl_env, lcl_env) @@ -407,6 +413,12 @@ getPmNablas = do { env <- getLclEnv; return (dsl_nablas env) } updPmNablas :: Nablas -> DsM a -> DsM a updPmNablas nablas = updLclEnv (\env -> env { dsl_nablas = nablas }) +addIncoherents :: S.Set EvId -> DsM a -> DsM a +addIncoherents incoherents = updLclEnv (\env -> env{ dsl_incoherents = incoherents `mappend` dsl_incoherents env }) + +getIncoherents :: DsM (S.Set EvId) +getIncoherents = dsl_incoherents <$> getLclEnv + getSrcSpanDs :: DsM SrcSpan getSrcSpanDs = do { env <- getLclEnv ; return (RealSrcSpan (dsl_loc env) Strict.Nothing) } diff --git a/compiler/GHC/HsToCore/Pmc/Desugar.hs b/compiler/GHC/HsToCore/Pmc/Desugar.hs index 8ebe472d5f..7958ef46db 100644 --- a/compiler/GHC/HsToCore/Pmc/Desugar.hs +++ b/compiler/GHC/HsToCore/Pmc/Desugar.hs @@ -154,8 +154,8 @@ desugarPat x pat = case pat of | WpCast co <- wrapper, isReflexiveCo co -> desugarPat x p | otherwise -> do (y, grds) <- desugarPatV p - wrap_rhs_y <- dsHsWrapper wrapper - pure (PmLet y (wrap_rhs_y (Var x)) : grds) + dsHsWrapper wrapper $ \wrap_rhs_y -> + pure (PmLet y (wrap_rhs_y (Var x)) : grds) -- (n + k) ===> let b = x >= k, True <- b, let n = x-k NPlusKPat _pat_ty (L _ n) k1 k2 ge minus -> do diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs index 63094c21dd..16dc9a8603 100644 --- a/compiler/GHC/HsToCore/Quote.hs +++ b/compiler/GHC/HsToCore/Quote.hs @@ -143,9 +143,9 @@ mkMetaWrappers q@(QuoteWrapper quote_var_raw m_var) = do mkWpTyApps [m_var] tyWrapper t = mkAppTy m_var t debug = (quoteWrapper, monadWrapper, m_var) - q_f <- dsHsWrapper quoteWrapper - m_f <- dsHsWrapper monadWrapper - return (MetaWrappers q_f m_f tyWrapper debug) + dsHsWrapper quoteWrapper $ \q_f -> do { + dsHsWrapper monadWrapper $ \m_f -> do { + return (MetaWrappers q_f m_f tyWrapper debug) } } -- Turn A into m A wrapName :: Name -> MetaM Type diff --git a/compiler/GHC/HsToCore/Types.hs b/compiler/GHC/HsToCore/Types.hs index d3e7f2ddbd..93a065a7da 100644 --- a/compiler/GHC/HsToCore/Types.hs +++ b/compiler/GHC/HsToCore/Types.hs @@ -14,6 +14,7 @@ module GHC.HsToCore.Types ( import GHC.Prelude (Int) import Data.IORef +import qualified Data.Set as S import GHC.Types.CostCentre.State import GHC.Types.Error @@ -78,6 +79,9 @@ data DsLclEnv -- ^ See Note [Long-distance information] in "GHC.HsToCore.Pmc". -- The set of reaching values Nablas is augmented as we walk inwards, refined -- through each pattern match in turn + , dsl_incoherents :: S.Set EvVar + -- ^ See Note [Desugaring incoherent evidence]: this field collects + -- all incoherent evidence variables in scope. } -- Inside [| |] brackets, the desugarer looks diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index 112268097f..356d36e0ab 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -1059,11 +1059,11 @@ addDeferredBinding ctxt err (EI { ei_evdest = Just dest, ei_pred = item_ty ; case dest of EvVarDest evar - -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm + -> addTcEvBind ev_binds_var $ mkWantedEvBind evar IsCoherent err_tm HoleDest hole -> do { -- See Note [Deferred errors for coercion holes] let co_var = coHoleCoVar hole - ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm + ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var IsCoherent err_tm ; fillCoercionHole hole (mkCoVarCo co_var) } } addDeferredBinding _ _ _ = return () -- Do not set any evidence for Given diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs index 57ee52144c..4019b44278 100644 --- a/compiler/GHC/Tc/Instance/Class.hs +++ b/compiler/GHC/Tc/Instance/Class.hs @@ -34,7 +34,6 @@ import GHC.Types.SafeHaskell import GHC.Types.Name ( Name, pprDefinedAt ) import GHC.Types.Var.Env ( VarEnv ) import GHC.Types.Id -import GHC.Types.Id.Make ( nospecId ) import GHC.Types.Var import GHC.Core.Predicate @@ -46,7 +45,7 @@ import GHC.Core.DataCon import GHC.Core.TyCon import GHC.Core.Class -import GHC.Core ( Expr(Var, App, Cast, Type) ) +import GHC.Core ( Expr(Var, App, Cast) ) import GHC.Utils.Outputable import GHC.Utils.Panic @@ -97,9 +96,10 @@ type SafeOverlapping = Bool data ClsInstResult = NoInstance -- Definitely no instance - | OneInst { cir_new_theta :: [TcPredType] - , cir_mk_ev :: [EvExpr] -> EvTerm - , cir_what :: InstanceWhat } + | OneInst { cir_new_theta :: [TcPredType] + , cir_mk_ev :: [EvExpr] -> EvTerm + , cir_coherence :: Coherence -- See Note [Coherence and specialisation: overview] + , cir_what :: InstanceWhat } | NotSure -- Multiple matches and/or one or more unifiers @@ -188,12 +188,12 @@ matchInstEnv dflags short_cut_solver clas tys ; case (matches, unify, safeHaskFail) of -- Nothing matches - ([], NoUnifiers, _) + ([], NoUnifiers{}, _) -> do { traceTc "matchClass not matching" (ppr pred $$ ppr (ie_local instEnvs)) ; return NoInstance } -- A single match (& no safe haskell failure) - ([(ispec, inst_tys)], NoUnifiers, False) + ([(ispec, inst_tys)], NoUnifiers coherence, False) | short_cut_solver -- Called from the short-cut solver , isOverlappable ispec -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT @@ -207,10 +207,11 @@ matchInstEnv dflags short_cut_solver clas tys -> do { let dfun_id = instanceDFunId ispec ; traceTc "matchClass success" $ vcat [text "dict" <+> ppr pred, + ppr coherence, text "witness" <+> ppr dfun_id <+> ppr (idType dfun_id) ] -- Record that this dfun is needed - ; match_one (null unsafeOverlaps) dfun_id inst_tys } + ; match_one (null unsafeOverlaps) coherence dfun_id inst_tys } -- More than one matches (or Safe Haskell fail!). Defer any -- reactions of a multitude until we learn more about the reagent @@ -221,16 +222,17 @@ matchInstEnv dflags short_cut_solver clas tys where pred = mkClassPred clas tys -match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcM ClsInstResult +match_one :: SafeOverlapping -> Coherence -> DFunId -> [DFunInstType] -> TcM ClsInstResult -- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv -match_one so dfun_id mb_inst_tys +match_one so coherence dfun_id mb_inst_tys = do { traceTc "match_one" (ppr dfun_id $$ ppr mb_inst_tys) ; (tys, theta) <- instDFunType dfun_id mb_inst_tys ; traceTc "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta) - ; return $ OneInst { cir_new_theta = theta - , cir_mk_ev = evDFunApp dfun_id tys - , cir_what = TopLevInstance { iw_dfun_id = dfun_id - , iw_safe_over = so } } } + ; return $ OneInst { cir_new_theta = theta + , cir_mk_ev = evDFunApp dfun_id tys + , cir_coherence = coherence + , cir_what = TopLevInstance { iw_dfun_id = dfun_id + , iw_safe_over = so } } } {- Note [Shortcut solving: overlap] @@ -262,9 +264,10 @@ was a puzzling example. matchCTuple :: Class -> [Type] -> TcM ClsInstResult matchCTuple clas tys -- (isCTupleClass clas) holds - = return (OneInst { cir_new_theta = tys - , cir_mk_ev = tuple_ev - , cir_what = BuiltinInstance }) + = return (OneInst { cir_new_theta = tys + , cir_mk_ev = tuple_ev + , cir_coherence = IsCoherent + , cir_what = BuiltinInstance }) -- The dfun *is* the data constructor! where data_con = tyConSingleDataCon (classTyCon clas) @@ -424,9 +427,10 @@ makeLitDict clas ty et , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] -- SNat n ~ Integer , let ev_tm = mkEvCast et (mkSymCo (mkTransCo co_dict co_rep)) - = return $ OneInst { cir_new_theta = [] - , cir_mk_ev = \_ -> ev_tm - , cir_what = BuiltinInstance } + = return $ OneInst { cir_new_theta = [] + , cir_mk_ev = \_ -> ev_tm + , cir_coherence = IsCoherent + , cir_what = BuiltinInstance } | otherwise = pprPanic "makeLitDict" $ @@ -457,19 +461,9 @@ matchWithDict [cls, mty] -- the WithDict dictionary: -- -- \@(r :: RuntimeRep) @(a :: TYPE r) (sv :: mty) (k :: cls => a) -> - -- nospec @(cls => a) k (sv |> (sub co ; sym co2)) - -- - -- where nospec :: forall a. a -> a ensures that the typeclass specialiser - -- doesn't attempt to common up this evidence term with other evidence terms - -- of the same type. - -- - -- See (WD6) in Note [withDict], and Note [nospecId magic] in GHC.Types.Id.Make. + -- k (sv |> (sub co ; sym co2)) ; let evWithDict co2 = mkCoreLams [ runtimeRep1TyVar, openAlphaTyVar, sv, k ] $ - Var nospecId - `App` - (Type $ mkInvisFunTy cls openAlphaTy) - `App` Var k `App` (Var sv `Cast` mkTransCo (mkSubCo co2) (mkSymCo co)) @@ -482,9 +476,10 @@ matchWithDict [cls, mty] [cls, mty] [evWithDict (evTermCoercion (EvExpr c))] mk_ev e = pprPanic "matchWithDict" (ppr e) - ; return $ OneInst { cir_new_theta = [mkPrimEqPred mty inst_meth_ty] - , cir_mk_ev = mk_ev - , cir_what = BuiltinInstance } + ; return $ OneInst { cir_new_theta = [mkPrimEqPred mty inst_meth_ty] + , cir_mk_ev = mk_ev + , cir_coherence = IsIncoherent -- See (WD6) in Note [withDict] + , cir_what = BuiltinInstance } } matchWithDict _ @@ -587,12 +582,14 @@ Some further observations about `withDict`: (WD6) In fact, we desugar `withDict @cls @mty @{rr} @r` to \@(r :: RuntimeRep) @(a :: TYPE r) (sv :: mty) (k :: cls => a) -> - nospec @(cls => a) k (sv |> (sub co2 ; sym co))) + k (sv |> (sub co2 ; sym co))) - That is, we cast the method using a coercion, and apply k to it. - However, we use the 'nospec' magicId (see Note [nospecId magic] in GHC.Types.Id.Make) - to ensure that the typeclass specialiser doesn't incorrectly common-up distinct - evidence terms. This is super important! Suppose we have calls + That is, we cast the method using a coercion, and apply k to + it. Moreover, we mark the evidence as incoherent, resulting in + the use of the 'nospec' magicId (see Note [nospecId magic] in + GHC.Types.Id.Make) to ensure that the typeclass specialiser + doesn't incorrectly common-up distinct evidence terms. This is + super important! Suppose we have calls withDict A k withDict B k @@ -672,9 +669,10 @@ matchTypeable _ _ = return NoInstance -- | Representation for a type @ty@ of the form @arg -> ret@. doFunTy :: Class -> Type -> Mult -> Type -> Type -> TcM ClsInstResult doFunTy clas ty mult arg_ty ret_ty - = return $ OneInst { cir_new_theta = preds - , cir_mk_ev = mk_ev - , cir_what = BuiltinInstance } + = return $ OneInst { cir_new_theta = preds + , cir_mk_ev = mk_ev + , cir_coherence = IsCoherent + , cir_what = BuiltinInstance } where preds = map (mk_typeable_pred clas) [mult, arg_ty, ret_ty] mk_ev [mult_ev, arg_ev, ret_ev] = evTypeable ty $ @@ -688,9 +686,10 @@ doFunTy clas ty mult arg_ty ret_ty doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult doTyConApp clas ty tc kind_args | tyConIsTypeable tc - = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) kind_args - , cir_mk_ev = mk_ev - , cir_what = BuiltinTypeableInstance tc } + = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) kind_args + , cir_mk_ev = mk_ev + , cir_coherence = IsCoherent + , cir_what = BuiltinTypeableInstance tc } | otherwise = return NoInstance where @@ -719,9 +718,10 @@ doTyApp clas ty f tk | isForAllTy (typeKind f) = return NoInstance -- We can't solve until we know the ctr. | otherwise - = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk] - , cir_mk_ev = mk_ev - , cir_what = BuiltinInstance } + = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk] + , cir_mk_ev = mk_ev + , cir_coherence = IsCoherent + , cir_what = BuiltinInstance } where mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2) mk_ev _ = panic "doTyApp" @@ -739,9 +739,10 @@ doTyLit kc t = do { kc_clas <- tcLookupClass kc ; let kc_pred = mkClassPred kc_clas [ t ] mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev) mk_ev _ = panic "doTyLit" - ; return (OneInst { cir_new_theta = [kc_pred] - , cir_mk_ev = mk_ev - , cir_what = BuiltinInstance }) } + ; return (OneInst { cir_new_theta = [kc_pred] + , cir_mk_ev = mk_ev + , cir_coherence = IsCoherent + , cir_what = BuiltinInstance }) } {- Note [Typeable (T a b c)] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -830,24 +831,27 @@ if you'd written matchHeteroEquality :: [Type] -> TcM ClsInstResult -- Solves (t1 ~~ t2) matchHeteroEquality args - = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ] - , cir_mk_ev = evDataConApp heqDataCon args - , cir_what = BuiltinEqInstance }) + = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ] + , cir_mk_ev = evDataConApp heqDataCon args + , cir_coherence = IsCoherent + , cir_what = BuiltinEqInstance }) matchHomoEquality :: [Type] -> TcM ClsInstResult -- Solves (t1 ~ t2) matchHomoEquality args@[k,t1,t2] - = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ] - , cir_mk_ev = evDataConApp eqDataCon args - , cir_what = BuiltinEqInstance }) + = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ] + , cir_mk_ev = evDataConApp eqDataCon args + , cir_coherence = IsCoherent + , cir_what = BuiltinEqInstance }) matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args) -- See also Note [The equality types story] in GHC.Builtin.Types.Prim matchCoercible :: [Type] -> TcM ClsInstResult matchCoercible args@[k, t1, t2] - = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ] - , cir_mk_ev = evDataConApp coercibleDataCon args - , cir_what = BuiltinEqInstance }) + = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ] + , cir_mk_ev = evDataConApp coercibleDataCon args + , cir_coherence = IsCoherent + , cir_what = BuiltinEqInstance }) where args' = [k, k, t1, t2] matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args) @@ -978,9 +982,10 @@ matchHasField dflags short_cut clas tys then do { -- See Note [Unused name reporting and HasField] addUsedGRE True gre ; keepAlive (greMangledName gre) - ; return OneInst { cir_new_theta = theta - , cir_mk_ev = mk_ev - , cir_what = BuiltinInstance } } + ; return OneInst { cir_new_theta = theta + , cir_mk_ev = mk_ev + , cir_coherence = IsCoherent + , cir_what = BuiltinInstance } } else matchInstEnv dflags short_cut clas tys } _ -> matchInstEnv dflags short_cut clas tys } diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index 6fc5b28ab0..f113820c02 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -2684,13 +2684,13 @@ neededEvVars implic@(Implic { ic_given = givens = needs `unionVarSet` acc needed_ev_bind needed (EvBind { eb_lhs = ev_var - , eb_is_given = is_given }) - | is_given = ev_var `elemVarSet` needed + , eb_info = info }) + | EvBindGiven{} <- info = ev_var `elemVarSet` needed | otherwise = True -- Keep all wanted bindings add_wanted :: EvBind -> VarSet -> VarSet - add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs - | is_given = needs -- Add the rhs vars of the Wanted bindings only + add_wanted (EvBind { eb_info = info, eb_rhs = rhs }) needs + | EvBindGiven{} <- info = needs -- Add the rhs vars of the Wanted bindings only | otherwise = evVarsOfTerm rhs `unionVarSet` needs ------------------------------------------------- diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 8375498a93..b5c65df24a 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -32,6 +32,7 @@ import GHC.Core.TyCo.Rep -- cleverly decomposes types, good for completeness c import GHC.Core.Coercion import GHC.Core.Coercion.Axiom import GHC.Core.Reduction +import GHC.Core.InstEnv ( Coherence(..) ) import GHC.Core import GHC.Types.Id( mkTemplateLocals ) import GHC.Core.FamInstEnv ( FamInstEnvs ) @@ -201,7 +202,7 @@ solveCallStack ev ev_cs = do -- `IP ip CallStack`. See Note [Overview of implicit CallStacks] cs_tm <- evCallStack ev_cs let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev)) - setEvBindIfWanted ev ev_tm + setEvBindIfWanted ev IsCoherent ev_tm canClass :: CtEvidence -> Class -> [Type] @@ -889,7 +890,7 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo ; ev_binds <- emitImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs given_ev_vars wanteds - ; setWantedEvTerm dest $ + ; setWantedEvTerm dest IsCoherent $ EvFun { et_tvs = skol_tvs, et_given = given_ev_vars , et_binds = ev_binds, et_body = w_id } @@ -1071,7 +1072,7 @@ can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _ -- Literals can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ | l1 == l2 - = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1) + = do { setEvBindIfWanted ev IsCoherent (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1) ; stopWith ev "Equal LitTy" } -- Decompose FunTy: (s -> t) and (c => t) @@ -2650,8 +2651,7 @@ canEqReflexive :: CtEvidence -- ty ~ ty -> TcType -- ty -> TcS (StopOrContinue Ct) -- always Stop canEqReflexive ev eq_rel ty - = do { setEvBindIfWanted ev (evCoercion $ - mkReflCo (eqRelRole eq_rel) ty) + = do { setEvBindIfWanted ev IsCoherent (evCoercion $ mkReflCo (eqRelRole eq_rel) ty) ; stopWith ev "Solved by reflexivity" } rewriteCastedEquality :: CtEvidence -- :: lhs ~ (rhs |> mco), or (rhs |> mco) ~ lhs @@ -3225,9 +3225,9 @@ rewriteEvidence new_rewriters (Reduction co new_pred) = do { mb_new_ev <- newWanted loc rewriters' new_pred ; massert (coercionRole co == ctEvRole ev) - ; setWantedEvTerm dest - (mkEvCast (getEvExpr mb_new_ev) - (downgradeRole Representational (ctEvRole ev) (mkSymCo co))) + ; setWantedEvTerm dest IsCoherent $ + mkEvCast (getEvExpr mb_new_ev) + (downgradeRole Representational (ctEvRole ev) (mkSymCo co)) ; case mb_new_ev of Fresh new_ev -> continueWith new_ev Cached _ -> stopWith ev "Cached wanted" } diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index df53e39fcd..d92dca7e3d 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -32,7 +32,7 @@ import GHC.Tc.Solver.Monad import GHC.Core import GHC.Core.Type as Type -import GHC.Core.InstEnv ( DFunInstType ) +import GHC.Core.InstEnv ( DFunInstType, Coherence(..) ) import GHC.Core.Class import GHC.Core.TyCon import GHC.Core.Predicate @@ -231,7 +231,7 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 }) where setEv :: (EvTerm,Ct) -> TcS () setEv (ev,ct) = case ctEvidence ct of - CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev + CtWanted { ctev_dest = dest } -> setWantedEvTerm dest IsCoherent ev -- TODO: plugins should be able to signal non-coherence _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!" -- | A pair of (given, wanted) constraints to pass to plugins @@ -665,9 +665,9 @@ interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason }) vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w)) , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ] ; case solveOneFromTheOther ct_i ct_w of - KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i) + KeepInert -> do { setEvBindIfWanted ev_w IsCoherent (swap_me swap ev_i) ; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) } - KeepWork -> do { setEvBindIfWanted ev_i (swap_me swap ev_w) + KeepWork -> do { setEvBindIfWanted ev_i IsCoherent (swap_me swap ev_w) ; updInertIrreds (\_ -> others) ; continueWith ct_w } } @@ -1028,10 +1028,10 @@ interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = t -- the inert from the work-item or vice-versa. ; case solveOneFromTheOther ct_i ct_w of KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr ct_w) - ; setEvBindIfWanted ev_w (ctEvTerm ev_i) + ; setEvBindIfWanted ev_w IsCoherent (ctEvTerm ev_i) ; return $ Stop ev_w (text "Dict equal" <+> ppr ct_w) } KeepWork -> do { traceTcS "lookupInertDict:KeepWork" (ppr ct_w) - ; setEvBindIfWanted ev_i (ctEvTerm ev_w) + ; setEvBindIfWanted ev_i IsCoherent (ctEvTerm ev_w) ; updInertDicts $ \ ds -> delDict ds cls tys ; continueWith ct_w } } } @@ -1102,9 +1102,10 @@ shortCutSolver dflags ev_w ev_i , ClassPred cls tys <- classifyPredType pred = do { inst_res <- lift $ matchGlobalInst dflags True cls tys ; case inst_res of - OneInst { cir_new_theta = preds - , cir_mk_ev = mk_ev - , cir_what = what } + OneInst { cir_new_theta = preds + , cir_mk_ev = mk_ev + , cir_coherence = coherence + , cir_what = what } | safeOverlap what , all isTyFamFree preds -- Note [Shortcut solving: type families] -> do { let solved_dicts' = addDict solved_dicts cls tys ev @@ -1123,7 +1124,7 @@ shortCutSolver dflags ev_w ev_i ; let ev_tm = mk_ev (map getEvExpr evc_vs) ev_binds' = extendEvBinds ev_binds $ - mkWantedEvBind (ctEvEvId ev) ev_tm + mkWantedEvBind (ctEvEvId ev) coherence ev_tm ; foldlM try_solve_from_instance (ev_binds', solved_dicts') @@ -1539,7 +1540,7 @@ interactEq inerts workItem@(CEqCan { cc_lhs = lhs , cc_ev = ev , cc_eq_rel = eq_rel }) | Just (ev_i, swapped) <- inertsCanDischarge inerts workItem - = do { setEvBindIfWanted ev $ + = do { setEvBindIfWanted ev IsCoherent $ evCoercion (maybeSymCo swapped $ downgradeRole (eqRelRole eq_rel) (ctEvRole ev_i) @@ -1608,7 +1609,7 @@ solveByUnification wd tv xi text "Left Kind is:" <+> ppr (typeKind tv_ty), text "Right Kind is:" <+> ppr (typeKind xi) ] ; unifyTyVar tv xi - ; setEvBindIfWanted wd (evCoercion (mkNomReflCo xi)) + ; setEvBindIfWanted wd IsCoherent (evCoercion (mkNomReflCo xi)) ; n_kicked <- kickOutAfterUnification tv ; return (Stop wd (text "Solved by unification" <+> pprKicked n_kicked)) } @@ -2269,7 +2270,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls -- See Note [No Given/Given fundeps] | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached - = do { setEvBindIfWanted ev (ctEvTerm solved_ev) + = do { setEvBindIfWanted ev IsCoherent (ctEvTerm solved_ev) ; stopWith ev "Dict/Top (cached)" } | otherwise -- Wanted, but not cached @@ -2305,7 +2306,7 @@ tryLastResortProhibitedSuperclass inerts , Just ct_i <- lookupInertDict (inert_cans inerts) loc_w cls xis , let ev_i = ctEvidence ct_i , isGiven ev_i - = do { setEvBindIfWanted ev_w (ctEvTerm ev_i) + = do { setEvBindIfWanted ev_w IsCoherent (ctEvTerm ev_i) ; ctLocWarnTcS loc_w $ TcRnLoopySuperclassSolve loc_w (ctPred work_item) ; return $ Stop ev_w (text "Loopy superclass") } @@ -2314,9 +2315,10 @@ tryLastResortProhibitedSuperclass _ work_item chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct) chooseInstance work_item - (OneInst { cir_new_theta = theta - , cir_what = what - , cir_mk_ev = mk_ev }) + (OneInst { cir_new_theta = theta + , cir_what = what + , cir_mk_ev = mk_ev + , cir_coherence = coherence }) = do { traceTcS "doTopReact/found instance for" $ ppr ev ; deeper_loc <- checkInstanceOK loc what pred ; checkReductionDepth deeper_loc pred @@ -2326,7 +2328,7 @@ chooseInstance work_item -- See Note [Instances in no-evidence implications] else do { evc_vars <- mapM (newWanted deeper_loc (ctRewriters work_item)) theta - ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars)) + ; setEvBindIfWanted ev coherence (mk_ev (map getEvExpr evc_vars)) ; emitWorkNC (freshGoals evc_vars) ; stopWith ev "Dict/Top (solved wanted)" }} where @@ -2591,9 +2593,10 @@ matchLocalInst pred loc { Just (dfun_id, tys, theta) | all ((theta `impliedBySCs`) . thdOf3) unifs -> - do { let result = OneInst { cir_new_theta = theta - , cir_mk_ev = evDFunApp dfun_id tys - , cir_what = LocalInstance } + do { let result = OneInst { cir_new_theta = theta + , cir_mk_ev = evDFunApp dfun_id tys + , cir_coherence = IsCoherent + , cir_what = LocalInstance } ; traceTcS "Best local instance found:" $ vcat [ text "pred:" <+> ppr pred , text "result:" <+> ppr result diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 7ff59baf4e..ad4e10ebf6 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -1701,19 +1701,19 @@ setWantedEq (HoleDest hole) co setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq: EvVarDest" (ppr ev) -- | Good for both equalities and non-equalities -setWantedEvTerm :: TcEvDest -> EvTerm -> TcS () -setWantedEvTerm (HoleDest hole) tm +setWantedEvTerm :: TcEvDest -> Coherence -> EvTerm -> TcS () +setWantedEvTerm (HoleDest hole) _coherence tm | Just co <- evTermCoercion_maybe tm = do { useVars (coVarsOfCo co) ; fillCoercionHole hole co } | otherwise = -- See Note [Yukky eq_sel for a HoleDest] do { let co_var = coHoleCoVar hole - ; setEvBind (mkWantedEvBind co_var tm) + ; setEvBind (mkWantedEvBind co_var IsCoherent tm) ; fillCoercionHole hole (mkCoVarCo co_var) } -setWantedEvTerm (EvVarDest ev_id) tm - = setEvBind (mkWantedEvBind ev_id tm) +setWantedEvTerm (EvVarDest ev_id) coherence tm + = setEvBind (mkWantedEvBind ev_id coherence tm) {- Note [Yukky eq_sel for a HoleDest] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1739,10 +1739,10 @@ fillCoercionHole hole co = do { wrapTcS $ TcM.fillCoercionHole hole co ; kickOutAfterFillingCoercionHole hole } -setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS () -setEvBindIfWanted ev tm +setEvBindIfWanted :: CtEvidence -> Coherence -> EvTerm -> TcS () +setEvBindIfWanted ev coherence tm = case ev of - CtWanted { ctev_dest = dest } -> setWantedEvTerm dest tm + CtWanted { ctev_dest = dest } -> setWantedEvTerm dest coherence tm _ -> return () newTcEvBinds :: TcS EvBindsVar diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 9213ceeab2..e3e7057bfa 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -1463,7 +1463,7 @@ tcSuperClasses skol_info dfun_id cls tyvars dfun_evs dfun_ev_binds sc_theta ; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls)) ; sc_ev_id <- newEvVar sc_pred - ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm + ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id IsCoherent sc_ev_tm ; let sc_top_ty = tcMkDFunSigmaTy tyvars (map idType dfun_evs) sc_pred sc_top_id = mkLocalId sc_top_name ManyTy sc_top_ty export = ABE { abe_wrap = idHsWrapper diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index 5d69962865..139d46fc98 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -22,7 +22,7 @@ module GHC.Tc.Types.Evidence ( isEmptyEvBindMap, evBindMapToVarSet, varSetMinusEvBindMap, - EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind, + EvBindInfo(..), EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind, evBindVar, isCoEvBindsVar, -- * EvTerm (already a CoreExpr) @@ -70,6 +70,7 @@ import GHC.Types.Basic import GHC.Core import GHC.Core.Class (Class, classSCSelId ) import GHC.Core.FVs ( exprSomeFreeVars ) +import GHC.Core.InstEnv ( Coherence(..) ) import GHC.Utils.Misc import GHC.Utils.Panic @@ -447,24 +448,29 @@ varSetMinusEvBindMap vs (EvBindMap dve) = vs `uniqSetMinusUDFM` dve instance Outputable EvBindMap where ppr (EvBindMap m) = ppr m +data EvBindInfo + = EvBindGiven { -- See Note [Tracking redundant constraints] in GHC.Tc.Solver + } + | EvBindWanted { ebi_coherence :: Coherence -- See Note [Desugaring incoherent evidence] + } + ----------------- -- All evidence is bound by EvBinds; no side effects data EvBind - = EvBind { eb_lhs :: EvVar - , eb_rhs :: EvTerm - , eb_is_given :: Bool -- True <=> given - -- See Note [Tracking redundant constraints] in GHC.Tc.Solver + = EvBind { eb_lhs :: EvVar + , eb_rhs :: EvTerm + , eb_info :: EvBindInfo } evBindVar :: EvBind -> EvVar evBindVar = eb_lhs -mkWantedEvBind :: EvVar -> EvTerm -> EvBind -mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm } +mkWantedEvBind :: EvVar -> Coherence -> EvTerm -> EvBind +mkWantedEvBind ev c tm = EvBind { eb_info = EvBindWanted c, eb_lhs = ev, eb_rhs = tm } -- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm mkGivenEvBind :: EvVar -> EvTerm -> EvBind -mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm } +mkGivenEvBind ev tm = EvBind { eb_info = EvBindGiven, eb_lhs = ev, eb_rhs = tm } -- An EvTerm is, conceptually, a CoreExpr that implements the constraint. @@ -845,8 +851,7 @@ findNeededEvVars ev_binds seeds add :: Var -> VarSet -> VarSet add v needs | Just ev_bind <- lookupEvBind ev_binds v - , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind - , is_given + , EvBind { eb_info = EvBindGiven, eb_rhs = rhs } <- ev_bind = evVarsOfTerm rhs `unionVarSet` needs | otherwise = needs @@ -940,12 +945,14 @@ instance Uniquable EvBindsVar where getUnique = ebv_uniq instance Outputable EvBind where - ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given }) + ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_info = info }) = sep [ pp_gw <+> ppr v , nest 2 $ equals <+> ppr e ] + -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing where - pp_gw = brackets (if is_given then char 'G' else char 'W') - -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing + pp_gw = brackets $ case info of + EvBindGiven{} -> char 'G' + EvBindWanted{} -> char 'W' instance Outputable EvTerm where ppr (EvExpr e) = ppr e diff --git a/docs/users_guide/9.8.1-notes.rst b/docs/users_guide/9.8.1-notes.rst index ad6f6f3709..a4230ffcca 100644 --- a/docs/users_guide/9.8.1-notes.rst +++ b/docs/users_guide/9.8.1-notes.rst @@ -27,6 +27,12 @@ Compiler This is convenient for TH code generation, as you can now uniformly use record wildcards regardless of number of fields. +- Incoherent instance applications are no longer specialised. The previous implementation of + specialisation resulted in nondeterministic instance resolution in certain cases, breaking + the specification described in the documentation of the `INCOHERENT` pragma. See GHC ticket + #22448 for further details. + + GHCi ~~~~ diff --git a/testsuite/tests/simplCore/should_run/T22448.hs b/testsuite/tests/simplCore/should_run/T22448.hs new file mode 100644 index 0000000000..97eb3064ba --- /dev/null +++ b/testsuite/tests/simplCore/should_run/T22448.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE MonoLocalBinds #-} +class C a where + op :: a -> String + +instance {-# OVERLAPPABLE #-} C a where + op _ = "C a" + {-# NOINLINE op #-} + +instance {-# INCOHERENT #-} C () where + op _ = "C ()" + {-# NOINLINE op #-} + +-- | Inhibit inlining, but keep specialize-ability +large :: a -> a +large x = x +{-# NOINLINE large #-} + +bar :: C a => a -> String +bar x = large (large (large (large (large (large (large (large (large (large (large (large (large (large (op x)))))))))))))) + +spec :: () -> String -- C () constraint is resolved to the specialized instance +spec = bar + +gen :: a -> String -- No C a constraint, has to choose the incoherent generic instance +gen = bar + +main :: IO () +main = do + putStrLn $ "spec () == " <> spec () + putStrLn $ "gen () == " <> gen () diff --git a/testsuite/tests/simplCore/should_run/T22448.stdout b/testsuite/tests/simplCore/should_run/T22448.stdout new file mode 100644 index 0000000000..bccf7a973a --- /dev/null +++ b/testsuite/tests/simplCore/should_run/T22448.stdout @@ -0,0 +1,2 @@ +spec () == C () +gen () == C a diff --git a/testsuite/tests/simplCore/should_run/all.T b/testsuite/tests/simplCore/should_run/all.T index a887d5cedb..527f44a1bc 100644 --- a/testsuite/tests/simplCore/should_run/all.T +++ b/testsuite/tests/simplCore/should_run/all.T @@ -107,3 +107,4 @@ test('T21229', normal, compile_and_run, ['-O']) test('T21575', normal, compile_and_run, ['-O']) test('T21575b', [], multimod_compile_and_run, ['T21575b', '-O']) test('T20836', normal, compile_and_run, ['-O0']) # Should not time out; See #20836 +test('T22448', normal, compile_and_run, ['-O1']) |