Skip to content

Re-quantify when generalising over rewrite rule types

Ryan Scott requested to merge wip/T17710 into master

Previously, tcRules would check for naughty quantification candidates (see Note [Naughty quantification candidates] in TcMType) when generalising over the type of a rewrite rule. This caused sensible-looking rewrite rules (like those in #17710 (closed)) to be rejected. A more permissing (and easier-to-implement) approach is to do what is described in Note [Generalising in tcTyFamInstEqnGuts] in TcTyClsDecls: just re-quantify all the type variable binders, regardless of the order in which the user specified them. After all, the notion of type variable specificity has no real meaning in rewrite rules, since one cannot "visibly apply" a rewrite rule. I have written up this wisdom in Note [Re-quantify type variables in rules] in TcRules.

As a result of this patch, compiling the ExplicitForAllRules1 test case now generates one fewer warning than it used to. As far as I can tell, this is benign, since the thing that the disappearing warning talked about was also mentioned in an entirely separate warning.

Fixes #17710 (closed).

Merge request reports