# Re: [isabelle] problem with sort inference

On Fri, 28 May 2010, Stephan Merz wrote:

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

`This behaviour has been there from the very first day of type classes in
``Isabelle. Until some years ago it was even more confusing, since Pure had
``its own "logic" type class, simular to "type" in HOL.
`

`Since we have a very powerful "user-space type system" mechanism for quite
``some time already, I have experimented with a global "type improvement"
``for Isabelle/HOL at some point, that specializes pending inference
``parameters to something of sort HOL.type. Unfortunately, it did not fully
``work out in certain border cases where the fully general types are needed
``internally (maybe it can be attempted again at some later stage).
`

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"
`

`Yes, the "default" sort is attached to any type variable that is explicit
``in the text, but does not have a sort constraint yet -- either directly or
``via the context.
`

`BTW, the long statement form allows to express your local context
``explicitly, without complicating the terms themselves:
`
lemma
fixes f :: "'a => 'c => 'b"
and g :: "'a => 'c"
assumes "b = a"
shows "f a (g a) = f b (g b)"
Makarius

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