Chaining CoeFun instances?

Stream: iris-lean

[Markus de Medeiros]

In Pranav's mutual fixpoints PR there are these two CoeFun instances

instance [OFE α] [OFE β] [OFE γ] : CoeFun (α -c> β -n> γ) (fun _ => α → β → γ) := ⟨fun f x => (f.f x).f⟩
instance [OFE α] [OFE β] [OFE γ] : CoeFun (α -c> β -c> γ) (fun _ => α → β → γ) := ⟨fun f x => (f.f x).f⟩

At this point in the code we already have CoeFun and OFE instances for α -c> β and α -n> β in scope. Anyone have any guesses why these extra coercions are necessary. or how to get Lean to pick up on the old ones so they can be eliminated?