The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

Hi Matthieu,

I've been able to fix the error.

Amazingly, the error message became much better when I inserted a type annotation
for "fds", even though the type I annotated was exactly the one that was also inferred.
The cause of the error was indeed that a cast with eq_rect was missing.

In my naive understanding of Coq, my expecation was that inserting a type annotation that
Coq can infer does not change the behavior of the compiler, but that seems to be wrong.

In any case, an error message of the form "term has type X while it is expected to have type X"
is rather puzzling. Maybe there should be a Coq FAQ with advice like "if you get a cryptic
error message, try to annotate all types in your definition and see if that improves the situation ;-)

Thanks for the suggestions from you and everyone else who replied!

Klaus

Am 02/05/17 um 12:26 schrieb Matthieu Sozeau:

Hi,

  The constraint it cannot solve is a conversion constraint while x1 is only a propositional equality, Coq is hence unable to use it during conversion. You probably need to rewrite with that x1 equality before you can typecheck your term, but we'd need a bit more context to tell you how. What's the term you're trying to typecheck precisely?

Best,

-- Matthieu

On Sat, Apr 29, 2017 at 12:04 AM Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de> wrote:

I'm stuck at a strange error message where I can't find anything about
on this mailing list or the documentation.

It looks something like this:

Error:
In environment
...
fds : id -> id -> {n : nat & eqn n}
...
x1 : projT1 (fds f c) = length tys1
x2 : projT2 (fds f c) = {| e_xtor := c; e_xtor_tyargs := cv; e_body :=
term |}
The term "fds" has type "id -> id -> {n : nat & eqn n}"
while it is expected to have type "id -> id -> {n : nat & eqn n}" (cannot
satisfy constraint
"eqn (length tys1)" == "(fun n : nat => eqn n) (projT1 (fds f c))").

The types that it wants to be identical are identical, and they are also
identical
if all implicit arguments, universe levels etc. are printed. "eqn" is a
dependent
type that expects a "nat".

The constraint it cannot satisfy follows from equation x1, but Coq doesn't
seem to be able to use that assumption.

I'm rather clueless what to do about this error. Any suggestions?

Klaus