1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
.. _empty-case:
Empty case alternatives
-----------------------
.. extension:: EmptyCase
:shortdesc: Allow empty case alternatives.
:since: 7.8.1
:status: Included in :extension:`GHC2024`, :extension:`GHC2021`
Allow empty case expressions.
The :extension:`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 :ghc-ticket:`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 :ghc-flag:`-Wincomplete-patterns` and
:ghc-flag:`-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.
|
