Typeclass resolution with functions

Stream: lean4

[Parth Shastri]

In the following code, Lean fails to find an instance despite it being able to for a more complex type.

class Para (ϕ : Type u → Type u)

instance : Para λ α => α where
instance [Para ϕ] [Para ϕ'] : Para λ α => ϕ α → ϕ' α where
instance [Para ϕ] : Para λ α => List (ϕ α) where

#synth Para λ α => α            -- instParaType
#synth Para λ α => α → α        -- instParaTypeForAll
#synth Para λ α => List (α → α) -- instParaTypeList
#synth Para λ α => List α       -- failed to synthesize  Para fun α => List α

#check @instParaTypeList _ instParaType -- Para fun α => List α

Running with set_option trace.Meta.synthInstance.instances true reveals that no candidate instances are found for the fourth resolution. From digging further, I was able to determine that the root of the issue lies in the DiscrTree.
When converting the type to a key, the type is eta-reduced in whnfDT, leading to the key path const Para, const List for the last example while the first three examples result in const Para, other. The three instances all have the key path const Para, other, so the first three examples succeed, while the last one fails.
It turns out in this particular case, the problem can be remedied by writing

instance [Para ϕ] : Para no_index λ α => List (ϕ α) where

but there is no obvious indication for the cases in which this is necessary.
Is this a known limitation of the typeclass system? Is it possible to modify the system to correctly resolve this case?