Stream: Coq users

Topic: "Not truly a recursive fixpoint" error


view this post on Zulip Bolton Bailey (May 27 2022 at 00:37):

Hello, a beginner question here: I have the following mwe based loosely on the content here. The first definition is fine, but the second gives the error Not a truly recursive fixpoint. [non-recursive,fixpoints]coqtop. Why does it do this, and how can I correct my definition to get a length function?

Open Scope list_scope.

Section MySection.

Variables A : Type.

    Fixpoint myrepeat (n count : nat) : list nat :=
    match count with
    | O => nil
    | S count' => n :: (myrepeat n count')
    end.

    Fixpoint mylength (l:list A) : nat :=
    match l with
      | nil => O
      | h :: t => S (length t)
    end.

End MySection.

view this post on Zulip Paolo Giarrusso (May 27 2022 at 01:31):

Coq is telling you that mylength is not recursive. That’s because it calls length, while maybe you wanted to call mylength?

view this post on Zulip Ali Caglayan (May 27 2022 at 11:24):

Perhaps we could give a more informative warning that suggests some possible arguments you probably wanted to give.

view this post on Zulip Ali Caglayan (May 27 2022 at 11:25):

Something like: Expected "mylength" in "_ :: _" branch to be recursive or something

view this post on Zulip Théo Zimmermann (May 27 2022 at 12:39):

Sometimes the warning is raised in situations where students use Fixpoint when they should have used Definition. So maybe the warning should suggest the two options: "If you did not intend to write a recursive definition, then use Definition instead. If you intended to write a recursive definition, then maybe you are missing a recursive call."

view this post on Zulip Ana de Almeida Borges (May 27 2022 at 12:56):

Has there ever been any discussion on how helpful error messages should try to be? Ali and I tried to write a very descriptive error message for Print Notation and at some point it was basically repeating the refman and super long, so we ended up removing many of the prompts we had added (although it still includes some).

view this post on Zulip Ana de Almeida Borges (May 27 2022 at 12:57):

I notice that most error messages in Coq don't do this kind of thing, but is it a design decision or simply something to be improved?

view this post on Zulip Li-yao (May 27 2022 at 13:17):

There's a lot of room for improvement in Coq error messages.

view this post on Zulip Théo Zimmermann (May 27 2022 at 14:05):

I don't think this is a design choice. IMHO we should eventually aim at much better error messages, even if that makes them super long, but it will take a long time to improve all the existing ones.

view this post on Zulip Paolo Giarrusso (May 27 2022 at 14:26):

I'd assume current errors are not good because it's very hard to write good ones; but overly long messages can also be bad.

view this post on Zulip Paolo Giarrusso (May 27 2022 at 14:27):

And an error message is an bad medium to give the user a course about a feature — a tutorial is a better place.

view this post on Zulip Paolo Giarrusso (May 27 2022 at 14:28):

e.g., https://twitter.com/b0rk/status/954366146505052160/photo/1 does _not_ teach the user what a comparison or a generic argument is — because their teaching material does that.

another great Rust compiler error message! (this is a parsing error which makes it extra impressive to me) https://twitter.com/b0rk/status/954366146505052160/photo/1

- 🔎Julia Evans🔍 (@b0rk)

view this post on Zulip Paolo Giarrusso (May 27 2022 at 14:33):

OTOH, the manual suffers the same problem, and fixing that is hard. Other times, the real problem lies in the excess complexity of the underlying features.

view this post on Zulip Paolo Giarrusso (May 27 2022 at 14:34):

(For instance, the manual doesn't document well how cbn and simpl differ, but arguably many of those differences are bugs.)

view this post on Zulip Paolo Giarrusso (May 27 2022 at 15:01):

I think even just applying tips from https://www.cs.utexas.edu/~wcook/presentations/Writing.pdf would help a lot; the original book (https://www.amazon.com/Style-Clarity-Chicago-Editing-Publishing/dp/0226899152) helped me learn to write much more clearly, early in my PhD

view this post on Zulip Bolton Bailey (May 27 2022 at 16:28):

Paolo Giarrusso said:

Coq is telling you that mylength is not recursive. That’s because it calls length, while maybe you wanted to call mylength?

Ah, silly mistake on my part, thanks.

view this post on Zulip Alexander Gryzlov (Jun 07 2022 at 11:41):

I think a system for good error messages should be at least partially formalized, e.g., there should be some kind of "refutation calculus" or "incorrectness logic" that the system could use to mechanically separate and minimize problems


Last updated: Jan 29 2023 at 05:03 UTC