Parameterized Coe instance not found

Stream: general

[Francisco Giordano]

My Coe instance below has a parameter α that appears to be hindering instance search . Why is this?

inductive Foo (α : Type) where
| foo

inductive Bar (α : Type) where
| foo : Foo α → Bar α

instance {α} : Coe (Foo α) (Bar α) := ⟨Bar.foo⟩

example : Bar α := Foo.foo -- type mismatch
example : Bar α := Foo.foo (α := α) -- ok