TestEquality clarification from core library devs

[robdockins]

The following patch has been approved and should eventually make it's way into base.

https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7333/diffs

It clarifies that testEquality should return Just Refl iff the corresponding type indices are the same, and reiterates that it is desirable that the class only be inhabited by singletons. This is incompatible with many of our typical uses of this class.

The actual class declaration will not change, so nothing will immediately break with future releases of base. However, going forward we will have to decide what to do about the fact that many of our uses of TestEquality will be considered law-breaking.

[travitch]

Fun. Since nearly all of our uses import the required class via Data.Parameterized.Classes (instead of the type equality module in base), we could always just duplicate the class definition with dire warnings that they are not the same. That would save us from having to change much client code.

That might ultimately be bad and confusing, though.

[robdockins]

I think duplicating the class and reusing the name would be strictly worse than doing nothing and having law-breaking instances.

[benjaminselfridge]

If I could go back in time, I would change EqF to correspond with OrdF. Our EqF is (I think) not really used much, because you have to know that the type indices are the same at compile time, whereas OrdF is heterogeneous, and the result gives you information both at the type- and value-level. EqF seems like a natural name for the corresponding equality type class.

Of course, going back and auditing all uses of TestEquality in Galois's codebase would be a nightmare. But if I had magical powers, that's probably what I would do.

I am not a huge fan of making our own TestEquality that conflicts with base, because I think TestEquality is already a bad name for the way we use it, and if we're going to fix the problem we should put our big boy pants on and fix the name while we're at it.

[robdockins]

I agree, EqF isn't terribly useful as-is. I'd be in favor of repurposing it, unless it is widely used in some way I'm not aware of.

Fortunately, we can make this transition gradually if we decide to do it, since TestEquality isn't going anywhere and we can have side-by-side instances for a time.

[benjaminselfridge]

I think repurposing EqF for this seems like a good idea; the only concern I have is that I'm not sure if EqF is actually used anywhere. But I'd be willing to spend a few hours investigating this.

[robdockins]

A moment of greping around leads me to believe we'll find very few uses. The only "real" use of eqF I can find is in the Eq instance for Pair, which flows into the Eq instance for MapF.

[eddywestbrook]

FWIW, the Heapster code uses testEquality a bunch for testing heterogeneous equality of expressions. As does the Hobbits library. If we have to call that typeclass something else, then that's fine, it's just annoying... :(

[benjaminselfridge]

I think Rob's point probably applies -- you should be able to keep using testEquality for as long as you feel like using it, and the migration to eqF (if it happens at all) can be gradual, I think.

[RyanGlScott]

Looking more at #132 (which moves in the direction of a more useful EqF class), I can't help but wonder if the new definition of EqF is too restrictive:

class EqF f where
  eqF :: f a -> f b -> Maybe (a :~: b)

I like the fact that the arguments (of type f a and f b) have different type parameters, which allows eqF to be used in more places than it currently can be used. I don't like the fact that it returns Maybe (a :~: b), however. The problem is that in the event that you have two equal values, you also have to produce a proof of equality between a and b. This can be done for some, but not all, data types. Consider Proxy, for instance:

data Proxy a = Proxy

Per Proxy's Eq and Eq1 instances, any two Proxy values are equal. Despite this, it would be impossible to implement an EqF instance for Proxy with the proposed class definition above. This is because if you have values of type Proxy a and Proxy b, then there is nothing to pattern-match on to convince GHC's typechecker that a equals b. We could return Nothing, I suppose, but I think that sends the wrong impression that the two Proxy values aren't equal. (As such, #132 removes the EqF Proxy instance entirely.)

I bring this up because I have a downstream application where I am relying on an EqF instance for a data type that is essentially the same as Proxy, and as far as I can tell, it would be impossible to support my use case using the proposed re-definition of EqF above. I'd like to come up with an alternative design that doesn't have this problem. Some possibilities:

1. Allow eqF to have arguments with different type indices, but return a Bool instead:

   class EqF f where
     eqF :: f a -> f b -> Bool

   This would have the disadvantage that you wouldn't be afforded the chance to learn that a :~: b in the event that a data type does offer such information, however.

2. Have eqF return a richer data type that encodes three possibilities. Something like:

   data BoolF a b
     = FalseF
     | TrueF (Maybe (a :~: b))
   
   class EqF f where
     eqF :: f a -> f b -> BoolF a b

   This way, it is obvious that eqF can conclude that two values are equal while opting not to produce an equality proof, making it suitable for an EqF Proxy instance.