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



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.





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