coe Subgroup (Units F)

Stream: lean4

[Bolton Bailey]

This code was produced from working Lean 3 code, but in Lean 4 theres an error

import Mathlib.Data.Polynomial.FieldDivision
import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Subgroup.Finite
import Mathlib.Data.Polynomial.Eval
import Mathlib.GroupTheory.OrderOfElement

open scoped Classical

variable {k : Type} [Field k] [Fintype k]

noncomputable def vanishingPoly (G : Subgroup (Units k)) : Polynomial k :=
  Polynomial.monomial (Fintype.card G) 1 - Polynomial.C 1

theorem vanish_poly_for_subgroup_elem (G : Subgroup (Units k)) (g : G) :
    (vanishingPoly G).eval (g) = 0 :=
  by sorry

The issue is that it's not coercing the g to k. Can I do this somehow without having to write .val.val?

[Ruben Van de Velde]

((g : k\^x) : k)?

[Bolton Bailey]

Well yes, but without that either. It was one character before, can I just import something to get it to recognize it can coerce this?

[Kevin Buzzard]

Coercions have totally changed in lean 4. Maybe you can add the appropriate coercion? I would tell you what this is but I don't understand the new system.

[Bolton Bailey]

This thread has gotten me thinking about my old pain points more and so I have been looking over my old issues, and this one was the one where I took the most extensive personal notes. For those who don't want to enter the Lean4 playground, there are two error messages emitted by the above declaration:

failed to synthesize instance
  Semiring ↥G

and

application type mismatch
  Polynomial.eval g (vanishingPoly G)
argument
  vanishingPoly G
has type
  Polynomial k : Type
but is expected to have type
  Polynomial { x // x ∈ G } : Type

Here are my notes:

The problem essentially boils down to the fact that g in the definition has not been cast to a field element and needs to be.

In the first error, Lean complains that it doesn't know how to derive that {x // x \in G} is a Semiring. This is already confusing for two reasons: Firstly, it is not clear where in the definition {x // x \in G} even comes up (the answer is that since G is a structure rather than itself a Type, g is technically not of type G but of type coe_sort G or ↥G in lean 3 notation, which seems to be represented as {x // x \in G} here). Secondly, it is not clear why we need to derive Semiring on it.

The second error is also confusing. It claims that vanishingPoly G is expected to have a type Polynomial { x // x ∈ G } but doesn't explain why it is expected to have this type. The reason is that because g is of type G, the eval function infers that it is working on a polynomial over G, and then decides that vanishingPoly G should be a polynomial over G. It is only once we realize this that we see that both errors have the same root cause: we need to derive semiring on G because we think we are supposed to make a polynomial over it and types that we have polynomials over are supposed to be semirings. We mismatch the type because vanishingPoly G is not a polynomial over G but over k.

Still unclear is why the type inference system decided that G was the right type in the first place. Shouldn't it have looked at the first argument vanishingPoly G and seen that the polynomial was over k and complained about the g argument not having the right type instead? The trouble is, despite appearances, vanishingPoly G is not the first explicit argument to eval. The definition of eval is:

/-- `eval x p` is the evaluation of the polynomial `p` at `x` -/
def eval : R → R[X] → R :=
  eval₂ (RingHom.id _)

What the heck? If your docstring describes the operation you are performing as "evaluation of the polynomial p at x" shouldn't that tell you that the more natural definition of this function is to permute the arguments and give it the type R[X] → R → R. This would leave the first argument as the polynomial and respect the dot notation convention that the value before a dotted function is the first argument to it.

Unfortunately, this was not done for Polynomial.eval - I believe the reason is that we wanted to have the map Polynomial.eval x be linear, as this is useful for some other definitions.

Leaving this aside, could we not have been more intelligent about the inference? Maybe we could have seen that respecting the polynomial argument's type would have led to fewer errors? Unfortunately probably not without a more expensive typechecker.

At the very least it seems like what would have been helpful here was:

1. Putting the type ascription error first: If your types are not even right, why are we trying to synthesize instances for them at all? (Counterpoint: There is nothing wrong, prior to typeclass inference, with the types on the partially-applied function eval g, it's only after the second application that the second error arises. This is why the order of arguments on eval makes this so devilish)
2. More information about why the type ascription happened. Something like:

application type mismatch
  Polynomial.eval g (vanishingPoly G)
the second explicit argument
  vanishingPoly G
has type
  Polynomial k : Type
but is expected to have type
  Polynomial { x // x ∈ G } : Type
because the first implicit argument to Polynomial.eval has been inferred as
  { x // x ∈ G } : Type
from the context of the first explicit argument
  g
having type
  { x // x ∈ G }

If this error message is too big then perhaps we could have a dropdown menu for people to click listing the chain of type inferences that led to the current type mismatch error.

[Bolton Bailey]

What do people think? Does it make sense to suppress typeclass inference errors when type mismatch errors occur nearby? Are either of these solutions even feasible with lean4's current error system?