Lean being stubborn with class instances

Stream: general

[Kenny Lau]

import linear_algebra.basic

#check λ f : (⊥ : ideal ℤ) →ₗ[ℤ] (⊥ : ideal ℤ), f 0
-- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

[Kenny Lau]

I think the cause is the fact that the ideal is a module over Z in two ways

[Kenny Lau]

in f, the module instance is the second one

[Kenny Lau]

but when I want to coerce f to a function, Lean can only deal with the first one

[Kenny Lau]

despite the fact that the module instances is already encoded in the type of f...