nonVoid is too conservative w.r.t. strict argument types
In the implementation of the pattern-match coverage checker, the nonVoid
function checks is some Type
is inhabitable by at least one constructor. However, nonVoid
currently does not recursively call itself on the strict argument types of each constructor that is considered. This means that certain exhaustive functions are mistakenly flagged as non-exhaustive, such as in the following example:
{-# LANGUAGE EmptyCase #-}
{-# OPTIONS -Wincomplete-patterns #-}
module Bug where
import Data.Void
data V = MkV !Void
data S = MkS !V
f :: S -> a
f x = case x of {}
$ /opt/ghc/head/bin/ghci Bug.hs
GHCi, version 8.7.20180827: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:7: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: (MkS _)
|
11 | f x = case x of {}
| ^^^^^^^^^^^^
The natural solution would be to call nonVoid
recursively on strict argument types, so as to be able to tell that S
in uninhabitable. But we can't just do this willy nilly, since we could run into infinite loops with recursive examples like this one:
data Abyss = MkAbyss !Abyss
stareIntoTheAbyss :: Abyss -> a
stareIntoTheAbyss x = case x of {}
Better solution: put a recursive type checker into nonVoid
, and bail out if recursion is detected.
Patch incoming.
Trac metadata
Trac field | Value |
---|---|
Version | 8.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |