The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Nov 16, 2016 at 01:23:04PM +0000, Matthieu Sozeau wrote:
> 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.

What you propose seems a bit too drastic, Existing Class marks
Eq as class "forever".  A lighter work around could be the following

  Class Foo (x : nat).
  Class TCPremise (P : Prop).
  Instance foo x : TCPremise (x = 2) -> Foo x.
  Hint Extern 0 (TCPremise (_ = _)) => reflexivity : typeclass_instances.

But frankly the use case of Ralf seems reasonable, and the contortion
above pretty ugly.

Can you explain what you mean by "wrong" instances, exactly?

Best,
-- 
Enrico Tassi