instance not synthesizing issue?

Stream: lean4

[Michael Jam]

This mwe was working on nightly-2021-08-18
The last line fails since nightly-2021-08-21
I could not simplify that example further, it still looks a bit convoluted...

class L0  where f : Type _
class A0  where a : Type _
class B0  where b : Type _
inductive F [A0] [B0] where
  | a (_ : A0.a)
  | b (_ : B0.b)
instance [A0] [B0] : L0 where f := F
class A1
instance [A1] : A0 where a := Nat
class L1 extends A1, B0
class C0 [L0]
-- instance [L1] : L0 := inferInstance
instance [L1] : C0 := ⟨⟩

Somehow, uncommenting the penultimate line helps lean, but I think it shouldn't be necessary

[Leonardo de Moura]

Thanks for finding this issue. Pushed a fix for it.

[Leonardo de Moura]

How can I install a specific lean commit with elan?

I use the following setup.
I have a toolchain for my stage1 build directory.

/home/leodemoura/projects/lean4/build/release/stage1

I use elan override to set this toolchain in my tests directory.