Lean can't synthesize class instances

Stream: new members

[Hanting Zhang]

import tactic
import data.mv_polynomial.rename

open equiv (perm)
open_locale big_operators

noncomputable theory

namespace mv_polynomial

variables {σ : Type*} {R : Type*}
variables {τ : Type*} {S : Type*}

def is_symmetric [comm_semiring R] (φ : mv_polynomial σ R) : Prop :=
∀ e : perm σ, rename e φ = φ

namespace is_symmetric

variables [comm_semiring R] [comm_semiring S] {φ ψ : mv_polynomial σ R}

@[simp]
lemma neg (hφ : is_symmetric φ) : is_symmetric (-φ) := by sorry -- fails, "failed to synthesize type class instance for `has_neg (mv_polynomial σ R)`"

end is_symmetric

end mv_polynomial

What is going on?

[Shing Tak Lam]

I'm not sure if you have to have comm_semiring R, but if I change it to comm_ring R and add an import then it works.

import tactic
import data.mv_polynomial.rename
import data.mv_polynomial.comm_ring -- NEW IMPORT

open equiv (perm)
open_locale big_operators

noncomputable theory

namespace mv_polynomial

variables {σ : Type*} {R : Type*}
variables {τ : Type*} {S : Type*}

def is_symmetric [comm_semiring R] (φ : mv_polynomial σ R) : Prop :=
∀ e : perm σ, rename e φ = φ

namespace is_symmetric

variables [comm_ring R] [comm_semiring S] {φ ψ : mv_polynomial σ R} -- CHANGED FROM [comm_semiring] TO [comm_ring R]

@[simp]
lemma neg (hφ : is_symmetric φ) : is_symmetric (-φ) := by sorry -- WORKS NOW

end is_symmetric

end mv_polynomial

[Hanting Zhang]

Thanks! I forgot about comm_semiring R. Why does the data.mv_polynomial.comm_ring import matter though? Does the type class inference system need it?

[Shing Tak Lam]

I think the comm_ring instance is defined in data.mv_polynomial.comm_ring, and data.mv_polynomial.rename doesn't import data.mv_polynomial.comm_ring, so the instance isn't available until you import that file.

[Hanting Zhang]

Ah, ok, thanks!