coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Kevin Sullivan <sullivan.kevinj AT gmail.com>
Subject: Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?
Date: Tue, 28 Nov 2017 10:33:39 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
Ironport-phdr: 9a23:3MHmbB0m9VW2tN+AsmDT+DRfVm0co7zxezQtwd8ZsegULfad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL3WbmHC57CYTFxPjLkI1Y72tQs+Bueq429iV3tWTPlwJ13KBZuZ5KwzzpgHMvOEXh5FjI+A/0F+BgXZWeuIe/n5sIVONlhC0styt+Jpi7S1W/fEs6c9GU431eq05SfpTCzFwYE4v48i+jxDHQ0Ot+30TGjEUjxxHKw3d7VThQYy3tTH14LkukBKGNNH7GOhnEQ+p6L1mHVq02So=

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

[Coq-Club] Missing a detail on type checking -- bad error reporting?, Kevin Sullivan, 11/27/2017
- Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Matthieu Sozeau, 11/27/2017
  - Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Kevin Sullivan, 11/27/2017
- Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Ralf Jung, 11/28/2017
  - Re: [Coq-Club] Missing a detail on type checking -- bad error reporting?, Pierre Courtieu, 11/28/2017