Skip to content

Check visibility of nested foralls in can_eq_nc (#18863)

Vladislav Zavialov requested to merge wip/int-index/caneqnc-deep-forall into master

Prior to this change, can_eq_nc checked the visibility of the outermost layer of foralls:

forall a. forall b. forall c. phi1
forall x. forall y. forall z. phi2
        ^^
     up to here

Then it delegated the rest of the work to can_eq_nc_forall, which split off all foralls:

forall a. forall b. forall c. phi1
forall x. forall y. forall z. phi2
                            ^^
                         up to here

This meant that some visibility flags were completely ignored. We fix this oversight by moving the check to can_eq_nc_forall.

Merge request reports