Email Gateway (Aug 18 2022 at 11:17): Email Gateway (Aug 18 2022 at 11:17):From: Clemens Ballarin <ballarin@in.tum.de>
Dear David,
the type variables in the error message are fixed ('a, not ?'a) and
hence do not unify.
The reason is that in the context of a locale, the parameters
(including type parameters) are considered given and hence cannot be
instantiated.
Unfortunately, locales and local theories are notorious in renaming
type variables, so the type names you write are not the type names
you will get. It's best to look at Isabelle's output at the
"begin" (after the locale declaration). For hhs, this is:
theory Ex
locale hhs =
fixes Adt :: "int => ('c * 'c) set"
and sem :: "int => (int => ('c * 'c) set) => ('c * 'c) set"
and sem_prod :: "('c * 'c) set => ('c * 'c) set => ('c * 'c) set"
and Adt' :: "int => ('d * 'd) set"
and sem' :: "int => (int => ('d * 'd) set) => ('d * 'd) set"
and sem_prod' :: "('d * 'd) set => ('d * 'd) set => ('d * 'd) set"
and \<psi> :: "'a => 'b"
assumes "!!i a. \<lbrakk>i\<rbrakk> a == a i"
and "!!i a. \<lbrakk>i\<rbrakk>r a == a i"
and "hhs op \<otimes> op \<otimes>r"
This should give you the right types. It also shows that the type of
\<psi> is unrelated to the types of the other parameter, which is
probably not what you intended.
Clemens
Last updated: Nov 04 2025 at 08:30 UTC