Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Variable 'b::{} not of sort type


view this post on Zulip Email Gateway (Aug 19 2022 at 08:55):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
We recently came across this surprising (to me) behaviour in Isabelle 2012 (also development version):

lemma "f x = f x"
apply (insert refl[where t="x"])

*** Type unification failed: Variable 'b::{} not of sort type


*** Failed to meet type constraint:


*** Term: x :: 'b
*** Type: ??'a

whereas the workaround

lemma "f x = f (x::'b)"
apply (insert refl[where t="x"])

works as expected.

I would have expected type inference to give 'b the default sort "type" (as it does to 'a, if you look at the output of "term f" with show_sorts on).

Am I expecting wrong or should this be changed?

Cheers,
Gerwin

view this post on Zulip Email Gateway (Aug 19 2022 at 08:55):

From: Lars Noschinski <noschinl@in.tum.de>
On 31.10.2012 07:14, Gerwin Klein wrote:

We recently came across this surprising (to me) behaviour in Isabelle 2012 (also development version):

lemma "f x = f x"
apply (insert refl[where t="x"])

*** Type unification failed: Variable 'b::{} not of sort type


*** Failed to meet type constraint:


*** Term: x :: 'b
*** Type: ??'a

f ist also a free variable, I assume? This is a long-standing behaviour.
I remember stumbling on this about two years ago and as far as I
remember the following discussion lead to the conclusion that changing
this behaviour would lead to problems with logics which don't have a
single default sort (HOLCF?).

whereas the workaround

lemma "f x = f (x::'b)"
apply (insert refl[where t="x"])

works as expected.

Fixing the type of f should also help.

view this post on Zulip Email Gateway (Aug 19 2022 at 08:56):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
On 31/10/2012, at 7:10 PM, Lars Noschinski <noschinl@in.tum.de> wrote:

On 31.10.2012 07:14, Gerwin Klein wrote:

We recently came across this surprising (to me) behaviour in Isabelle 2012 (also development version):

lemma "f x = f x"
apply (insert refl[where t="x"])

*** Type unification failed: Variable 'b::{} not of sort type


*** Failed to meet type constraint:


*** Term: x :: 'b
*** Type: ??'a

f ist also a free variable, I assume? This is a long-standing behaviour. I remember stumbling on this about two years ago and as far as I remember the following discussion lead to the conclusion that changing this behaviour would lead to problems with logics which don't have a single default sort (HOLCF?).

Is that discussion online somewhere? Im skeptical. The type of f is also free, and it does get the default sort. In fact, if that wouldn't usually happen, nothing in Isabelle would work without annotation.

What does the parser do when it sees a free type variable in a function range in HOLCF? Why is it hard to implement the same behaviour in inference?

whereas the workaround

lemma "f x = f (x::'b)"
apply (insert refl[where t="x"])

works as expected.

Fixing the type of f should also help.

Mentioning the type 'b in any way seems to helps.

It's rare enough that I don't really care, and it's easy to work around, but it cost us several hours to diagnose, distill an example and to report. It should at least be documented.

Cheers,
Gerwin

view this post on Zulip Email Gateway (Aug 19 2022 at 09:19):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
Lars politely didn't point out my lame Google skills and sent me this link:

http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01573.html

I guess the conclusion is, we stick with the workaround. I hope my email had enough additional keywords in it to make this show up in searches more easily.

Cheers,
Gerwin

view this post on Zulip Email Gateway (Aug 19 2022 at 09:21):

From: Makarius <makarius@sketis.net>
The main keywords are "Strugatsky" and "Stalker" :-)

Skimming over the thread cited above of this recurrent Isabelle type class
topic, I take it as a reminder to improve the PIDE document feedback about
results of type-inference (in Isabelle/jEdit only, not Proof General / TTY
anymore). Then users will see better what type-inference has produced for
them, with extra markup for freshly introduced types and their sorts.

Until this happens (not before the coming release), I recommend to read
the book, such that the jokes and allusions about the "Zone" become easier
to understand. See also http://en.wikipedia.org/wiki/Roadside_Picnic

Makarius


Last updated: Mar 28 2024 at 20:16 UTC