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 -Wincomplete-patterns -fforce-recomp #-}
{-# 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: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: Void _
   |
11 | f x = case x of {}
   |       ^^^^^^^^^^^^

test.hs:25:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘g’: Patterns not matched: RTrans _ _
   |
25 | g RA = ()
   | ^^^^^^^^^...

test.hs:29:7: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    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 top-down search for inhabitants, whereas set approximations are more of a bottom-up approach: Begin with the empty set, add inhabitants by instantiating nullary constructors and so on, then iterate to build recursive values bottom-up 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