# [isabelle] Pitfall with type-classes in Isar-Lemma format

Hi all,
(Referring to Isabelle2011-1)
I recently ran into the following pitfall:
lemma pitfall1:
notes [[show_sorts]]
notes test = refl[where 'a='a]
fixes x::"'a::default"
shows "x=x"
thm test -- "'a has the wrong sort here!"
using test apply -
Now it outputs:
type variables:
'a :: type
'a :: default
and, of course, apply (rule test) fails. When inspecting this failure,
the already confused user gets the following trace from the unifier
(even with show_sorts turned on!)
The following types do not unify:
'a \<Rightarrow> 'a \<Rightarrow> bool
'a \<Rightarrow> 'a \<Rightarrow> bool
I would expect that a type-variable with the same name should also have
the same sort -- at least when I introduce it within the
scope of the very same lemma.
And even more strange, this pitfall can be resolved by just swapping the
notes and the fixes declaration:
lemma pitfall1_resolved:
fixes x::"'a::default"
notes [[show_sorts]]
notes test = refl[where 'a='a]
shows "x=x"
by (rule test)
Regards,
Peter

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