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

Cheers,
Gerwin






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