The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/12/2016 04:15 AM, Soegtrop, Michael wrote:
> Dear Jonathan, Daniel,
>
> > I don't think there is a way tactically to decide if a definition is an 
> > instance
> I thought about it once more: one issue with eauto is that it will also use 
> local hypothesis. So these must be cleared before the test and this must be 
> undone after the test. Below is a tactic which does this with a few test 
> cases.

Another issue is that the typeclass_instances db can contain hints that 
solve the goal with a non-instance in 1 step even if it isn't a 
typeclass-typed goal.  If hole refinement is used instead: just "pose (_ 
: T) as Hex" - if it doesn't fail, then at least we know T is a Class, 
but that doesn't mean that it was filled in with an instance, again due 
to typeclass_instance hints.  The reason is that typeclasses are duck 
types - any way you can fill in their requirements works.  The 
"Instance" syntax is little (nothing?) more than a normal definition 
combined with a resolve hint for the typeclass_instances db.

But, maybe this is good enough - in that the required unfolding would 
work for such "faked" instances as well?   Because a faked instance is 
just a good as a real one?

Or maybe unfolding all projections that simplify is good enough, even if 
they're just projections on plain old records?

-- Jonathan