Opened 3 years ago

Closed 3 years ago

Last modified 23 months ago

#10180 closed task (fixed)

Lint check: Empty alternatives imply bottoming scrutinee

Reported by: nomeata Owned by: nomeata
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 7.11
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Change History (24)

comment:1 Changed 3 years ago by nomeata

Status: newinfoneeded

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?

Last edited 3 years ago by simonpj (previous) (diff)

comment:2 Changed 3 years ago by nomeata

Ok, added it to the linter for now; whether exprIsBottom should be extended is a different question.

Next linter error when compiling GHC:

It complains about this code:

*** Core Lint errors : in result of Simplifier ***
<no location info>: Warning:
    In a case alternative: (False)
    No alternatives for a case scrutinee not known to diverge for sure: \ (@ a_agBy) ->
                                                                          lvl_smAM @ a_agBy ds3_alsA
[…]
lvl_smAM :: forall a_agBy. Type -> a_agBy
[LclId, Arity=1, CallArity=1, Str=DmdType <B,1*U>b]
lvl_smAM =
  \ (@ a_agBy) (fn_ty_smsv :: Type) ->
    throw1
      @ GhcException
      @ a_agBy
      (PprPanic lvl_smAL (pprType fn_ty_smsv))
      $fExceptionGhcException
[…]
                                      case \ (@ a_agBy) -> lvl_smAM @ a_agBy ds3_alsA
                                      of _ [Occ=Dead] {

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

Last edited 3 years ago by nomeata (previous) (diff)

comment:3 in reply to:  1 Changed 3 years ago 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.

comment:4 in reply to:  2 ; Changed 3 years ago by simonpj

Replying to 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.

Simon

comment:5 in reply to:  4 Changed 3 years ago by nomeata

Hi,

Replying to simonpj:

Very interesting.

  • What program gives rise to case (x::Void) of {}?

Precisely that program :-)

See Data.Void:

absurd :: Void -> a
absurd a = case a 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.

I’ll do that first, and afterwards look into moving the no-constructor-test into exprIsBottom.

Replying to simonpj:

Replying to 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.

comment:6 Changed 3 years ago by simonpj

BTW, there should be no need to check both exprIsHNF and exprIsBottom!

comment:7 Changed 3 years ago by simonpj

branch wip/T10180

comment:8 Changed 3 years ago by nomeata

There is no end of reasons why something diverges:

=====> T2431(normal) 339 of 4438 [0, 0, 0] 
cd ./deSugar/should_compile &&  "/home/jojo/build/haskell/ghc-validate/inplace/bin/ghc-stage2" -c T2431.hs -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-db -rtsopts -fno-warn-tabs -fno-ghci-history  -ddump-simpl -dsuppress-uniques > T2431.comp.stderr 2>&1
Compile failed (status 256) errors were:
*** Core Lint errors : in result of Simplifier ***
T2431.hs:8:8: Warning:
    [in body of lambda with binder x :: Int :~: Bool]
    No alternatives for a case scrutinee not known to diverge for sure: x
*** Offending Program ***
absurd :: forall a. Int :~: Bool -> a
[LclIdX,
 Arity=1,
 Str=DmdType,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
absurd = \ (@ a) (x :: Int :~: Bool) -> case x of _ [Occ=Dead] { }

*** End of Offense ***

I’m beginning to wonder if the lint rule is a good idea. After all, by trying to add such a rule we are saying “definite divergence must be obvious”, and hence we would be precluding the compiler to derive and use definite divergence that is non-obvious, or that was obvious at one point in the pipeline, but isn’t any more later when the linter runs.

Here is an example of non-trivially always empty types: Void wrapped deeply in some strict data type. Or even Void as the result of a type function wrapped deeply in some strict data type.

comment:9 Changed 3 years ago 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

comment:10 Changed 3 years ago by nomeata

I’ll be happy to pursue this course and see how far it will take us, but my gut feeling is that this will never be complete and even if GHC+the test suite go through, someone will be able to figure out how to make the linter fail erroneously.

Making the check use dataConCannotMatch now, but it uses Unify.typesCantMatch which does not even look through newtypes (yet), so this will only get us so far...

comment:11 Changed 3 years ago by nomeata

Status: infoneedednew

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.

comment:12 Changed 3 years ago by simonpj

Perhaps in CoreUtils which contains the other place that dataConCannotMatch is called, so it's a related chunk of code.

comment:13 Changed 3 years ago by nomeata

Sounds good, thanks! Will push this as soon as the build validates on phabricator.

comment:14 Changed 3 years ago by Joachim Breitner <mail@…>

In 5673bfc49ec1e54a1540197078041a9da9754fa3/ghc:

exprIsBottom should look through type lambdas

as evaluting (\ (@ a) -> e) diverges if and only if evaluating e
diverges. This was found in the context of #10180.

comment:15 Changed 3 years ago by Joachim Breitner <mail@…>

In a0678f1f0e62496c108491e1c80d5eef3936474a/ghc:

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.

comment:16 Changed 3 years ago by nomeata

Resolution: fixed
Status: newclosed

comment:17 Changed 3 years ago 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

comment:18 Changed 3 years ago by Joachim Breitner <mail@…>

In 8f08069668f12ce019be3277bc4baacb477a77ed/ghc:

Add Note [No alternatives lint check]

in a follow up to #10180.

comment:19 Changed 3 years ago by nomeata

Of course, sorry for the negligence.

comment:20 Changed 3 years ago by Joachim Breitner <mail@…>

In 6cf0c7962c582eefb84cdf2735504d034fb16314/ghc:

Some stress tests for the empty case linter

This is a variation of T2431 where the emptyness of the type is hidden
behind a newtype, a type family and a closed type family. In all cases,
it would be sound for the compiler to determine that the equality type
is empty and the case alternatives may be dropped.

At the moment, GHC does _not_ determine that. But if it ever does, this
test ensures that we do not forget to make the lint from #10180 smarter
as well.

comment:21 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 33cfa5ff9db4e7886b3e7c2eed5ac1c75436bc4c/ghc:

More comments (related to Trac #10180)

comment:22 Changed 3 years ago by nomeata

A small change in the simplifier settings showed a False Positive of the new lint check: https://phabricator.haskell.org/D851#23033

Given that the check is known to be not complete, I suggest to turn it into a lint warning.

comment:23 Changed 3 years ago by simonpj

Let's not move too fast See my comments on Phab:D851.

comment:24 Changed 23 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.