Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] (PATCH) Interaction of 'a default sort with ax...

Email Gateway (Oct 11 2026 at 21:59):

From: Alex Mobius <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] (PATCH) Interaction of 'a default sort with axiomatic type classes and constant importing

Going to be top-quoting since this is a self-quote.

As I found no man to help me, I turned to machine. Our large language
brethern seems to have pinned down the cause, and the fix makes sense to
me, though I am not very good at ML. I tried to refactor it into a
palatable form; maybe the developers will see it fit to include this.

To reiterate, the issue is that when the class's default sort for its 'a
type is improved compared to the superclasses', the superclasses'
definitions weren't correctly imported into the context; instead broken
local e definitions were imported that referred to locale fixes rather
than top-level class consts. Attached is the patch against Isabelle
2025-2 distribution, as well as a slightly expanded repro suite.

With warmest regards,

Alex.

On 04/06/2026 13:21, Alex Mobius wrote:

As I've previously written, assigning a sort to type variable 'a in locale axioms triggers surprising behaviour: it sometimes succeeds and sometimes fails, and the locale context ends up with a copy of theorems that refer to (normally inaccessible) locale fixes, instead of class polymorphic constants. I stumbled upon this in HOLCF, but this can crop up up any time you use a symbol in assumptions that fixes the sort of one of its typevars and wasn't defined in the class context.

I managed to create a reproduction that does not use HOLCF, and demonstrates the quirks rather minimally. Text included and attached for convenience.

theory Repro2 imports Main begin

(* this sort assignment fails (ord incompatible with default sort type), I am not sure why *)
class order_chain = order +
assumes "∃x::(nat⇒'a::ord). ∀i. x i ≤ x (Suc i)"

(* However if we make local copies of type classes, the same thing succeeds *)
class ord2 =
fixes less_eq2 :: "'a ⇒ 'a ⇒ bool"
and less2 :: "'a ⇒ 'a ⇒ bool"
begin

notation
less_eq2 (‹'(≤2')›) and
less_eq2 (‹(‹notation=‹infix ≤››_/ ≤2 _)› [51, 51] 50) and
less2 (‹'(<2')›) and
less2 (‹(‹notation=‹infix <››_/ <2 _)› [51, 51] 50)
end

class preorder2 = ord2 +
assumes less_le2_not_le2: "x <2 y ⟷ x ≤2 y ∧ ¬ (y ≤2 x)"
and order2_refl [iff]: "x ≤2 x"
and order2_trans: "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z"
begin

lemma order2_le_trans: "x <2 y ⟹ y <2 z ⟹ x <2 z"
unfolding less_le2_not_le2
using order2_trans by blast
end

class order2 = preorder2 +
assumes order2_antisym: "x ≤2 y ⟹ y ≤2 x ⟹ x = y"

class order2_chain = order2 +
assumes "∃x::(nat⇒'a::preorder2). ∀i. x i ≤2 x (Suc i)"
begin
(* We have succeeded, but the local context is weird: local facts now refer to e.g.
locale fixed variable less_eq2, which is distinct from polymorphic constant less_eq2 *)
lemma "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z" by (fact order2_trans) (* fails *)
lemma "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z" by (fact preorder2_class.order2_trans) (succeeds)
end

(* Weirdly this works with base classes but with superclass ord (because it has no axioms maybe?)
*)
class order_chain_higher_sort = ord +
assumes "∃x::(nat⇒'a::order). ∀i. x i ≤ x (Suc i)"

end

class-base-sort-syntax.patch
class-base-sort-repro.tar.gz

Email Gateway (Oct 27 2026 at 15:55):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
Subject: [isabelle] (PATCH) Interaction of 'a default sort with axiomatic type classes and constant importing

Hi Alex,

thanks for pinning the ancient issue down.

I have examined your patches and they seem to capture the right idea.

It will take some time until I have adapted them, though.

Regards,
Florian

Am 11.10.26 um 23:58 schrieb Alex Mobius (via cl-isabelle-users Mailing
List):

Going to be top-quoting since this is a self-quote.

As I found no man to help me, I turned to machine. Our large language
brethern seems to have pinned down the cause, and the fix makes sense to
me, though I am not very good at ML. I tried to refactor it into a
palatable form; maybe the developers will see it fit to include this.

To reiterate, the issue is that when the class's default sort for its 'a
type is improved compared to the superclasses', the superclasses'
definitions weren't correctly imported into the context; instead broken
local e definitions were imported that referred to locale fixes rather
than top-level class consts. Attached is the patch against Isabelle
2025-2 distribution, as well as a slightly expanded repro suite.

With warmest regards,

Alex.

On 04/06/2026 13:21, Alex Mobius wrote:

As I've previously written, assigning a sort to type variable 'a in
locale axioms triggers surprising behaviour: it sometimes succeeds and
sometimes fails, and the locale context ends up with a copy of
theorems that refer to (normally inaccessible) locale fixes, instead
of class polymorphic constants. I stumbled upon this in HOLCF, but
this can crop up up any time you use a symbol in assumptions that
fixes the sort of one of its typevars and wasn't defined in the class
context.

I managed to create a reproduction that does not use HOLCF, and
demonstrates the quirks rather minimally. Text included and attached
for convenience.

theory Repro2 imports Main begin

(* this sort assignment fails (ord incompatible with default sort
type), I am not sure why *)
class order_chain = order +
   assumes "∃x::(nat⇒'a::ord). ∀i. x i ≤ x (Suc i)"

(* However if we make local copies of type classes, the same thing
succeeds *)
class ord2 =
   fixes less_eq2 :: "'a ⇒ 'a ⇒ bool"
     and less2 :: "'a ⇒ 'a ⇒ bool"
begin

notation
   less_eq2  (‹'(≤2')›) and
   less_eq2  (‹(‹notation=‹infix ≤››_/ ≤2 _)›  [51, 51] 50) and
   less2  (‹'(<2')›) and
   less2  (‹(‹notation=‹infix <››_/ <2 _)›  [51, 51] 50)
end

class preorder2 = ord2 +
   assumes less_le2_not_le2: "x <2 y ⟷ x ≤2 y ∧ ¬ (y ≤2 x)"
   and order2_refl [iff]: "x ≤2 x"
   and order2_trans: "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z"
begin

lemma order2_le_trans: "x <2 y ⟹ y <2 z ⟹ x <2 z"
   unfolding less_le2_not_le2
   using order2_trans by blast
end

class order2 = preorder2 +
   assumes order2_antisym: "x ≤2 y ⟹ y ≤2 x ⟹ x = y"

class order2_chain = order2 +
   assumes "∃x::(nat⇒'a::preorder2). ∀i. x i ≤2 x (Suc i)"
begin
(* We have succeeded, but the local context is weird: local facts now
refer to e.g.
locale fixed variable less_eq2, which is distinct from polymorphic
constant less_eq2 *)
lemma "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z" by (fact order2_trans) (* fails *)
lemma "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z" by (fact
preorder2_class.order2_trans) (succeeds)
end

(* Weirdly this works with base classes but with superclass ord
(because it has no axioms maybe?)
*)
class order_chain_higher_sort = ord +
   assumes "∃x::(nat⇒'a::order). ∀i. x i ≤ x (Suc i)"

end

Last updated: Oct 29 2026 at 04:52 UTC