我在使用ReasonmL进行了更多操作，并从以下示例中发现type t上的模式匹配无法解决错误
错误：此模式与t（float）类型的值匹配，但是期望与t（int）类型的值匹配的模式float类型与int类型不兼容
type t('a) =
| One: t(int)
| Two: t(float);
let x =
fun
| One => None
| Two => None;
从某种程度上来说，如果这与函数的返回类型有关，这对我来说很有意义。
我找到了答案（我认为）to an equivalent question。对于第二部分，答案似乎是有点忽略构造函数的绑定类型。在ReasonmL中是否可能相同？
P.s .：请对术语进行书呆子的纠正，我仍在学习什么。
P.p.s .：我知道我可以通过显式键入x来解决原始问题，但我真的很喜欢fun语法，因为它很有趣。
简单的答案是，GADT使类型系统的表达能力太强而无法完全推断出来。 例如，在您的情况下，以下两个函数都是合计的（aka它们处理输入的所有可能值
let one = (One) => None
let two = (Two) => None
您可以通过在OCaml语法中添加显式的反驳条款来检查它们的总和（原因语法尚未更新为包括这些内容）：
let one = function
| One -> None
| _ -> .
这里的点.表示该子句左侧描述的模式在语法上是有效的，但是由于某些类型限制，它没有引用任何实际值。
因此，您需要告诉类型检查器您打算为任何t(a)匹配类型为a的值，这需要使用局部抽象类型来完成：
let x (type a,(x:t(a))) = switch(x){
| One => None
| Two => None
}
有了此局部抽象注释，类型检查器知道不应将其a全局替换为具体类型（aka应该认为局部a是某种未知的抽象类型） ，但可以在匹配GADT时在本地进行优化。
严格来说，仅在模式上需要注释，因此您可以编写
let x (type a) = fun
| (One:t(a)) => None
| Two => None
请注意，对于带有GADT的递归函数，您可能需要使用完全显式的多态局部抽象类型表示法：
type t(_) =
| Int(int): t(int)
| Equal(t('a),t('a)):t(bool)
let rec eval: type any. t(any) => any = fun
| Int(n) => n
| Equal(x,y) => eval(x) = eval(y)
的区别在于eval是递归多态的。参见https://caml.inria.fr/pub/docs/manual-ocaml-4.09/polymorphism.html#sec60。
编辑：注释返回类型
为避免可怕的“此类型将逃避其作用域”，通常需要使用另一个注释，即在保留模式匹配时添加注释。 一个典型的例子是函数：
let zero (type a,(x:t(a)) = switch (x){
| One => 0
| Two => 0.
}
此处存在歧义，因为类型检查器在分支One中知道int=a，但是在离开此上下文时，它需要选择方程式的一侧或另一侧。 （在这种特定情况下，类型检查器将(0: int)留在自己的设备上，因为0是一个整数，并且该类型与本地抽象类型没有任何联系，因此它是更合乎逻辑的结论。 a。）
可以通过在本地使用显式注释来避免这种歧义
let zero (type a,(x:t(a))) = switch (x){
| One => ( 0 : a )
| Two => ( 0. : a )
}
或整个功能
let zero (type a): t(a) => a = fun
| One => 0
| Two => 0.
可能很快就会有人提出适当的解释，但是简短的答案是您需要使用局部抽象类型来代替类型变量。
let x: type a. t(a) => option(a) =
fun
| One => None
| Two => None;
为什么？嗯，这对我来说仍然是个谜，尤其是在这种情况下，它只是一个幻像类型，而没有涉及该类型的实际值。但我怀疑至少是由本段（或以下内容）from the manual解释的：
GADT的类型推断非常困难。这是由于某些类型从分支转义时可能变得模棱两可。例如，在上述Int情况下，n可以具有int类型或a类型，并且在该分支之外它们不是等效的。作为第一近似，如果使用不包含自由类型变量的类型（在scrutinee和返回类型上）都注释了模式匹配，则类型推断将始终起作用。上面的示例就是这种情况，这要归功于类型批注仅包含本地抽象类型。