Skip to content

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

Sebastian Graf requested to merge wip/T18341 into master

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

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 (closed).

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

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

In summary, this patch fixes #18341 (closed), #17725 (closed), #18273 (closed).

Edited by Sebastian Graf

Merge request reports