The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Note that Clément Pit-claudel implemented something to help in these
cases in his company-coq mode for emacs/proofgeneral: it uses diff
facility on error messages to show what differs in two big types.

See the tutorial M-x company-coq-tutorial.

Best,
Pierre


2017-11-28 10:33 GMT+01:00 Ralf Jung 
<jung AT mpi-sws.org>:
> Hi,
>
>> The term
>>  "{|
>>   field_final := isFinal;
>>   field_value := value;
>>   field_rwt_ok := pf |}"
>> has type
>>  "Field
>>     mTipe_string
>>     "io.compression.codecs"
>>     io_compression_codecs_rwt"
>> while it is expected to have type
>>  "Field
>>     mTipe_string
>>     "io_compression_codecs"
>>     io_compression_codecs_rwt".
>
> Would it be possible to improve that error message?  For example, when
> similar errors are shown in Rust, it shows both the two overall types
> that do not match, but also the concrete place in both of them that
> fails to match -- so here, it would additionally show that it has type
> "io.compression.codecs" while it is expected to have
> "io_compression_codecs".  This is really useful, even more so if the
> only difference is in implicit arguments that are otherwise not even
> printed.
>
> ; Ralf