基于Type.Reflection与Nats的泛型类型：Natty存储问题问询

先把你的代码场景补全，方便更清晰地理解问题：

{-# LANGUAGE DataKinds, GADTs, TypeOperators, Typeable #-}
import Type.Reflection

-- 类型级的Nat定义
data Nat = Z | S Nat

-- 由类型级Nat索引的Natty类型
data Natty (n :: Nat) where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

-- 存储类型级Nat的TypeRep可以正常工作
foo :: Nat -> TypeRep
foo Z = typeRep @Z
foo (S _) = typeRep @(S Z)  -- 这里无报错

-- 但存储Natty对应的类型Rep就会触发错误
boo :: Natty n -> TypeRep
boo _ = typeRep @n  -- 报错：No instance for (Typeable n) arising from a use of ‘typeRep’

为什么Haskell无法自动推断n具备Typeable约束？ #

核心原因是：Natty n里的n是类型级别的Nat（属于Nat kind的类型），而GHC的类型系统不会默认认为所有Nat kind的类型都自动实现了Typeable。

虽然我们知道Natty的构造器只能生成Z或者S n这类类型的实例，但GHC的类型检查是保守的——它不会仅凭n属于Nat kind就推断出Typeable n。Typeable是一个显式的类型类，即使你给值级的Nat推导了Typeable，也不等于所有类型级的Nat成员都自动拥有Typeable实例（比如递归的类型级结构S (S Z)需要每层都满足Typeable约束）。

解决方法 #

最直接且常规的方案就是给boo函数显式添加Typeable n的约束：

boo :: Typeable n => Natty n -> TypeRep
boo _ = typeRep @n

这样GHC就明确知道n是具备Typeable实例的类型，就能正常生成对应的TypeRep了。

如果你不想在函数签名里加约束，也可以把Typeable证据嵌入到Natty的构造器中：

data Natty (n :: Nat) where
  Zy :: Typeable Z => Natty Z
  Sy :: Typeable (S n) => Natty n -> Natty (S n)

boo :: Natty n -> TypeRep
boo Zy = typeRep @Z
boo (Sy _) = typeRep @(S n)

不过这种方式会增加定义的复杂度，一般更推荐第一种方案。

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