Investigate use of "Filtered Unification"
When I talked with Matthieu at ICFP about our unification problems, he told me to look at "filtered unification" and thought it might help. The docs are at https://coq.inria.fr/refman/addendum/type-classes.html#coq:flag.typeclasses-filtered-unification.
So, let's look at that at some point. ;)