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.