Improve type error explanation for partially applied functor

[art-w]

I found the error message for partially applied functors to be confusing when the argument doesn't type check:

module type A = sig type a val missing : a end
module type B = sig type b end

module Make (A : A) (B : B) = struct end

module A_impl = struct type a = unit end

module Partial = Make (A_impl)
(*               ^^^^^^^^^^^^^
Error: The functor application is ill-typed.
       These arguments:
         A_impl
       do not match these parameters:
         functor (A : A) (B : B) -> ...
       1. An argument appears to be missing with module type A
       2. Modules do not match:
            A_impl : sig type a = unit end
          is not included in
            B
*)

It looks like some magic is happening to guess which functor parameter is missing, but when there are no good choices it introduces the missing arguments on the left rather than the right, leading to an unexpected error message (... assuming the partial application was otherwise correct)

module Partial = Make (<missing> : A) (A_impl : B)  (* current error *)

(* I expected the error to keep [A_impl] as the first parameter,
   optionally mentioning that the second argument [B] is missing *)
module Partial = Make (A_impl)
(*               ^^^^^^^^^^^^^
Error: The functor application is ill-typed.
       These arguments:
         A_impl
       do not match these parameters:
         functor (A : A) (B : B) -> ...
       1. Modules do not match:
            A_impl : sig type a = unit end
          is not included in
            A
          The value `missing' is required but not provided
       2. An argument appears to be missing with module type B
*)

(Obviously low priority considering the rarity of partially applied functors!)

[gasche]

@Octachron I'm not fond of #12988 as a proposed fix to this issue. My understanding is that when there are several choices that are just as good (from the algorithm's perspective), you tweaked the heuristic on which one to choose to make this specific example work better, at the cost of a degradation in other examples.

My three cents:

1. If there are several optimal edit paths that look very different, should we consider not showing any of them, instead of showing one of them? (maybe sometimes they share a common prefix that they agree on, and we could still show something?) This gets rid of the "some magic is happening to guess one option" feeling that I agree is disturbing.
2. Here my internal algorithm tells me that A_impl is closer to A than to B, so I know that the two edit paths are not equivalent. Could we integrate such metrics in our distance computation? (For example: count the number the disagreeing items as part of the distance between two signatures. Or maybe the proportion of disagreeing items.)
3. @art-w, you are one of the best people around to look at this and have good advice.

[Octachron]

The diffing algorithm is heuristic by nature.
To keep the algorithm efficient we must cut branches early rather than storing all possible possible paths.

Having a finer grained measure of change distance is definitively part on my plans, but our current weight are already underspecified.

Typically, the more principled version of my change would be to make weight dependent on the position in the diffing matrix: the rule for the functor application will be that inserting missing argument is cheaper near end corner of the matrix. But this introduces even more parameters to choose compared to hard-wiring a prefer for path ending with insertion amongst the path with same weight.

[art-w]

I actually like @Octachron fix! Even with a more fancy algorithm that would weight the similarity of the parameters with the expected interfaces, I expect that it would be necessary to break ties in favor of the application order as it produces the least surprising error message (defaulting to "no magic").