When looking for unifications of a goal with an instance of this class, we “freeze” all the existentials appearing in the goals, meaning that they are considered rigid during unification and cannot be instantiated.
You have to add more type annotations sometimes but as far as I can tell the types are ambiguous in such situations anyway. @gmalecha do you have any experience with that option?
I recently discovered this wonderful option:
Set Typeclass Strict Resolution, which would help avoid infinite loop problems such as that motivating https://github.com/coq-community/coq-ext-lib/pull/106.You have to add more type annotations sometimes but as far as I can tell the types are ambiguous in such situations anyway. @gmalecha do you have any experience with that option?