The Coq mailing list

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

On 03/05/2014 02:16 PM, Kevin Sullivan wrote:
> Separately, I'd note that the error message produced for the last line 
> of this short code segment is this: Error: The term "append_nil" has 
> type "Monoid" while it is expected to have type "Monoid". This doesn't 
> seem quite right.

The message sounds right to me, considering normal Coq conventions, 
because the parameter to [Monoid] is marked as implicit.  Try the usual 
fix of running [Set Printing All], or another command to trigger a less 
verbose printing mode that still includes what you need.