Removing universes from Tot and GTot comps

[aseemr]

This PR removes universes from Tot and GTot computation types in reflection and typechecker syntax.

• In both cases, Total and GTotal cases take only one argument, the result type of the computation.
• In reflection, moving the decreases clauses out of C_Total and C_GTotal to the common C_Eff case.

It is a breaking change for the reflection clients, see tests changes in the PR for a few examples.

There is no performance impact, see the regression graphs below in the comments.

[aseemr]

runlim regresion slopes for time and space for ulib (generated using the script in #2786), with --admit_smt_queries true.

[nikswamy]

Thanks @aseemr!

Just some context:

The internal abstract syntax in the compiler maintained an option universe field in the representation of Tot t and GTot t computations, which is meant to memoize the universe of the type argument t. However, this memoization was always a bit messy, the field was often not set, and setting it involved creating a new AST node, rather than updating memo refence ... so, the memoization was not very effective either.

In an earlier PR, when we were reflecting universes into the FStar.Reflection syntax, we added this universe field to the reflection counterparts of Tot and GTot, i.e., C_Total and C_GTotal. But, this was, in hindsight, a mistake. Tot and GTot are primitives in F*, and like other primitive type constructors, e.g., -> they are inherently universe polymorphic, without requiring a universe instantiation. Adding a universe to C_Total and C_GTotal made the reflection syntax of arrows asymmetric, i.e., t -> t' is represented as t -> C_Total t' (Some u), meaning, effectively, that the arrow takes a universe argument for the co-domain but not for its domain---which is weird, and led to some confusion in our F* specification of the F* typing judgment.

So, this PR systematically removes the universes argument from the internal compiler representation of Tot and GTot, and correspondingly also from C_Total and C_GTotal. This is a breaking change to the reflection API.

Note, in doing so, we also took the opportunity to clean up the reflection of the decreases clause in Tot and GTot computation types--they are no longer present there, but are added to the representation of C_Eff, the representation of general computation types (which includes user-defined effects and their universe annotations).