如何在OCaml中的各个模块之间使用GADT，而不会发出警告？

Question

我有两个文件：gadt1.ml和gadt2.ml，第二个取决于第一个。

gadt1.ml：

type never
type _ t1 = A1 : never  t1 | B1 : bool t1
type _ t2 = A2 : string t2 | B2 : bool t2
let get1 : bool t1 -> bool = function B1 -> true
let get2 : bool t2 -> bool = function B2 -> true

gadt2.ml：

let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> true
let get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true

当我使用ocaml 4.02.3（ocamlbuild gadt2.native）进行编译时，我收到关于函数Gadt2.get1尚未穷举的警告8。我很不解的是Gadt2.get1提高了，同时警告Gadt1.get1并Gadt2.get2没有。

我的假设是空类型never不能等于，bool因此Gadt2.get1不应发出警告。另一方面，如果我Gadt2.get1使用arguments 调用，则会A1收到类型错误（按需）。警告是预期的行为还是错误？我错过了什么？

顺便说一句，添加-principal到编译标志不会更改任何内容。

Answer 1

Gadt2只能看到的接口Gadt1，而不是其实现。该界面如下所示：

type never
type _ t1 = A1 : never  t1 | B1 : bool t1
type _ t2 = A2 : string t2 | B2 : bool t2
val get1 : bool t1 -> bool
val get2 : bool t2 -> bool

请注意，这type never是抽象的-没有什么可以阻止实现RHS的实现了。特别是，您可以在gadt1.ml中写入type never = bool，这时将传递A1给成为合理的get1，因此get1需要为此做准备。

相反，string是非抽象类型：它具有已知的表示形式，因此它不可能等于bool，因此A2永远不会传递给get2。

您似乎想做的never是声明一个不是抽象但为空的类型，将其表示形式公开为根本没有构造函数。不幸的是，OCaml对此没有很好的支持。定义本地编译器可以判断为空的类型的能力有点怪异，而手册中并未真正提及。无法在模块签名中表达“此类型为空”。