Skip to content

Track visibility in forall-coercions

Matthew Craven requested to merge wip/forall-vis-coercions into master

This is a prototype of the implementation approach to solution (b) at ghc-proposals issue 558 as I proposed in these comments.

It also addresses #22537 (closed) both

  • Bug
  • Opportunity

I implemented this because the "drop the visibilities-distinction entirely in Core" approach proposed by @int-index and pursued in !9594 (closed) and !9912 (closed) still doesn't sit right by me, and I think the cost of the "track visibilities properly in Core" approach is likely entirely reasonable.

TODOs include:

  • Fiddle with pretty-printing
  • Bring the documented Core formalism up-to-date with this

cc @int-index @rae @simonpj

This patch does just two things:

  1. Track the visibilities of both sides in any ForAllCo. See the data constructor for ForAllCo in GHC.Core.TyCo.Rep.
  2. Establish a lint-checked invariant that a ForAllCo with nominal role must have the same visibility on both sides. See the typing rule in Note [Forall coercions] in GHC.Core.TyCo.Rep.

That's it! Most of the changes in this patch are adapting existing bits of code to the extra two fields of ForAllCo in "obvious" ways. But there are tricky bits in:

  • the coercion optimizer
  • the typechecker
    • tricky mostly because the existing matching of forall-types is very obviously not correct, even ignoring issues of visibility; therefore it doesn't effectively suggest a reasonable way of doing things
  • hopefully nowhere else, because if so it's no longer top-of-mind
Edited by Simon Peyton Jones

Merge request reports