local attributes and extends

Stream: general

[Sebastien Gouezel]

I would like to declare a structure extending a class, and make it locally a class. Then I expect typeclass inference to find instances of the smaller class automatically, but I can't get this to work. Is there a syntax I am missing here?

structure myclass2 (α : Type*) extends has_zero α :=
(foo : α)

local attribute [instance] myclass2.to_has_zero
local attribute [class] myclass2

instance I2 {α : Type*} [myclass2 α] : has_zero α := by apply_instance -- fails