Explicit type variable instantiation for pattern synonyms?

125 views Asked by At

Suppose, I have the following code

data F a where
  F :: Typeable a => F a

asType :: forall b a. Typeable b => F a -> Maybe (a :~: b, F b)
asType e@F{} = case eqT @b @a of
  Just Refl -> Just (Refl, e)
  Nothing -> Nothing

pattern AsType :: forall a b. Typeable a => (a ~ b) => F a -> F b
pattern AsType e <- (asType @a -> Just (Refl, e))

pattern AsInt :: Typeable b' => (Int ~ b') => F Int -> F b'
pattern AsInt e <- AsType e -- doesn't compile

If I could explicitly instantiate the type parameter a in AsType with Int and the type parameter b with b' it would probably work.

I tried to give AsType it an explicit type signature ((AsType :: …) e) and it's a parsing error. I tried to use type applications — to no avail as well.

How can I make it work, if it's possible? If not, why?

(I can implement AsInt through a pattern view with asType, but that it isn't interesting and also more verbose)

0

There are 0 answers