I would like to announce the release of Deriving v0.1.0 (GitHub - arthuraa/deriving: Class instances for Coq inductive types with little boilerplate, available as coq-deriving on OPAM). It is a library for automating the generation of MathComp class instances for inductive types, akin to how deriving declarations work in OCaml or Haskell. With a few lines of code, you can derive instances of eqType, choiceType, etc. for your types. The instances are defined using the recursion scheme for the types, and they can be generated even for mutually inductive and nested inductive types (provided that you define the recursion scheme yourself). Check the GitHub page for examples!

For count and choice, it converts the inductive type to a tree representation (GenTree.tree in choice.v), and transports the instances by cancellation. For finite, it generates an enumeration of the type, trying to respect the order of the constructors. For order, it generates a comparison function that compares the elements lexicographically, using the order of the constructors to break ties.

The main difficulty I foresee for dealing with non-uniform parameters is coming up with a generic representation of an inductive type. With uniform parameters, I can just use a list with the types of the arguments of each constructor; when they are non-uniform (or when we have a dependent type), I imagine I would have to use a telescope to encode the constructor types.