Refactor the code printing explanation for unification errors

[Armael]

This patches refactor explanation/has_explanation to avoid duplicating the pattern matches, the first time to check if there is an explanation, and the second time to actually get it. Instead, explanation now returns a (Format.formatter -> unit) option; in the Some case one can call the closure to compute and print the explanation.

[Octachron]

The changes look ok.

However, in term of refactoring, I would rather go one step further: define a concrete type for unification explanations, and split explanation into a find_explanation: … -> explanation option function and an associated printer pp_explanation: Format.formatter -> explanation -> unit.

[gasche]

See minor Changes comment, but otherwise the patch is fine and I approve of it.

Florian's proposal is reasonable but it also sounds like a lot more work (because the author of the patch would have to understand each explanation and painfully track its data dependencies). I will follow what @Armael thinks is best here, but I would be of the opinion that we could merge this now, and consider this major rewrite as a separate step.

[gasche]

The credits should be on their own line.

[Armael]

Indeed, @Octachron proposition means the explanation would be computed earlier (when checking if there is one), and one would have to check that this does not interferes with code that happens between the current has_explanation and explanation. All in all I'm in favor of just merging this now :-).

[gasche]

You may have done something unexpected while rebasing your branch to fix the Change entry because the current patchset shown by Github is not at all what I would expect.

[Armael]

Oops, sorry. Should be fixed now.

[gasche]

", review by Florian Angeletti and Gabriel Scherer"?

[Armael]

indeed, sorry. fixed.