[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 4 commits: Fix unification with oversaturated type families
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Thu Apr 6 05:00:47 UTC 2023
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
7c16f3be by Krzysztof Gogolewski at 2023-04-04T17:13:00-04:00
Fix unification with oversaturated type families
unify_ty was incorrectly saying that F x y ~ T x are surely apart,
where F x y is an oversaturated type family and T x is a tyconapp.
As a result, the simplifier dropped a live case alternative (#23134).
- - - - -
c165f079 by sheaf at 2023-04-04T17:13:40-04:00
Add testcase for #23192
This issue around solving of constraints arising from superclass
expansion using other constraints also borned from superclass expansion
was the topic of commit aed1974e. That commit made sure we don't emit
a "redundant constraint" warning in a situation in which removing the
constraint would cause errors.
Fixes #23192
- - - - -
24097692 by Ben Gamari at 2023-04-06T01:00:40-04:00
nonmoving: Disable slop-zeroing
As noted in #23170, the nonmoving GC can race with a mutator zeroing the
slop of an updated thunk (in much the same way that two mutators would
race). Consequently, we must disable slop-zeroing when the nonmoving GC
is in use.
Closes #23170
- - - - -
2b79e386 by Brandon Chinn at 2023-04-06T01:00:40-04:00
Fix reverse flag for -Wunsupported-llvm-version
- - - - -
8 changed files:
- compiler/GHC/Core/Unify.hs
- docs/users_guide/using-warnings.rst
- rts/include/rts/storage/ClosureMacros.h
- + testsuite/tests/simplCore/should_run/T23134.hs
- + testsuite/tests/simplCore/should_run/T23134.stdout
- testsuite/tests/simplCore/should_run/all.T
- + testsuite/tests/typecheck/should_compile/T23192.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1,6 +1,6 @@
-- (c) The University of Glasgow 2006
-{-# LANGUAGE ScopedTypeVariables, PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, MultiWayIf #-}
{-# LANGUAGE DeriveFunctor #-}
@@ -47,6 +47,7 @@ import GHC.Types.Unique
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Exts( oneShot )
+import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Data.FastString
@@ -994,6 +995,59 @@ These two TyConApps have the same TyCon at the front but they
(legitimately) have different numbers of arguments. They
are surelyApart, so we can report that without looking any
further (see #15704).
+
+Note [Unifying type applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Unifying type applications is quite subtle, as we found
+in #23134 and #22647, when type families are involved.
+
+Suppose
+ type family F a :: Type -> Type
+ type family G k :: k = r | r -> k
+
+and consider these examples:
+
+* F Int ~ F Char, where F is injective
+ Since F is injective, we can reduce this to Int ~ Char,
+ therefore SurelyApart.
+
+* F Int ~ F Char, where F is not injective
+ Without injectivity, return MaybeApart.
+
+* G Type ~ G (Type -> Type) Int
+ Even though G is injective and the arguments to G are different,
+ we cannot deduce apartness because the RHS is oversaturated.
+ For example, G might be defined as
+ G Type = Maybe Int
+ G (Type -> Type) = Maybe
+ So we return MaybeApart.
+
+* F Int Bool ~ F Int Char -- SurelyApart (since Bool is apart from Char)
+ F Int Bool ~ Maybe a -- MaybeApart
+ F Int Bool ~ a b -- MaybeApart
+ F Int Bool ~ Char -> Bool -- MaybeApart
+ An oversaturated type family can match an application,
+ whether it's a TyConApp, AppTy or FunTy. Decompose.
+
+* F Int ~ a b
+ We cannot decompose a saturated, or under-saturated
+ type family application. We return MaybeApart.
+
+To handle all those conditions, unify_ty goes through
+the following checks in sequence, where Fn is a type family
+of arity n:
+
+* (C1) Fn x_1 ... x_n ~ Fn y_1 .. y_n
+ A saturated application.
+ Here we can unify arguments in which Fn is injective.
+* (C2) Fn x_1 ... x_n ~ anything, anything ~ Fn x_1 ... x_n
+ A saturated type family can match anything - we return MaybeApart.
+* (C3) Fn x_1 ... x_m ~ a b, a b ~ Fn x_1 ... x_m where m > n
+ An oversaturated type family can be decomposed.
+* (C4) Fn x_1 ... x_m ~ anything, anything ~ Fn x_1 ... x_m, where m > n
+ If we couldn't decompose in the previous step, we return SurelyApart.
+
+Afterwards, the rest of the code doesn't have to worry about type families.
-}
-------------- unify_ty: the main workhorse -----------
@@ -1035,31 +1089,63 @@ unify_ty env ty1 (TyVarTy tv2) kco
= uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
unify_ty env ty1 ty2 _kco
+
+ -- Handle non-oversaturated type families first
+ -- See Note [Unifying type applications]
+ --
+ -- (C1) If we have T x1 ... xn ~ T y1 ... yn, use injectivity information of T
+ -- Note that both sides must not be oversaturated
+ | Just (tc1, tys1) <- isSatTyFamApp mb_tc_app1
+ , Just (tc2, tys2) <- isSatTyFamApp mb_tc_app2
+ , tc1 == tc2
+ = do { let inj = case tyConInjectivityInfo tc1 of
+ NotInjective -> repeat False
+ Injective bs -> bs
+
+ (inj_tys1, noninj_tys1) = partitionByList inj tys1
+ (inj_tys2, noninj_tys2) = partitionByList inj tys2
+
+ ; unify_tys env inj_tys1 inj_tys2
+ ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
+ don'tBeSoSure MARTypeFamily $ unify_tys env noninj_tys1 noninj_tys2 }
+
+ | Just _ <- isSatTyFamApp mb_tc_app1 -- (C2) A (not-over-saturated) type-family application
+ = maybeApart MARTypeFamily -- behaves like a type variable; might match
+
+ | Just _ <- isSatTyFamApp mb_tc_app2 -- (C2) A (not-over-saturated) type-family application
+ -- behaves like a type variable; might unify
+ -- but doesn't match (as in the TyVarTy case)
+ = if um_unif env then maybeApart MARTypeFamily else surelyApart
+
+ -- Handle oversaturated type families.
+ --
+ -- They can match an application (TyConApp/FunTy/AppTy), this is handled
+ -- the same way as in the AppTy case below.
+ --
+ -- If there is no application, an oversaturated type family can only
+ -- match a type variable or a saturated type family,
+ -- both of which we handled earlier. So we can say surelyApart.
+ | Just (tc1, _) <- mb_tc_app1
+ , isTypeFamilyTyCon tc1
+ = if | Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
+ , Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
+ -> unify_ty_app env ty1a [ty1b] ty2a [ty2b] -- (C3)
+ | otherwise -> surelyApart -- (C4)
+
+ | Just (tc2, _) <- mb_tc_app2
+ , isTypeFamilyTyCon tc2
+ = if | Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
+ , Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
+ -> unify_ty_app env ty1a [ty1b] ty2a [ty2b] -- (C3)
+ | otherwise -> surelyApart -- (C4)
+
+ -- At this point, neither tc1 nor tc2 can be a type family.
| Just (tc1, tys1) <- mb_tc_app1
, Just (tc2, tys2) <- mb_tc_app2
, tc1 == tc2
- = if isInjectiveTyCon tc1 Nominal
- then unify_tys env tys1 tys2
- else do { let inj | isTypeFamilyTyCon tc1
- = case tyConInjectivityInfo tc1 of
- NotInjective -> repeat False
- Injective bs -> bs
- | otherwise
- = repeat False
-
- (inj_tys1, noninj_tys1) = partitionByList inj tys1
- (inj_tys2, noninj_tys2) = partitionByList inj tys2
-
- ; unify_tys env inj_tys1 inj_tys2
- ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
- don'tBeSoSure MARTypeFamily $ unify_tys env noninj_tys1 noninj_tys2 }
-
- | isTyFamApp mb_tc_app1 -- A (not-over-saturated) type-family application
- = maybeApart MARTypeFamily -- behaves like a type variable; might match
-
- | isTyFamApp mb_tc_app2 -- A (not-over-saturated) type-family application
- , um_unif env -- behaves like a type variable; might unify
- = maybeApart MARTypeFamily
+ = do { massertPpr (isInjectiveTyCon tc1 Nominal) (ppr tc1)
+ ; unify_tys env tys1 tys2
+ }
-- TYPE and CONSTRAINT are not Apart
-- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
@@ -1160,16 +1246,16 @@ unify_tys env orig_xs orig_ys
-- Possibly different saturations of a polykinded tycon
-- See Note [Polykinded tycon applications]
-isTyFamApp :: Maybe (TyCon, [Type]) -> Bool
--- True if we have a saturated or under-saturated type family application
+isSatTyFamApp :: Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
+-- Return the argument if we have a saturated type family application
-- If it is /over/ saturated then we return False. E.g.
-- unify_ty (F a b) (c d) where F has arity 1
-- we definitely want to decompose that type application! (#22647)
-isTyFamApp (Just (tc, tys))
- = not (isGenerativeTyCon tc Nominal) -- Type family-ish
+isSatTyFamApp tapp@(Just (tc, tys))
+ | isTypeFamilyTyCon tc
&& not (tys `lengthExceeds` tyConArity tc) -- Not over-saturated
-isTyFamApp Nothing
- = False
+ = tapp
+isSatTyFamApp _ = Nothing
---------------------------------
uVar :: UMEnv
=====================================
docs/users_guide/using-warnings.rst
=====================================
@@ -1615,7 +1615,7 @@ of ``-W(no-)*``.
:shortdesc: Warn when using :ghc-flag:`-fllvm` with an unsupported
version of LLVM.
:type: dynamic
- :reverse: -Wno-monomorphism-restriction
+ :reverse: -Wno-unsupported-llvm-version
:category:
:since: 7.8
=====================================
rts/include/rts/storage/ClosureMacros.h
=====================================
@@ -479,11 +479,13 @@ EXTERN_INLINE StgWord8 *mutArrPtrsCard (StgMutArrPtrs *a, W_ n)
memory we're about to zero.
Thus, with the THREADED RTS and +RTS -N2 or greater we must not zero
- immutable closure's slop.
+ immutable closure's slop. Similarly, the concurrent GC's mark thread
+ may race when a mutator during slop-zeroing. Consequently, we also disable
+ zeroing when the non-moving GC is in use.
Hence, an immutable closure's slop is zeroed when either:
- - PROFILING && era > 0 (LDV is on) or
+ - PROFILING && era > 0 (LDV is on) && !nonmoving-gc-enabled or
- !THREADED && DEBUG
Additionally:
@@ -535,8 +537,10 @@ zeroSlop (StgClosure *p,
#endif
;
- // Only if we're running single threaded.
- const bool can_zero_immutable_slop = getNumCapabilities() == 1;
+ const bool can_zero_immutable_slop =
+ // Only if we're running single threaded.
+ getNumCapabilities() == 1
+ && !RTS_DEREF(RtsFlags).GcFlags.useNonmoving; // see #23170
const bool zero_slop_immutable =
want_to_zero_immutable_slop && can_zero_immutable_slop;
=====================================
testsuite/tests/simplCore/should_run/T23134.hs
=====================================
@@ -0,0 +1,37 @@
+{-# LANGUAGE GHC2021, DataKinds, TypeFamilies #-}
+module Main where
+
+import Data.Maybe
+import Data.Kind
+
+main :: IO ()
+main = putStrLn str
+
+str :: String
+str = case runInstrImpl @(TOption TUnit) mm MAP of
+ C VOption -> "good"
+ C Unused -> "bad"
+
+runInstrImpl :: forall inp out. Value (MapOpRes inp TUnit) -> Instr inp out -> Rec out
+runInstrImpl m MAP = C m
+
+type MapOpRes :: T -> T -> T
+type family MapOpRes c :: T -> T
+type instance MapOpRes ('TOption x) = 'TOption
+
+mm :: Value (TOption TUnit)
+mm = VOption
+{-# NOINLINE mm #-}
+
+type Value :: T -> Type
+data Value t where
+ VOption :: Value ('TOption t)
+ Unused :: Value t
+
+data T = TOption T | TUnit
+
+data Instr (inp :: T) (out :: T) where
+ MAP :: Instr c (TOption (MapOpRes c TUnit))
+
+data Rec :: T -> Type where
+ C :: Value r -> Rec (TOption r)
=====================================
testsuite/tests/simplCore/should_run/T23134.stdout
=====================================
@@ -0,0 +1 @@
+good
=====================================
testsuite/tests/simplCore/should_run/all.T
=====================================
@@ -110,4 +110,4 @@ test('T20836', normal, compile_and_run, ['-O0']) # Should not time out; See #208
test('T22448', normal, compile_and_run, ['-O1'])
test('T22998', normal, compile_and_run, ['-O0 -fspecialise -dcore-lint'])
test('T23184', normal, compile_and_run, ['-O'])
-
+test('T23134', normal, compile_and_run, ['-O0 -fcatch-nonexhaustive-cases'])
=====================================
testsuite/tests/typecheck/should_compile/T23192.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Werror=redundant-constraints #-}
+
+module EventThing where
+
+class Monad m => Event m where
+ thingsForEvent :: m [Int]
+
+class Monad m => Thingy m where
+ thingies :: m [Int]
+
+-- Check that we don't get a redundant constraint warning for "Monad m".
+-- See #19690.
+instance (Monad m, Event m) => Thingy m where
+ thingies = thingsForEvent
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -870,3 +870,4 @@ test('T21443', normal, compile, [''])
test('QualifiedRecordUpdate',
[ extra_files(['QualifiedRecordUpdate_aux.hs']) ]
, multimod_compile, ['QualifiedRecordUpdate', '-v0'])
+test('T23192', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/56c9caee6e9355115f7c2c50e94f42d9f441ab8f...2b79e3865d19ec02b3dba02052c2627c8ea0edb2
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/56c9caee6e9355115f7c2c50e94f42d9f441ab8f...2b79e3865d19ec02b3dba02052c2627c8ea0edb2
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/20230406/434078f5/attachment-0001.html>
More information about the ghc-commits
mailing list