#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * priority: normal => highest Comment: Core Lint errors in a release candidate are ''bad''. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): To be fair, this wasn't introduced in GHC 8.2.1. This error also appears in 8.0 as well (but not in 7.10). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nomeata): I believe the mistake is in `CoreLint` here. The question is: How can `CoreLint` know that `x_ap6` is both void and evaluated, hence cannot actually exist? Probably we just need to change the code {{{ 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) } }}} to something that runs the first check only when `scrut_diverges` is false (if `scrut_diverges`, then it cannot be in normal form). Or find out why `exprIsHNF scrut` is `True` here. Or maybe the outer `case` of {{{ case ds_dUn of { Foo x_ap6 -> case x_ap6 of { } } }}} should be empty, as the pattern `Foo x` is already absurd (due to the bang). Many options :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):

Or find out why exprIsHNF scrut is True here.

It's because in a case alternative {{{ K x -> ...x... }}} where `K` is strict, we know that when we unpack `K x`, the field `x` must be evaluated. So it is marked as such, and hence responds True to `exprIsHNF`. Joachim's solition is right; but it's very much a corner case and a bit hard to get right. E.g. {{{ data T a = T1 !(F a) Int | ... }}} When we pattern match on `T1 x y :: T X`, is that pattern impossible? WEll it depends on whether `(F X)` evaluates to an empty type. Hard to be sure it is fully nailed. Better, I think, to say that {{{ case x of {} }}} is fine if `x :: T` where `T` has no data constructors. That would silence the warning and is obviously correct. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Hmm. Let's stand back a bit. * The simplifier (via `CoreSyn.filterAlts`) can eliminate branches of a case that can't happen, because of (a) GADT matching and (b) lexically enclosing case expressions. * Lint can't guarantee to come to the same conclusion becuase of floating. Eg {{{ data T = A | B | C f x = case x of A -> e1 _ -> ...(case x of B -> e1 C -> e3)... ===> f x = let t = case x of B -> e1 C -> e3 in case x of A -> e1 _ -> ...t... }}} Before, it's clear that the inner case is exhaustive, but not so clear after the transformation. * So currently Lint doesn't attempt to complain about inexhaustive cases. * EXCEPT if there are zero alternatives. And for that, strangely, Lint makes two separate checks. First, in the `Case` equation for `lintCoreExpr`: {{{ -- 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) } }}} Second in `checkCaseAlts`: {{{ ; checkL (isJust maybe_deflt || not is_infinite_ty || null alts) (nonExhaustiveAltsMsg e) } }}} Clearly we should do this stuff in only one place. I now propose that we remove the "null alts" check altogether. It's just an extreme case of having filtered out all alternatives. The current code treats it specially, but this ticket has convinced me that it's not special afte all. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Without reading all the commentary above: I conjecture that the only way to get this right is to come up with some datatype which serves as evidence that an empty case is acceptable. There may be several constructors of the datatype depending on why GHC believes the empty case, and we may need to do transformations to elements of this type during simplification, etc. In other words, it's all quite like what `Coercion` does for type equality. Then, Lint could check various invariants of the datatype. (Also known as typing rules.) Is this worth it? It certainly doesn't seem like it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.2.3 Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.2.2 => 8.2.3 Comment: It doesn't seem like this will happen for 8.2.2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: patch Priority: highest | Milestone: 8.2.3 Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4160 Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Simon asked me to note here that his remark in comment:9 about `checkCaseAlts` was a bit off. The `null alts` there is doing something a bit different: allowing case matches with no alternatives on "nearly- infinite" types like `Int#`. Pulling that test out actually makes the build fail. Why? That's not actually entirely clear to me. Somewhere in `Text` internals, we get a Core Lint error {{{ 5258 <no location info>: warning: 5259 In a case alternative: (I# n#_a4mN :: Int#) 5260 Case expression with non-exhaustive alternatives 5261 case lvl_sfty n#_a4mN of wild_00 { } }}} This is slightly surprising, because the relevant `lvl_sfty` seems to be {{{ 29713 lvl_sfty :: Int# -> Int# 29714 [LclId, 29715 Arity=1, 29716 Str=x, 29717 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, 29718 WorkFree=True, Expandable=True, Guidance=NEVER}] 29719 lvl_sfty 29720 = \ (n#_a4mW :: Int#) -> 29721 error 29722 @ 'IntRep 29723 @ Int# 29724 ($dIP_saA9 29725 `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N) 29726 :: (CallStack :: *) ~R# (?callStack::CallStack :: Constraint))) 29727 (augment 29728 @ Char 29729 lvl_sftt 29730 (augment 29731 @ Char 29732 lvl_sftv 29733 (augment 29734 @ Char 29735 lvl_sftx 29736 (showSignedInt $fShow(,)1 (I# n#_a4mW) ([] @ Char))))) }}} which is just a call to `error`. One other question: the `exprIsHNF` error was clearly hosed, and badly so. But should we leave the `scrut_diverges` warning in place? That seems like it's useful, even if it's not reliable. If we decide to leave that in place, can/should we apply it to `Int#` and such as well? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13990: Core Lint error on empty case -------------------------------------+------------------------------------- Reporter: mbieleck | Owner: (none) Type: bug | Status: patch Priority: highest | Milestone: 8.2.3 Component: Compiler | Version: 8.2.1-rc3 Resolution: | Keywords: core-lint | case Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4160 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"6b52b4c832f888f7741a4ba0fec1fdac10244f6d/ghc" 6b52b4c8/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="6b52b4c832f888f7741a4ba0fec1fdac10244f6d" 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13990#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler