Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 6caa6508 by Adam Gundry at 2025-04-20T10:54:22-04:00 Fix specialisation of incoherent instances (fixes #25883) GHC normally assumes that class constraints are canonical, meaning that the specialiser is allowed to replace one dictionary argument with another provided that they have the same type. The `-fno-specialise-incoherents` flag alters INCOHERENT instance definitions so that they will prevent specialisation in some cases, by inserting `nospec`. This commit fixes a bug in 7124e4ad76d98f1fc246ada4fd7bf64413ff2f2e, which treated some INCOHERENT instance matches as if `-fno-specialise-incoherents` was in effect, thereby unnecessarily preventing specialisation. In addition it updates the relevant `Note [Rules for instance lookup]` and adds a new `Note [Canonicity for incoherent matches]`. - - - - - 0426fd6c by Adam Gundry at 2025-04-20T10:54:23-04:00 Add regression test for #23429 - - - - - eec96527 by Adam Gundry at 2025-04-20T10:54:23-04:00 user's guide: update specification of overlapping/incoherent instances The description of the instance resolution algorithm in the user's guide was slightly out of date, because it mentioned in-scope given constraints only at the end, whereas the implementation checks for their presence before any of the other steps. This also adds a warning to the user's guide about the impact of incoherent instances on specialisation, and more clearly documents some of the other effects of `-XIncoherentInstances`. - - - - - 16 changed files: - compiler/GHC/Core/InstEnv.hs - compiler/GHC/Tc/Solver/Dict.hs - docs/users_guide/exts/instances.rst - + testsuite/tests/simplCore/should_compile/T25883.hs - + testsuite/tests/simplCore/should_compile/T25883.substr-simpl - + testsuite/tests/simplCore/should_compile/T25883b.hs - + testsuite/tests/simplCore/should_compile/T25883b.substr-simpl - + testsuite/tests/simplCore/should_compile/T25883c.hs - + testsuite/tests/simplCore/should_compile/T25883c.substr-simpl - + testsuite/tests/simplCore/should_compile/T25883d.hs - + testsuite/tests/simplCore/should_compile/T25883d.stderr - + testsuite/tests/simplCore/should_compile/T25883d_import.hs - testsuite/tests/simplCore/should_compile/all.T - + testsuite/tests/simplCore/should_run/T23429.hs - + testsuite/tests/simplCore/should_run/T23429.stdout - testsuite/tests/simplCore/should_run/all.T Changes: ===================================== compiler/GHC/Core/InstEnv.hs ===================================== @@ -599,7 +599,7 @@ These functions implement the carefully-written rules in the user manual section on "overlapping instances". At risk of duplication, here are the rules. If the rules change, change this text and the user manual simultaneously. The link may be this: -http://www.haskell.org/ghc/docs/latest/html/users_guide/glasgow_exts.html#in... +https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/instances.htm... The willingness to be overlapped or incoherent is a property of the instance declaration itself, controlled by its `OverlapMode`, as follows @@ -627,14 +627,22 @@ of the target constraint (C ty1 .. tyn). The search works like this. (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.Dict. - -(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/. - -(IL2) If there are no candidates, the search fails. + the search fails unless -XIncoherentInstances is enabled. See + Note [Instance and Given overlap] in GHC.Tc.Solver.Dict. This is + implemented by the first guard in matchClassInst. + +(IL1) Find `all_matches` and `all_unifs` in `lookupInstEnv`: + - all_matches: 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/. + - all_unifs: all non-incoherent instances that *unify with but do not match* + the target constraint. These are not candidates, but might match later if + the target constraint is furhter instantiated. See + `data PotentialUnifiers` for more precise details. + +(IL2) If there are no candidates, the search fails + (lookupInstEnv returns no final_matches). The PotentialUnifiers are returned + by lookupInstEnv for use in error message generation (mkDictErr). (IL3) Eliminate any candidate `IX` for which there is another candidate `IY` such that both of the following hold: @@ -644,29 +652,39 @@ of the target constraint (C ty1 .. tyn). The search works like 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.) - This is done by `pruneOverlappingMatches` -(IL4) If all the remaining candidates are *incoherent*, the search succeeds, - returning an arbitrary surviving candidate. + In addition, provided there is at least one candidate, eliminate any other + candidates that are *incoherent*. (In particular, if all remaining candidates + are incoherent, all except an arbitrarily chosen one will be eliminated.) + + This is implemented by `pruneOverlappedMatches`, producing final_matches in + lookupInstEnv. See Note [Instance overlap and guards] and + Note [Incoherent instances]. + +(IL4) If exactly one *incoherent* candidate remains, the search succeeds. + (By the previous step, there cannot be more than one incoherent candidate + remaining.) - If any coherent or non-canonical incoherent unifiers were discarded, - return NoUnifiers EvNonCanonical; if only canonical incoherent unifiers - were discarded, return NoUnifiers EvCanonical + In this case, lookupInstEnv returns the successful match, and it returns + NoUnifiers as the final_unifs, which amounts to skipping the following + steps. -(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". +(IL5) If more than one candidate remains, the search fails. (We have already + eliminated the incoherent candidates, and we have no way to select + between non-incoherent candidates.) -(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. +(IL6) Otherwise there is exactly one candidate remaining. The all_unifs + computed at step (IL1) are returned from lookupInstEnv as final_unifs. - If any are *coherent* (not incoherent) return them - as PotentialUnifiers. + If there are no potential unifiers, the search succeeds (in matchInstEnv). + If there is at least one (non-incoherent) potential unifier, matchInstEnv + returns a NotSure result and refrains from committing to the instance. + + Incoherent instances are not returned as part of the potential unifiers. This + affects error messages: they will not be listed as "potentially matching instances" + in an "Overlapping instances" or "Ambiguous type variable" error. + See also Note [Recording coherence information in `PotentialUnifiers`]. - If all are *incoherent* (OverlapFlag = Incoherent or NonCanonical) - return (NoUnifiers nc), where nc is EvNonCanonical if any of the discarded - unifiers are NonCanonical. Notice that these rules are not influenced by flag settings in the client module, where the instances are *used*. These rules make it @@ -894,8 +912,8 @@ instances, i.e. with `-fno-specialise-incoherents`. To avoid this incoherence breaking the specialiser, -* We label as "non-canonical" the dictionary constructed by a (potentially) - incoherent use of an ClsInst whose `OverlapFlag` is `NonCanonical`. +* We label as "non-canonical" any dictionary constructed by a (potentially) + incoherent use of an ClsInst. * We do not specialise a function if there is a non-canonical dictionary in the /transistive dependencies/ of its dictionary @@ -922,7 +940,9 @@ 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. + in step (IL4) or (IL6) of the instance lookup: see + Note [Recording coherence information in `PotentialUnifiers`] and + Note [Canonicity for incoherent matches]. * 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. @@ -930,6 +950,47 @@ Here are the moving parts: * In the desugarer we exploit this info: see Note [Desugaring non-canonical evidence] in GHC.HsToCore.Expr. See also Note [nospecId magic] in GHC.Types.Id.Make. + + +Note [Canonicity for incoherent matches] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When the selected instance is INCOHERENT at step (IL4) of +Note [Rules for instance lookup], we ignore all unifiers, +whether or not they are marked with INCOHERENT pragmas. +This is implemented by returning NoUnifiers in final_unifs. +NoUnifiers takes an argument indicating whether the match was canonical +as described in Note [Coherence and specialisation: overview] and +Note [Recording coherence information in `PotentialUnifiers`]. + +To determine whether an incoherent match was canonical, we look *only* +at the OverlapFlag of the instance being matched. For example: + + class C a + instance {-# INCOHERENT #-} C a -- (1) + instance C Int -- (2) + + [W] C tau + +Here we match instance (1) and discard instance (2). If (1) is Incoherent +(under -fspecialise-incoherents), it is important that we treat the match +as EvCanonical so that we do not block specialisation (see #25883). + +What about the following situation: + + instance {-# INCOHERENT #-} C a -- (1), in a module with -fspecialise-incoherents (Incoherent) + instance {-# INCOHERENT #-} C Int -- (2), in a module with -fno-specialise-incoherents (NonCanonical) + + [W] C tau + +Again we match instance (1) and discard instance (2). It is not obvious +whether Incoherent or NonCanonical should "win" here, but it seems more +consistent with the previous example to look only at the flag on instance (1). + +What about if the only instance that can match is marked as NonCanonical? +In this case are no unifiers at all, so all_unifs = NoUnifiers EvCanonical. +It is not obvious what -fno-specialise-incoherents should do here, but +currently it returns NoUnifiers EvCanonical. + -} type DFunInstType = Maybe Type @@ -1070,8 +1131,8 @@ data PotentialUnifiers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we find a matching instance, there might be other instances that could potentially unify with the goal. For `INCOHERENT` instances, we -don't care (see steps IL4 and IL6 in Note [Rules for instance -lookup]). But if we have potentially unifying coherent instance, we +don't care (see step (IL6) in Note [Rules for instance lookup]). +But if we have potentially unifying coherent instance, we report these `OneOrMoreUnifiers` so that `matchInstEnv` can go down the `NotSure` route. @@ -1081,6 +1142,21 @@ solution is canonical or not (see Note [Coherence and specialisation: overview] for why we care at all). So when the set of potential unifiers is empty, we record in `NoUnifiers` if the one solution is `Canonical`. + +For example, suppose we have: + + class C x y + instance C a Bool -- (1) + instance {-# INCOHERENT #-} C Int a -- (2) + + [W] C x Bool + +Here instance (1) matches the Wanted, and since instance (2) is INCOHERENT +we want to succeed with the match rather than getting stick at step (IL6). +But if -fno-specialise-incoherents was enabled for (2), the specialiser is +not permitted to specialise this dictionary later, so lookupInstEnv reports +the PotentialUnifiers as NoUnifiers EvNonCanonical. + -} instance Outputable CanonicalEvidence where @@ -1101,10 +1177,18 @@ getCoherentUnifiers :: PotentialUnifiers -> [ClsInst] getCoherentUnifiers NoUnifiers{} = [] getCoherentUnifiers (OneOrMoreUnifiers cls) = NE.toList cls +-- | Are there no *coherent* unifiers? nullUnifiers :: PotentialUnifiers -> Bool nullUnifiers NoUnifiers{} = True nullUnifiers _ = False +-- | Are there any unifiers, ignoring those marked Incoherent (but including any +-- marked NonCanonical)? +someUnifiers :: PotentialUnifiers -> Bool +someUnifiers (NoUnifiers EvCanonical) = False +someUnifiers _ = True + + instEnvMatchesAndUnifiers :: InstEnv -- InstEnv to look in -> VisibleOrphanModules -- But filter against this @@ -1209,10 +1293,13 @@ lookupInstEnv check_overlap_safe tys = (final_matches, final_unifs, unsafe_overlapped) where + -- (IL1): Find all instances that match the target constraint (home_matches, home_unifs) = instEnvMatchesAndUnifiers home_ie vis_mods cls tys (pkg_matches, pkg_unifs) = instEnvMatchesAndUnifiers pkg_ie vis_mods cls tys all_matches = home_matches <> pkg_matches all_unifs = home_unifs <> pkg_unifs + + -- (IL3): Eliminate candidates that are overlapped or incoherent 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 @@ -1230,10 +1317,13 @@ lookupInstEnv check_overlap_safe (m:ms) | isIncoherent (fst m) -- Incoherent match, so discard all unifiers, but -- keep track of dropping coherent or non-canonical ones + -- if the match is non-canonical. + -- See Note [Canonicity for incoherent matches] -> assertPpr (null ms) (ppr final_matches) $ - case all_unifs of - OneOrMoreUnifiers{} -> NoUnifiers EvNonCanonical - NoUnifiers{} -> all_unifs + NoUnifiers $ + if isNonCanonical (fst m) && someUnifiers all_unifs + then EvNonCanonical + else EvCanonical _ -> all_unifs -- Note [Safe Haskell isSafeOverlap] ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -926,7 +926,8 @@ matchClassInst dflags inerts clas tys loc -- First check whether there is an in-scope Given that could -- match this constraint. In that case, do not use any instance -- whether top level, or local quantified constraints. --- See Note [Instance and Given overlap] +-- See Note [Instance and Given overlap] and see +-- (IL0) in Note [Rules for instance lookup] in GHC.Core.InstEnv | not (xopt LangExt.IncoherentInstances dflags) , not (isCTupleClass clas) -- It is always safe to unpack constraint tuples ===================================== docs/users_guide/exts/instances.rst ===================================== @@ -417,7 +417,7 @@ Overlapping instances :status: Deprecated Deprecated extension to weaken checks intended to ensure instance resolution - termination. + termination. Use ``OVERLAPPING``, ``OVERLAPPABLE`` or ``OVERLAPS`` pragmas instead. .. extension:: IncoherentInstances :shortdesc: Allow definitions of instances that may result in incoherence. @@ -429,7 +429,9 @@ Overlapping instances :status: Deprecated Deprecated extension to weaken checks intended to ensure instance resolution - termination. + termination. Use ``INCOHERENT`` pragmas instead. Also permits classes to + have non-nominal roles, and affects the instance resolution algorithm for + in-scope given constraints. In general, as discussed in :ref:`instance-resolution`, *GHC requires that it be unambiguous which instance declaration should be used to @@ -473,11 +475,15 @@ 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: +- If there are any in-scope given constraints that might match the target + constraint (after unifying any metavariables), and + :extension:`IncoherentInstances` is not enabled, the search fails. + - Find all instances :math:`I` that *match* the target constraint; that is, the target constraint is a substitution instance of :math:`I`. These instance declarations are the *candidates*. -- If no candidates remain, the search fails +- If there are no candidates, the search fails. - Eliminate any candidate :math:`IX` for which there is another candidate :math:`IY` such that both of the following hold: @@ -498,7 +504,7 @@ like this: - Otherwise there is exactly one non-incoherent candidate; call it the "prime candidate". -- Now find all instances, or in-scope given constraints, that *unify* with +- 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 @@ -596,8 +602,8 @@ declaration, thus: :: (You need :extension:`FlexibleContexts` to do this.) -In the unification check in the final bullet, GHC also uses the -"in-scope given constraints". Consider for example :: +As an example of the "in-scope given constraints" in the first bullet, +consider :: instance C a Int @@ -609,7 +615,7 @@ top-level instance, because a particular call of ``g`` might instantiate both ``b`` and ``c`` to the same type, which would allow the constraint to be solved in a different way. This latter restriction is principally to make the constraint-solver complete. -(Interested folk can read ``Note [Instance and Given overlap]`` in ``TcInteract``.) +(Interested folk can read ``Note [Instance and Given overlap]`` in ``GHC.Tc.Solver.Dict``.) It is easy to avoid: in a type signature avoid a constraint that matches a top-level instance. The flag :ghc-flag:`-Wsimplifiable-class-constraints` warns about such signatures. @@ -660,6 +666,22 @@ matches a top-level instance. The flag :ghc-flag:`-Wsimplifiable-class-constrai to reject module ``Help`` on the grounds that a later instance declaration might overlap the local one.) +.. warning:: + GHC's optimiser (in particular, the :ghc-flag:`-fspecialise` option) + assumes that type-classes are coherent, and hence it may replace + any type-class dictionary argument with another dictionary of the same + type. + + This may cause unexpected results if incoherence occurs due to incoherent + or overlapping instances, and there is an observable difference between the + instances (see :ghc-ticket:`22448` and :ghc-ticket:`24924` for examples). + + The :ghc-flag:`-fno-specialise-incoherents <-fspecialise-incoherents>` will + inhibit specialisation in the presence of some incoherent instance matches, + which may help avoid this issue at the cost of runtime performance. + Alternatively, specialisation can be disabled entirely with + :ghc-flag:`-fno-specialise <-fspecialise>`. + .. _instance-sigs: Instance signatures: type signatures in instance declarations ===================================== testsuite/tests/simplCore/should_compile/T25883.hs ===================================== @@ -0,0 +1,20 @@ +-- By default -fspecialise-incoherents is in effect, so the call to m in f +-- should get specialised even though there is another potential instance. + +{-# LANGUAGE UndecidableInstances #-} +module T25833 (y) where + +class C a where + m :: a -> a + +instance {-# INCOHERENT #-} Num a => C a where + m = (* 3) + +instance C () where + m = id + +f :: Num a => a -> a +f = m + +y :: Int +y = f 2 ===================================== testsuite/tests/simplCore/should_compile/T25883.substr-simpl ===================================== @@ -0,0 +1 @@ +y = I# 6# \ No newline at end of file ===================================== testsuite/tests/simplCore/should_compile/T25883b.hs ===================================== @@ -0,0 +1,21 @@ +-- Under -fno-specialise-incoherents, the call to m in f should not be +-- specialised, because there is another possible (though unused) instance. + +{-# OPTIONS_GHC -fno-specialise-incoherents #-} +{-# LANGUAGE UndecidableInstances #-} +module T25833b (y) where + +class C a where + m :: a -> a + +instance {-# INCOHERENT #-} Num a => C a where + m = (* 3) + +instance C () where + m = id + +f :: Num a => a -> a +f = m + +y :: Int +y = f 2 ===================================== testsuite/tests/simplCore/should_compile/T25883b.substr-simpl ===================================== @@ -0,0 +1 @@ +y = nospec m \ No newline at end of file ===================================== testsuite/tests/simplCore/should_compile/T25883c.hs ===================================== @@ -0,0 +1,18 @@ +-- Here -fno-specialise-incoherents is in effect, but f refers unambiguously to +-- a single instance (because there are no others), so it should be specialised. + +{-# OPTIONS_GHC -fno-specialise-incoherents #-} +{-# LANGUAGE UndecidableInstances #-} +module T25833c (y) where + +class C a where + m :: a -> a + +instance {-# INCOHERENT #-} Num a => C a where + m = (* 3) + +f :: Num a => a -> a +f = m + +y :: Int +y = f 2 ===================================== testsuite/tests/simplCore/should_compile/T25883c.substr-simpl ===================================== @@ -0,0 +1 @@ +y = I# 6# \ No newline at end of file ===================================== testsuite/tests/simplCore/should_compile/T25883d.hs ===================================== @@ -0,0 +1,14 @@ +{-# OPTIONS_GHC -fno-specialise-incoherents #-} + +module T25883d (y) where + +import T25883d_import + +instance {-# INCOHERENT #-} C () where + m = id + +f :: Num a => a -> a +f = m + +y :: Int +y = f 2 \ No newline at end of file ===================================== testsuite/tests/simplCore/should_compile/T25883d.stderr ===================================== @@ -0,0 +1 @@ +y = I# 6# ===================================== testsuite/tests/simplCore/should_compile/T25883d_import.hs ===================================== @@ -0,0 +1,11 @@ +-- This module defines an instance with -fspecialise-incoherents in effect, +-- then it will be imported by a module that uses -fno-specialise-incoherents. + +{-# LANGUAGE UndecidableInstances #-} +module T25883d_import where + +class C a where + m :: a -> a + +instance {-# INCOHERENT #-} Num a => C a where + m = (* 3) ===================================== testsuite/tests/simplCore/should_compile/all.T ===================================== @@ -536,3 +536,8 @@ test('T25197', [req_th, extra_files(["T25197_TH.hs"]), only_ways(['optasm'])], m test('T25389', normal, compile, ['-O -ddump-simpl -dsuppress-uniques -dno-typeable-binds']) test('T24359a', normal, compile, ['-O -ddump-rules']) test('T25713', [grep_errmsg('W:::')], compile, ['-O -ddump-simpl']) + +test('T25883', normal, compile_grep_core, ['']) +test('T25883b', normal, compile_grep_core, ['']) +test('T25883c', normal, compile_grep_core, ['']) +test('T25883d', [extra_files(['T25883d_import.hs'])], multimod_compile_filter, ['T25883d', '-O -ddump-simpl -dno-typeable-binds -dsuppress-all -dsuppress-uniques', r'grep -e "y ="']) ===================================== testsuite/tests/simplCore/should_run/T23429.hs ===================================== @@ -0,0 +1,39 @@ +{-# OPTIONS_GHC -fno-specialise-incoherents #-} +{-# LANGUAGE MonoLocalBinds #-} +class C a where + op :: a -> String + +instance {-# OVERLAPPABLE #-} C a where + op _ = "C a" + {-# NOINLINE op #-} + +instance {-# INCOHERENT #-} C (Maybe a) where + op _ = "C (Maybe a)" + {-# NOINLINE op #-} + +instance {-# INCOHERENT #-} C (Maybe ()) where + op _ = "C (Maybe ())" + {-# 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)))))))))))))) + +gen :: a -> String -- No C a constraint, has to choose the incoherent generic instance +gen = bar + +specMaybe :: Maybe a -> String -- C () constraint is resolved to the specialized instance for Maybe a +specMaybe = bar + +specMaybeUnit :: Maybe () -> String -- C () constraint is resolved to the specialized instance for Maybe () +specMaybeUnit = bar + +main :: IO () +main = do + putStrLn $ "gen () == " <> gen (Just ()) + putStrLn $ "specMaybe () == " <> specMaybe (Just ()) + putStrLn $ "specMaybeUnit () == " <> specMaybeUnit (Just ()) ===================================== testsuite/tests/simplCore/should_run/T23429.stdout ===================================== @@ -0,0 +1,3 @@ +gen () == C a +specMaybe () == C (Maybe a) +specMaybeUnit () == C (Maybe ()) ===================================== testsuite/tests/simplCore/should_run/all.T ===================================== @@ -119,3 +119,4 @@ test('T24725', normal, compile_and_run, ['-O -dcore-lint']) test('T25096', normal, compile_and_run, ['-O -dcore-lint']) test('AppIsHNF', normal, compile_and_run, ['-O']) test('T24359b', normal, compile_and_run, ['-O']) +test('T23429', normal, compile_and_run, ['-O']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e2f2f9d08274c90e775a35dc5b776f7... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e2f2f9d08274c90e775a35dc5b776f7... You're receiving this email because of your account on gitlab.haskell.org.