PmCheck: Positive info doesn't imply there is an inhabitant (#18960)
Consider T18960
:
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.
Fixes #18960 (closed). This MR also accepts new test output for T14059b
and marks it as unbroken, which it has been for quite a while.