Structure extends

Stream: new members

[Martin Dvořák]

In the exercises from "Lean for the Curious Mathematician" (2020), there is this example of extending a structure.

structure Group :=
  (G : Type*)
  (op : G → G → G)
  (infix * := op) -- temporary notation `*` for `op`, just inside this structure declaration
  (op_assoc' : ∀ (x y z : G), (x * y) * z = x * (y * z))
  (id : G)
  (notation 1 := id) -- temporary notation `1` for `id`, just inside this structure declaration
  (id_op' : ∀ (x : G), 1 * x = x)
  (inv : G → G)
  (postfix ⁻¹ := inv) -- temporary notation `⁻¹` for `inv`, just inside this structure declaration
  (op_left_inv' : ∀ (x : G), x⁻¹ * x = 1)

structure CommGroup extends Group :=
  (infix * := op)
  (op_comm : ∀ (x y : G), x * y = y * x)

def rat_Group : Group :=
{ G := ℚ,
  op := (+), -- you can put parentheses around an infix operation to talk about the operation itself.
  op_assoc' := add_assoc,
  id := 0,
  id_op' := zero_add,
  inv := λ x, -x,
  op_left_inv' := neg_add_self }

def rat_CommGroup : CommGroup :=
{ G := ℚ, op_comm := add_comm, ..rat_Group }

SOURCE:
https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/wednesday/structures.lean

Why do we have to explicitly state G := ℚ on the last line but not the other fields? What is the general rule?

Is it because CommGroup contains a field op_comm which refers to G explicitly? Do these have to be always restated before instantiating the new fields and before calling ..superstructure in the definition?

[Ruben Van de Velde]

The problem seems to be that add_comm is itself a theorem about all add_comm_semigroups G, so Lean can't figure out what to fill in forG. It seems to be fine with a hint:

def rat_CommGroup : CommGroup :=
{ op_comm := @add_comm ℚ _, ..rat_Group }

or:

lemma add_comm' (a b : ℚ) : a + b = b + a := add_comm _ _

def rat_CommGroup : CommGroup :=
{ op_comm := add_comm', ..rat_Group }