Avoid potential loops related to `compose`.

The current setup is relying on unification not producing trivial solutions such as g ~= (fun x => x) ◯ g which would lead to loops. We use a new typeclass to prevent such loops.

This change is necessary for enabling functional eta in unification during typeclass resolution (see https://github.com/rocq-prover/rocq/pull/20798). It is also a good idea to have independently of that change since there is no spec for unification and even if there was, it certainly would not exclude the behavior that leads to TC loops.