修复地区扩展中的类型变量

Question

考虑到这段代码

locale A =
  fixes foo :: "'a"

locale B = A +
  fixes bar :: "'a × 'a"

locale C' = A +
  fixes baz :: "'a"
begin
  sublocale B foo "(foo, baz)".
end

我得到了

Type unification failed

Failed to meet type constraint:

Term:  (foo, baz) :: 'b × 'a
Type:  'b × 'b

因此，伊莎贝尔似乎不明白baz和foo应该是同一类型的。有办法解决这个问题吗？

Answer 1

问题在于您对locales、B和C的声明。B的声明等价于以下内容

locale B = A foo for foo +
  fixes bar :: "'a * 'a"

区域设置导入只记住参数的名称，而不记住类型变量的名称。因此，由于尚未为foo指定类型，B参数的最一般类型如下：

 foo :: 'b
 bar :: 'a * 'a

您可以使用命令print_locale B看到这一点。同样的情况发生在locale C的声明中。

如果您希望foo和bar具有相同的类型，则必须在区域设置声明中将连接显式化。有两种方法可以做到这一点。

locale B = A foo
  for foo :: 'a
  +
  fixes bar :: "'a * 'a"

和

locale B = A +
  constrains foo :: 'a
  fixes bar :: "'a * 'a"