[Git][ghc/ghc][wip/9.2.6-backports] 3 commits: Fix an assertion check in addToEqualCtList
Zubin (@wz1000)
gitlab at gitlab.haskell.org
Wed Feb 1 11:55:26 UTC 2023
Zubin pushed to branch wip/9.2.6-backports at Glasgow Haskell Compiler / GHC
Commits:
346886bf by Simon Peyton Jones at 2023-02-01T16:00:06+05:30
Fix an assertion check in addToEqualCtList
The old assertion saw that a constraint ct could rewrite itself
(of course it can) and complained (stupid).
Fixes #22645
(cherry picked from commit 3d55d8ab51ece43c51055c43c9e7aba77cce46c0)
- - - - -
bd5ace54 by Simon Peyton Jones at 2023-02-01T16:36:28+05:30
Fix shadowing lacuna in OccurAnal
Issue #22623 demonstrated another lacuna in the implementation
of wrinkle (BS3) in Note [The binder-swap substitution] in
the occurrence analyser.
I was failing to add TyVar lambda binders using
addInScope/addOneInScope and that led to a totally bogus binder-swap
transformation.
Very easy to fix.
(cherry picked from commit e193e53790dd5886feea3cf4c9c17625d188291b)
- - - - -
e311168e by Sebastian Graf at 2023-02-01T17:24:19+05:30
DmdAnal: Don't panic in addCaseBndrDmd (#22039)
Rather conservatively return Top.
See Note [Untyped demand on case-alternative binders].
I also factored `addCaseBndrDmd` into two separate functions `scrutSubDmd` and
`fieldBndrDmds`.
Fixes #22039.
(cherry picked from commit d2be80fd9b222963e8dd09a30f78c106e00da7f9)
- - - - -
10 changed files:
- compiler/GHC/Core/Opt/DmdAnal.hs
- compiler/GHC/Core/Opt/OccurAnal.hs
- + testsuite/tests/simplCore/should_compile/T22623.hs
- + testsuite/tests/simplCore/should_compile/T22623a.hs
- testsuite/tests/simplCore/should_compile/all.T
- + testsuite/tests/stranal/should_compile/T22039.hs
- testsuite/tests/stranal/should_compile/all.T
- + testsuite/tests/typecheck/should_fail/T22645.hs
- + testsuite/tests/typecheck/should_fail/T22645.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Core/Opt/DmdAnal.hs
=====================================
@@ -439,10 +439,11 @@ dmdAnal' env dmd (Case scrut case_bndr ty [Alt alt bndrs rhs])
-- whole DmdEnv
!(!bndrs', !scrut_sd)
| DataAlt _ <- alt
- , id_dmds <- addCaseBndrDmd case_bndr_sd dmds
- -- See Note [Demand on scrutinee of a product case]
- = let !new_info = setBndrsDemandInfo bndrs id_dmds
- !new_prod = mkProd id_dmds
+ -- See Note [Demand on the scrutinee of a product case]
+ , let !scrut_sd = scrutSubDmd case_bndr_sd dmds
+ , let !fld_dmds' = fieldBndrDmds scrut_sd (length dmds)
+ = let !new_info = setBndrsDemandInfo bndrs fld_dmds'
+ !new_prod = mkProd fld_dmds'
in (new_info, new_prod)
| otherwise
-- __DEFAULT and literal alts. Simply add demands and discard the
@@ -556,11 +557,32 @@ dmdAnalSumAlt env dmd case_bndr (Alt con bndrs rhs)
, WithDmdType rhs_ty rhs' <- dmdAnal rhs_env dmd rhs
, WithDmdType alt_ty dmds <- findBndrsDmds env rhs_ty bndrs
, let (_ :* case_bndr_sd) = findIdDemand alt_ty case_bndr
- -- See Note [Demand on scrutinee of a product case]
- id_dmds = addCaseBndrDmd case_bndr_sd dmds
+ -- See Note [Demand on case-alternative binders]
+ -- we can't use the scrut_sd, because it says 'Prod' and we'll use
+ -- topSubDmd anyway for scrutinees of sum types.
+ scrut_sd = scrutSubDmd case_bndr_sd dmds
+ id_dmds = fieldBndrDmds scrut_sd (length dmds)
-- Do not put a thunk into the Alt
- !new_ids = setBndrsDemandInfo bndrs id_dmds
- = WithDmdType alt_ty (Alt con new_ids rhs')
+ !new_ids = setBndrsDemandInfo bndrs id_dmds
+ = -- pprTrace "dmdAnalSumAlt" (ppr con $$ ppr case_bndr $$ ppr dmd $$ ppr alt_ty) $
+ WithDmdType alt_ty (Alt con new_ids rhs')
+
+-- See Note [Demand on the scrutinee of a product case]
+scrutSubDmd :: SubDemand -> [Demand] -> SubDemand
+scrutSubDmd case_sd fld_dmds =
+ -- pprTraceWith "scrutSubDmd" (\scrut_sd -> ppr case_sd $$ ppr fld_dmds $$ ppr scrut_sd) $
+ case_sd `plusSubDmd` mkProd fld_dmds
+
+-- See Note [Demand on case-alternative binders]
+fieldBndrDmds :: SubDemand -- on the scrutinee
+ -> Arity
+ -> [Demand] -- Final demands for the components of the DataCon
+fieldBndrDmds scrut_sd n_flds =
+ case viewProd n_flds scrut_sd of
+ Just ds -> ds
+ Nothing -> replicate n_flds topDmd
+ -- Either an arity mismatch or scrut_sd was a call demand.
+ -- See Note [Untyped demand on case-alternative binders]
{-
Note [Analysing with absent demand]
@@ -672,6 +694,89 @@ worker, so the worker will rebuild
x = (a, absent-error)
and that'll crash.
+Note [Demand on case-alternative binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The demand on a binder in a case alternative comes
+ (a) From the demand on the binder itself
+ (b) From the demand on the case binder
+Forgetting (b) led directly to #10148.
+
+Example. Source code:
+ f x@(p,_) = if p then foo x else True
+
+ foo (p,True) = True
+ foo (p,q) = foo (q,p)
+
+After strictness analysis, forgetting (b):
+ f = \ (x_an1 [Dmd=1P(1L,ML)] :: (Bool, Bool)) ->
+ case x_an1
+ of wild_X7 [Dmd=MP(ML,ML)]
+ { (p_an2 [Dmd=1L], ds_dnz [Dmd=A]) ->
+ case p_an2 of _ {
+ False -> GHC.Types.True;
+ True -> foo wild_X7 }
+
+Note that ds_dnz is syntactically dead, but the expression bound to it is
+reachable through the case binder wild_X7. Now watch what happens if we inline
+foo's wrapper:
+ f = \ (x_an1 [Dmd=1P(1L,ML)] :: (Bool, Bool)) ->
+ case x_an1
+ of _ [Dmd=MP(ML,ML)]
+ { (p_an2 [Dmd=1L], ds_dnz [Dmd=A]) ->
+ case p_an2 of _ {
+ False -> GHC.Types.True;
+ True -> $wfoo_soq GHC.Types.True ds_dnz }
+
+Look at that! ds_dnz has come back to life in the call to $wfoo_soq! A second
+run of demand analysis would no longer infer ds_dnz to be absent.
+But unlike occurrence analysis, which infers properties of the *syntactic*
+shape of the program, the results of demand analysis describe expressions
+*semantically* and are supposed to be mostly stable across Simplification.
+That's why we should better account for (b).
+In #10148, we ended up emitting a single-entry thunk instead of an updateable
+thunk for a let binder that was an an absent case-alt binder during DmdAnal.
+
+This is needed even for non-product types, in case the case-binder
+is used but the components of the case alternative are not.
+
+Note [Untyped demand on case-alternative binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With unsafeCoerce, #8037 and #22039 taught us that the demand on the case binder
+may be a call demand or have a different number of fields than the constructor
+of the case alternative it is used in. From T22039:
+
+ blarg :: (Int, Int) -> Int
+ blarg (x,y) = x+y
+ -- blarg :: <1!P(1L,1L)>
+
+ f :: Either Int Int -> Int
+ f Left{} = 0
+ f e = blarg (unsafeCoerce e)
+ ==> { desugars to }
+ f = \ (ds_d1nV :: Either Int Int) ->
+ case ds_d1nV of wild_X1 {
+ Left ds_d1oV -> lvl_s1Q6;
+ Right ipv_s1Pl ->
+ blarg
+ (case unsafeEqualityProof @(*) @(Either Int Int) @(Int, Int) of
+ { UnsafeRefl co_a1oT ->
+ wild_X1 `cast` (Sub (Sym co_a1oT) :: Either Int Int ~R# (Int, Int))
+ })
+ }
+
+The case binder `e`/`wild_X1` has demand 1!P(1L,1L), with two fields, from the call
+to `blarg`, but `Right` only has one field. Although the code will crash when
+executed, we must be able to analyse it in 'fieldBndrDmds' and conservatively
+approximate with Top instead of panicking because of the mismatch.
+In #22039, this kind of code was guarded behind a safe `cast` and thus dead
+code, but nevertheless led to a panic of the compiler.
+
+You might wonder why the same problem doesn't come up when scrutinising a
+product type instead of a sum type. It appears that for products, `wild_X1`
+will be inlined before DmdAnal.
+
+See also Note [mkWWstr and unsafeCoerce] for a related issue.
+
Note [Aggregated demand for cardinality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
FIXME: This Note should be named [LetUp vs. LetDown] and probably predates
=====================================
compiler/GHC/Core/Opt/OccurAnal.hs
=====================================
@@ -1725,7 +1725,7 @@ occAnalRhs :: OccEnv -> RecFlag -> Maybe JoinArity
-> CoreExpr -- RHS
-> (UsageDetails, CoreExpr)
occAnalRhs env is_rec mb_join_arity rhs
- = case occAnalLamOrRhs env bndrs body of { (body_usage, bndrs', body') ->
+ = case occAnalLamOrRhs env1 bndrs body of { (body_usage, bndrs', body') ->
let final_bndrs | isRec is_rec = bndrs'
| otherwise = markJoinOneShots mb_join_arity bndrs'
-- For a /non-recursive/ join point we can mark all
@@ -1737,6 +1737,7 @@ occAnalRhs env is_rec mb_join_arity rhs
in (rhs_usage, mkLams final_bndrs body') }
where
(bndrs, body) = collectBinders rhs
+ env1 = addInScope env bndrs
occAnalUnfolding :: OccEnv
-> RecFlag
@@ -2005,7 +2006,7 @@ partially applying lambdas. See the calls to zapLamBndrs in
occAnal env expr@(Lam _ _)
= -- See Note [Occurrence analysis for lambda binders]
- case occAnalLamOrRhs env bndrs body of { (usage, tagged_bndrs, body') ->
+ case occAnalLamOrRhs env1 bndrs body of { (usage, tagged_bndrs, body') ->
let
expr' = mkLams tagged_bndrs body'
usage1 = markAllNonTail usage
@@ -2015,6 +2016,7 @@ occAnal env expr@(Lam _ _)
(final_usage, expr') }
where
(bndrs, body) = collectBinders expr
+ env1 = addInScope env bndrs
occAnal env (Case scrut bndr ty alts)
= case occAnal (scrutCtxt env alts) scrut of { (scrut_usage, scrut') ->
@@ -2284,12 +2286,13 @@ data OccEnv
-- See Note [The binder-swap substitution]
-- If x :-> (y, co) is in the env,
- -- then please replace x by (y |> sym mco)
- -- Invariant of course: idType x = exprType (y |> sym mco)
- , occ_bs_env :: VarEnv (OutId, MCoercion)
- , occ_bs_rng :: VarSet -- Vars free in the range of occ_bs_env
+ -- then please replace x by (y |> mco)
+ -- Invariant of course: idType x = exprType (y |> mco)
+ , occ_bs_env :: !(IdEnv (OutId, MCoercion))
-- Domain is Global and Local Ids
-- Range is just Local Ids
+ , occ_bs_rng :: !VarSet
+ -- Vars (TyVars and Ids) free in the range of occ_bs_env
}
@@ -2578,25 +2581,29 @@ Some tricky corners:
(BS3) We need care when shadowing. Suppose [x :-> b] is in occ_bs_env,
and we encounter:
- - \x. blah
- Here we want to delete the x-binding from occ_bs_env
-
- - \b. blah
- This is harder: we really want to delete all bindings that
- have 'b' free in the range. That is a bit tiresome to implement,
- so we compromise. We keep occ_bs_rng, which is the set of
- free vars of rng(occc_bs_env). If a binder shadows any of these
- variables, we discard all of occ_bs_env. Safe, if a bit
- brutal. NB, however: the simplifer de-shadows the code, so the
- next time around this won't happen.
+ (i) \x. blah
+ Here we want to delete the x-binding from occ_bs_env
+
+ (ii) \b. blah
+ This is harder: we really want to delete all bindings that
+ have 'b' free in the range. That is a bit tiresome to implement,
+ so we compromise. We keep occ_bs_rng, which is the set of
+ free vars of rng(occc_bs_env). If a binder shadows any of these
+ variables, we discard all of occ_bs_env. Safe, if a bit
+ brutal. NB, however: the simplifer de-shadows the code, so the
+ next time around this won't happen.
These checks are implemented in addInScope.
-
- The occurrence analyser itself does /not/ do cloning. It could, in
- principle, but it'd make it a bit more complicated and there is no
- great benefit. The simplifer uses cloning to get a no-shadowing
- situation, the care-when-shadowing behaviour above isn't needed for
- long.
+ (i) is needed only for Ids, but (ii) is needed for tyvars too (#22623)
+ because if occ_bs_env has [x :-> ...a...] where `a` is a tyvar, we
+ must not replace `x` by `...a...` under /\a. ...x..., or similarly
+ under a case pattern match that binds `a`.
+
+ An alternative would be for the occurrence analyser to do cloning as
+ it goes. In principle it could do so, but it'd make it a bit more
+ complicated and there is no great benefit. The simplifer uses
+ cloning to get a no-shadowing situation, the care-when-shadowing
+ behaviour above isn't needed for long.
(BS4) The domain of occ_bs_env can include GlobaIds. Eg
case M.foo of b { alts }
=====================================
testsuite/tests/simplCore/should_compile/T22623.hs
=====================================
@@ -0,0 +1,34 @@
+{-# LANGUAGE GHC2021 #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module T22623 where
+
+import T22623a
+
+type BindNonEmptyList :: NonEmpty -> NonEmpty -> [Q]
+type family BindNonEmptyList (x :: NonEmpty) (y :: NonEmpty) :: [Q] where
+ BindNonEmptyList ('(:|) a as) c = Tail c ++ Foldr2 a c as
+
+sBindNonEmptyList ::
+ forall (t :: NonEmpty)
+ (c :: NonEmpty). SNonEmpty t -> SNonEmpty c -> SList (BindNonEmptyList t c :: [Q])
+sBindNonEmptyList
+ ((:%|) (sA :: SQ a) (sAs :: SList as)) (sC :: SNonEmpty c)
+ = let
+ sMyHead :: SNonEmpty c -> SQ (MyHead a c)
+ sMyHead ((:%|) x _) = x
+
+ sFoldr :: forall t. SList t -> SList (Foldr2 a c t)
+ sFoldr SNil = SNil
+ sFoldr (SCons _ sYs) = SCons (sMyHead sC) (sFoldr sYs)
+
+ sF :: Id (SLambda (ConstSym1 c))
+ sF = SLambda (const sC)
+
+ sBs :: SList (Tail c)
+ _ :%| sBs = applySing sF sA
+ in
+ sBs %++ sFoldr sAs
=====================================
testsuite/tests/simplCore/should_compile/T22623a.hs
=====================================
@@ -0,0 +1,60 @@
+{-# LANGUAGE GHC2021 #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T22623a where
+
+import Data.Kind
+
+type Id :: Type -> Type
+type family Id x
+type instance Id x = x
+
+data Q
+data SQ (x :: Q)
+
+data NonEmpty where
+ (:|) :: Q -> [Q] -> NonEmpty
+
+type Tail :: NonEmpty -> [Q]
+type family Tail y where
+ Tail ('(:|) _ y) = y
+type MyHead :: Q -> NonEmpty -> Q
+type family MyHead x y where
+ MyHead _ ('(:|) c _) = c
+
+type SList :: [Q] -> Type
+data SList z where
+ SNil :: SList '[]
+ SCons :: SQ x -> SList xs -> SList (x:xs)
+
+type SNonEmpty :: NonEmpty -> Type
+data SNonEmpty z where
+ (:%|) :: SQ x -> SList xs -> SNonEmpty (x :| xs)
+
+data TyFun
+type F = TyFun -> Type
+
+type Apply :: F -> Q -> NonEmpty
+type family Apply f x
+
+type ConstSym1 :: NonEmpty -> F
+data ConstSym1 (x :: NonEmpty) :: F
+type instance Apply (ConstSym1 x) _ = x
+
+type SLambda :: F -> Type
+newtype SLambda (f :: F) =
+ SLambda { applySing :: forall t. SQ t -> SNonEmpty (f `Apply` t) }
+
+type Foldr2 :: Q -> NonEmpty -> [Q] -> [Q]
+type family Foldr2 a c x where
+ Foldr2 _ _ '[] = '[]
+ Foldr2 a c (_:ys) = MyHead a c : Foldr2 a c ys
+
+type (++) :: [Q] -> [Q] -> [Q]
+type family (++) xs ys where
+ (++) '[] ys = ys
+ (++) ('(:) x xs) ys = '(:) x (xs ++ ys)
+
+(%++) :: forall (x :: [Q]) (y :: [Q]). SList x -> SList y -> SList (x ++ y)
+(%++) SNil sYs = sYs
+(%++) (SCons sX sXs) sYs = SCons sX (sXs %++ sYs)
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -367,3 +367,4 @@ test('T20200', normal, compile, [''])
test('T20820', normal, compile, ['-O0'])
test('T22491', normal, compile, ['-O2'])
test('T22662', normal, compile, [''])
+test('T22623', normal, multimod_compile, ['T22623', '-O -v0'])
=====================================
testsuite/tests/stranal/should_compile/T22039.hs
=====================================
@@ -0,0 +1,59 @@
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Bug where
+
+import Control.Exception
+import Data.Typeable
+import Unsafe.Coerce
+
+data Error
+ = Error Int String
+ | forall e . Exception e => SomeError Int e
+ deriving (Typeable)
+
+fromError :: Exception e => Error -> Maybe e
+fromError e@(Error _ _) = cast e
+fromError (SomeError _ e) = cast e
+-- {-# NOINLINE fromError #-}
+
+instance Eq Error where
+ Error i s == Error i' s' = i == i' && s == s'
+ SomeError i e == SomeError i' e' = i == i' && show e == show e'
+ _ == _ = False
+
+instance Show Error where
+ show _ = ""
+
+instance Exception Error
+
+-- newtype
+data
+ UniquenessError = UniquenessError [((String, String), Int)]
+ deriving (Show, Eq)
+
+instance Exception UniquenessError
+
+test :: SomeException -> IO ()
+test e = case fromError =<< fromException e :: Maybe UniquenessError of
+ Just err -> print err
+ _ -> pure ()
+
+--
+-- Smaller reproducer by sgraf
+--
+
+blarg :: (Int,Int) -> Int
+blarg (x,y) = x+y
+{-# NOINLINE blarg #-}
+
+f :: Either Int Int -> Int
+f Left{} = 0
+f e = blarg (unsafeCoerce e)
+
+blurg :: (Int -> Int) -> Int
+blurg f = f 42
+{-# NOINLINE blurg #-}
+
+g :: Either Int Int -> Int
+g Left{} = 0
+g e = blurg (unsafeCoerce e)
=====================================
testsuite/tests/stranal/should_compile/all.T
=====================================
@@ -69,3 +69,4 @@ test('T20663', [ grep_errmsg(r'\$wyeah ::') ], compile, ['-dppr-cols=1000 -ddump
test('T19180', normal, compile, [''])
test('T19849', normal, compile, [''])
+test('T22039', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T22645.hs
=====================================
@@ -0,0 +1,9 @@
+module T22645 where
+
+import Data.Coerce
+
+type T :: (* -> *) -> * -> *
+data T m a = MkT (m a)
+
+p :: Coercible a b => T Maybe a -> T Maybe b
+p = coerce
=====================================
testsuite/tests/typecheck/should_fail/T22645.stderr
=====================================
@@ -0,0 +1,15 @@
+
+T22645.hs:9:5: error: [GHC-25897]
+ • Couldn't match type ‘a’ with ‘b’ arising from a use of ‘coerce’
+ ‘a’ is a rigid type variable bound by
+ the type signature for:
+ p :: forall a b. Coercible a b => T Maybe a -> T Maybe b
+ at T22645.hs:8:1-44
+ ‘b’ is a rigid type variable bound by
+ the type signature for:
+ p :: forall a b. Coercible a b => T Maybe a -> T Maybe b
+ at T22645.hs:8:1-44
+ • In the expression: coerce
+ In an equation for ‘p’: p = coerce
+ • Relevant bindings include
+ p :: T Maybe a -> T Maybe b (bound at T22645.hs:9:1)
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -629,3 +629,4 @@ test('T19397E4', extra_files(['T19397S.hs']), multimod_compile_fail,
test('T20043', normal, compile_fail, [''])
test('T20260', normal, compile_fail, [''])
test('T21130', normal, compile_fail, [''])
+test('T22645', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e50494f5489ebc7049a892829b78cf8bac2df6b6...e311168e37f5196614d04709b6e48f9a7f3c83d4
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/e50494f5489ebc7049a892829b78cf8bac2df6b6...e311168e37f5196614d04709b6e48f9a7f3c83d4
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/20230201/7b3db466/attachment-0001.html>
More information about the ghc-commits
mailing list