Testing type equality concisely - Haskell

I was unhappy with having to tinker with Refls when trying multiple matches on TypeRep, and I've ended up with these helpers:

-- introduces result in scope
pattern Is :: () => a ~~ b => Maybe (a :~~: b)
pattern Is = Just HRefl

-- let's me pass expected type as type argument
as :: forall a b. Typeable a => TypeRep b -> Maybe (a :~~: b)
as = eqTypeRep typeRep

which can be used as

case typeOf x of
  (as @Int -> Is) -> _ -- x ~~ Int in scope

Am I reinventing the wheel and there's already something similar or better?

the () => is some hack for pattern synonyms?

PatternSynonyms are sort of interesting because the can both want and provide constraints - to make it possible to declare both situations, GHC recognizes two separate constraints in their signatures as corresponding options

So Is wants () (nothing) and provides a ~~ b :big_smile:

Once we have type applications in patterns, we'll be able to do

As @Int -> _

(I guess)

so does that mean you can't write (a, b) => ... as a => b => ... instead? :o

Not in signatures of patterns, but you can otherwise

It's a hack, but not a terrible one

I would snoop around singletons, to see if there is something like what you've defined