# Re: [isabelle] Extra type variables, type classes and locales

Quoting Christoph Feller <c_feller at informatik.uni-kl.de>:

Hallo,
I have with a hidden extra type variable again and again I have no
clue what exactly went wrong. I've made a small example:
class testC = type +
fixes from_nat :: "nat => 'a"
and to_nat :: "'a => nat"
locale Test =
fixes dummy :: "'a::testC"
assumes dd: "ALL z::'a::testC. to_nat z ~= 0"
begin
definition ftest :: "nat => 'a list" where "ftest n == [from_nat n]"
inductive test::"nat => nat => bool"
where
"((ftest a)::'a list) = ((ftest b)::'a list) ==> test a b"
...
I thought the locale not only fixed dummy but also 'a so that it isn't
necessarily an extra type variable in the inductive definition. Am I
wrong or is there another mistake in my example?
Thanks in advance,
Christoph

Hi Christoph,
I think you are right to expect this to work.

`When you define a locale like "Test", the locale package defines a
``predicate of the same name, which encodes all of the locale
``assumptions. Usually the predicate takes all of the parameters from
``"fixes" declarations as arguments. However, locales like your "Test"
``example require some special treatment. For example:
`
thm Test_def
Test TYPE(?'a::testC) == ALL z::?'a::testC. to_nat z ~= 0

`As you can see, the locale predicate "Test" does not depend on the
``locale parameter "dummy", but it still depends on the type variable 'a.
`

`I would have expected the locale package to use the same trick to
``encode functions like your "test". That is, an extra hidden
``TYPE(?'a::testC) parameter should be added to make the type checker
``happy. I would consider this to be a bug in the locale implementation.
`

`By the way, the following definition *does* work inside the locale.
``Just like your inductive definition of "test", it uses type variable
``'a on the right-hand side, but no type variable appears in the type of
``the constant. The only difference is that this one also uses the
``locale constant "dummy" on the right-hand side.
`
definition
test2 :: "nat => bool"
where
"test2 n = (((ftest n) :: 'a list) = [dummy])"
- Brian

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