The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Indeed it does.  Thanks!  I guess I was implicitly assuming that all [Hint]s got [progress] implicitly stuck in front of them, but I guess not.

-Jason

On Sunday, July 14, 2013, Adam Chlipala wrote:

Perhaps changing that last hint to
    Hint Extern 3 => progress cbv beta : typeclass_instances.
would help, by avoiding exponential blow-up of the search space even for cases where the hint never does anything.

On 07/14/2013 07:34 PM, Jason Gross wrote:

I would like to know what reductions are performed between typeclass inference and goal presentation.  I know some variant of beta reduction is applied, because I have had typeclass resolution fail with an error message about finding an instance for [Foo ((fun x => <_expression_ involving x>) z)], and then been presented with the goal [Foo (<_expression_ with x replaced by z>)].

I'm trying to figure out how to make typeclass resolution not fail in cases that [typeclasses eauto] succeeds.  I've been able to solve one case with
Hint Extern 0 => assumption : typeclass_instances.
and another with
Hint Extern 0 => match goal with |- appcontext[(fun _ => _) _] => cbv beta end : typeclass_instances.
but adding
Hint Extern 3 => cbv beta : typeclass_instances.
makes typeclass resolution run around in circles.