OCaml数据类型定义中的方括号`[`与`]`是什么含义？

你在Coq v8.11版本Genarg模块中看到的如下定义：

type rlevel = [
| `rlevel
]

不属于常规OCaml代数数据类型（ADT）的语法范畴，是OCaml进阶特性**多态变体（Polymorphic Variant）**的写法，普通ADT入门教程、基础语法文档一般不会覆盖这部分内容。

具体语义拆解 #

• 多态变体的类型定义用方括号[]包裹所有可接受的变体构造器，和常规ADT直接在等号后列大写开头构造器的写法有明显区别。
• 反引号`开头的标识符是多态变体的构造器，这类构造器不需要提前绑定到某个固定类型，可以跨不同的多态变体类型复用。
• 上述代码的实际作用是定义一个名为rlevel的类型，这个类型只有唯一的合法值： `rlevel。如果用常规ADT实现等价效果，写法是type rlevel = Rlevel，二者核心语义接近，但多态变体支持更灵活的类型组合、子类型推导能力。

Coq使用该写法的原因 #

Genarg模块负责Coq泛型语法参数的层级抽象，这类单构造器的多态变体标记类型，是为了适配多态变体的开放扩展特性：后续可以直接把rlevel和其他同类层级标记类型组合成更大的联合多态变体类型，不需要写额外的构造器转换、包装代码，方便Coq本体和第三方插件扩展不同的语法参数层级。

多态变体属于OCaml的进阶特性，日常业务代码使用频率很低，大多出现在编译器、可扩展框架这类对类型灵活性要求高的代码库中，因此基础语法资料很少提及。

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