基于上下文选择类型类实例：GHC 9.x下的新探讨

该话题已被多次讨论，随着Haskell的发展，我们重新审视在现代Haskell（GHC 9.0-9.2版本）中如何解决以下问题：

假设我们需要一个计算给定类型值存储字节数的函数，需区分两种情况：

• 固定大小数据类型：比如Int32，无论具体值是什么，都占用4字节；
• 可变大小数据类型：比如自定义类型data C = A Int32 | B Int32 Int32，A构造子占用4字节，B构造子占用8字节。

为此我们定义两个基础类型类：

1. 固定大小类型类，无需传入值，通过Proxy参数即可确定大小：

class FixedSize a where 
  fixedSize :: p a -> Int

2. 可变大小类型类，必须传入具体值才能计算大小：

class VariableSize a where 
  variableSize :: a -> Int

接下来，我们需要计算列表的总存储大小，但列表元素可能是固定或可变大小，因此自然需要两个计算函数：

• 固定大小元素的列表大小计算：

listSize :: (FixedSize a) => [a] -> Int
listSize _ = (* fixedSize (Proxy @a)) . length

• 可变大小元素的列表大小计算：

listSize :: (VariableSize a) => [a] -> Int
listSize = sum . map variableSize

但如果尝试定义统一的Size类型类，并为[a]直接写两个实例，会编译失败：

class Size a where 
  size :: a -> Int

instance (FixedSize a) => Size [a] where
  size _ = (* fixedSize (Proxy @a)) . length

instance (VariableSize a) => Size [a] where
  size = sum . map variableSize

这是因为Haskell的实例选择是基于类型而非上下文的，编译器无法根据上下文判断应该选用哪个Size [a]实例。

现有解决方案：开放类型族+非一致实例 #

为解决这个问题，我们可以借助GHC的高级重叠实例技巧，核心是定义反映上下文的类型级谓词，利用多参数类型类和重叠实例选择更具体的实现。其中一种对用户最便捷的方案是基于开放类型族的改进版本：

class Size a where 
  size :: a -> Int

class FixedSize a where
  type FixedSized a :: Bool
  type FixedSized a = 'True  -- 默认实例为固定大小
  fixedSize :: p a -> Int

#include "MachDeps.h"
instance FixedSize Int where
  fixedSize _ = SIZEOF_HSINT

class ListSize (isElemFixed :: Bool) a where
  listSize :: p isElemFixed -> a -> Int

instance (ListSize (FixedSized a) [a]) => Size [a] where
  size = listSize $ Proxy @(FixedSized a)

instance (FixedSize a) => ListSize 'True [a] where
  listSize _ = trace "elem size is fixed" . (* fixedSize (Proxy @a)) . length

instance {-# INCOHERENT #-} (Size a) => ListSize any [a] where
  listSize _ = trace "elem size is variable" . sum . map size

test1 = size [1::Int,2,3]  -- 应触发固定大小分支
test2 = size [[1::Int], [2,3,4]]  -- 应触发可变大小分支

该方案默认行为符合预期，用户无需额外维护过多实例，只有当显式错误定义FixedSized实例时才会出问题。但它依赖了非一致实例（incoherent instances），而Haskell文档明确说明编译器可自由选择任意非一致实例，存在不可预测性。

技术问题解答 #

问题1：为何此处必须使用非一致实例？当第一个参数为'True时，ListSize 'True [a]是否无法直接覆盖ListSize any [a]并被选中？ #

当FixedSize a成立时，FixedSized a等于'True，此时ListSize 'True [a]和ListSize any [a]都匹配目标约束ListSize 'True [a]。虽然ListSize 'True [a]看起来更具体，但GHC的重叠实例规则要求：只有当一个实例的头部严格比另一个更具体（即所有参数都能匹配，且至少有一个参数是更具体的类型），才能自动选择更具体的实例。

这里两个实例的第二个参数都是[a]，没有差异，GHC无法确定哪个实例更“具体”——因为any可以匹配'True，而'True也属于any的范围，编译器无法自动判定优先级，因此需要用INCOHERENT标记告诉编译器：即使存在多个匹配实例，也可以任意选择（实际中我们依赖它优先选更具体的'True实例）。

问题2：是否存在破坏代码的方式？即当FixedSize a在作用域中时，让编译器选择ListSize any [a]（可变大小元素的实现）？ #

理论上存在这种可能，但实际中很难触发。GHC在处理非一致实例时，会优先尝试选择更具体的实例，只有当无法确定具体性时才会随机选择。不过如果通过一些技巧（比如通过类型同义词隐藏FixedSize a的约束，或者在局部作用域中引入模糊的类型约束），可能会让编译器误选ListSize any [a]。

比如定义一个类型同义词隐藏约束：

type F a = [a]

若在某个作用域中编译器无法推断FixedSized a的具体值，可能会选中可变大小分支，但这种情况属于极端场景，正常使用下不会出现。

问题3：这些实例是否真的是非一致的？是否只是编译器无法证明一致性，能否手动证明？ #

从语义上看，我们的意图是当FixedSize a成立时优先使用ListSize 'True [a]，否则使用ListSize any [a]，逻辑上是自洽的。但从GHC的实例匹配规则来看，它们是非一致的：因为存在FixedSize a成立的上下文，两个实例都能匹配ListSize 'True [a]，且编译器无法自动验证两个实例的实现是否等价。

手动证明一致性的前提是：当FixedSize a成立时，Size a的实现（如果存在）和FixedSize a的fixedSize计算结果一致，但这不是编译器能自动验证的，因此必须标记为非一致。

问题4：在现代Haskell中是否有完全不同的方案解决此问题？即编译时基于元素类型选择合适的列表大小计算函数？ #

有几种更安全的替代方案：

1. 类型类默认方法+重叠实例
   定义统一的Size类，为固定大小类型提供默认实现，可变大小类型手动重载：

   class Size a where
     size :: a -> Int
     -- 默认实现：如果是固定大小类型，使用fixedSize
     default size :: FixedSize a => a -> Int
     size _ = fixedSize (Proxy @a)
   
   instance FixedSize a => Size a  -- 重叠实例，优先匹配固定大小类型
   instance VariableSize a => Size a where
     size = variableSize
   
   -- 列表实例
   instance Size a => Size [a] where
     size xs = case isFixedSize (Proxy @a) of
       'True -> length xs * fixedSize (Proxy @a)
       'False -> sum (map size xs)
   
   -- 类型族判断是否为固定大小
   type family IsFixedSize a :: Bool where
     IsFixedSize a = 'True
   

   用户只需为可变大小类型重载IsFixedSize为'False，无需非一致实例。

2. GADTs+类型约束
   定义GADT区分固定/可变大小类型，显式传递类型证据：

   data Sized a where
     FixedSized :: FixedSize a => Sized a
     VariableSized :: VariableSize a => Sized a
   
   listSize :: Sized a -> [a] -> Int
   listSize FixedSized _ = (* fixedSize (Proxy @a)) . length
   listSize VariableSized = sum . map variableSize
   

   这种方式类型安全性更高，无需依赖重叠实例，但需要用户显式传递Sized a证据。

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