Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] (PATCH) `sublocale` in a class causes subclass...

Email Gateway (Oct 12 2026 at 02:06):

From: Alex Mobius <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] (PATCH) sublocale in a class causes subclass declarations with a raised sort to fail

Another bug with non-default-sort classes I hit: if a class has a raised
sort for its type variable, say S (because its "assumes" use a constant
with a sort bound for example), and there is a "sublocale" declaration
in its superclass, the declaration fails with "Type inference imposes
additional sort constraint {subclass_sort} of type parameter 'a of sort
{superclass_sort}". In absence of the sublocale declaration, the
subclass declaration goes through.

As far as i understand, the mechanism is that replaying the locale
definitions fixes sort of 'a to what it was at the time of sublocale.
The easiest fix I've found is to restore the constraints specifically
after superclass body replay in classes. It feels a little iffy, but
should be sound, as monotonicity of sorts for 'a is established elsewhere.

Disclaimer: finding the root cause of this bug was machine-assisted and
the fix, as well as the test suite, is machine-generated. I did my best
to think about and test all of the corner cases that could break, and
the patch itself is tiny, which gives me hopes about its correctness. I
would kindly ask the maintainers to take a more informed look.

With best wishes,

Alex.

sublocale-leak-repro.tar.gz
sublocale-leak.patch

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

From: Florian Haftmann <florian.haftmann@cit.tum.de>
Subject: [isabelle] (PATCH) sublocale in a class causes subclass declarations with a raised sort to fail

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 12.10.26 um 04:06 schrieb Alex Mobius (via cl-isabelle-users Mailing
List):

Another bug with non-default-sort classes I hit: if a class has a raised
sort for its type variable, say S (because its "assumes" use a constant
with a sort bound for example), and there is a "sublocale" declaration
in its superclass, the declaration fails with "Type inference imposes
additional sort constraint {subclass_sort} of type parameter 'a of sort
{superclass_sort}". In absence of the sublocale declaration, the
subclass declaration goes through.

As far as i understand, the mechanism is that replaying the locale
definitions fixes sort of 'a to what it was at the time of sublocale.
The easiest fix I've found is to restore the constraints specifically
after superclass body replay in classes. It feels a little iffy, but
should be sound, as monotonicity of sorts for 'a is established elsewhere.

Disclaimer: finding the root cause of this bug was machine-assisted and
the fix, as well as the test suite, is machine-generated. I did my best
to think about and test all of the corner cases that could break, and
the patch itself is tiny, which gives me hopes about its correctness. I
would kindly ask the maintainers to take a more informed look.

With best wishes,

Alex.

Last updated: Oct 29 2026 at 04:52 UTC