6.2.14. Empty case alternatives¶
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.