Failed module instance search

Stream: general

[Chris Hughes]

For some reason this instance search is failing. Does someone know why?

import tactic
import linear_algebra.tensor_algebra.basic

example (R : Type) [comm_ring R] (ι : Type)
  (M : ι → Type) [Π (i : ι), add_comm_group (M i)]
  [Π (i : ι), module R (M i)]
  (N : Type)
  [add_comm_group N]
  [module R N] : module R (Π i : ι, (M i →ₗ[R] N)) :=
by apply_instance

It can find an instance for both M i →ₗ[R] N and Π i : ι, N so I don't understand why it fails

[Yaël Dillies]

Is it not pi types troubles again?

[Eric Wieser]

See docs#pi.matrix_algebra for another example of this problem

[Eric Wieser]

The solution workaround is just to add a duplicate instance

[Eric Wieser]

Perhaps like this:

import tactic
import linear_algebra.tensor_algebra.basic

-- example below fails without this
/-- A special case of `pi.module` for `linear_map.module` when the codomain is not
dependently typed. -/
instance pi.linear_map_module_domain {ι R R₂ S M₂ : Type*} {M : ι → Type*}
  [semiring R]
  [semiring R₂] [Π i, add_comm_monoid (M i)] [add_comm_monoid M₂] [Π i, module R (M i)]
  [module R₂ M₂] {σ₁₂ : R →+* R₂} [semiring S] [module S M₂]
  [smul_comm_class R₂ S M₂]:
    module S (Π i, M i →ₛₗ[σ₁₂] M₂) :=
by apply_instance

example (R : Type) [comm_ring R] (ι : Type)
  (M : ι → Type) [Π (i : ι), add_comm_group (M i)]
  [Π (i : ι), module R (M i)]
  (N : Type)
  [add_comm_group N]
  [module R N] : module R (Π i : ι, (M i →ₗ[R] N)) :=
by apply_instance

(edited to be semilinear too)