## Stream: general

### Topic: Using type classes in an extends clause

#### Eric Wieser (Oct 05 2020 at 16:31):

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 (Oct 05 2020 at 16:34):

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

#### Eric Wieser (Oct 14 2020 at 10:13):

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

#### Mario Carneiro (Oct 14 2020 at 10:15):

old_structure_cmd doesn't handle dependencies between parents

#### Mario Carneiro (Oct 14 2020 at 10:19):

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 (Oct 14 2020 at 10:21):

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 (Oct 14 2020 at 10:26):

Unfortunately that creates repetition where I was trying to eliminate it

#### Eric Wieser (Oct 14 2020 at 10:27):

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

#### Eric Wieser (Oct 14 2020 at 10:32):

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

#### Mario Carneiro (Oct 14 2020 at 10:35):

can you use a type alias?

#### Eric Wieser (Oct 14 2020 at 12:03):

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 (Oct 14 2020 at 12:08):

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

Last updated: May 08 2021 at 03:17 UTC