From 4a6b7c876b42a6b116a81b0b7209d5e38b7ff97a Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sebastian.graf@kit.edu>
Date: Mon, 7 Aug 2023 11:19:43 +0200
Subject: [PATCH] Clarify floating of unsafeEqualityProofs (#23754)
---
compiler/GHC/Core/Utils.hs | 19 ++++---------------
libraries/base/Unsafe/Coerce.hs | 27 +++++++++++++++++----------
2 files changed, 21 insertions(+), 25 deletions(-)
diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index 833f2d657339..1a4a23362360 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -1679,7 +1679,7 @@ app_ok fun_ok primop_ok fun args
-- and we'd need to actually test n_val_args == 0.)
-- Functions that terminate fast without raising exceptions etc
- -- See Note [Discarding unnecessary unsafeEqualityProofs]
+ -- See (U12) of Note [Implementing unsafeCoerce]
| fun `hasKey` unsafeEqualityProofIdKey -> True
| otherwise -> False
@@ -1876,20 +1876,6 @@ GHC.Builtin.PrimOps.
Note that exprIsHNF /can/ and does take advantage of evaluated-ness;
it doesn't have the trickiness of the let-can-float invariant to worry about.
-Note [Discarding unnecessary unsafeEqualityProofs]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In #20143 we found
- case unsafeEqualityProof @t1 @t2 of UnsafeRefl cv[dead] -> blah
-where 'blah' didn't mention 'cv'. We'd like to discard this
-redundant use of unsafeEqualityProof, via GHC.Core.Opt.Simplify.rebuildCase.
-To do this we need to know
- (a) that cv is unused (done by OccAnal), and
- (b) that unsafeEqualityProof terminates rapidly without side effects.
-
-At the moment we check that explicitly here in exprOkToDiscard,
-but one might imagine a more systematic check in future.
-
-
************************************************************************
* *
exprIsHNF, exprIsConLike
@@ -1973,6 +1959,9 @@ exprIsHNFlike is_con is_con_unf = is_hnf_like
| isValArg a = app_is_value e 1
| otherwise = is_hnf_like e
is_hnf_like (Let _ e) = is_hnf_like e -- Lazy let(rec)s don't affect us
+ is_hnf_like (Case e b _ as)
+ | Just rhs <- isUnsafeEqualityCase e b as
+ = is_hnf_like rhs
is_hnf_like _ = False
-- 'n' is the number of value args to which the expression is applied
diff --git a/libraries/base/Unsafe/Coerce.hs b/libraries/base/Unsafe/Coerce.hs
index 368c204f471b..e1b00ce10d71 100644
--- a/libraries/base/Unsafe/Coerce.hs
+++ b/libraries/base/Unsafe/Coerce.hs
@@ -73,16 +73,7 @@ Now our bad case can't happen. We'll have
UnsafeRefl (co :: t1 ~ t2) -> ....(x |> co)....
and the (x |> co) mentions the evidence 'co', which prevents it
-floating.
-
-But what stops the whole (case unsafeEqualityProof of ...) from
-floating? Answer: we never float a case on a redex that can fail
-outside a conditional. See Primop.hs,
-Note [Transformations affected by primop effects].
-And unsafeEqualityProof (being opaque) is definitely treated as
-can-fail.
- (Huh? It seems we have a special-case in exprOkForSpeculation (app_ok)
- /specifically/ allowing unsafeEqualityProof. Something smells wrong. #23754)
+floating. See also wrinkle (U11) below.
While unsafeCoerce is a perfectly ordinary function that needs no
special treatment, Unsafe.Coerce.unsafeEqualityProof is magical, in
@@ -215,6 +206,22 @@ There are yet more wrinkles
the kind-/homogeneous/ unsafeEqualityProof twice.
See Note [Wiring in unsafeCoerce#] in Desugar.
+
+(U11) But what stops the whole (case unsafeEqualityProof of ...) from
+ being speculated out of a conditional? (E.g., strict float out.)
+ Answer: we never float a case on something that is not an HNF
+ ('exprIsHNF') outside a conditional.
+ See Note [Floating single-alternative cases].
+
+(U12) In #20143 we found
+ case unsafeEqualityProof @t1 @t2 of UnsafeRefl cv[dead] -> blah
+ where 'blah' didn't mention 'cv'. We'd like to discard this
+ redundant use of unsafeEqualityProof, via GHC.Core.Opt.Simplify.rebuildCase.
+ To do this we need to know
+ (a) that cv is unused (done by OccAnal), and
+ (b) that unsafeEqualityProof terminates rapidly without side effects.
+ At the moment we check that explicitly in GHC.Core.Utils.exprOkToDiscard,
+ but one might imagine a more systematic check in future.
-}
-- | This type is treated magically within GHC. Any pattern match of the
--
GitLab