Skip to content
  • Sebastian Graf's avatar
    PmCheck: Handle ⊥ and strict fields correctly (#18341) · 3777be14
    Sebastian Graf authored
    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:
        T12227
    3777be14