The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

This is a deliberate change to avoid "wrong" instances which generate non-class goals from polluting search. 

You just need to declare the head as a class using Existing Class eq for example here, because you're really 

treating it as a class. Sorry for not updating the CHANGES yet, the refman has been updated though.

Best,

-- Matthieu

On Wed, Nov 16, 2016 at 2:15 PM Ralf Jung <jung AT mpi-sws.org> wrote:

Hi all,

while porting our development to Coq 8.6, we stumbled upon a backwards
incompatibility with respect to typeclass resolution and Extern hints.
In previous Coq versions, if applying a typeclass instance created goals
that are not typeclasses, Extern hints would still be executed:

Class Foo (x : nat).

Instance foo x : x = 2 -> Foo x.
Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.

Typeclasses eauto := debug.
Check (_ : Foo 2).
(*
Debug: 1.1: apply foo on (Foo 2)
Debug: 1.1.1.1: (*external*) reflexivity on (2 = 2)

foo 2 eq_refl : Foo 2
     : Foo 2
*)

That was with Coq 8.5.  However, with 8.6, resolution fails:

(*
Debug: 1: looking for (Foo 2) without backtracking
Debug: 1: no match for (Foo 2) , 1 possibilities

?f : Foo 2
     : Foo 2
where
?f : [ |- Foo 2]
*)

Was this a deliberate change of behavior? If yes, what is the rationale?
I don't find this mentioned in the CHANGELOG.

For now, we found a work-around (make the Extern Hint apply to the shape
of the goal *before* the instance is applied). However, this is harder
to maintain because we essentially have to both write the instance, and
then write a Hint Extern matching whenever the instance matches,
applying the instance manually, and then solving the arriving goals with
tactics.

Kind regards,
Ralf