[Git][ghc/ghc][master] Don't specialise incoherent instance applications
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Tue Feb 28 01:04:05 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
b56025f4 by Gergő Érdi at 2023-02-27T13:34:22+00:00
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 changed files:
- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/HsToCore/Arrows.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Binds.hs-boot
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/HsToCore/Match/Constructor.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/Pmc/Desugar.hs
- compiler/GHC/HsToCore/Quote.hs
- compiler/GHC/HsToCore/Types.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types/Evidence.hs
- docs/users_guide/9.8.1-notes.rst
- + testsuite/tests/simplCore/should_run/T22448.hs
- + testsuite/tests/simplCore/should_run/T22448.stdout
- testsuite/tests/simplCore/should_run/all.T
Changes:
=====================================
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 at 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.
+
************************************************************************
=====================================
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) ;
=====================================
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)
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -16,7 +16,7 @@ lower levels it is preserved with @let@/@letrec at 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) } }
{-**********************************************************************
=====================================
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
=====================================
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) } } }
=====================================
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
=====================================
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
=====================================
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) }
=====================================
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
=====================================
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
=====================================
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
=====================================
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
=====================================
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 at .
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 }
=====================================
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
-------------------------------------------------
=====================================
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" }
=====================================
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
=====================================
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
=====================================
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
=====================================
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
=====================================
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
~~~~
=====================================
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 ()
=====================================
testsuite/tests/simplCore/should_run/T22448.stdout
=====================================
@@ -0,0 +1,2 @@
+spec () == C ()
+gen () == C a
=====================================
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'])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b56025f448646de40446a133f140f62c8a49cabf
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b56025f448646de40446a133f140f62c8a49cabf
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230227/35d9b0cc/attachment-0001.html>
More information about the ghc-commits
mailing list