Opened 3 years ago

Closed 3 years ago

#11806 closed bug (duplicate)

GHC does not warn for mistakenly empty case

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.3
Keywords: PatternMatchWarnings Cc: gkaracha
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: #10746, #7669, #11390 Differential Rev(s):
Wiki Page:

Description

{-# LANGUAGE EmptyCase #-}
{-# OPTIONS_GHC -Wall -fwarn-incomplete-uni-patterns #-}

oops :: Int -> a
oops x = case x of {}

Since Int is inhabited, I would expect a warning, but I get none. Since empty case is typically used in situations where programmers want GHC to see an absurdity, this seems most unfortunate.

Change History (8)

comment:1 Changed 3 years ago by simonpj

Cc: gkaracha added

Yes that is odd. If you have

module T11806 where

f1 :: Int -> Int
f1 x = case x of { 1 -> 2 }

f2 :: Bool -> Int
f2 x = case x of { True -> 2 }

you get (with 8.0)

T11806.hs:7:8: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative:
        Patterns not matched: p where p is not one of {1}

T11806.hs:10:8: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: False

but if you remove all the branches, you get no warnings at all!

I'm adding George (who is responsible for pattern match overlap checks) in cc.

comment:2 in reply to:  description Changed 3 years ago by gkaracha

Replying to dfeuer:

{-# LANGUAGE EmptyCase #-}
{-# OPTIONS_GHC -Wall -fwarn-incomplete-uni-patterns #-}

oops :: Int -> a
oops x = case x of {}

Since Int is inhabited, I would expect a warning, but I get none. Since empty case is typically used in situations where programmers want GHC to see an absurdity, this seems most unfortunate.

Indeed. Yet, I feel like there is a big misconception here, from the you said

Since Int is inhabited

It is indeed inhabited, but like any other type in Haskell, where every type is inhabited. That is, for the following (see #11390) a warning should also be expected:

silly1 :: Void -> Void
silly1 x = case x of {}

There have been separate discussions on this (see related tickets #10746, #7669, #11390) and I think that we have a design choice to make here. Unless you force the argument in some other way like:

silly2 :: Void -> Void
silly2 x = x `seq` case x of {}

or

silly3 :: Void -> Void
silly3 (!x) = case x of {}

then it is indeed non-exhaustive. This means that in almost all cases, an empty case expression will issue a warning (which I think is the right thing to do). Of course, in silly2 and silly3 the warning is too conservative but remember that type inhabitation is undecidable. Hence, I see two choices here. We can:

  1. Always issue a non-exhaustive warning for empty case expressions, or
  2. Never issue a non-exhaustive warning for empty case expressions.

I am pointing this out because before #7669 we would issue the warning you seek here and it has been intentionally changed.

comment:3 Changed 3 years ago by gkaracha

comment:4 Changed 3 years ago by gkaracha

Keywords: PatternMatchWarnings added

comment:5 Changed 3 years ago by nomeata

gkaracha, you are right that dfeuer’s working is unfortunate. He probably should have said “inhabited by a value” (in contrast to “inhabited by ⊥”).

I don’t follow your argument about silly1 and your conclusion. I would say that an empty case should issue an warning whenever the type has a constructor (and in with GADTs, if GHC cannot prove this constructor to have an impossible type).

comment:6 Changed 3 years ago by dfeuer

nomeata speaks my mind. When I said "inhabited", I meant properly inhabited. Empty case should issue a warning under the conditions he indicates. If the type of the scrutinee is not apart from the result types of all constructors, then I've made a mistake and I want to know about it.

comment:7 Changed 3 years ago by simonpj

Indeed. Another way to see it is via my examples in comment:1. It is extremely unexpected that removing one alternative from an exhaustive Boolean case would yield a warning, but removing both alternatives does not.

comment:8 Changed 3 years ago by dfeuer

Resolution: duplicate
Status: newclosed

This appears to be a duplicate of #10746

Note: See TracTickets for help on using tickets.