能否通过种类签名让Haskell类型系统自动识别闭集类型的类约束？

我有一些用特定种类T的类型（'A/'B）标记的计算，希望在代码中依赖该类型，因此通过实例将类型映射回去，代码示例如下：

data T = A | B  -- 同时生成类型'A和'B

class R (t :: T) where r :: Proxy t -> T
instance R 'A where r _ = A
instance R 'B where r _ = B

foo :: forall (t :: T) . R t => Bar T Int
foo = case r (Proxy :: Proxy t) of A -> ....

目前这种写法可行，但我想知道，既然已经为类型t标注了种类，能否省去每次编写R t约束的步骤？是否可以重构该方案以提升使用便捷性？

方案一：使用singletons库（推荐） #

这是Haskell中处理类型到值映射的标准解决方案，它能自动为枚举类型生成单例类型、对应的实例和映射函数，彻底省去手动编写类型类和实例的麻烦。

首先启用必要扩展并引入库：

{-# LANGUAGE TemplateHaskell, Singletons, DataKinds, TypeApplications #-}

import Data.Singletons.TH

用模板Haskell自动生成单例相关代码：

-- 自动生成单例类型（如`SA`对应`'A`、`SB`对应`'B`）、`SingI`实例、`fromSing`映射函数等
$(singletons [d|
  data T = A | B deriving (Eq, Show)
|])

现在你可以直接使用SingI约束（所有属于T种类的类型都自动满足该约束），或者用withSing避免显式约束：

多态版本（保留t的多态性）

foo :: forall (t :: T) . SingI t => Bar T Int
foo = case fromSing (sing @t) of
  A -> ...  -- 处理'A分支
  B -> ...  -- 处理'B分支

非多态版本（直接绑定单例值）

如果不需要多态性，也可以用withSing直接获取对应单例值，无需显式约束：

foo :: Bar T Int
foo = withSing $ \singT -> case fromSing singT of
  A -> ...
  B -> ...

方案二：手动实现简化约束（不依赖外部库） #

如果不想引入第三方库，我们可以利用GHC的扩展特性，通过闭合类型族+全局约束来减少重复代码：

启用必要扩展：

{-# LANGUAGE DataKinds, TypeFamilies, ConstraintKinds, RankNTypes #-}

import GHC.Exts (Constraint)

data T = A | B

-- 类型类：分派到具体值
class R (t :: T) where
  r :: Proxy t -> T

-- 为所有T的构造子实现实例（仅需手动编写一次）
instance R 'A where r _ = A
instance R 'B where r _ = B

定义全局约束，表明所有T种类的类型都满足R：

-- 全局约束：所有t :: T都满足R t
type AllR = forall (t :: T) . R t

-- 证明该约束成立（因为已实现所有实例）
allR :: AllR
allR = undefined

之后在函数中只需使用AllR约束即可，无需重复写R t：

foo :: forall (t :: T) . AllR => Bar T Int
foo = case r (Proxy :: Proxy t) of
  A -> ...
  B -> ...

关键说明 #

• 由于Haskell是静态类型语言，值层面的分支逻辑必须通过类型类或单例类型来分派，无法完全跳过类型约束，但可以通过工具库自动生成约束所需的实例，减少手动代码量。
• singletons库不仅支持枚举类型，还能处理更复杂的自定义种类，是Haskell类型级编程的常用工具。

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