The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

(Sorry — the examples you were talking about were about the other issue.  I’m also interested in those, though!)

  - B

On Jun 19, 2017, at 11:23 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

What I had most problems with initially is that some type classes have implicit parameters. This works quite well when the nesting level of these parameters is small, but when the nesting of parameters gets deeper one can have the issue that unification takes long, that error messages are hard to understand and that later in a proof one might require certain relations between different parameters of a type class which are not explicit when the initial resolution was done and that an instance is chosen which is not compatible with these requirements, although there is one which would be compatible. The solution is typically to explicitly specify some of the implicit parameters, especially their relation to each other. Another advantage of stating certain things explicitly is that it is easier to understand what actually happens. Let me see if I can find a few examples.