error messages: conflict explanations as a footnote

[Octachron]

This PR proposes to make the name conflicts part of error messages

Line 5, characters 4-74:
  Definition of class type "a"
Line 2, characters 2-36:
  Definition of class type "a/2"

an explicit footnote, by adding a footnote field in the error report type.

This has three advantages from my point of view:

• First, it makes it clearer than the name conflict explanation is semantically not part of the main error messages nor any of the error submessages. And when we switch to structured output, it will make it easier for external tools to isolate this part of the error message (and display it as a footnote?).

• Second, this makes it easier to handle the name conflicts global state. With this changes, we are by construction checking the existence of name conflicts once, when producing the final error report. This removes the temptation to print name conflict explanations at intermediary points (which is currently done for first class modules and functors).

• Third, the new behavior is easier to reproduce while removing global states from the error message printing machinery.
  (I have upcoming PR that makes this point clearer, but I thought that this change stand on its own).

[gasche]

I'm nervous about the proposed design:

• (minor) I wonder why you are not using delayed_msg defined below as the field type
• (minor) the msg type carries a location, by consistency I would expect the delayed_msg also to locate each footnote. (So: a list of footnotes with each a location, I guess?)
• you conflate "footnote", which I understand as "less important information, collected on the side", with "delayed printing"
• I understand that you want to delay printing of the delayed-message until a complete report is generated, but currently you delay it until the report is printed, and I don't see why this is necessary.

My impression is that the thunk could be applied at the moment where the report value is constructed -- in practice this happens in the Location.errorf function -- so that the field type here does not have the unit -> part anymore. I don't know if this would be a big improvement, but the design would still feel a bit more principled to me. (It depends on whether you think of the report as a piece of data, or merely as an API for the errorf functions.)

[Octachron]

I agree that that the design is weird. What happens is that currently, the printing of the error message is effectful and it might generate new footnotes. Thus we need to delay the computation of the footnote until after the printing of the main and suberror messages.

And this design is in fact less weird than the current one, where we might access multiple time to the list of conflicts at printing time and ends up with a printed error message which depends on the evaluation strategy of multiply nested Format.formatter -> unit closures.

My plan is to make this weirdness disappears in the next PR which makes the printing of error-message non-effectful without sacrificing formatting.

(minor) the msg type carries a location, by consistency I would expect the delayed_msg also to locate each footnote. (So: a list of footnotes with each a location, I guess?)

Having a list of footnote with optional locations would be an improvement to the existing error messages, but I will propose to do that later once we don't have anymore delayed footnote producers.

[gasche]

The argument as I understand it is: "it's a little weird now, but you can check that there is nothing deeply wrong, and trust me it will get better later". I trust you, and I could check. Approved.

(If someones feels tactfully discerning in a similar way, feel free to have a look at my own #13138. )