Skip to content

PmCheck: Positive info doesn't imply there is an inhabitant (#18960)

Sebastian Graf requested to merge wip/T18960 into master

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.

Merge request reports