haskell - 我怎样才能写出这个模式同义词而没有歧义的类型错误？

Question

使用 ViewPatterns和 Data.Typeable ，我已经设法编写了一个函数，该函数允许我编写类似于类型案例分析的内容。观察:

{-# LANGUAGE GADTs, PatternSynonyms, RankNTypes, ScopedTypeVariables
           , TypeApplications, TypeOperators, ViewPatterns #-}

import Data.Typeable

viewEqT :: forall b a. (Typeable a, Typeable b) => a -> Maybe ((a :~: b), b)
viewEqT x = case eqT @a @b of
  Just Refl -> Just (Refl, x)
  Nothing -> Nothing

evilId :: Typeable a => a -> a
evilId (viewEqT @Int -> Just (Refl, n)) = n + 1
evilId (viewEqT @String -> Just (Refl, str)) = reverse str
evilId x = x

以上evilId函数确实非常邪恶，因为它使用 Typeable彻底颠覆参数化:

ghci> evilId True
True
ghci> evilId "hello"
"olleh"

由于我喜欢作恶，我对此很满意，但是上面的语法很嘈杂。我希望能够更清楚地编写相同的代码，因此我决定编写一个模式同义词:

pattern EqT :: forall b a. (Typeable a, Typeable b) => (a ~ b) => b -> a
pattern EqT x <- (viewEqT @b -> Just (Refl, x))

我想我可以使用这个模式同义词来使我的邪恶案例分析更容易阅读:

evilId :: Typeable a => a -> a
evilId (EqT (n :: Int)) = n + 1
evilId (EqT (str :: String)) = reverse str
evilId x = x

可悲的是，这根本不起作用。 GHC 在对模式进行类型检查之前似乎没有引用我的类型注释，因此它认为 b在每个模式中都是一个不明确的变量。有什么方法可以用模式同义词干净地包装这些模式，还是会被我的长 View 模式卡住？

Answer 1

如果目标是找到一些干净的语法来实现您的 evilId函数，你可以这样写:

{-# Language ScopedTypeVariables, GADTs, TypeApplications #-}

module Demo where

import Data.Typeable

evilId :: forall a. Typeable a => a -> a
evilId x
  | Just Refl <- eqT @a @Int    = x+1
  | Just Refl <- eqT @a @String = reverse x
  | otherwise                   = x

不幸的是，这对解决模式同义词的歧义没有帮助。