Note [Incompleteness and linearity]

GHC/HsToCore/Utils.hs:421 compiler

The default branch of an incomplete pattern match is compiled to a call
to 'error'.
Because of linearity, we wrap it with an empty case. Example:

f :: a %1 -> Bool -> a
f x True = False

Adding 'f x False = error "Non-exhaustive pattern..."' would violate
the linearity of x.
Instead, we use 'f x False = case error "Non-exhaustive pattern..." :: () of {}'.
This case expression accounts for linear variables by assigning bottom usage
(See Note [Bottom as a usage] in GHC.Core.Multiplicity).
This is done in mkErrorAppDs, called from mkFailExpr.
We use '()' instead of the original return type ('a' in this case)
because there might be representation polymorphism, e.g. in

g :: forall (a :: TYPE r). (() -> a) %1 -> Bool -> a
g x True = x ()

adding 'g x False = case error "Non-exhaustive pattern" :: a of {}'
would create an illegal representation-polymorphic case binder.
This is important for pattern synonym matchers, which often look like this 'g'.

Similarly, a hole
h :: a %1 -> a
h x = _
is desugared to 'case error "Hole" :: () of {}'. Test: LinearHole.

Instead of () we could use Data.Void.Void, but that would require
moving Void to GHC.Types: partial pattern matching is used in modules
that are compiled before Data.Void.
We can use () even though it has a constructor, because
Note [Case expression invariants] point 4 in GHC.Core is satisfied
when the scrutinee is bottoming.

You might wonder if this change slows down compilation, but the
performance testsuite did not show up any regressions.

For uniformity, calls to 'error' in both cases are wrapped even if -XLinearTypes
is disabled.

References 2

Referenced by 2