The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.