为何已实现所有DataKinds实例仍需为Haskell函数添加约束？

首先看原始代码：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

data RegStatus = Registered | Anonim

newtype UserId (r :: RegStatus) = UserId Int

class GetRegStatus (r :: RegStatus)  where
  getRegStatus :: UserId r -> RegStatus

instance GetRegStatus 'Registered where
  getRegStatus _ = Registered

instance GetRegStatus 'Anonim where
  getRegStatus _ = Anonim

getStatus :: forall (r :: RegStatus).  UserId r -> RegStatus
getStatus = getRegStatus

运行时触发错误：

Error: No instance for (GetRegStatus r) arising from a use of `getRegStatus'

虽然已经为RegStatus的所有DataKinds构造子实现了GetRegStatus实例，但必须添加约束才能让代码正常运行：

getStatus :: forall r. GetRegStatus r =>  UserId r -> RegStatus
getStatus = getRegStatus

解决方案：用闭式类型族替代类型类 #

Haskell类型类遵循开放世界假设——编译器无法确定你已经实现了所有可能的实例（比如未来可能给RegStatus新增构造子），因此必须显式添加约束。而闭式类型族是封闭的，能明确覆盖所有类型情况，让编译器确认无需额外约束。

修改后的代码：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-} -- 新增该扩展

data RegStatus = Registered | Anonim

newtype UserId (r :: RegStatus) = UserId Int

-- 定义闭式类型族，覆盖所有RegStatus构造子
type family GetRegStatus (r :: RegStatus) :: RegStatus where
  GetRegStatus 'Registered = 'Registered
  GetRegStatus 'Anonim = 'Anonim

getStatus :: forall (r :: RegStatus). UserId r -> RegStatus
getStatus _ = case (undefined :: GetRegStatus r) of
  Registered -> Registered
  Anonim -> Anonim

另一种简洁实现：利用类型族确定性推导 #

如果不想用case，也可以直接通过类型族的确定性让编译器推导值：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}

data RegStatus = Registered | Anonim deriving Show

newtype UserId (r :: RegStatus) = UserId Int

type family GetRegStatus (r :: RegStatus) :: RegStatus where
  GetRegStatus 'Registered = 'Registered
  GetRegStatus 'Anonim = 'Anonim

getStatus :: forall (r :: RegStatus). UserId r -> RegStatus
getStatus _ = statusVal where
  statusVal :: GetRegStatus r
  statusVal = case statusVal of {} -- 借助类型族的封闭性让编译器自动推导

这样getStatus函数就不需要任何类型类约束，编译器能通过闭式类型族确认所有r :: RegStatus都有对应的结果。

内容的提问来源于stack exchange，提问作者Николай Николай