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



On 01/11/2012, at 9:33 AM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:

> 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?

Lars politely didn't point out my lame Google skills and sent me this link:

http://www.mail-archive.com/isabelle-dev at 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






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