Coq模块使用问题：如何暴露参数化类型的类型等式？

你遇到的核心问题是模块密封导致类型等式被隐藏：当用Module a : A声明模块时，Coq会将a的接口严格限制为A的定义，只对外暴露t : Type，而隐藏了t := nat这个具体实现细节。因此在模块B中导入后，Coq无法得知t和nat是同一类型，自然会抛出类型不匹配的错误。

下面是几种可行的解决方式：

方案1：取消模块密封 #

直接去掉模块a的: A声明，让Coq完全暴露a的内部定义，这样t = nat的等式会被全局可见：

Module Type A.
  Parameter t : Type.
End A.

Module a.  (* 不密封模块，保留所有内部定义的可见性 *)
  Definition t := nat.
End a.

Module B.
  Module Import InstanceOfA := a.
  Definition x : t := 2.
  Definition sum (t1 t2 : t) : nat :=  t1 + t2.    
End B.

方案2：使用子类型声明（保留接口约束） #

如果你需要保留a满足模块类型A的约束，但又不想隐藏内部实现，可以用<: A替代: A，声明a是A的子类型，这样Coq会保留a的透明性：

Module Type A.
  Parameter t : Type.
End A.

Module a <: A.  (* 子类型声明，既满足A的接口，又暴露内部定义 *)
  Definition t := nat.
End a.

Module B.
  Module Import InstanceOfA := a.
  Definition x : t := 2.
  Definition sum (t1 t2 : t) : nat :=  t1 + t2.    
End B.

为什么之前的恒等函数没用？ #

你尝试定义t -> nat的恒等函数无效，是因为模块密封后，该函数的类型被隐藏为a.t -> nat，而导入到B中的t是InstanceOfA.t——Coq此时不知道这两个t和nat是等价的，所以即使有恒等函数，也需要显式调用，无法自动触发强制转换。而上面两种方案让Coq直接知晓t的具体类型，自然能自动处理类型匹配和运算。

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