Zulip Chat Archive

Stream: general

Topic: universe issue when providing new instance


view this post on Zulip Julian Külshammer (Feb 28 2021 at 19:32):

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?

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:41):

Try adding an explicit type annotation to C?

view this post on Zulip Julian Külshammer (Feb 28 2021 at 19:46):

When it is defined or where it breaks?

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 19:48):

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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 19:48):

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

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:49):

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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 19:50):

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 ? ?)

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:54):

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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 19:56):

It used to work :-(

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 19:57):

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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 20:02):

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?

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 20:31):

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 ?)

view this post on Zulip Eric Wieser (Feb 28 2021 at 20:35):

I'm having exterior_algebra flashbacks

view this post on Zulip Eric Wieser (Feb 28 2021 at 20:35):

Is something irreducible?

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 20:38):

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

view this post on Zulip Eric Wieser (Feb 28 2021 at 20:39):

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

view this post on Zulip Eric Wieser (Feb 28 2021 at 20:40):

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

view this post on Zulip Eric Wieser (Feb 28 2021 at 20:40):

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

view this post on Zulip Julian Külshammer (Feb 28 2021 at 20:51):

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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 22:58):

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

view this post on Zulip Julian Külshammer (Feb 28 2021 at 23:00):

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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 23:01):

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.

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 23:02):

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?

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 23:09):

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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 23:14):

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.

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 23:18):

@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

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 23:21):

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.

view this post on Zulip Julian Külshammer (Mar 01 2021 at 08:27):

@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.

view this post on Zulip Julian Külshammer (Mar 01 2021 at 20:24):

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.


Last updated: May 16 2021 at 21:11 UTC