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 CoercionHoles is that they don't really have an identity. They should just be mutable cells. We shouldn't ever e.g. compare two CoercionHoles 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] in GHC.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.)