How to reuse type variables from locales

I want to fix a few functions and constants of arbitrary types in a locale for a bunch of Foo definitions. I then want to fix some additional functions and constants in another locale for a bunch of Bar definitions which will want to use the same types as the Foo definitions.

locale Foo =       fixes theFoo  ::  'foo
locale Bar = Foo + fixes makeBar :: "'foo ⇒ 'bar"

context Bar
begin
definition theBar :: 'bar where "theBar = makeBar theFoo"
(* Here, theFoo is not a 'foo, but rather an 'a *)
end

But this does not work, because the Bar's 'foo is a new free type variables and the Foo's 'foo gets renamed to 'a, so now the types don't match. How can I reuse 'foo from Foo inside Bar?

Solution

As you've seen, the free type variables are not matched automatically. From the point of view of compositionality, this actually makes sense.

print_locale Bar
(*
locale Bar
  fixes theFoo :: "'a"
    and makeBar :: "'foo ⇒ 'bar"
*)

Locales can be understood as structures that are parameterized over the fixed variables. Accordingly, Isabelle has a syntax to provide these parameters, which can also be used to link the type variables explicitly using for:

locale Bar =
  Foo theFoo
    for theFoo :: 'foo
+
  fixes makeBar :: "'foo ⇒ 'bar"

print_locale Bar
(*
locale Bar
  fixes theFoo :: "'foo"
    and makeBar :: "'foo ⇒ 'bar" 
*)

By the way, this feature can also be used to rename parts of the locale (for instance, we could write Foo theFoo2 for theFoo2 :: 'foo) or to instantiate some of its parameters with more concrete objects.

In many cases, you don't have to explicitly match the variables: If you have assumptions linking the two fixed names, Isabelle will infer that they need corresponding types. For the minimal example, this looks contrived, I know:

locale Bar =
  Foo +
  fixes makeBar :: "'foo ⇒ 'bar"
  assumes "makeBar theFoo = makeBar theFoo"

print_locale Bar
(*
locale Bar
  fixes theFoo :: "'foo"
    and makeBar :: "'foo ⇒ 'bar"
  assumes "Bar theFoo makeBar"
*)