Adam Dingle (Apr 07 2026 at 16:25): Adam Dingle (Apr 07 2026 at 16:25):As an experiment, I'm trying to define my own equality operator and a congruence axiom. I first tried this:
axiomatization
eq :: "'a ⇒ 'a ⇒ bool"
where
comb : "eq s t ⟹ eq u v ⟹ eq (s u) (t v)"
Isabelle complains:
Type unification failed
Type error in application: operator not of function type
Operator: s :: 'a
Operand: u :: 'a
Why isn't Isabelle inferring a proper polymorphic type for s, t, u, and v?
I then tried moving the definition of comb into a separate axiomatization statement:
axiomatization
eq :: "'a ⇒ 'a ⇒ bool"
axiomatization
where
comb : "eq s t ⟹ eq u v ⟹ eq (s u) (t v)"
Now I just get a warning:
Introduced fixed type variable(s): 'a, 'b in "s" or "t" or "u" or "v"
Is the warning benign? Is there some way to make it go away? Thanks for any advice.
Maximilian Schäffeler (Apr 07 2026 at 17:05):You might want to inspect the theory "HOL" (import as HOL.HOL). There, the axiomatization commands produce similar warnings.
Adam Dingle (Apr 08 2026 at 06:04):I realized that in my second example above, adding a universal quantifier makes the warning go away:
axiomatization
where
comb : "⋀s t u v . eq s t ⟹ eq u v ⟹ eq (s u) (t v)"
However, this doesn't help if I put this into the same axiomatization statement where I declare "eq", as in my first example above. I'm not sure why.
Mathias Fleury (Apr 08 2026 at 06:07):have tried to explicitly put types?
Mathias Fleury (Apr 08 2026 at 06:07):the warning states that Isabelle added types (which is sometimes what you want but often enough a mistake)
Mathias Fleury (Apr 08 2026 at 06:08):so add the types yourself and Isabelle should not complain…
Adam Dingle (Apr 08 2026 at 06:18):I tried adding explicit types, without the universal quantifier:
axiomatization
where
comb : "eq (s :: 'a ⇒ 'b) (t :: 'a ⇒ 'b) ⟹ eq (u :: 'a) (v :: 'a) ⟹ eq (s u) (t v)"
However Isabelle still issues a warning:
Introduced fixed type variable(s): 'a, 'b in "s" or "t" or "u" or "v"
So it seems that the quantifier is necessary if I want the warning to disappear.
Mathias Fleury (Apr 08 2026 at 06:21):that is a feature right?
Mathias Fleury (Apr 08 2026 at 06:22):Isabelle type unification does: disregard every type annotation, then come up with its own type, and only then combine those inferred types with the ones you provided
Mathias Fleury (Apr 08 2026 at 06:22):So I am not surprised that annotations are not declaring types
Adam Dingle (Apr 08 2026 at 06:33):I could consider this behavior to be a feature if I really understood how Isabelle's type inference worked, but some things are still mysterious to me:
lemma comb: "eq s t ⟹ eq u v ⟹ eq (s u) (t v)"
sorry
Now Isabelle does not report the "introduced fixed type variables" warning. So apparently type inference works differently in an axiomatization statement than in a lemma; I'm not sure why.
axiomatization
eq :: "'a ⇒ 'a ⇒ bool"
where
comb : "⋀s t u v . eq s t ⟹ eq u v ⟹ eq (s u) (t v)"
Then type checking fails completely:
Type unification failed
Type error in application: operator not of function type
Operator: s :: 'a
Operand: u :: 'a
I don't see why.
Fabian Huch (Apr 08 2026 at 07:29):Polymorphism in Pure and HOL is schematic (standard HM-polymorphism): a polymorphic type does not exist, only a polymorphic type schema. You can declare a polymorphic constant (this gives you a polymorphic let-binding) and then axiomatize something about a specific instance, but here you have a fixed 'a.
Fabian Huch (Apr 08 2026 at 07:30):So the following will also not work:
lemma
fixes P :: "'a ⇒ bool"
shows "P (1::nat)"
But you can declare the polymorphic constant P:
consts P :: "'a ⇒ bool"
and later on create your axiomatization:
axiomatization where ax: "P (1::nat)"
(this has nothing to do with equality or function types per se)
Adam Dingle (Apr 08 2026 at 07:34):Fabian: This is helpful and explains some of the mystery, thanks.
Last updated: Apr 14 2026 at 09:21 UTC