Support level polymorphism #143
Description
The surface syntax of SynthLean does not currently support universe polymorphism, forcing us to use hacks such as three different sorry axioms, and in general exponentially many definitions. This is a serious usability issue. I think we can fix this without changing the deeply embedded syntax, by compiling def name.{u} into a function def name : (u : Nat) → CheckedDef ..; in other words, replace internal universe polymorphism with an external definition schema. However, this is currently a little tricky: we require that the maximum universe appearing within any subterm of a well-formed term be bounded by univMax. Given an arbitrary u, there is no reason why that should hold. The schema should really then be def name : (u : Nat) → Constraints u → CheckedDef .. where Constraints u is a set of linear constraints on u that guarantee the output is well-formed. This sounds annoying to implement and use (c.f. Rocq) and I'd rather maybe just get rid of the global univMax : Nat, replacing it by an operation univMax : Expr → Nat that produces the maximal universe appearing in a given expression.