Haskell中多态/多种类（polykinded）元组的种类是什么？

核心原因说明 #

首先明确几个GHC的底层设计规则，你的问题都可以从这几个规则推导出来：

1. Constraint元组是GHC内置重载的特殊构造器
   你最早写的All函数里用的(,)，当所有子项都属于Constraint种类时，这个(,)的种类是Constraint -> Constraint -> Constraint，嵌套的约束元组会被GHC自动展平，空的()在这个场景下也会被识别为种类为Constraint的空约束，所以可以正常工作。
   我们平时用的带单引号的'(,)是普通的提升数据构造器，只能构造(k1, k2)种类的元组值，和Constraint元组完全不是同一个东西，所以你测试'(,) 'True 'False得到的是(Bool, Bool)种类的居住者，和你代码里用的(,)没有关系。

2. 你写的All'看起来是泛化的，实际只支持返回Type的场景
   GHC在编译类型族的定义时，会先从等式右侧推断种类：

• 你第一个等式写的是All' c '[] = ()，不带任何种类标注的()默认种类是Type（也就是*），所以GHC直接把All'签名里的返回种类参数r实例化为了Type
• 第二个等式里的(c x, All' c xs)用到的(,)也会被匹配成Type -> Type -> Type的普通类型构造器，进一步锁定了r ~ Type
  你后面用:info All'看到的所有等式的r都是*，就是这个原因。当你传入返回Constraint的Eq时，没有匹配的类型族等式，所以归约就卡住了。

实现全种类泛化的方案 #

如果要让All'同时支持Constraint、Type等多种返回种类，你需要手动重载空值和拼接操作，针对不同的返回种类提供不同的实现：

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, ConstraintKinds, UndecidableInstances #-}

-- 重载不同种类的空值
type family Nil :: r where
  Nil @Type = ()
  Nil @Constraint = ()

-- 重载不同种类的二元拼接
type family Append (a :: r) (b :: r) :: r where
  Append @Type a b = (a, b)
  Append @Constraint a b = (a, b)

type family All' (c :: k -> r) (xs :: [k]) :: r where
  All' c '[] = Nil @r
  All' c (x ': xs) = Append @r (c x) (All' c xs)

测试验证：

-- 约束场景正常工作
>>> :kind! All' Eq '[Int, Double, Float]
All' Eq '[Int, Double, Float] :: Constraint
= (Eq Int, (Eq Double, (Eq Float, () :: Constraint)))

-- Type场景正常工作
>>> :kind! All' Maybe '[Int, Double, Float]
All' Maybe '[Int, Double, Float] :: *
= (Maybe Int, (Maybe Double, (Maybe Float, ())))

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