#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by nomeata): * status: new => infoneeded Comment: Sure enough, it trips over this {{{ *** Core Lint errors : in result of Simplifier *** libraries/base/Data/Void.hs:66:8: Warning: [in body of lambda with binder a_a2y6 :: Void] No alternatives for a case scrutinee not known to diverge for sure: a_a2y6 }}} Simon, what would you prefer: Should `exprIsBottom e` hold for all `e` where the type is a data type with no constructors, or should the lint check take that into account? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj):

Simon, what would you prefer: Should `exprIsBottom e` hold for all `e` where the type is a data type with no constructors, or should the lint check take that into account?

Very interesting. * What program gives rise to `case (x::Void) of {}`? * Yes, I think there is a case for making `exprIsBottom` hold for data types with no constructors; after all, such an expression is bound to diverge. * A slightly less pervasive change would to to say that an empty `case` is ok on a data type that has an empty set of constructors. Less pervasive in the sense that it affects this Lint check only, whereas the `exprIsBottom` fix would have broader implications: good ones, I think, but also rare. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by nomeata): Hi, Replying to [comment:3 simonpj]:

Very interesting. * What program gives rise to `case (x::Void) of {}`?

* Yes, I think there is a case for making `exprIsBottom` hold for data types with no constructors; after all, such an expression is bound to

* A slightly less pervasive change would to to say that an empty `case` is ok on a data type that has an empty set of constructors. Less

Precisely that program :-) See `Data.Void`: {{{ absurd :: Void -> a absurd a = case a of {} }}} diverge. pervasive in the sense that it affects this Lint check only, whereas the `exprIsBottom` fix would have broader implications: good ones, I think, but also rare. I’ll do that first, and afterwards look into moving the no-constructor- test into `exprIsBottom`. Replying to [comment:4 simonpj]:

Replying to [comment:2 nomeata]:

...

So there is a lambda under the case, but it is a type lambda. Bogus or not?

Ha! There's a missing case in `exprIsBottom`: {{{ exprIsBottom (Lam v e) | isTyVar v = exprIsBottom e }}} Well spotted.

I’ll add that and see if the linter is happy then. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): branch `wip/T10180` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Well that's why I said (somewhere) that I wasn't certain this would work, but it would be interesting to know. The point is: to make the empty case, GHC '''knew''' at some point that the expression must diverge. So how has it lost that knowledge? I think that in this case it's a use of `dataConCantMatch`. So maybe we can beef up `isEmptyTy` to use that information? (And ultimately perhaps beef up `exprIsBottom`.) My point is, this is a useful quest. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by nomeata): * status: infoneeded => new Comment: Ok, with the better `isEmptyTy`, it goes through, see Phab:D753. I’m not sure where best to put `isEmptyTy`. My first guess was `Types.hs`, but that would require extending `DataCon.hs-boot`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by nomeata): Sounds good, thanks! Will push this as soon as the build validates on phabricator. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by Joachim Breitner ): In [changeset:"a0678f1f0e62496c108491e1c80d5eef3936474a/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="a0678f1f0e62496c108491e1c80d5eef3936474a" New Lint check: no alternatives implies bottoming expression detected either by exprIsBottom or by an empty type. This was suggested by SPJ and fixes #10180. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Wuuld it be possible to add a `Note` to `isEmptyTy` and the call in CoreLint, explaiing what is going on, and referring to this ticket. As its stands there is zero commentary. Thanks Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by nomeata): Of course, sorry for the negligence. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"33cfa5ff9db4e7886b3e7c2eed5ac1c75436bc4c/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="33cfa5ff9db4e7886b3e7c2eed5ac1c75436bc4c" More comments (related to Trac #10180) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10180: Lint check: Empty alternatives imply bottoming scrutinee -------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Let's not move too fast See my comments on Phab:D851. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10180#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler