The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Samuel E. Moelius III wrote:
> When you get the error ``Cannot solve a second-order unification 
> problem'', that means that Coq thinks you are asking it to infer a 
> function, correct?

I think that's right.

> In the code below, if you comment out the use of ``generalize'', you 
> get this error.  So, if the above is right, what is the function that 
> it thinks you are asking it to infer in this case?
>
> Is there a way to find this out, in general?

I think the best way to answer this question is to print the proof terms 
generated in a number of proofs.  You'll see that [rewrite] needs to 
choose a function that expresses which occurrences of the equality 
lefthand side you want to replace.

Another little Coq quirk that's good to know for getting more 
informative error messages in such cases: when you get the second-order 
unification complaint when trying to rewrite with a proof of [A = B], 
try running [pattern A] instead.  I think it's guaranteed to fail, but 
the error message expresses why it's not possible to build a well-typed 
function by abstracting over all occurrences of [A] (which is what 
[rewrite] does when you don't specify positional arguments).

> I don't know if this is the same thing, but I have wondered if there 
> was a theorem in the standard library that would do the following in 
> one step.
>
>     apply eq_proofs_unicity.
>     decide equality.
>
> If anyone knows of such a theorem, I would be interested.

It seems impossible to implement [decide equality] as a theorem without 
reflecting type syntax into an inductive type.