Weird error message

Stream: new members

[Katherine Cordwell]

I'm trying to use nat.prime.coprime_iff_not_dvd, which has signature nat.prime.coprime_iff_not_dvd : nat.prime ?M_1 → (nat.coprime ?M_1 ?M_2 ↔ ¬?M_1 ∣ ?M_2). But when I try to call it, I get an "maximum class-instance resolution depth has been reached" error, and I have no idea why.

[Patrick Massot]

We need more context

[Patrick Massot]

Could you try to get a minimized version of your code, still showing the error, but not much more?

[Katherine Cordwell]

I have p and q that are nats and I write
"have iffconc: nat.prime p → (nat.coprime p q ↔ ¬ p | q), from apply nat.prime.coprime_iff_not_dvd,"
which is the line that gives the error message.

[Kenny Lau]

maybe your p and q are integers

[Katherine Cordwell]

The context says "p q : ℕ", so I don't think so?

[Patrick Massot]

You may have the wrong vertical bar

[Kenny Lau]

right, make sure that it is \|

[Kenny Lau]

which results in a different bar than |

[Katherine Cordwell]

Oh great, that fixed it! Thanks so much

[Patrick Massot]

also, from apply doesn't mean anything

[Patrick Massot]

No problem. Welcome to Lean Zulip!

[Rob Lewis]

The vertical bar thing drives me nuts. I've been using this notation for years and I still mix the two up periodically. It never sticks in my brain.

[Travis Hance]

to tack onto this question, what exactly does the "maximum class-instance resolution depth has been reached" error message mean, in general? Every time I see it I know it just means I have a type error somewhere but the error never helps me find it and part of that is because I don't know what it means.

[Patrick Massot]

Do you know the basics of the type class system?

[Kevin Buzzard]

What it actually means is that Lean was trying to solve a typeclass problem, and it failed because it gave up

[Kevin Buzzard]

because things weren't looking good

[Kevin Buzzard]

What is misleading about the message is that sometimes Lean is trying to solve a completely random problem which you had no intention of making it solve; that's what was happening above.

[Kevin Buzzard]

The real error was some subtle syntax error (| instead of \|) and Lean got completely confused; the error message was ultimately irrelevant.

[Kenny Lau]

yeah Lean can work on its error messages

[Kevin Buzzard]

The | indicates the end of something, so Lean was faced with ¬ p with p : nat

[Kenny Lau]

but again, [insert saying about how it's easy to complain]

[Simon Hudon]

If you had to choose three error messages that you want to be more informative, which ones would it be?

[Patrick Massot]

Error message craft is highly non-trivial. In this case I would say that maximal depth error message would be much easier if it included an indication of what type class problem it failed to solve

[Patrick Massot]

That one would certainly be in my top 3

[Kevin Buzzard]

import data.nat.prime

example (p : ℕ) : ¬ p := sorry
/-
maximum class-instance resolution depth has been reached yada yada
-/

[Kevin Buzzard]

-- import data.nat.prime

example (p : ℕ) : ¬ p := sorry
/-
type mismatch at application
  ¬p
term
  p
has type
  ℕ
but is expected to have type
  Prop
-/

[Simon Hudon]

Excellent. How would you feel about a sort of introductory paragraph (or link to one) about type class search, instance problem and the main candidates tried?

[Kevin Buzzard]

So it's the import which causes it, on this occasion. Of course, the input is garbage

[Kevin Buzzard]

Whenever I see it I assume it's user error (i.e. my fault) rather than Lean actually failing to do type class inference

[Simon Hudon]

@Patrick Massot It might be worth opening an issue to start pitching specific improvements

[Patrick Massot]

Simon, I don't understand. Do you mean you want a link in the error message?

[Patrick Massot]

opening an issue where?

[Patrick Massot]

In the community fork?

[Kevin Buzzard]

@Travis Hance the answer to your question is that there's a thing called typeclass inference, which is invoked whenever you leave out an input to a function but the input is in [] square brackets. Lean invokes an algorithm called the type class inference algorithm, which searches through a database trying to find the term you didn't supply explicitly. If the algorithm is called accidentally then of course it can fail -- the unhelpful error message just means "you called typeclass inference and it didn't work"

[Simon Hudon]

@Patrick Massot yes community fork. And the link I'm talking about is like Rust errors: https://doc.rust-lang.org/edition-guide/rust-2018/the-compiler/improved-error-messages.html

[Simon Hudon]

When you have an error in Rust, it gives you a rule number and if you query the compiler about that rule it explains why it's there.

[Rob Lewis]

Printing the failing problem would be nice. But a lot of time time, the question isn't really which problem it failed to solve, it's why the search went deep before failing.

[Kevin Buzzard]

In this case Lean saw ¬ p and thought "hmm, p is a natural and it's supposed to be a proposition, that must mean that there is a coercion from naturals to propositions, I'll pass that over to the type class inference system because that handles coercions, and I'll leave it looking for a natural map from natural numbers to true/false statements". Lean fails to find that natural map, because nobody told Lean such a map, but unfortuately along the way it gets very keen on the idea of using canonically_ordered_comm_semiring in some way, and ends up in an infinite loop.

[Rob Lewis]

In Kevin's example, the culprit is with_top.canonically_ordered_comm_semiring looping for some reason.

[Kevin Buzzard]

The garbage out is because of the garbage input -- trying to coerce a natural to a proposition.

[Kevin Buzzard]

instance [canonically_ordered_comm_semiring α] [decidable_eq α] :
  canonically_ordered_comm_semiring (with_top α) := ...

in ordered_ring, which for some reason is being imported by data.nat.prime

[Patrick Massot]

Oh my God. When I read Kevin's message I thought it was a joke, because we suffered of lot with with_zero and ordered commutative monoids in the perfectoid project. But it seems with_top.canonically_ordered_comm_semiring is indeed involved here

[Patrick Massot]

Printing the failing problem would be nice. But a lot of time time, the question isn't really which problem it failed to solve, it's why the search went deep before failing.

I think what you ask is complicated. Displaying the failing problem would already be immensely useful

[Patrick Massot]

for instance, you could see immediately that Lean went looking for a coercion from nat to Prop in that case

[Simon Hudon]

I agree, that would be a good start

[Kevin Buzzard]

data.nat.basic imports algebra.ordered_ring which contains the offending instance.

[Simon Hudon]

Is that in mathlib? Is it universally problematic?

[Kevin Buzzard]

Yes this is all mathlib

[Patrick Massot]

It doesn't sound quite right that basics of natural numbers involves canonically ordered commutative semi-ring. That must be my mathematician bad habits...

[Kevin Buzzard]

it's OK, I don't think data.nat.basic is used very much

[Kevin Buzzard]

sounds pretty obscure to me

[Kevin Buzzard]

to be honest I am extremely surprised I didn't see this loop earlier

[Kevin Buzzard]

If you had to choose three error messages that you want to be more informative, which ones would it be?

deterministic timeout was my #1 choice last week when we were in perfectoid hell

[Kevin Buzzard]

It should have said "just change that Type* to Type u and I'll stop complaining"

[Rob Lewis]

I think what you ask is complicated. Displaying the failing problem would already be immensely useful

Oh, of course. "Why the search went deep" doesn't really have a well-defined answer. Printing the failing target is helpful when you accidentally invoke type class problems, and it's simple enough to do. But in that situation, you often don't want type class inference to time out, you want it to fail fast. It would be better to see a standard type checking error there than any kind of type class message.

[Kevin Buzzard]

Without the import you get the standard typechecking error, as you know

[Rob Lewis]

Right. That instance is worrying. It seems like there are too many metavariables for it to be applied here, so I'm not sure exactly why it's looping.

[Rob Lewis]

But it's late, I'm exhausted, not gonna investigate now.

[Patrick Massot]

Have a good night! (I should go to bed too)

[Mario Carneiro]

There is nothing wrong with that instance as written. I assume it is trying to solve a canonically_ordered_comm_semiring ? kind of problem?

[Mario Carneiro]

Here's an abbreviated trace:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_3 : has_coe_to_sort ℕ := @coe_sort_trans ?x_5 ?x_6 ?x_7 ?x_8
[class_instances] (1) ?x_7 : has_coe_t_aux ℕ ?x_6 := @coe_base_aux ?x_9 ?x_10 ?x_11
[class_instances] (2) ?x_11 : has_coe ℕ ?x_10 := @nat.cast_coe ?x_14 ?x_15 ?x_16 ?x_17
[class_instances] (3) ?x_16 : has_one (with_zero ?x_18) := @with_zero.has_one ?x_24 ?x_25
[class_instances] (4) ?x_25 : has_one ?x_24 := @with_top.has_one ?x_26 ?x_27 ?x_28
[class_instances] (5) ?x_27 : canonically_ordered_comm_semiring ?x_26 := @with_top.canonically_ordered_comm_semiring ?x_29 ?x_30 ?x_31 ?x_32 ?x_33
[class_instances] (6) ?x_30 : canonically_ordered_comm_semiring ?x_29 := @with_top.canonically_ordered_comm_semiring ?x_34 ?x_35 ?x_36 ?x_37 ?x_38
...

The problem is a confusion of whether typeclass parameters are supposed to be input or output parameters. The canonically_ordered_comm_semiring instance assumes it will only ever be called on a concrete type, so the metavariable indicates the problem lies elsewhere. Similarly, with_zero.has_one assumes it is being called on a concrete type. So we must conclude that for nat.cast_coe to work correctly, it must only be called on concrete types. But that's not how the coe instances work, in particular coe_sort_trans:

instance coe_sort_trans {a : Sort u₁} {b : Sort u₂} [has_coe_t_aux a b] [has_coe_to_sort.{u₂ u₃} b] : has_coe_to_sort.{u₁ u₃} a

This is an instance which invents b from nothing, as a metavariable. It solves has_coe_to_sort a by trying to solve has_coe_t_aux a ?b (which quickly boils down to solving has_coe a ?b) and then if that is successful it looks for has_coe_to_sort b. This kind of forward searching doesn't work with the mathlib instances, since you can't enumerate all the types which have coercions from nat (there are infinitely many). In fact due to the DFS search order it never gets around to checking any of them and instead builds infinitely large instances and overflows.

[Floris van Doorn]

It would be nice if type class inference stops when its argument is a metavariable (note: I'm not saying it should stop when its argument contains a metavariable), so that nat.cast_coe would just fail, because the type class inference gives up once it has to find an instance of has_one ?x. If we ever rely on type class inference continuing in these cases, we should just provide more information.

[Mario Carneiro]

We could have a marker in_param that says "this argument must be a concrete type for this to trigger", or at least it shouldn't instantiate a metavariable in this slot. Better yet, it seems like this should be the default behavior for anything other than out_param

[Mario Carneiro]

In this case, that means that canonically_ordered_comm_semiring ?x_26 := @with_top.canonically_ordered_comm_semiring would not unify, because the metavar ?x_26 is treated as a constant

[Mario Carneiro]

Of course this sort of defeats the purpose of using a metavariable to begin with, but like I said, has_coe seems confused about whether its inputs are outputs or not

[Mario Carneiro]

coe_sort_trans seems like a very suspicious instance

[Katherine Cordwell]

Still on the thread of weird error messages, why might Lean be giving me an "unexpected end of comment block" error on a blank line?

[Katherine Cordwell]

Hmm never mind I solved it--an earlier comment was causing problems and the error message just manifested on an unrelated line.

[Mario Carneiro]

the location of this error could be improved (logically it should go on the comment open token, or the entire unclosed comment region)

[Katherine Cordwell]

Mostly what threw me off was that there were several (correct) theorems between the problematic comment and the error message.

[Kevin Buzzard]

Error messages are not the best in Lean 3. I remember realising how much better I had become at fixing up my own code when I had started getting the hang of working out what they were actually telling me. Another tip: don't try and debug the third error message -- the problem might be the unintended chaos caused by the first one.

[Mario Carneiro]

That's generally true in any programming language, I think. Compilers try their best to recover from an error but it's rarely successful