feat: elaborate explicit universe levels

src/Init/Lean/Elab/Term.lean

@@ -774,9 +774,6 @@ fun stx expectedType? => do
     withMacroExpansion stx.val (elabTerm newStx expectedType?)
   | _ => throwError stx.val "unexpected array literal syntax"
 
-def elabExplicitUniv (stx : Syntax) : TermElabM (List Level) :=
-pure [] -- TODO
-
 private partial def resolveLocalNameAux (lctx : LocalContext) : Name → List String → Option (Expr × List String)
 | n, projs =>
   match lctx.findFromUserName? n with

src/Init/Lean/Elab/TermApp.lean

@@ -292,6 +292,14 @@ private def elabAppLVals (ref : Syntax) (f : Expr) (lvals : List LVal) (namedArg
 when (!lvals.isEmpty && explicit) $ throwError ref "invalid use of field notation with `@` modifier";
 elabAppLValsAux ref namedArgs args expectedType? explicit f lvals
 
+def elabExplicitUniv (stx : Syntax) : TermElabM (List Level) := do
+let lvls := stx.getArg 1;
+lvls.foldSepRevArgsM
+  (fun stx lvls => do
+    lvl ← elabLevel stx;
+    pure (lvl::lvls))
+  []
+
 private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array NamedArg → Array Arg → Option Expr → Bool → Array TermElabResult → TermElabM (Array TermElabResult)
 | f, lvals, namedArgs, args, expectedType?, explicit, acc =>
   if f.getKind == choiceKind then
@@ -312,7 +320,7 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
     -- Remark: `id.<namedPattern>` should already have been expanded
     match id with
     | Syntax.ident _ _ n preresolved => do
-      us        ← elabExplicitUniv (mkNullNode us);
+      us ← if us.isEmpty then pure [] else elabExplicitUniv (us.get! 0);
       funLVals ← resolveName f n preresolved us;
       funLVals.foldlM
         (fun acc ⟨f, fields⟩ => do

tests/lean/run/frontend1.lean

@@ -160,7 +160,12 @@ f a
 
 
 #eval run "#check let x := one + zero; x + x"
-set_option trace.Elab true
+-- set_option trace.Elab true
 #eval run "#check (fun x => let v := x.w; v + v) s4"
 #eval run "#check fun x => foo x (let v := x.w; v + one) s4"
 #eval run "#check fun x => foo x (let v := x.w; let w := x.x; v + w + one) s4"
+#eval fail "#check id.{1,1}"
+#eval fail "#check @id.{0} Nat"
+#eval run "#check @id.{1} Nat"
+#eval run "universes u #check id.{u}"
+#eval fail "universes u #check id.{v}"