The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 05/15/2014 12:44 PM, Jonathan wrote:
> I have been experimenting (in the trunk version) with the "typeclasses 
> eauto with core" tactic as a fully-backtracking alternative to eauto.  
> However, there are cases where eauto solves a goal but typeclasses 
> eauto with core fails.  Some of these cases are quite trivial, such as 
> applying a single constructor when the goal inductive type has a 
> Constructors hint (which is visible in Print Hint output), where that 
> constructor completely solves the goal.
>
> Is it ever supposed to be the case that typeclasses eauto with core 
> fails when eauto succeeds at solving a goal, or is that a potential 
> bug with typeclasses eauto with core?  If this is expected behavior, 
> is there a way to use typeclasses eauto with core, or something 
> similar that does full backtracking over evars, so that it is at least 
> as powerful as normal eauto?
>
> -- Jonathan

Upon further experimentation, the problem appears to be due to the 
presence of type aliases.

This might be related to bug 2920: Type class resolution breaks under 
aliasing - although it doesn't fail with a "please report" error 
message, it just prevents typeclasses eauto from succeeding. I'll file a 
bug report...

-- Jonathan