Incorrect conflict explanation for type error messages

[trefis]

The following test:

#!/bin/bash

before=$(pwd)
tmp=$(mktemp -d)

ocamlc=ocamlc

cd $tmp

echo >foo.mli "type t = int"
cat  >bar.mli <<EOF
type t = int
val f: int -> t -> int
EOF

$ocamlc -c foo.mli
$ocamlc -c bar.mli

cat >bar.ml <<EOF
include Foo
let f (_ : float) (_ : t) = 3
include Foo
EOF

$ocamlc -c bar.ml

cd $before

rm -r $tmp

Gives the following error on 4.13:

File "bar.ml", line 1:
Error: The implementation bar.ml does not match the interface bar.cmi: 
       Values do not match:
         val f : float -> t/2 -> int
       is not included in
         val f : int -> t/1 -> int
       File "bar.mli", line 2, characters 0-22: Expected declaration
       File "bar.ml", line 2, characters 4-5: Actual declaration
       File "foo.mli", line 1, characters 0-12:
         Definition of type t/1
       File "foo.mli", line 1, characters 0-12:
         Definition of type t/2

which I find misleading.

On 4.14, it prints:

File "bar.ml", line 1:
Error: The implementation bar.ml does not match the interface bar.cmi: 
       Values do not match:
         val f : float -> t/2 -> int
       is not included in
         val f : int -> t/1 -> int
       The type float -> t/2 -> int is not compatible with the type
         int -> t/1 -> int
       Type float is not compatible with type int 
       File "foo.mli", line 1, characters 0-12:
         Definition of type t/1
       File "foo.mli", line 1, characters 0-12:
         Definition of type t/2
       File "bar.mli", line 2, characters 0-22: Expected declaration
       File "bar.ml", line 2, characters 4-5: Actual declaration

which is undeniably better (and I would guess a result of #10407 ).

This was reported by @dinosaure after spending hours trying to fix:

File "src/mirage/mirage.ml", line 1:
Error: The implementation src/mirage/mirage.pp.ml
       does not match the interface src/mirage/.dream__mirage.objs/byte/dream__mirage__Mirage.cmi:
        ... ... ... ... In module Make:
       Values do not match:
         val https :
           ?stop:Lwt_switch.t ->
           port:int ->
           ?prefix:string ->
           stack ->
           ?cfg:Tls.Config.server ->
           ?error_handler:error_handler -> handler/1 -> unit Lwt.t
       is not included in
         val https :
           ?stop:Lwt_switch.t ->
           port:int ->
           ?prefix:string ->
           Stack.t ->
           ?cfg:Tls.Config.server ->
           ?error_handler:error_handler -> handler/2 -> unit Lwt.t
       File "src/mirage/mirage.mli", lines 185-193, characters 2-17:
         Expected declaration
       File "src/mirage/mirage.ml", line 202, characters 6-11:
         Actual declaration
       File "src/pure/inmost.ml", line 138, characters 0-40:
         Definition of type handler/1
       File "src/pure/inmost.ml", line 138, characters 0-40:
         Definition of type handler/2

(where it's somewhat harder to notice that the compiler points you in the wrong direction).

[Drup]

Are you saying you want ... diffs for arrow types errors ? :D

[Octachron]

I think that the issue at hand is the conflict explanation that points twice to the exact same location which is not exactly helpful.

[trefis]

I think that the issue at hand is the conflict explanation that points twice to the exact same location which is not exactly helpful.

Indeed, if you look at the location it becomes obvious that the issue is not with handler, even though the error message with its /1 and /2 seems to hint that it is.

[Octachron]

A simple solution in this specific case would be to not differentiate identifiers which points to a declaration with the same uid.
Otherwise, a more precise option would be to compute normalized path for each identifiers before differentiating them (which would be quite similar to activating -short-paths for colliding identifiers).

[gasche]

Two remarks:

• if two identifiers are equivalent, then indeed we should try not to explain why they are different, because they are not (we could normalize before diffing or, possibly more natural, check inequivalence during diffing)
• a clearer display of which elements don't match in an arrow type would indeed help; this can be done by diffing, Arthur Charguéraud also had specific user-interface proposals in Improving Type Error Messages in OCaml , 2015 (Section 2, pages 3-8) using a tabular presentation.

[github-actions]

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.