The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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.

Thanks,

Jason