universe issue when providing new instance

Stream: general

[Julian Külshammer]

In #6481 I attempted to remove the commutativity assumption on the ground (semi)ring when constructing the mv_polynomial ring. It was no problem removing the commutativity assumption from the definition but as soon as I added the semiring instance, much later in the file eval\2_eta broke which to me seems unrelated and I read the error message as there being a problem with universes, though I don't understand why. Can someone clarify why this happens and how this can be solved?

[Eric Wieser]

Try adding an explicit type annotation to C?

[Julian Külshammer]

When it is defined or where it breaks?

[Kevin Buzzard]

@[simp] lemma eval₂_eta (p : mv_polynomial σ R) : eval₂ (C : R →+* mv_polynomial σ R) X p = p := fixes the first problem.

[Kevin Buzzard]

I am assuming that this wasn't needed before. What has happened?

[Eric Wieser]

The elaborator gets stuck because it can't invoke typeclass inference to convert comm_semiring to semiring?

[Kevin Buzzard]

The second error is more scary:

type mismatch at application
  eval₂_comp_left (map g)
term
  map g
has type
  mv_polynomial ?m_1 S₁ →+* mv_polynomial ?m_1 S₂ : Type (max (max ? v) ? w)
but is expected to have type
  ?m_1 →+* ?m_2 : Type (max ? ?)

[Eric Wieser]

The elaborator is very bad when it comes to bundled homs with a domain that is itself a bundled hom, from what I recall

[Kevin Buzzard]

It used to work :-(

[Kevin Buzzard]

The error is now on eval₂_comp_left on line 748.

[Kevin Buzzard]

refine eq.trans (eval₂_comp_left (map g) (C.comp f) X p) _, in tactic mode works where line 748 in the link above used to fail. rw also fails, it's not often I use eq.trans! What is going on here?

[Kevin Buzzard]

I think this is the heart of the problem for the next error:

type mismatch at application
  (eval₂_hom ?m_5 g).comp f
term
  f
has type
  @ring_hom ?m_1 (@mv_polynomial σ ?m_2 (@comm_semiring.to_semiring ?m_2 ?m_3)) (@comm_semiring.to_semiring ?m_1 ?m_4)
    (@comm_semiring.to_semiring (@mv_polynomial σ ?m_2 (@comm_semiring.to_semiring ?m_2 ?m_3)) ?m_5) : Type (max
        ?
        u_1
        ?)
but is expected to have type
  @ring_hom ?m_1 (@mv_polynomial σ ?m_2 (@comm_semiring.to_semiring ?m_2 ?m_3)) (@comm_semiring.to_semiring ?m_1 ?m_4)
    (@mv_polynomial.semiring ?m_2 σ (@comm_semiring.to_semiring ?m_2 ?m_3)) : Type (max ? u_1 ?)

[Eric Wieser]

I'm having exterior_algebra flashbacks

[Eric Wieser]

Is something irreducible?

[Kevin Buzzard]

The PR literally just changes [comm_semiring] to [semiring] in the definition of mv_polynomial and adds an instance

 instance [semiring R]: semiring (mv_polynomial σ R) := add_monoid_algebra.semiring

and that's it

[Eric Wieser]

Yeah, but that might be enough to make an existing irreducible change from not a problem to very much a problem

[Eric Wieser]

I ran into some very similar looking problems when I weakened direct_sum from requiring add_comm_group to add_comm_monoid

[Eric Wieser]

Which were only really resolved by doing the weakening in even more places

[Julian Külshammer]

Thanks for looking into this. Note that changing [comm_semiring] to [semiring] didn't break anything yet, only the new instance did.

[Kevin Buzzard]

OK I managed to fix everything and I pushed, but goodness knows what other trouble we'll run into.

[Julian Külshammer]

Thanks a lot I'll continue working on it tomorrow.

[Kevin Buzzard]

If R is a comm_semiring, then we have two routes to semiring (mv_polynomial S R), one via "R is a semiring and hence mv polys are a semiring", and one via "mv_polynomials are a comm_semiring and hence a semiring". Are these defeq? If not then this is a problem.

[Kevin Buzzard]

This issue no doubt shows up all over the place -- some random algebraic functor will send commutative X's to commutative X's and general X's to X's and there will be a corresponding diamond. Is it always defeq in mathlib? What happens when it isn't?

[Kevin Buzzard]

It just occurred to me that perhaps another solution is to decrease the priority of the semiring -> mv_poly semiring instance.

[Kevin Buzzard]

Hmm, they do seem to be defeq in this case. I don't understand why I have to add the type ascriptions. I don't really understand what Eric was saying, but I'm sure he knows more about this than me. The type mismatch error above seems to be a red herring, I don't know why that wasn't unifying.

[Kevin Buzzard]

@Julian Külshammer My commit fixed the erorrs in the file but made the code worse (I added a bunch of type ascriptions). Another fix is to replace your instance [semiring R]: semiring (mv_polynomial σ R) := add_monoid_algebra.semiring with

def foo [semiring R]: semiring (mv_polynomial σ R) := add_monoid_algebra.semiring
attribute [instance, priority 90] foo

[Kevin Buzzard]

I see that there are errors in other files after my type ascription fix so I think the correct / easiest thing to do is to just add the instance at a lower priority. I have no feeling about the problems this will cause elsewhere.

[Julian Külshammer]

@Kevin Buzzard I managed to break it again by moving the definition of the semiring homomorphism C to the semiring section. The proof fails at the same places which you fixed earlier and then reverted, e.g. eval\2_eta. I pushed to show what is happening. This only happened when moving the definitions of monomial and C, i.e. ll. 117--128.

[Julian Külshammer]

I made some progress, at the moment I can see two similar problems to what we had before in ring_theory.polynomial.basic and two deterministic timeouts in ring_theory.polynomial.homogeneous. I'm still curious what the problem is here if anyone has some more insight.