Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
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:
a ~~ b
Once we have type applications in patterns, we'll be able to do
As @Int -> _
so does that mean you can't write (a, b) => ... as a => b => ... instead? :o
(a, b) => ...
a => b => ...
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