Instances for dependent function types

[Tragicus]

Motivation for this change

Generalizes the instances on function types to dependent function types. The same generalization is happening in mathcomp (see https://github.com/math-comp/math-comp/pull/1256) and it needs to be done here first for backwards compatibility. EDIT: WIP because we are waiting for unification features in Coq that make unifying dependent functions work.

Checklist

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

I observe that this PS shares similarities with PR https://github.com/math-comp/analysis/pull/1379 while the latter is marked as draft. Maybe you intended this one as well to be a draft?

[Tragicus]

What is the justification for the mandatory addition of constants for the application of blah_cst lemmas? Do we know where the problem comes from?

cst is not dependent (and can not be), so I can not define the operations on dependent functions using it. Then, when Rocq tries to unify cst ?c with 1 : U -> V, it reduces the problem to fun=> ?c = fun t : U => GRing.one ((fun=> V) t) and then to ?c = GRing.one ((fun=> V) t). This fails because ?c can not use t in its instantiation. I believe I have a solution for that, but it needs to be integrated into Coq, so it will take some time, and the impact looks minor according to the CI.

[Tragicus]

I extracted this from the other PR and extended it when I realized I needed to generalize things here first. It is ready for review.