基于GADTs的类型化形式语言中showVal实现报错问题

咱们先来拆解编译器报错的核心原因：你的Character类里showVal的类型签名没有把Typey s中的s和第二个参数a的类型关联起来。原来的签名里，a1（编译器报错里的变量名）是一个独立的刚性类型变量，和s所属的c a没有绑定关系，导致当你尝试匹配Typey EqualSign时，编译器没办法推断出a1应该是()，自然就报类型不匹配的错误了。

修复方案：明确类型关联 #

我们只需要调整Character类的定义，让showVal的类型签名明确s和a的绑定关系——通过forall把a和s的作用域绑定在一起，这样编译器就能根据s的构造函数推断出对应的a类型了。

修改后的完整代码如下：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Kind

data Typey (s :: c) = Marker

-- 修改Character类的showVal签名，绑定a和s的作用域
class Character c where
  showVal :: forall a (s :: c a). Typey s -> a -> ShowS

class Character (Letter l) => Alphabet l where
  data family Letter l :: * -> *

data Symbol l (a :: Letter l s) where
  Terminal :: (Alphabet l) => s -> Symbol l (a :: Letter l s)

instance (Alphabet l) => Show (Symbol l a) where
  showsPrec d (Terminal val) = showVal (Marker :: Typey a) val

-- 示例语言
data ExampleLanguage = ExampleLanguage

instance Alphabet ExampleLanguage where
  data Letter ExampleLanguage a where
    Variable :: Letter ExampleLanguage String
    Comment :: Letter ExampleLanguage String
    EqualSign :: Letter ExampleLanguage ()
    Deref :: Letter ExampleLanguage ()

-- 现在可以正常匹配每个Letter构造函数对应的类型了
instance Character (Letter ExampleLanguage) where
  showVal (_ :: Typey Variable) = showString
  showVal (_ :: Typey Comment) = showString
  showVal (_ :: Typey EqualSign) = const $ showString "="
  showVal (_ :: Typey Deref) = const $ showString "*"

test :: Symbol ExampleLanguage Comment
test = Terminal "some comment"

-- 测试其他构造函数
testEqual :: Symbol ExampleLanguage EqualSign
testEqual = Terminal ()

为什么这样能解决问题？ #

修改后的showVal签名forall a (s :: c a). Typey s -> a -> ShowS告诉编译器：对于每个s（属于c a类型），第二个参数的类型a是和s绑定的。当你匹配Typey EqualSign时，编译器知道这个s对应的a是()，所以const $ showString "="的类型() -> ShowS就完全符合要求了。同样，Variable对应的a是String，showString的类型String -> ShowS也能完美匹配。

现在你运行show test会得到"some comment"，show testEqual会得到=，完全符合预期。

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