为什么添加定义会更改语言环境导入的类型正确性？

Question

考虑此示例-请注意F1和F2相同。

theory Scratch  
  imports Main
begin

locale F0 =   
  fixes meaning :: ‹'model ⇒ 'a set›  ("⟦_⟧")

locale F1 = F0 +
  fixes γ :: ‹'a set ⇒ 'model›
  assumes sound: ‹L ⊆ ⟦γ L⟧›
  (* Typechecks. *)

definition (in F0) "models m L ≡ L ⊆ ⟦m⟧"  

locale F2 = F0 +
  fixes γ :: ‹'a set ⇒ 'model›
  assumes sound: ‹L ⊆ ⟦γ L⟧›
  (* Does not typecheck, see below. *)

end

语言环境F2-与类型正确的F1相同，只不过我们向F0添加了定义-失败，并显示错误消息：

Type unification failed

Type error in application: incompatible operand type

Operator:  meaning :: 'a ⇒ 'b set
Operand:   γ L :: 'model

[显然，在进行类型检查F2时，类型检查器是否突然决定自由类型变量'a和'model不能是同一东西？

Answer 1

Isabelle工具倾向于在所有地方（包括语言环境）“标准化”类型变量的名称。当他们这样做时，所有类型变量都会从左到右被'a，'b，'c等取代。显然，definition命令以某种方式触发了此操作。因此，'a中的'model和F0突然变成'b和'a。

如果要覆盖此内容，则可以明确指定类型变量：

locale F2 = F0 meaning
  for meaning :: "'model ⇒ 'a set" +
  fixes γ :: ‹'a set ⇒ 'model›
  assumes sound: ‹L ⊆ meaning (γ L)›

或
locale F2 = F0 +
  constrains meaning :: "'model ⇒ 'a set"
  fixes γ :: ‹'a set ⇒ 'model›
  assumes sound: ‹L ⊆ meaning (γ L)›