Type mismatch `Iff.rfl` in instance defintion

Stream: lean4

[Bolton Bailey]

I am trying to define an alternative structure for Polynomials that can be more easily computed with. When I get to proving that this type is a CommSemiring it gives me an error, saying there is a type mismatch on Iff.rfl. But I don't see how I am using that lemma. How can I avoid this error?

import Std.Data.Rat.Basic
import Std.Data.List.Basic
import Mathlib.Algebra.Ring.Defs
import Mathlib.Data.Finset.Basic
import Mathlib.Probability.Distributions.Uniform


def List.matchLength (a : List α) (b : List α) (unit : α) : List α × List α :=
  if a.length < b.length then
    (a ++ .replicate (b.length - a.length) unit, b)
  else
    (a, b ++ .replicate (a.length - b.length) unit)

section Polynomial

/-- A type analogous to `Polynomial` that supports computable operations. This polynomial is represented internally as a list of coefficients. For example the list `[1,2,3]` represents the polynomial `1 + 2x + 3x^2`.
 -/
def Polynomial' (R : Type) [Semiring R] := List R

def Polynomial'.mk {R : Type} [Semiring R] (l : List R) : Polynomial' R := l

def Polynomial'.toList {R : Type} [Semiring R] (p : Polynomial' R) : List R := p

/-- Evaluates a polynomial at a given value. -/
def Polynomial'.eval {R : Type} [Semiring R] (r : R) (p : Polynomial' R) : R :=
  (p.enum.map (fun ⟨i, a⟩ => a * r ^ i)).sum

def Polynomial'.C {R : Type} [Semiring R] (r : R) : Polynomial' R := [r]

def Polynomial'.X {R : Type} [Semiring R] : Polynomial' R := [0, 1]

def Polynomial'.add {R : Type} [Semiring R] (p q : Polynomial' R) : Polynomial' R :=
  let ⟨p', q'⟩ := List.matchLength p q 0
  List.zipWith (· + ·) p' q'

def Polynomial'.smul {R : Type} [Semiring R] (r : R) (p : Polynomial' R) : Polynomial' R :=
  List.map (fun a => r * a) p

def Polynomial'.mul {R : Type} [Semiring R] (p q : Polynomial' R) : Polynomial' R :=
  (p.enum).foldl (fun a ⟨n, b⟩ => a.add (Polynomial'.mk (((List.replicate n (0 : R))) ++ (Polynomial'.smul b q).toList))) []

def Polynomial'.neg {R : Type} [Ring R] (p : Polynomial' R) : Polynomial' R := List.map (· * -1) p

def Polynomial'.sub {R : Type} [Ring R] (p q : Polynomial' R) : Polynomial' R := p.add q.neg

def Polynomial'.pow {R : Type} [Semiring R] (p : Polynomial' R) (n : Nat) : Polynomial' R := List.foldl (fun a b => a.mul p) (Polynomial'.C 1) (List.replicate n p)

instance {R : Type} [Semiring R] : Zero (Polynomial' R) := ⟨[]⟩
instance {R : Type} [Semiring R] : One (Polynomial' R) := ⟨Polynomial'.C 1⟩
instance {R : Type} [Semiring R] : Add (Polynomial' R) := ⟨Polynomial'.add⟩
instance {R : Type} [Semiring R] : Mul (Polynomial' R) := ⟨Polynomial'.mul⟩
instance {R : Type} [Ring R] : Neg (Polynomial' R) := ⟨Polynomial'.neg⟩
instance {R : Type} [Ring R] : Sub (Polynomial' R) := ⟨Polynomial'.sub⟩
instance {R : Type} [Semiring R] : Pow (Polynomial' R) Nat := ⟨Polynomial'.pow⟩
instance (R : Type) [Semiring R] : Inhabited (Polynomial' R) := ⟨[]⟩


instance (R : Type) [CommSemiring R] : CommSemiring (Polynomial' R)
  where -- Why is it complaining about Iff? thats not even present here.
    add := Polynomial'.add
    add_assoc := sorry
    zero := Polynomial'.C 0
    zero_add := sorry
    add_zero := sorry
    nsmul n p := _
    add_comm := sorry
    mul := Polynomial'.mul
    left_distrib := sorry
    right_distrib := sorry
    zero_mul := sorry
    mul_zero := sorry
    mul_assoc := sorry
    one := Polynomial'.C 1
    one_mul := sorry
    mul_one := sorry
    mul_comm := sorry

[Eric Wieser]

The complaint is coming from a default value for a field you did not specify

[Eric Wieser]

I think there is a tracking issue about making this possible to guess from the error message

[Bolton Bailey]

See here for me finding a similar error in an instance I was writing, I do not understand how I can get an error that says "unknown declaration" immediately under that exact declaration.

[Bolton Bailey]

Eric Wieser said:

I think there is a tracking issue about making this possible to guess from the error message

I would be happy to upvote this if you can link it to me.

[Michael Stoll]

Is this lean4#2950 ?