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



On 31/10/2012, at 7:10 PM, Lars Noschinski <noschinl at 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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.