像 `Type.eq` / `Typing_equal.equal` 这样的平等证人有什么用？

Question

type ('a, 'b) equal = ('a, 'b) t

(source) 有什么用？我在 Coq 中使用过

refl

，但还不需要像 OCaml 中那样的东西。

类型在 Base

和 即将发布的 OCaml Stdlib 版本中定义。

我怎么知道什么时候使用这种类型，使用这种类型的代码是什么样的？

Base 文档 说：

Type_equal 的目的是表示类型检查器不知道的类型相等性，可能是因为类型相等性取决于动态数据，或者可能是因为类型系统不够强大。

所以听起来我正在寻找类型相等性取决于动态数据或类型系统不够强大的示例，

equal

 类型是有帮助的。

我在

equal

中找到了Stdlib.camlinternalFormat

类型

的用法，但没看懂