structure value invalid

Stream: new members

[Yakov Pechersky]

An unfamiliar error:

invalid structure value {...}, expected type is not known(solution: use qualified structure instance { struct_id . ... }

I don't think I can easily make a #mwe. This might have to do with clashing class names, I've defined my own group and am trying to say

def to_group (G : Type*) [group G] : _root_.group G :=
{ mul := group.op,
  mul_assoc := λ _ _ _, (group.assoc' _ _ _).symm,
  one := group.e,
  one_mul := group.e_op',
  mul_one := group.op_e',
  inv := group.inv,
  div := λ f g, group.op f (group.inv g),
  div_eq_mul_inv := λ _ _, rfl,
  mul_left_inv := group.inv_op' }

[Julian Berman]

Does it in fact work if you do what it says? -- i.e. { _root_.group G . mul := group.op, blabla }?

[Julian Berman]

I'm pretty sure I've seen that error before but I'm sure in much simpler poking than whatever you're up to