Locale解释后继承问题：如何避免调用g方法的类型统一错误

我正在理解locale/interpretation层面的“继承”机制。现有抽象locale（locA），其中定义了方法g；具体locale（locB）是该抽象locale的实例/模型。请问如何使用g方法以避免出现“类型统一（type unification）”错误？

示例代码 #

theory InstOverwrite

imports Main
begin

locale locA = 
  fixes f :: "'a ⇒ 'b"
begin

definition g :: "'a set ⇒ 'b set" where 
  "g X = f`X"
end

locale locB = 
  fixes fb :: "nat ⇒ nat"
  assumes fb_def: "fb n = n*2"
begin

interpretation locA
  apply unfold_locales
  done
end

context locB
begin
definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ locA.g X}"
end

end

错误信息 #

Type unification failed: Clash of types "_ set" and "_ ⇒ _"

Type error in application: incompatible operand type

Operator: locA.g :: (??'a ⇒ ??'b) ⇒ ??'a set ⇒ ??'b set
Operand: X :: nat set

问题原因与解决方案 #

问题出在调用locA.g的方式：当在locB中解释locA时，Isabelle会生成一个绑定到fb的实例版本，但直接写locA.g会引用未实例化的通用版本——这个版本需要先接收f参数（类型为'a ⇒ 'b），再接收集合参数，直接传集合X会导致类型不匹配。

有两种修复方式：

方式1：使用带名称的解释实例 #

在locB的interpretation步骤中，给locA的实例指定名称并明确绑定参数，调用时使用该限定名：

locale locB = 
  fixes fb :: "nat ⇒ nat"
  assumes fb_def: "fb n = n*2"
begin

interpretation A: locA fb  -- 绑定locA的f参数为fb，并将实例命名为A
  apply unfold_locales
  done
end

context locB
begin
definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ A.g X}"  -- 调用实例化后的A.g
end

方式2：将locB定义为locA的子locale #

更贴合“继承”语义的写法是直接让locB继承locA，这样locA的定义会直接融入locB上下文，无需额外interpretation：

locale locA = 
  fixes f :: "'a ⇒ 'b"
begin
definition g :: "'a set ⇒ 'b set" where 
  "g X = f`X"
end

-- 直接继承locA，指定f参数为fb
locale locB = locA fb for fb :: "nat ⇒ nat"
  assumes fb_def: "fb n = n*2"

context locB
begin
definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ g X}"  -- 直接使用g，上下文已绑定到fb的实例
end

两种方式均可解决类型错误，方式2更符合locale继承的设计意图，代码更简洁。

内容的提问来源于stack exchange，提问作者Alicia M.