CoVar in CoercionHole?
GHC currently carries a CoVar
inside of a CoercionHole
. I've always been uncomfortable about this design, because the whole point of CoercionHole
s is that they don't really have an identity. They should just be mutable cells. We shouldn't ever e.g. compare two CoercionHole
s for equality, which is the real point of having a CoVar
.
Yet the design has been motivated by simplicity in floatEqualities
: we can't float an equality out of an implication that has a free coercion hole as a wanted. So indeed we do need an identity for coercion holes. Now, happily, !4200 (closed) has gotten rid of floatEqualities
, and so that motivation no longer stands.
This ticket is about what we should do; it is copied from !4200 (comment 318286). @simonpj says:
See orphaned
Note [CoercionHoles and coercion free variables]
inGHC.Core.TyCo.Rep
. Since we aren't doing floating any more, that Note doesn't make sense any more. I think we still want a CoVar in a coercion hole
- For debugging printouts
- Again debugging, so we can check that we fill in with something of the right kind
- And perhaps, so that when taking free vars, we get free vars of the kind of the hole
But I'm unsure of the third point, esp since the free-var code just point to the now-bogus
Note [CoercionHoles and coercion free variables]
.
We absolutely need a way of tracking holes for debugging. Previous to giving them a CoVar
, they had a Unique
, just for printing. I think we should restore that.
We also need a kind. Not only for debugging, but also so that we can write coercionKind
.
During free-var taking, we sometimes want to look deeply and sometimes shallowly. I think this will take a little scrutiny.
But I would prefer to have a Unique
and a Kind
, not a CoVar
. (I know a CoVar
is essentially a Unique
paired with a Kind
. But it could easily be abused if stored together.)