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

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?


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