Confusing error message: a scaling problem

Stream: lean4

[Kenny Lau]

From my personal experience, one of the biggest obstacles on the way to learning Lean is confusing error messages. For example, I have encountered:

Type mismatch
  IsScalarTower.of_algebraMap_eq'
has type
  @IsScalarTower ?m.3 ?m.4 ?m.5 Algebra.toSMul Algebra.toSMul
but is expected to have type
  @IsScalarTower R S A inst✝¹.toSMul inst✝

which is confusing, because (if you imagine the subterms are more complex in actual Mathlib usage) the types that mismatch clearly obviously match.

This is from a minimised example (see appendix 1). I have tried to minimise it more (appendix 2), but at a smaller scale the error message is actually helpful, where it says:

failed to synthesize
  Ring S

Now it's entirely possible that I have misdiagnosed the problem, and it might not actually be a scaling thing, but nevertheless one cannot deny that the first error message is confusing to beginners (and even to me, when I see this messge I can't know which instance failed to synthesize, so I have to check them one by one).

Thoughts?

[Kenny Lau]

Appendix 1:

class Algebra (R A : Type) extends SMul R A

class IsScalarTower (R S A : Type) [SMul R S] [SMul S A] : Prop

theorem IsScalarTower.of_algebraMap_eq' {R S A : Type}
    [Algebra R S] [Algebra S A] :
    IsScalarTower R S A := ⟨⟩

variable {R S A : Type}
variable [Algebra R S] [SMul S A]

theorem foo : IsScalarTower R S A :=
  IsScalarTower.of_algebraMap_eq' -- error

Appendix 2:

class Semiring (R : Type) : Type extends Mul R
class Ring (R : Type) extends Semiring R

instance : Semiring Nat where

theorem foo {R S : Type} [Ring R] [Ring S] (x : R) (y : S) :
    x = x ↔ y = y :=
  ⟨fun _ ↦ rfl, fun _ ↦ rfl⟩

variable {R S : Type} [Ring R] [Semiring S]
example (x : R) (y : S) : x = x ↔ y = y :=
  foo x y -- error

[Kenny Lau]

btw the actual error message I encountered inside mathlib doesn't have the @:
image.png

[Kenny Lau]

update: in this case actually after more diagnosis was that the two synthesised instances were not defeq. still I think Lean should point this out.

[Kenny Lau]

Thomas Preu said:

Over ℝ I'd like to inferre (-1) = 0 from (-1) ^ n = 0 in a proof by contradiction where n : ℕ. It seemed that eq_zero_of_zpow_eq_zero was the right theorem, however I get an error.
So I thought I should do a simple explicit example and tried

#eval eq_zero_of_zpow_eq_zero ((2 : ℝ) ^ (3 : ℤ) = (0 : ℝ) : Prop)

to get:

application type mismatch
  eq_zero_of_zpow_eq_zero (2 ^ 3 = 0)
argument
  2 ^ 3 = 0
has type
  Prop : Type
but is expected to have type
  ?m.46818 ^ ?m.46819 = 0 : Prop

What am I doing wrong?

[Kenny Lau]

another case of confusing error message

[Kevin Buzzard]

That error message explains exactly what the problem is. Is it confusing? Lean is a functional language, functions take inputs, inputs have types, the user has given an input of the wrong type and the error says exactly that.

What the user is probably confused by is not the error message, but the difference between the statement of a theorem, and the proof of a theorem. In Lean these are two different things and need to be carefully distinguished. docs#eq_zero_of_zpow_eq_zero wants to eat a proof that 2^3=0 (which has type 2^3=0) and it's been given the statement that 2^3=0 (which has type Prop).

[Kenny Lau]

oh, i didn't even notice that, my bad

[Ruben Van de Velde]

There were two issues in that message, one about pow vs zpow and the other one that was actually quoted

[Ruben Van de Velde]

I also stopped reading after seeing "zpow" and "\N"