Skip to content

PmCheck: Refactor the inhabitation test and fix unlifted fields (#18249)

Sebastian Graf requested to merge wip/T18249 into master

We used to produce inhabitants of a pattern-match refinement type Nabla in the checker in at least two different and mostly redundant ways:

  1. There was provideEvidence which is used by GHC.HsToCore.PmCheck to produce non-exhaustive patterns, which produces inhabitants of a Nabla as a sub-refinement type where all match variables are instantiated.
  2. There also was ensure{,All}Inhabited which worked slightly different, but was whenever new type constraints or negative term constraints were added. See below why provideEvidence and ensureAllInhabited can't be the same function, the main reason being performance.
  3. 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:

  1. Proper handling of unlifted types and strict fields, fixing #18249 (closed), without any code duplication between GHC.HsToCore.PmCheck.Oracle.instCon (was mkOneConFull) and GHC.HsToCore.PmCheck.checkGrd.
  2. instCon can perform the nonVoid test (3) simply by emitting unliftedness constraints for strict fields.
  3. nonVoid (3) is thus simply expressed by a call to inhabitationTest.
  4. Similarly, ensureAllInhabited (2), which we called after adding type info, now can similarly be expressed as the fuel-based inhabitationTest.

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.

Edited by Sebastian Graf

Merge request reports