[Git][ghc/ghc][wip/T23862] Cpr: Turn an assertion into a check to deal with some dead code (#23862)

[Sebastian Graf (@sgraf812)]

Sebastian Graf pushed to branch wip/T23862 at Glasgow Haskell Compiler / GHC


Commits:
2a90dd5e by Sebastian Graf at 2023-12-05T11:31:50+01:00
Cpr: Turn an assertion into a check to deal with some dead code (#23862)

See the new `Note [Dead code may contain type confusions]`.

Fixes #23862.

- - - - -


4 changed files:

- compiler/GHC/Core/Opt/CprAnal.hs
- + testsuite/tests/cpranal/should_compile/T23862.hs
- + testsuite/tests/cpranal/should_compile/T23862.stderr
- testsuite/tests/cpranal/should_compile/all.T


Changes:

=====================================
compiler/GHC/Core/Opt/CprAnal.hs
=====================================
@@ -274,7 +274,7 @@ cprAnalAlt env scrut_ty (Alt con bndrs rhs)
       | DataAlt dc <- con
       , let ids = filter isId bndrs
       , CprType arity cpr <- scrut_ty
-      , assert (arity == 0 ) True
+      , arity == 0 -- See Note [Dead code may contain type confusions]
       = case unpackConFieldsCpr dc cpr of
           AllFieldsSame field_cpr
             | let sig = mkCprSig 0 field_cpr
@@ -430,6 +430,43 @@ cprFix orig_env orig_pairs
             (id', rhs', env') = cprAnalBind env id rhs
 
 {-
+Note [Dead code may contain type confusions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In T23862, we have a nested case match that looks like this
+
+  data CheckSingleton (check :: Bool) where
+    Checked :: CheckSingleton True
+    Unchecked :: CheckSingleton False
+  data family Result (check :: Bool) a
+  data instance Result True a = CheckedResult a
+  newtype instance Result True a = UncheckedResult a
+
+  case m () of Checked co1 ->
+    case m () of Unchecked co2 ->
+      case ((\_ -> True)
+             |> .. UncheckedResult ..
+             |> sym co2
+             |> co1) :: Result True (Bool -> Bool) of
+        CheckedResult f -> CheckedResult (f True)
+
+Clearly, the innermost case is dead code, because the `Checked` and `Unchecked`
+cases are apart.
+However, both constructors introduce mutually contradictory coercions `co1` and
+`co2` along which GHC generates a type confusion:
+
+  1. (\_ -> True) :: Bool -> Bool
+  2. newtype coercion UncheckedResult (\_ -> True) :: Result False (Bool -> Bool)
+  3. |> ... sym co1 ... :: Result check (Bool -> Bool)
+  4. |> ... co2 ... :: Result True (Bool -> Bool)
+
+Note that we started with a function, injected into `Result` via a newtype
+instance and then match on it with a datatype instance.
+
+We have to handle this case gracefully in `cprAnalAlt`, where for the innermost
+case we see a `DataAlt` for `CheckedResult`, yet have a scrutinee type that
+abstracts the function `(\_ -> True)` with arity 1.
+In this case, don't pretend we know anything about the fields of `CheckedResult`!
+
 Note [The OPAQUE pragma and avoiding the reboxing of results]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider:


=====================================
testsuite/tests/cpranal/should_compile/T23862.hs
=====================================
@@ -0,0 +1,19 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+
+module T23862 where
+
+data family Result (check :: Bool) a
+data instance Result True a = CheckedResult a
+newtype instance Result False a = UncheckedResult a
+
+data CheckSingleton (check :: Bool) where
+   Checked :: CheckSingleton True
+   Unchecked :: CheckSingleton False
+
+app :: (() -> CheckSingleton check) -> Result check Bool
+app m = case (m (), m ()) of
+ (Checked, Unchecked)
+   | CheckedResult x <- UncheckedResult (\_ -> True)
+   -> CheckedResult (x True)


=====================================
testsuite/tests/cpranal/should_compile/T23862.stderr
=====================================
@@ -0,0 +1,18 @@
+
+T23862.hs:17:12: warning: [GHC-40564] [-Winaccessible-code (in -Wdefault)]
+    • Inaccessible code in
+        a pattern with constructor: Unchecked :: CheckSingleton False,
+        in a case alternative
+      Couldn't match type ‘True’ with ‘False’
+    • In the pattern: Unchecked
+      In the pattern: (Checked, Unchecked)
+      In a case alternative:
+          (Checked, Unchecked)
+            | CheckedResult x <- UncheckedResult (\ _ -> True)
+            -> CheckedResult (x True)
+
+T23862.hs:18:6: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In a case alternative:
+        (Checked, Unchecked) | CheckedResult x <- UncheckedResult
+                                                    (\ _ -> True) -> ...


=====================================
testsuite/tests/cpranal/should_compile/all.T
=====================================
@@ -22,3 +22,5 @@ test('T18401', [ grep_errmsg(r'^T18401\.\S+ ::') ], compile, ['-ddump-simpl -dsu
 test('T18824', [ grep_errmsg(r'JoinId[^\n]*Cpr') ], compile, ['-ddump-exitify -dppr-cols=1000 -dsuppress-uniques'])
 
 test('T20539', [], compile, ['']) # simply should not crash
+
+test('T23862', [], compile, ['']) # simply should not crash



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2a90dd5e74a64291fd81374099d7422e2ae84721

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2a90dd5e74a64291fd81374099d7422e2ae84721
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/20231205/895e78f9/attachment-0001.html>