typeclass - Coq: typeclasses vs dependent records -

i can't understand difference between typeclasses , dependent records in coq. reference manual gives syntax of typeclasses, says nothing , how should use them. bit of thinking , searching reveals typeclasses are dependent records bit of syntactic sugar allows coq automatically infer implicit instances , parameters. seems algorithm typeclasses works better when there more or less 1 possible instance of in given context, that's not big issue since can move fields of typeclass parameters, removing ambiguity. instance declaration automatically added hints database can ease proofs break them, if instances general , caused proof search loops or explosions. there other issues should aware of? heuristic choosing between two? e.g. lose if use records , set instances implicit parameters whenever possible?

you right: type classes in coq records special plumbing , inference (there's special case of single-method type classes, doesn't affect answer in way). therefore, reason choose type classes on "pure" dependent records benefit special inference them: inference plain dependent records not powerful , doesn't allow omit information.

as example, consider following code, defines monoid type class, instantiating natural numbers:

class monoid := monoid {   op : -> -> a;   id : a;   opa : forall x y z, op x (op y z) = op (op x y) z;   idl : forall x, op id x = x;   idr : forall x, op x id = x }.  require import arith.  instance nat_plus_monoid : monoid nat := {|   op := plus;   id := 0;   opa := plus_assoc;   idl := plus_o_n;   idr := fun n => eq_sym (plus_n_o n) |}. 

using type class inference, can use definitions work monoid directly nat, without supplying type class argument, e.g.

definition times_3 (n : nat) := op n (op n n). 

however, if make above definition regular record replacing class , instance record , definition, same definition fails:

toplevel input, characters 38-39: error: in environment n : nat term "n" has type "nat" while expected have type  "monoid ?11". 

the caveat type classes instance inference engine gets bit lost sometimes, causing hard-to-understand error messages appear. being said, it's not disadvantage on dependent records, given possibility isn't available there.