The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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