## Evidence for equality constraints on typeclass methods isn’t erased

Generally, I expect `a ~ b`

constraints to have no runtime cost, so I was surprised to discover that they sometimes do. If I understand correctly, constraints of type `a ~ b`

are boxed versions of `a ~# b`

, the latter of which have no runtime representation. Ordinarily, this boxing and unboxing is eliminated via worker/wrapper just like any other boxing, but worker/wrapper can only be performed at call sites to known functions, so equality constraints on typeclass methods are not erased unless the method is specialized. This program illustrates that:

```
{-# LANGUAGE ConstrainedClassMethods, TypeFamilies #-}
module M where
type family F a
class C a where
m :: F a ~ Int => a -> Bool
f :: (C a, F a ~ Int) => a -> Bool
f x = not (m x)
```

Compiling with `-O -ddump-simpl`

reveals that the call to `m`

inside `F a ~ Int`

really does pass a boxed equality.

This seems silly to me. As far as I can tell, equalities are aggressively forced, so it would be entirely safe to perform a worker/wrapper-esque transformation to the `C`

constructor itself. Specifically, GHC could desugar `C`

into the following:

```
newtype C a = $WC { $wm :: F a ~# Int -> a -> Bool }
C :: (F a ~ Int => a -> Bool) -> C a
C m = $WC { $wm = m `seq` \co -> m (Eq# co) }
m :: (C a, F a ~ Int) => a -> Bool
m ($WC { $wm }) (Eq# co) = $wm co
```

The equality argument would be erased on both ends via the same mechanism that exists today for worker/wrapper DataCons, and the resulting program would be slightly more efficient.

Maybe there is some problem with this scheme I’m not seeing; it’s entirely possible. I don’t know all the subtleties. But seeing as it seems totally sound to me based on the investigation I’ve done so far, and since equalities *not* being erased was so surprising to me, I feel like it isn’t entirely unreasonable to consider this a bug rather than a missing feature (though that is admittedly arguable).