[isabelle-dev] Typing problem in autogenerated axiom

[Dominique Unruh]

Dear all,

while trying to export proof terms from Isabelle, I stumbled upon the
following typing issue which might be a bug.

In HOL.thy, an axiom class ord is defined which fixes a constant
less_eq (syntactic sugar is <=):

> term HOL.ord_class.less_eq;
"op <="
  :: "'a::ord => 'a::ord => bool"

In Ordering.thy, an instantiation for the type constructor fun of this
axiom class is given. Besides other things, this instantiation defines
the axiom le_fun_def_raw:

> ML {* Thm.axiom (the_context()) "Orderings.le_fun_def_raw" *};
val it =
   "ord_fun_inst.less_eq_fun ==
      %(f::?'a::{} => ?'b::{}) g::?'a::{} => ?'b::{}.
         ALL x::?'a::{}. f x <= g x" : Thm.thm

Notice the "f x <= g x" part which represents an application of
HOL.ord_class.less_eq (you can verify this by adding "|> Thm.prop_of"
before *} in the above ML command). f x and g x have type "?'b::{}"
which does not have class ord. So less_eq needs to have type "?'b::{}
=> ?'b::{} => bool" which does does not match "'a::ord => 'a::ord =>
bool". So, as far as I understand the type system of Isabelle, the
axiom le_fun_def_raw is not well-typed.

(NB: You cannot get the axiom le_fun_def_raw by writing "thm
Orderings.le_fun_def_raw" in the Isabelle toplevel, this only
retrieves the theorem with the same name. This theorem has different
types.)

My question is the following:

* Is this a bug?
* If not, why is le_fun_def_raw well-typed? Where can I find a
description of Isabelle's type system?

Best wishes,
Dominique.


PS: I noticed the following possibly related fact:

> ML {* the_context() |> Sign.consts_of |> (fn c => Consts.read_const c "HOL.ord_class.less_eq") *};
val it = Const ("HOL.ord_class.less_eq", "?'a::{} => ?'a::{} => bool")
: Term.term

Now suddenly the type of less_eq does not contain type classes, in
contrast to what "term HOL.ord_class.less_eq;" outputs. I do not
understand why.