From 74741bf6135daba5d9db59f48117a88726c13063 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Dec 2019 10:52:22 -0800
Subject: [PATCH] feat: elaborate explicit universe levels

---
 src/Init/Lean/Elab/Term.lean    |  3 ---
 src/Init/Lean/Elab/TermApp.lean | 10 +++++++++-
 tests/lean/run/frontend1.lean   |  7 ++++++-
 3 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 765c595839..b1a5f5ed47 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/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
diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean
index 06e0254e72..ee5f5e7f77 100644
--- a/src/Init/Lean/Elab/TermApp.lean
+++ b/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
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index bdc522361c..9deb49a8a9 100644
--- a/tests/lean/run/frontend1.lean
+++ b/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}"