confusing error involving `.cmi` and `<here>`

[mimoo]

I'm getting the following error when building my project:

File "src/lib/crypto/kimchi_backend/common/bigint.ml", line 1:
Error: The implementation src/lib/crypto/kimchi_backend/common/bigint.pp.ml
       does not match the interface src/lib/crypto/kimchi_backend/common/.kimchi_backend_common.objs/byte/kimchi_backend_common__Bigint.cmi:
        ... The second module type is not included in the first ...
       At position module type Intf = <here>
       The value `of_hex' is required but not provided
       File "src/lib/crypto/kimchi_backend/common/bigint.ml", line 34, characters 10-35:
         Expected declaration

I'm a bit confused as to why there are .cmi files involved, and also what the <here> means here.

I think removing .cmi files from errors would be a great change : o

[gasche]

module type Intf = <here> means that the position that is meant in the error message is what corresponds to <here> in the real signature, that is, the definition of the module type Intf.

A .cmi is involved because the error comes from a mismatch between the implementation of a compilation unit and its interface. The implementation is typically defined in a file foo.ml and the interface in a file foo.mli, and in the present case their definitions do not match. The type-checker refers to the compiled interface file foo.cmi instead of the interface file foo.mli, because it is what it sees as its own abstraction level. (In general the compiler does not try to make guesses at how compiled files were produced, which could be fragile.)

[mimoo]

Thanks! I guessed as much but thought this was still vague enough that it was worthy of an issue o.o

Perhaps it should talk about foo.ml(i) if it knows for sure that this is where it came from? The presence of a .cmi really is weird imo and not very user friendly

perhaps

At position module type Intf = <here>
       The value `of_hex' is required but not provided

could become

6 |
7 | type Intf = ...
8 |             ^^^
       At this position the value `of_hex' is required but not provided

[Octachron]

The presence of a .cmi really is weird imo and not very user friendly

Why is the presence of a cmi file weirder than the presence of a mli file? The compiler reports from where it reads the interface. Typically, if the user provided both a mli and ml files in the command line invocation, the compiler will report the error using the mli file location. If the compiler read the interface from a cmi file, it seems better to report that fact rather than try to somehow reconstruct a history of this cmi file.

Concerning the error message itself, an important point to keep in mind is that this is a type error at the level of module types. Module type components don't necessarily have locations in the source file. Typically, replacing the error message for

module type t = sig
  type eq
  module F:
    sig
       module type r =sig type t = eq end
    end -> sig end
end

module M: sig
  module type s = t with type eq := int
end = struct
  module type u = t with type eq := float      
end

     ...
      At position module type r = <here>
      Type declarations do not match:
        type t = int
      is not included in
        type t = float
      The type t is not equal to the type float

by

6 |
7 |    module type u = t with type eq := float       
8 |                                  ^^^^^^^^^^^^^^^^^
      Type declarations do not match:
        type t = int
      is not included in
        type t = float
      The type t is not equal to the type float

would extremely unhelpful.

It could be interesting to track more precisely the location of the conflict (but this possibly not straightforward) but it might be more efficient to be more explicit about deep module type conflict at a certain path:

When comparing the module type component Intf

if it the <here> marker and the At position that was the source of the confusion.

In the past, it was hard to find a way to describe paths that scale to path within functor (in the second argument of the functor A.B.C in the fourth argument of the functor D.E.F ...). But nowadays, the functor error messages use the higher-level diffing errors for functor arguments, and thus we only have to find nice way to describe paths to modules and module types that goes at worse through functor body.

When comparing the module type Intf in the functor body of A.B.F in the module C.B.D in the functor body of A.G

[mimoo]

Why is the presence of a cmi file weirder than the presence of a mli file?

because the .cmi file does not let me know where the error is in my source tree, whereas an .mli file is present and I can check it.

it seems better to report that fact rather than try to somehow reconstruct a history of this cmi file

I'm not sure about the internals of the compiler, perhaps this is a limitation in which case that's fine, but if this is information that can potentially be passed around in an option then IMO it would be much clearer for users (in general you shouldn't have to know about compiler internals to understand an error and how to act on it)

[Octachron]

There are no compiler internals here, a cmi file is an explicit object that is explicitly consumed by the compiler CLI. It might be that cmi files are build system internals however.

Moreover, in general there is no one-to-one mapping between a mli file and a cmi file: a cmi file is a result of a compilation command and thus the same mli can produce many cmi files. The error might be not in your source tree but in the command that produced the cmi. Or the error could no longer be in the source tree because the state of the filesystem changed after the creation of the cmi file.

Consequently, it seems brittle to remove the information about the cmi from the error message. However, we could deprioritize it if we recorded the path of the mli file in the cmi.

What would you think of :

the interface src/lib/common/Bigint.mli (read from the compiled interface src/lib/crypto/kimchi_backend/common/.kimchi_backend_common.objs/byte/kimchi_backend_common__Bigint.cmi)

?

[lpw25]

I think we should avoid mentioning .cmi files. The error message is meant for consumption by the programmer, and the programmer does not know what a .cmi file is: the build systems very helpfully abstract such details away.

Your argument about the .cmi file potentially being stale or similar equally applies to all type error messages, but we're not about to have:

This expression has type int but was expected to have type 'a list because of .opam/4.14.0/lib/ocaml/stdlib__List.cmi

We report locations from .mli files stored in .cmi files all the time, and it seems reasonable to talk about the .mli file here too.

[Octachron]

Good point. I agree that from within a project or a source tree, the command line argument is implicitly part of the state of the source tree. It makes sense to report only the mli file and rely on this implicit context. This makes even more sense since other errors are already using the mli locations stored in the cmi.

[mimoo]

Consequently, it seems brittle to remove the information about the cmi from the error message. However, we could deprioritize it if we recorded the path of the mli file in the cmi.

can't we keep a global hashmap of cmi paths to their original mli files? And if you don't have that then print a message about a cmi if that's the best we can do. Sorry that's the best I have since I don't know about the internals :P

[Octachron]

See #12052 for a heuristic to retrieve a source file from a compiled interface .

[mimoo]

that was fast!

[github-actions[bot]]

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.

[shindere]

I have read both this issue and #12052. My understanding is that the reported problem has been acknowledged as being real and, at the same time, #12052 has been closed in favour of a not-yet implemented better solution.

On this basis, I am removing the Stale label from this issue so that it remains open.

[gasche]

We have a candidate PR for the better solution, #12654, but it needs more work to be mergeable. (The original author, an external contributor, does not seem to be able to push this further. I am considering doing this work myself but I haven't gotten to it yet.)

[shindere]

Oh, thanks for the reference!

Depending on how urgent this is, that's something I could see myself working on.