The Coq mailing list

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

Hi Jan,

thanks for your answer! I'm not sure how to apply your suggestion, though.
This error does not happen in a proof but in the definition of an
inductive datatype.
I tried to formulate your assertion (adapted to my situation) as a lemma
and add it to the rewrite hint database,
but that doesn't change the error.

Any ideas? Maybe I need some kind of cast?

Klaus



Am 29/04/17 um 11:59 schrieb Jan Bessai:
> Hi,
>
>> 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.
>
> I came across issues like that when porting a proof from Coq 8.5 to
> 8.6. My guess is reduction during unification got less intelligent but
> more predictable. I usually get around these cases doing something like
>
> assert (x_eq: x = f y). {
>   unfold f; destruct y; simpl; reflexivity.
> }
> rewrite x_eq.
>
> potentially using "rewrite in" or simpler proofs for x_eq.
>
> This is a bit explicit and brittle, but I tend to prefer it over
> overly intelligent magic.
> Hope this helps.
>
> Bests,
>  Jan
>
>
>
>