Locale ignores operation notation

Question

The following works fine:

class test1 = semilattice_sup +
  fixes x :: "'a"
  assumes "x < y"

But when I replace class by locale:

locale test2 = semilattice_sup +
  fixes x :: "'a"
  assumes "x < y"

I get the error:

Type unification failed: Variable 'a::type not of sort ord

The error can be fixed as follows:

locale test2 = semilattice_sup +
  fixes x :: "'a"
  assumes "less x y"

But is it possible to use < notation?

---

UPDATE

Here is a similar problem:

datatype 'a ty = A | B

instantiation ty :: (order) order
begin
definition "x < y ≡ x = A ∧ y = B"
definition "x ≤ y ≡ (x :: 'a ty) = y ∨ x < y"
instance
  apply intro_classes
  using less_eq_ty_def less_ty_def by auto
end

locale loc = semilattice_sup +
  fixes f :: "'a ⇒ 't :: order"
begin
definition "g ≡ inv f"
end

class cls = semilattice_sup +
  fixes f :: "'a ⇒ 'a ty"
begin
interpretation base: loc .
abbreviation "g ≡ base.g"
end

The interpretation fails with the following error:

Type unification failed: Variable 'a::type not of sort semilattice_sup

Answer 1

Would

locale test2 =
  fixes x :: "'a :: semilattice_sup"
  assumes "x < y"

be an option for you? In this case you no longer base your locale on another locale, but instead require the type of x to be an instance of the class semilattice_sup, which allows you to use nice infix syntax for less.