PmCheck: Refactor the inhabitation test and fix unlifted fields (#18249)
We used to produce inhabitants of a pattern-match refinement type Nabla in the checker in at least two different and mostly redundant ways:
- There was
provideEvidence
which is used byGHC.HsToCore.PmCheck
to produce non-exhaustive patterns, which produces inhabitants of a Nabla as a sub-refinement type where all match variables are instantiated. - There also was
ensure{,All}Inhabited
which worked slightly different, but was whenever new type constraints or negative term constraints were added. See below whyprovideEvidence
andensureAllInhabited
can't be the same function, the main reason being performance. - And last but not least there was the
nonVoid
test, which tested that a given type was inhabited. We did use this for strict fields and -XEmptyCase in the past.
The overlap of (3) with (2) was always a major pet peeve of mine. The
latter was quite efficient and proven to work for recursive data types,
etc, but could not handle negative constraints well (e.g. we often want
to know if a refined type is empty, such as { x:[a] | x /= [] }
).
Lower Your Guards suggested that we could get by with just one, by
replacing both functions with inhabitationTest
in this patch.
That was only possible by implementing the structure of φ constraints
as in the paper, namely the semantics of φ constructor constraints.
This has a number of benefits:
- Proper handling of unlifted types and strict fields, fixing #18249 (closed),
without any code duplication between
GHC.HsToCore.PmCheck.Oracle.instCon
(wasmkOneConFull
) andGHC.HsToCore.PmCheck.checkGrd
. -
instCon
can perform thenonVoid
test (3) simply by emitting unliftedness constraints for strict fields. -
nonVoid
(3) is thus simply expressed by a call toinhabitationTest
. - Similarly,
ensureAllInhabited
(2), which we called after adding type info, now can similarly be expressed as the fuel-basedinhabitationTest
.
See the new Note [Why inhabitationTest doesn't call generateInhabitants]
why we still have to stick to "test" (1).
Fixes #18249 (closed) and brings nice metric decreases for T17836
(-76%) and
T17836b
(-46%), as well as T18478
(-8%) at the cost of a few very
minor regressions (< +2%), potentially due to the fact that
generateInhabitants
is more careful at suggesting the minimal COMPLETE
set.