diff options
author | Sebastian Graf <sebastian.graf@kit.edu> | 2020-11-19 14:32:33 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-01-17 05:46:45 -0500 |
commit | 23a545df75002060ed7bcb8bcc0e0511b7f9fb7d (patch) | |
tree | cfd5a6eb4d7939517af036c0e27b21f756f50e92 /testsuite | |
parent | fe344da9be83be4c7c0c7f76183acfe0a234cc5d (diff) | |
download | haskell-23a545df75002060ed7bcb8bcc0e0511b7f9fb7d.tar.gz |
PmCheck: Positive info doesn't imply there is an inhabitant (#18960)
Consider `T18960`:
```hs
pattern P :: a -> a
pattern P x = x
{-# COMPLETE P :: () #-}
foo :: ()
foo = case () of
P _ -> ()
```
We know about the match variable of the case match that it is equal to `()`.
After the match on `P`, we still know it's equal to `()` (positive info), but
also that it can't be `P` (negative info). By the `COMPLETE` pragma, we know
that implies that the refinement type of the match variable is empty after the
`P` case.
But in the PmCheck solver, we assumed that "has positive info" means
"is not empty", thus assuming we could omit a costly inhabitation test. Which
is wrong, as we saw above.
A bit of a complication arises because the "has positive info" spared us
from doing a lot of inhabitation tests in `T17836b`. So we keep that
check, but give it a lower priority than the check for dirty variables
that requires us doing an inhabitation test.
Needless to say: This doesn't impact soundness of the checker at all,
it just implements a better trade-off between efficiency and precision.
Fixes #18960.
Metric Decrease:
T17836
Diffstat (limited to 'testsuite')
-rw-r--r-- | testsuite/tests/pmcheck/complete_sigs/T18960.hs | 13 | ||||
-rw-r--r-- | testsuite/tests/pmcheck/complete_sigs/T18960b.hs | 20 | ||||
-rw-r--r-- | testsuite/tests/pmcheck/complete_sigs/T18960b.stderr | 20 | ||||
-rw-r--r-- | testsuite/tests/pmcheck/complete_sigs/all.T | 2 |
4 files changed, 55 insertions, 0 deletions
diff --git a/testsuite/tests/pmcheck/complete_sigs/T18960.hs b/testsuite/tests/pmcheck/complete_sigs/T18960.hs new file mode 100644 index 0000000000..ed441647d7 --- /dev/null +++ b/testsuite/tests/pmcheck/complete_sigs/T18960.hs @@ -0,0 +1,13 @@ +{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-} +{-# LANGUAGE PatternSynonyms #-} + +module T18960 where + +pattern P :: a -> a +pattern P x = x +{-# COMPLETE P :: () #-} + +foo :: () +foo = case () of + P _ -> () + diff --git a/testsuite/tests/pmcheck/complete_sigs/T18960b.hs b/testsuite/tests/pmcheck/complete_sigs/T18960b.hs new file mode 100644 index 0000000000..0cccc8aff1 --- /dev/null +++ b/testsuite/tests/pmcheck/complete_sigs/T18960b.hs @@ -0,0 +1,20 @@ +{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-} +{-# LANGUAGE PatternSynonyms #-} + +module T18960b where + +pattern P :: a -> a +pattern P x = x +{-# COMPLETE P :: () #-} + +bar :: () +bar = case undefined of + P ((), "hello") -> () + -- prints too many of apparently the same missing patterns, + -- because we prefer to report positive info (@((), [])@) rather than + -- negative info (@P ((), x:_) where x is not one of {'h'}@) + +baz :: () +baz = case undefined of + P ((), "hello") -> () + -- This function is proof that we in theory can provide a "better" warning. diff --git a/testsuite/tests/pmcheck/complete_sigs/T18960b.stderr b/testsuite/tests/pmcheck/complete_sigs/T18960b.stderr new file mode 100644 index 0000000000..6af7fa7bc1 --- /dev/null +++ b/testsuite/tests/pmcheck/complete_sigs/T18960b.stderr @@ -0,0 +1,20 @@ + +T18960b.hs:11:7: warning: [-Wincomplete-patterns (in -Wextra)] + Pattern match(es) are non-exhaustive + In a case alternative: + Patterns of type ‘((), String)’ not matched: + P ((), []) + P ((), (p : P _)) where p is not one of {'h'} + P ((), ['h']) + P ((), ('h' : p : P _)) where p is not one of {'e'} + ... + +T18960b.hs:18:7: warning: [-Wincomplete-patterns (in -Wextra)] + Pattern match(es) are non-exhaustive + In a case alternative: + Patterns of type ‘((), String)’ not matched: + P ((), []) + P ((), (p : P _)) where p is not one of {'h'} + P ((), ['h']) + P ((), ('h' : p : P _)) where p is not one of {'e'} + ... diff --git a/testsuite/tests/pmcheck/complete_sigs/all.T b/testsuite/tests/pmcheck/complete_sigs/all.T index 2728121160..dc80cb3d0e 100644 --- a/testsuite/tests/pmcheck/complete_sigs/all.T +++ b/testsuite/tests/pmcheck/complete_sigs/all.T @@ -26,3 +26,5 @@ test('T14851', normal, compile, ['']) test('T17149', normal, compile, ['']) test('T17386', normal, compile, ['']) test('T18277', normal, compile, ['']) +test('T18960', normal, compile, ['']) +test('T18960b', normal, compile, ['']) |