PmCheck: Inhabitation testing through set approximations
The coverage checker lacks the inductive reasoning to find that data types like data Void = Void !Void
are empty.
Here are a few examples:
{# OPTIONS_GHC Wincompletepatterns fforcerecomp #}
{# LANGUAGE GADTs, DataKinds, KindSignatures, EmptyCase #}
module Lib where
data Void = Void !Void
 Detecting that 'Void' is empty requires inductive reasoning.
f :: Void > a
f x = case x of {}  exhaustive!
data Nat = Z  S Nat
data R (a :: Nat) (b :: Nat) where
RA :: R Z (S Z)
RB :: R Z (S (S Z))
RTrans :: !(R a b) > !(R b c) > R a c
 Detecting that it's not possible to instantiate RTrans is quite a bit harder
 and requires reasoning about set approximations
 (https://dl.acm.org/doi/pdf/10.1145/1292597.1292606).
g :: R a b > ()
g RA = ()
g RB = ()  exhaustive!
h :: R (S Z) b > ()
h x = case x of {}  exhaustive!
Current output:
test.hs:11:7: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In a case alternative: Patterns not matched: Void _

11  f x = case x of {}
 ^^^^^^^^^^^^
test.hs:25:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’: Patterns not matched: RTrans _ _

25  g RA = ()
 ^^^^^^^^^...
test.hs:29:7: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In a case alternative: Patterns not matched: RTrans _ _

29  h x = case x of {}
 ^^^^^^^^^^^^
I think detecting emptiness of Void
is entirely within reach of the current implementation of the coverage checker (Edit: Not anymore). The same can't be said about R
: We need another model for that based on set approximations (https://dl.acm.org/doi/pdf/10.1145/1292597.1292606). I think the problem is that instCon
performs sort of a recursive topdown search for inhabitants, whereas set approximations are more of a bottomup approach: Begin with the empty set, add inhabitants by instantiating nullary constructors and so on, then iterate to build recursive values bottomup from the inhabitants of the last iteration. Exactly how inductive values are defined, but quite unlike what we currently do for inhabitation testing.
This ticket is just to track that deficiency and maybe implement support for Void
. The same applies to

UVoid
from #18249 (closed) 
Abyss
from #15305 (closed).  Empty unlifted sums, from #18773