The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Just to be clear, I'm not advocating for eq to become a class in general (although it might have uses), I'd rather have people use wrapping classes like Enrico suggested to delimit cleanly the goals the are left to resolution. Another idea to correct this issue of classification is to tag the holes/premisses rather than relying on the types. Anyway, it seems this change has more far reaching consequences than expected (due to globality of Existing Class declarations for example) and we'll need some time to settle on a design, so we'll revert that change in 8.6. Thanks for the quick feedback, everyone!

On Wed, Nov 16, 2016 at 2:47 PM Matthieu Sozeau <mattam AT mattam.org> wrote:

I'm curious about the actual use cases of using such non-class premises around, I'd be happy to hear about others. We can still go back on this cleanup.

-- Matthieu

On Wed, Nov 16, 2016 at 2:40 PM Matthieu Sozeau <mattam AT mattam.org> wrote:

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