Using type classes in an extends clause

Stream: general

[Eric Wieser]

I'm finding that this code:

universe u

-- works fine without this
set_option old_structure_cmd true

/-- A semigroup is a type with an associative op. -/
class base_semigroup (G : Type u) (op : G → G → G) :=
(op_assoc' : ∀ a b c : G, op (op a b) c = op a (op b c))

class mul_semigroup (G : Type u) extends has_mul G, base_semigroup G (*)

gives me the weird error

type mismatch at application
  @has_mul.mul G mul
term
  mul
has type
  G → G → G
but is expected to have type
  has_mul G

If I remove old_structure_cmd then it works fine.

[Eric Wieser]

Using (@has_mul.mul G ‹has_mul G›) doesn't help either, it still infers an object of the wrong type

[Eric Wieser]

Pinging this since I'm still curious what's going on here

[Mario Carneiro]

old_structure_cmd doesn't handle dependencies between parents

[Mario Carneiro]

What actually needs to go in that position is (@has_mul.mul G ⟨mul⟩), but it seems that the elaboration context is not correct to even allow you to write this

[Mario Carneiro]

the workaround is to do

class mul_semigroup (G : Type u) extends has_mul G :=
(op_assoc' : ∀ a b c : G, (*) ((*) a b) c = (*) a ((*) b c))

instance mul_semigroup.to_base_semigroup (G) [mul_semigroup G] :
  base_semigroup G (*) := ⟨mul_semigroup.op_assoc'⟩

which is what old_structure_cmd does anyway

[Eric Wieser]

Unfortunately that creates repetition where I was trying to eliminate it

[Eric Wieser]

But I suppose it does at least enable the generalization I was hoping for

[Eric Wieser]

For context, my motivation is needing two different group structures on the same type, (⋏) and (*)

[Mario Carneiro]

can you use a type alias?

[Eric Wieser]

No, because if I use

abbreviation mul_semigroup [has_mul G] := base_semigroup G (*)

then every user of mul_semigroup has to remember to provide has_mul explicitly.

[Eric Wieser]

(oh, unless you meant to make a ⋏ b = to_wedge a * to_wedge b, in which case yes, that was my backup plan)