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