Skip to content

Don't mark closed type family equations as occurrences

Ryan Scott requested to merge wip/T18470 into master

Previously, rnFamInstEqn would mark the name of the type/data family used in an equation as an occurrence, regardless of what sort of family it is. Most of the time, this is the correct thing to do. The exception is closed type families, whose equations constitute its definition and therefore should not be marked as occurrences. Overzealously counting the equations of a closed type family as occurrences can cause certain warnings to not be emitted, as observed in #18470 (closed).

This fixes #18470 (closed) with a little bit of extra-casing in rnFamInstEqn. To accomplish this, I added an extra ClosedTyFamInfo field to the NonAssocTyFamEqn constructor of AssocTyFamInfo and refactored the relevant call sites accordingly so that this information is propagated to rnFamInstEqn.

Edited by Ryan Scott

Merge request reports