6.2.15. Empty case alternatives

EmptyCase

Since:7.8.1

Allow empty case expressions.

The EmptyCase extension enables case expressions, or lambda-case expressions, that have no alternatives, thus:

case e of { }   -- No alternatives

or

\case { }       -- -XLambdaCase is also required

This can be useful when you know that the expression being scrutinised has no non-bottom values. For example:

data Void
f :: Void -> Int
f x = case x of { }

With dependently-typed features it is more useful (see #2431). For example, consider these two candidate definitions of absurd:

data a :~: b where
  Refl :: a :~: a

absurd :: True :~: False -> a
absurd x = error "absurd"    -- (A)
absurd x = case x of {}      -- (B)

We much prefer (B). Why? Because GHC can figure out that (True :~: False) is an empty type. So (B) has no partiality and GHC is able to compile with -Wincomplete-patterns and -Werror. On the other hand (A) looks dangerous, and GHC doesn’t check to make sure that, in fact, the function can never get called.