# [isabelle] problem with sort inference

I'm having a problem with sort inference in Isabelle/HOL: when I enter
lemma "b = a ==> f a (g a) = f b (g b)"
the following types and sorts are inferred:
variables:
g :: 'a => 'c
f :: 'a => 'c => 'b
a, b :: 'a
type variables:
'a, 'b :: type
'c :: {}
Note the sort {} for type variable 'c. This prevents me to do something like
lemma "b = a ==> f a (g a) = f b (g b)"
proof -
from fun_cong have "f a = f b ==> f a (g a) = f b (g a)"
which yields
*** Type unification failed: Variable 'c::{} not of sort type
*** Type error in application: Incompatible operand type
since fun_cong expects functions between types of sort "type".
I can get around this problem by stating the lemma in the form
lemma "b = a ==> (f::'a => 'c => 'b) a ((g::'a => 'c) a) = f b (g b)"
that is by explicitly annotating the term with the inferred types (even without stating sort constraints) -- I assume that is because the explicitly given type variables receive the default sort "type". I understand that the inferred type is more general, but it is actually useless. As a user, I find that behavior quite strange -- bug or feature?
Thanks,
Stephan

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