The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

The goal is to be able to recognize what is and what isn't a class goal from its type.

When doing resolution during refinement we need that information.

One can also argue that if you put Hint Extern (_ = _) => reflexivity : typeclass_instances

in your file then you can expect Definition foo : 0 = 0 := _. to typecheck.

-- Matthieu

On Wed, Nov 16, 2016 at 2:33 PM Enrico Tassi <enrico.tassi AT inria.fr> wrote:

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