Type class inference problem

Stream: mathlib4

[Joël Riou]

While trying to port CategoryTheory.Abelian.Transfer !4#3424 I have encountered a problem with instance inference. For example, the definition cokernelIso has the assumption [HasCokernels C], but I had to explicitly add

  haveI : ∀ (X' Y' : C) (f' : X' ⟶ Y'), HasCokernel f' :=
    fun _ _ => Limits.HasCokernels.has_colimit

in the code, otherwise the rest of the code would not compile (timeout or some class HasColimit (parallel_pair _ 0)) not found), see https://github.com/leanprover-community/mathlib4/pull/3424/files#diff-3c62b4c9940438de2b684c86d991bc23bbcb57d825c21943b2ecf22f7f327ce8R83-R96

Obviously, Limits.HasCokernels.has_colimit is already declared as an instance, so that I do not see how to fix this.

In the same file, I was not able to make the statement coimageIsoImage_hom work, because the processing of the file becomes unbearably slow on my computer.