Weird error from `old_structure_cmd`

Stream: general

[Eric Wieser]

Is this a bug, or just a limitation?

import algebra.ring.basic

set_option old_structure_cmd true

@[protect_proj] class no_zero_divisor_ring (α : Type*) extends ring α, no_zero_divisors α

gives

type mismatch at application
  @ring.to_distrib α right_distrib
term
  right_distrib
has type
  ∀ (a b c : α), (a + b) * c = a * c + b * c
but is expected to have type
  ring α

[Anne Baanen]

I'm guessing this is because no_zero_divisors uses instance arguments rather than structure fields for 0 and *?

[Eric Wieser]

Your statement is true, although that doesn't help me understand why that fails!

[Mario Carneiro]

old_structure_cmd does not support dependent sequences of parents

[Eric Wieser]

It would be nice if it stated that rather than blew up, but I guess there's little motivation to change it with lean4 now available

[Eric Wieser]

Although I can't help but feel we'll want to build some automation to emulate parts of old_structure_cmd, and maybe then we can try to support that use-case.