rcases with new style classes

Stream: general

[Eric Rodriguez]

As an example, consider this:

import tactic.rcases
class foo := (bar : ℕ → ℕ)

class foobar extends foo := (zero : 1 = bar 2)

example (h : foobar) : false :=
begin
  unfreezingI { rcases h with ⟨a, b⟩, },
end

I would expect this code to unpack this. And indeed it does, if you change _either_ or both of the classes to structure. But for some reason this doesn't work at all when they are both classes. What's going on? How am I meant to use rcases in this case?

[Eric Wieser]

Does @⟨a, b⟩ as a pattern work?

[Eric Rodriguez]

that does work, thanks! weird that that's needed

[Eric Wieser]

It's because base classes to class constructors are (typeclass) implicit arguments and so aren't included in anonymous constructor notation