"Not truly a recursive fixpoint" error · Coq users

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.

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?

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.

Ali Caglayan (May 27 2022 at 11:25):

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

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."

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).

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?

Li-yao (May 27 2022 at 13:17):

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.

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.

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.

Paolo Giarrusso (May 27 2022 at 14:28):

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)

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.

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.)

Paolo Giarrusso (May 27 2022 at 15:01):

Bolton Bailey (May 27 2022 at 16:28):

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

Stream: Coq users

Topic: "Not truly a recursive fixpoint" error

Bolton Bailey (May 27 2022 at 00:37):