Commit 3777be14 authored by Sebastian Graf's avatar Sebastian Graf

PmCheck: Handle ⊥ and strict fields correctly (#18341)

In #18341, we discovered an incorrect digression from Lower Your Guards.
This MR changes what's necessary to support properly fixing #18341.

In particular, bottomness constraints are now properly tracked in the
oracle/inhabitation testing, as an additional field
`vi_bot :: Maybe Bool` in `VarInfo`. That in turn allows us to
model newtypes as advertised in the Appendix of LYG and fix #17725.
Proper handling of ⊥ also fixes #17977 (once again) and fixes #18670.

For some reason I couldn't follow, this also fixes #18273.

I also added a couple of regression tests that were missing. Most of
them were already fixed before.

In summary, this patch fixes #18341, #17725, #18273, #17977 and #18670.

Metric Decrease:
parent 6abe4a1c
Pipeline #24556 failed with stages
in 288 minutes and 32 seconds