Zulip Chat Archive

Stream: general

Topic: Failed module instance search


Chris Hughes (May 11 2022 at 11:11):

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 (May 11 2022 at 11:12):

Is it not pi types troubles again?

Eric Wieser (May 11 2022 at 11:12):

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

Eric Wieser (May 11 2022 at 11:13):

The solution workaround is just to add a duplicate instance

Eric Wieser (May 11 2022 at 11:16):

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)


Last updated: Dec 20 2023 at 11:08 UTC