OCaml模块签名不匹配：如何让编译器认可B1.OutputZ属于CZType？

问题场景与初始代码 #

先看这段OCaml代码：

module A = struct
  module type ZType = sig
    type z
  end
end

module B = struct
  module M (InputZ : A.ZType) = struct
    module OutputZ = InputZ
  end
end

module C = struct
  module type CZType = sig
    type z = { s : int }
  end

  module M (Z1 : CZType) = struct
    module B1 = B.M(Z1)
    module Z2 : A.ZType with type z = Z1.z = B1.OutputZ
    module Z3 : CZType = Z2 (* 此行出现签名不匹配错误 *)
  end
end

C.CZType是A.ZType的特化版本，唯一区别是CZType里的z被明确指定为{ s : int }记录类型。

我原本认为以下逻辑能让代码通过类型检查：

• Z2.z与Z1.z类型完全一致（来自签名约束with type z = Z1.z）
• Z1符合CZType签名
• 因此Z2.z必然是{ s : int }记录类型
• 进而Z3应该符合CZType签名

但编译器抛出了签名不匹配错误：

Signature mismatch:
Modules do not match: sig type z = Z1.z end is not included in CZType
Type declarations do not match:
  type z = Z1.z
is not included in
  type z = { s : int; }
Their kinds differ.

问题核心 #

Andreas Rossberg准确指出了问题本质：B模块完全不知道C的存在，因此无法约束OutputZ.z具备CZType要求的类型种类（type kind）——也就是无法保证z是记录类型。

尝试的参数化方案（存在缺陷） #

为了让B适配期望的输出模块类型，我尝试对B做进一步参数化：

module A = struct
  module type ZType = sig
    type z
  end
end

module type TypeModType = sig
  (* 无法约束T为A.ZType的子类型 *)
  module type T
end

module B = struct
  module M (TypeMod : TypeModType) = struct
    module M (InputZ : TypeMod.T) = struct
      module OutputZ = InputZ
      type z = InputZ.z (* 此行报错 *)
    end
  end
end

module C = struct
  module type CZType = sig
    type z = { s : int }
  end

  module M (Z1 : CZType) = struct
    module B1 = B.M(struct module type T = CZType end)
    module B2 = B1.M(Z1)
    (* 这一行现在可以正常通过检查 *)
    module Z2: CZType = B2.OutputZ
  end
end

但这个方案有明显缺陷：无法约束B所参数化的模块类型范围，要么完全不限制，要么只能指定单一类型，没办法限定在A.ZType的子类型范围内。

最终解决方案（更新） #

基于Andreas Rossberg的结论——OCaml仅保留类型同一性（type identity），但不会保留类型种类（type kind），只需在外部定义一个符合目标种类的类型，就能修复问题。以下是完整示例：

module type Graph = sig
  type id
  type attrs
  type node = {
    neighbors : id list;
    attrs : attrs
  }
end

type point = { x: int; y: int }

module type LocatedGraph = sig
  type id
  type attrs = point
  type node = {
    neighbors : id list;
    attrs : attrs
  }
end

module AugmentedGraph (OrigGraph : Graph) = struct
  type id = Orig of OrigGraph.id | Added of int
  type attrs = OrigGraph.attrs
  type node = {
    neighbors : id list;
    attrs : attrs
  }
end

module IntLocatedGraph = struct
  type id = int
  type attrs = point
  type node = {
    neighbors : id list;
    attrs : attrs
  }
end

module AugmentedIntLocatedGraph = AugmentedGraph(IntLocatedGraph)
module AugmentedIntLocatedGraphIsLocatedGraph : LocatedGraph = AugmentedIntLocatedGraph

这个方案同时实现了三个核心特性：

• 参数化（Parametricity）：如果AugmentedGraph接收的参数符合LocatedGraph签名，那么输出模块也会符合LocatedGraph签名
• 约束函子参数类型：AugmentedGraph只能应用于Graph或其子类型
• 封装性（Encapsulation）：AugmentedGraph无需知晓LocatedGraph的存在，就能生成符合该签名的模块

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