The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

After pulling in 8.6beta1, this change hit me as well.

My understanding of Matthieu's change is that the extern hints are only 
used by the "typeclasses eauto with somedb" variant. Even for extern 
hints placed in typeclass_instances.   Here's an example (in 8.6beta1):

Variable A : Type.
Axiom a : A.

Class Foo := {}.

Instance foo1 (a:A) : Foo.

Hint Extern 0 A => exact a : typeclass_instances.

Goal Foo.
Fail typeclasses eauto.
typeclasses eauto with typeclass_instances.
Qed.


whereas in 8.5, that first "typeclasses eauto" would have succeeded.

IMHO the question is: what is the point to placing an extern hint in 
typeclass_instances vs. a different db?  Perhaps the only reason to do 
so is because one at least wants those hints to fire at some point 
during refinement (as well as during "typeclasses eauto" with no 
mentioned db).

One can argue that top-level refinement should not be induced by an A 
goal (unless A is declared an Existing Class), but that is a separate 
argument from not allowing a sub-refinement on an A subgoal of an 
ongoing refinement (as with foo1:Foo above).

-- Jonathan


On 11/16/2016 08:47 AM, Matthieu Sozeau 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