[commit: ghc] master: Remove unreliable Core Lint empty case checks (6b52b4c)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/6b52b4c832f888f7741a4ba0fec1fdac10244f6d/ghc

>---------------------------------------------------------------

commit 6b52b4c832f888f7741a4ba0fec1fdac10244f6d
Author: David Feuer <david.feuer at gmail.com>
Date:   Thu Nov 9 17:54:11 2017 -0500

    Remove unreliable Core Lint empty case checks
    
    Trac #13990 shows that the Core Lint checks for empty case are
    unreliable, and very hard to make reliable. The consensus (among
    simonpj, nomeata, and goldfire) seems to be that they should be
    removed altogether. Do that.
    
    Add test
    
    Reviewers: goldfire, bgamari
    
    Reviewed By: bgamari
    
    Subscribers: rwbarton, thomie
    
    GHC Trac Issues: #13990
    
    Differential Revision: https://phabricator.haskell.org/D4161


>---------------------------------------------------------------

6b52b4c832f888f7741a4ba0fec1fdac10244f6d
 compiler/coreSyn/CoreLint.hs                       | 57 ++++++++++++++--------
 testsuite/tests/simplCore/should_compile/T13990.hs | 14 ++++++
 testsuite/tests/simplCore/should_compile/all.T     |  1 +
 3 files changed, 53 insertions(+), 19 deletions(-)

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 4b6defd..7f52dbb 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -799,13 +799,9 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
      ; (alt_ty, _) <- lintInTy alt_ty
      ; (var_ty, _) <- lintInTy (idType var)
 
-     -- See Note [No alternatives lint check]
-     ; when (null alts) $
-     do { checkL (not (exprIsHNF scrut))
-          (text "No alternatives for a case scrutinee in head-normal form:" <+> ppr scrut)
-        ; checkWarnL scrut_diverges
-          (text "No alternatives for a case scrutinee not known to diverge for sure:" <+> ppr scrut)
-        }
+     -- We used to try to check whether a case expression with no
+     -- alternatives was legitimate, but this didn't work.
+     -- See Note [No alternatives lint check] for details.
 
      -- See Note [Rules for floating-point comparisons] in PrelRules
      ; let isLitPat (LitAlt _, _ , _) = True
@@ -932,23 +928,46 @@ checkJoinOcc var n_args
 {-
 Note [No alternatives lint check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Case expressions with no alternatives are odd beasts, and worth looking at
-in the linter (cf Trac #10180).  We check two things:
+Case expressions with no alternatives are odd beasts, and it would seem
+like they would worth be looking at in the linter (cf Trac #10180). We
+used to check two things:
 
-* exprIsHNF is false: certainly, it would be terribly wrong if the
-  scrutinee was already in head normal form.
+* exprIsHNF is false: it would *seem* to be terribly wrong if
+  the scrutinee was already in head normal form.
 
 * exprIsBottom is true: we should be able to see why GHC believes the
   scrutinee is diverging for sure.
 
-In principle, the first check is redundant: exprIsBottom == True will
-always imply exprIsHNF == False.  But the first check is reliable: If
-exprIsHNF == True, then there definitely is a problem (exprIsHNF errs
-on the right side).  If the second check triggers then it may be the
-case that the compiler got smarter elsewhere, and the empty case is
-correct, but that exprIsBottom is unable to see it. In particular, the
-empty-type check in exprIsBottom is an approximation. Therefore, this
-check is not fully reliable, and we keep both around.
+It was already known that the second test was not entirely reliable.
+Unfortunately (Trac #13990), the first test turned out not to be reliable
+either. Getting the checks right turns out to be somewhat complicated.
+
+For example, suppose we have (comment 8)
+
+  data T a where
+    TInt :: T Int
+
+  absurdTBool :: T Bool -> a
+  absurdTBool v = case v of
+
+  data Foo = Foo !(T Bool)
+
+  absurdFoo :: Foo -> a
+  absurdFoo (Foo x) = absurdTBool x
+
+GHC initially accepts the empty case because of the GADT conditions. But then
+we inline absurdTBool, getting
+
+  absurdFoo (Foo x) = case x of
+
+x is in normal form (because the Foo constructor is strict) but the
+case is empty. To avoid this problem, GHC would have to recognize
+that matching on Foo x is already absurd, which is not so easy.
+
+More generally, we don't really know all the ways that GHC can
+lose track of why an expression is bottom, so we shouldn't make too
+much fuss when that happens.
+
 
 Note [Beta redexes]
 ~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/simplCore/should_compile/T13990.hs b/testsuite/tests/simplCore/should_compile/T13990.hs
new file mode 100644
index 0000000..cbf3949
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T13990.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE EmptyCase, GADTs #-}
+
+module T13990 where
+
+data T a where
+  TInt :: T Int
+
+absurd :: T Bool -> a
+absurd v = case v of {}
+
+data Foo = Foo !(T Bool)
+
+absurdFoo :: Foo -> a
+absurdFoo (Foo x) = absurd x
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index e411a6d..0b85692 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -284,3 +284,4 @@ test('T14272', normal, compile, [''])
 test('T14270a', normal, compile, [''])
 test('T14152', [ only_ways(['optasm']), check_errmsg(r'dead code') ], compile, ['-ddump-simpl'])
 test('T14152a', [ only_ways(['optasm']), check_errmsg(r'dead code') ], compile, ['-fno-exitification -ddump-simpl'])
+test('T13990', normal, compile, ['-dcore-lint -O'])