Data.Dynamic为何采用见证而非类型类约束实现？

Data.Dynamic的两种等价定义 #

Data.Dynamic的实现如下：

data Dynamic where
    Dynamic :: TypeRep a -> a -> Dynamic

我认为下面这个定义和它是等价的：

data Dynamic where
    Dynamic :: Typeable a => a -> Dynamic

理由很简单：通过withTypeable可以从TypeRep a推导出Typeable约束，反过来通过typeRep也能从Typeable约束获取对应的TypeRep a。

核心疑问：该选见证字段还是类型类约束？ #

我平时习惯用类型类约束来定义GADT，以此实现存在类型。但看到Data.Dynamic的实现后，我开始纠结：是不是应该改用「见证」字段来替代类型类约束？选择这两种方式时，需要考虑哪些因素？

进一步思考：看场景选择 #

举个例子，对比下面两个定义：

data SillyListA m where
  SillyListA :: Ord a => (a -> m ()) -> [a] -> SillyListA m 

data SillyListB m where
  SillyListB :: (a -> a -> Ordering) -> (a -> m ()) -> [a] -> SillyListB m 

这里显式传递排序函数而非仅依赖Ord约束是有实际价值的：同一类型可以对应多种排序规则，第二种定义不需要借助newtype就能实现这一点。

但对于TypeRep a这种单例类型，显式传递见证字段的意义就不大了——因为每个类型对应的TypeRep是唯一的，不会出现同一类型有多个不同见证的情况。

我曾觉得见证字段有个小优势：模式匹配时可以直接提取字段，不用写类型应用。比如第一种Dynamic定义可以这么写：

f (Dynamic tr x) = ...

而约束版本则需要写类型应用：

f (Dynamic @a x) = ...

不过实际编码时，我还是会写成：

f (Dynamic @a _ x) = ...

因为如果函数内部有依赖显式类型的子逻辑，作用域里的类型变量会很有用；而且很少有函数直接以TypeRep a为参数，它们通常需要类型应用或者Proxy @a，所以我还是得让类型变量处于作用域内。

自定义类型的两种写法纠结 #

我自己的代码里定义了这样一个类型（如果已有现成实现欢迎告知）：

data DynamicF f where
  DynamicF :: forall (a :: Type) f. TypeRep a -> f a -> DynamicF f

这是模仿Data.Dynamic写的，但现在觉得或许下面这个用约束的版本更好：

data DynamicF f where
  DynamicF :: forall (a :: Type). Typeable a => f a -> DynamicF f

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