如何在Haskell中结合GADTs与DataKinds实现类型级构造器约束

你写的translate :: BaseExpr -> Expr a签名的语义是「对任意调用者指定的ExprType类型a，都能返回对应类型的Expr a」，这显然不可能实现——BaseExpr的结构是运行时确定的，返回的Expr的类型标签完全由输入的BaseExpr决定，调用者根本没有选择a的空间，所以编译器会报错类型不匹配。
这不是对GADTs和DataKinds的误用，只是你把类型变量的量化方向搞反了。

你需要用存在类型把返回的Expr的类型标签包装起来，对外隐藏具体的a，后续使用时通过GADT的模式匹配自动还原类型信息即可。
完整可运行的代码如下（需要GHC >= 8.10，开启对应扩展）：

{-# LANGUAGE KindSignatures, DataKinds, GADTs, StandaloneKindSignatures, PolyKinds #-}
module NewGadt where

data ExprType = Var | Nest

data Expr (a :: ExprType) where
  ExprVar :: String -> Expr Var
  ExprNest :: Expr a -> Expr Nest

-- 存在类型包装，隐藏具体的ExprType标签
data SomeExpr where
  SomeExpr :: Expr a -> SomeExpr

data BaseExpr
  = BaseExprVar String
  | BaseExprNest BaseExpr

-- 翻译函数返回包装后的存在类型
translate :: BaseExpr -> SomeExpr
translate (BaseExprVar id) = SomeExpr $ ExprVar id
translate (BaseExprNest expr) = case translate expr of
  SomeExpr inner -> SomeExpr $ ExprNest inner

-- 你原来的类型安全函数完全保留
printVariable :: Expr Var -> IO ()
printVariable (ExprVar id) = putStrLn id

printNested :: Expr Nest -> IO ()
printNested (ExprNest inner) = putStrLn "nested expression"

printExpr :: Expr a -> IO ()
printExpr expr@ExprVar {} = printVariable expr
printExpr expr@ExprNest {} = printNested expr

-- 使用示例：从BaseExpr转译后调用处理函数
handleBaseExpr :: BaseExpr -> IO ()
handleBaseExpr be = case translate be of
  SomeExpr e -> printExpr e

• 向printVariable传入Expr Nest类型的参数时，编译器会正常报错，满足你的类型安全要求
• 运行时传入任意结构的BaseExpr都能正确转译和处理，不会丢失类型信息

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