如何为Haskell模式同义词显式实例化类型变量？

问题背景 #

给出以下Haskell代码：

{-# LANGUAGE GADTs, PatternSynonyms #-}

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 -- 无法编译

尝试通过显式指定AsType的类型参数a为Int、b为b'来让AsInt编译，试过添加显式类型签名和直接写类型应用都报错，想知道有没有可行方法，或者失败的原因（已知直接用asType写模式视图可行，但不够简洁）。

可行解决方法 #

开启TypeApplications和ScopedTypeVariables扩展，通过视图模式包裹类型应用来显式指定AsType的参数，修改后的代码如下：

{-# LANGUAGE GADTs, PatternSynonyms, TypeApplications, ScopedTypeVariables #-}

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 :: forall b'. Typeable b' => (Int ~ b') => F Int -> F b'
pattern AsInt e <- (AsType @Int @b' e)

核心是将AsType的调用包裹在括号内，用@Int和@b'显式指定其两个类型参数，ScopedTypeVariables则确保b'在模式的作用域内可被引用。

如果不想用括号包裹，也可以先定义一个固定了a为Int的中间模式别名，再基于它实现AsInt：

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

pattern AsInt :: forall b'. Typeable b' => (Int ~ b') => F Int -> F b'
pattern AsInt e <- AsTypeInt e

原代码编译失败的原因 #

1. 类型推断歧义：原代码中AsType e未指定类型参数，GHC无法自动关联AsType的a与AsInt约束中的Int，也无法将AsType的b与b'绑定，导致类型匹配失败。
2. 模式语法限制：Haskell的模式别名语法不支持直接在模式位置写AsType :: ... e这种显式类型标注；单纯的AsType @Int e也不符合模式解析规则，必须包裹成视图模式（括号内的表达式），GHC才能正确处理类型应用。

内容的提问来源于stack exchange，提问作者Artem Yu