Zulip Chat Archive

Stream: new members

Topic: Lean can't synthesize class instances


view this post on Zulip Hanting Zhang (Jan 16 2021 at 18:40):

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 ( : 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?

view this post on Zulip Shing Tak Lam (Jan 16 2021 at 19:01):

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 ( : is_symmetric φ) : is_symmetric (-φ) := by sorry -- WORKS NOW

end is_symmetric

end mv_polynomial

view this post on Zulip Hanting Zhang (Jan 16 2021 at 19:06):

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?

view this post on Zulip Shing Tak Lam (Jan 16 2021 at 19:10):

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.

view this post on Zulip Hanting Zhang (Jan 16 2021 at 19:12):

Ah, ok, thanks!


Last updated: May 18 2021 at 17:44 UTC