perf: skip `preprocessOutParam` for noMVars queries

This reverts part of the `OrderDual` workaround from #12286.

The `preprocessOutParam` step is morally not needed when the type has
no metavariables, because output params should be uniquely determined
by the input params. The optimization was removed because
semireducible type aliases like `OrderDual` caused TC resolution to
fail (e.g. `FunLike F (OrderDual α) (OrderDual β)` where the last
two arguments are output parameters — without `preprocessOutParam`,
TC resolution fails because it cannot unfold `OrderDual`).

This is an experimental branch for testing whether Mathlib's
`OrderDual` refactoring has progressed enough to restore this
optimization.
1 file changed