Stop converting constructors universe instances (and parameters too)

[mattam82]

Description of the problem

The invariants of conversion and unification should ensure that we only compare terms that have a common supertype. In this case it means for constructors we could stop converting their universe instances and parameters (they have indeed to be applied to the same number of parameters and by invariant they should be convertible). This could have an impact on unification, to be experimented.

[SkySkimmer]

I experimented with skipping conversion of parameters (and domain of lambdas), see https://github.com/coq/coq/wiki/Performance-experiments#skipping-conversion-of-parameters-of-constructors-and-of-the-domain-of-lambdas-failed
TLDR with the current right-to-left order of processing application arguments converting parameters/domains allows early failure so it doesn't work out.

[ppedrot]

Wasn't that solved by #6747?

[SkySkimmer]

No, that was only the universe instances.

[SkySkimmer]

Doesn't work out as a perf improvement in practice.