6.2.14. Empty case alternatives

EmptyCase

Since:

7.8.1

Status:

Included in GHC2021

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

Note that it is not allowed for \cases, since it would be unclear how many patterns are being matched.

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.