class instance unification fails

Stream: general

[Yury G. Kudryashov]

I tried to use the @... (multiplicative G) ... trick in data/monoid_algebra to get defs/proofs for add_monoid_algebra. Now polynomial.algebra fails, see https://github.com/leanprover-community/mathlib/pull/2492/checks?check_run_id=614475313

[Yury G. Kudryashov]

Here is the error message with set_option pp.all true:

/home/urkud/projects/mathlib/polynomial/src/data/polynomial.lean:31:39: error: type mismatch, term
  @add_monoid_algebra.algebra.{?l_1 ?l_2} ?m_3 ?m_4 ?m_5 ?m_6
has type
  @algebra.{?l_1 (max ?l_2 ?l_1)} ?m_3
    (@add_monoid_algebra.{?l_1 ?l_2} ?m_3 ?m_4 (@comm_semiring.to_semiring.{?l_1} ?m_3 ?m_5))
    ?m_5
    (@add_monoid_algebra.semiring.{?l_1 ?l_2} ?m_3 ?m_4 (@comm_semiring.to_semiring.{?l_1} ?m_3 ?m_5) ?m_6) : Type (max
        ?l_2
        ?l_1)
but is expected to have type
  @algebra.{u u} R (@polynomial.{u} R _inst_1) _inst_1
    (@comm_semiring.to_semiring.{u} (@polynomial.{u} R _inst_1) (@polynomial.comm_semiring.{u} R _inst_1)) : Type u

[Yury G. Kudryashov]

How can I debug failures like this one?

[Scott Morrison]

I think

instance : algebra R (polynomial R) :=
begin
   convert @add_monoid_algebra.algebra R ℕ _ _,
end

helps.

[Scott Morrison]

That then fails with:

[Scott Morrison]

1 goal
R : Type u,
_inst_1 : comm_semiring.{u} R
⊢ @eq.{u+1} (semiring.{u} (@polynomial.{u} R _inst_1))
    (@comm_semiring.to_semiring.{u} (@polynomial.{u} R _inst_1) (@polynomial.comm_semiring.{u} R _inst_1))
    (@add_monoid_algebra.semiring.{u 0} R nat (@comm_semiring.to_semiring.{u} R _inst_1) nat.add_monoid)

[Scott Morrison]

So we're ending up in semiring two different ways.

[Chris Hughes]

And they're not defeq?

[Yury G. Kudryashov]

Definition of comm_semiring is here: https://github.com/leanprover-community/mathlib/blob/polynomial-review/src/data/monoid_algebra.lean#L469

[Yury G. Kudryashov]

instance [comm_semiring k] [add_comm_monoid G] : comm_semiring (add_monoid_algebra k G) :=
{ .. add_monoid_algebra.semiring, .. @monoid_algebra.comm_semiring k (multiplicative G) _ _ }

I wonder why they're not defeq.

[Yury G. Kudryashov]

This works:

attribute [ext] semiring
instance : algebra R (polynomial R) :=
begin
   convert @add_monoid_algebra.algebra R ℕ _ _,
   ext1; refl
end

[Yury G. Kudryashov]

If I prove all zero_mul etc as lemmas using the @ ... multiplicative trick, then feed them to instance : semiring (add_monoid_algebra k G), then polynomial.algebra works without any tricks. If I replace, e.g., one_mul := one_mul with one_mul := @one_mul (monoid_algebra k (multiplicative G)) _, then it doesn't work.

[Scott Morrison]

Adding instance : semiring (polynomial R) := add_monoid_algebra.semiring before instance comm_semiring ... solves the problem.

[Yury G. Kudryashov]

I'll try once lean will recompile mathlib (added a simp lemma to algebra/group/hom).