Use hint mode + more often

This is the result of the discussion at https://mattermost.mpi-sws.org/iris/pl/wpjk3kpbx7bf5brh7o3319c8uo

added 7 commits

• da340de2 - make Type params mode +
• 1390f476 - Use ! for classes with "functional dependency".
• 94d96758 - Hacks; might be due to a Coq bug.
• 65017a1c - Consistent pattern for functional dependencies.
• 3aaeed9c - Fix some real ambiguities.
• 1534af50 - Also use + for monad.
• 09a53f1f - Derive keys.

Compare with previous version

That "functional dependencies" pattern needs some explanation, and a comment each time it is used -- 2 hint modes are rather surprising. SOmething like (* B has a functional dependency on A *).

Also I don't understand the last commit, what are "derive keys" and why do those changed modes make sense?

What is the justification for + !? Couldn't this still be nat (some_projection _) and now it has to guess whether this is a list or a set or whatever?

added S-waiting-for-author label

Closing since changes here probably make little sense until https://github.com/coq/coq/issues/18078 is figured out.

closed