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).