Is an argument of type `a ~# b` relevant?

I was just browsing for a function like splitForAllTyCoVars/splitPiTys etc. that allowed myself to skip through all irrelevant arrows in a type like that of Eq# :: forall a. (a ~# a) -> a ~ a. Note that I consider all the pi binders in that type as irrelevant; there is no computational content whatsoever.

In that light, I found

-- | Extract a relevant type, if there is one.
binderRelevantType_maybe :: TyCoBinder -> Maybe Type
binderRelevantType_maybe (Named {}) = Nothing
binderRelevantType_maybe (Anon _ ty)  = Just (scaledThing ty)

And was hoping to combine it with splitPiTys. But alas, that function returns Just "a ~# a" for a ~# a, because it is an Anon binder.

I know that such coercion args are vital for our Core type theory, but I really wouldn't say that a ~# b is relevant for any a or b.

To me it looks like this is an anomaly in the usual "t -> is relevant, forall (a::t). is irrelevant" mantra, but still one worth considering.