The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Jason,

  this was a bug in the type class resolution code, which failed to recognize 
[?4 (Object (Index2Cat C'))] where ?4 was defined as [IsTrunc…] as a type 
class evar.

  This is fixed in the HoTT/coq repository.
Best,
-- Matthieu

On 16 juil. 2013, at 17:35, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> On code like [Definition foo := bar.], with [Set Printing All.], I get the 
> error message
> 
> 
> Toplevel input, characters 363-380:                                         
>                                                                 
> Error:                                                                      
>                                                                 
> Cannot infer this placeholder.                                              
>                                                                 
> Could not find an instance for "IsTrunc (nat_to_trunc_index O)              
>                                                                 
>                                   (Object (Index2Cat C'))" in environment:  
>                                                                 
>                                                                             
>                                                                 
> fs : Funext                                                                 
>                                                                 
> I : Type                                                                    
>                                                                 
> Index2Cat : forall _ : I, PreCategory                                       
>                                                                 
> H0 : forall i : I, IsTrunc (nat_to_trunc_index O) (Object (Index2Cat i))    
>                                                                 
> C' : I  
> 
> 
> Setting [Typeclasses eauto := debug.] shows that coq jumps straight from 
> the input to the error message, with no typeclass search in between.  If I 
> replace [Definition foo := bar.] with [Definition foo : T. refine bar. Grab 
> Existential Variables.  typeclasses eauto. Defined.], it goes through.  The 
> relevant code is at theories/Groupoid/Functor.v in 
> https://github.com/JasonGross/HoTT-categories/tree/typeclass-error.  Does 
> anyone have any ideas what the problem might be?
> 
> Thanks,
> Jason