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
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.
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: ??'af 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
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
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