From 3ee8ceafb4e6dafa1e5e314cf25e6ea4901808e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 3 Apr 2022 08:33:52 -0700
Subject: [PATCH] feat: better error message when constructor parameter
 universe level is too big

---
 RELEASES.md                                 |  2 ++
 src/Lean/Elab/Inductive.lean                | 34 ++++++++++++++++-----
 tests/lean/ctorUnivTooBig.lean              | 17 +++++++++++
 tests/lean/ctorUnivTooBig.lean.expected.out | 18 +++++++++++
 4 files changed, 64 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/ctorUnivTooBig.lean
 create mode 100644 tests/lean/ctorUnivTooBig.lean.expected.out

diff --git a/RELEASES.md b/RELEASES.md
index faeee0f959..96594360c2 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* Improve error message when constructor parameter universe level is too big.
+
 * Add support for `for h : i in [start:stop] do .. ` where `h : i ∈ [start:stop]`. This feature is useful for proving
   termination of functions such as:
 ```lean
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 4c4913aa95..b2f9543b2d 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -392,17 +392,37 @@ def checkResultingUniverse (u : Level) : TermElabM Unit := do
     if !u.isZero && !u.isNeverZero then
       throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'{indentD u}"
 
-private def checkResultingUniverses (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
-  let u ← getResultingUniverse indTypes
+/--
+  Execute `k` using the `Syntax` reference associated with constructor `ctorName`.
+-/
+def withCtorRef (views : Array InductiveView) (ctorName : Name) (k : TermElabM α) : TermElabM α := do
+  for view in views do
+    for ctorView in view.ctors do
+      if ctorView.declName == ctorName then
+        return (← withRef ctorView.ref k)
+  k
+
+private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
+  let u ← instantiateLevelMVars (← getResultingUniverse indTypes)
   checkResultingUniverse u
   unless u.isZero do
     indTypes.forM fun indType => indType.ctors.forM fun ctor =>
       forallTelescopeReducing ctor.type fun ctorArgs type =>
         for ctorArg in ctorArgs[numParams:] do
-          let v ← getLevel (← inferType ctorArg)
-          -- TODO
-          trace[Meta.debug] "checkCtorArgLevel, {v} <= {u}"
-          return ()
+          let type ← inferType ctorArg
+          let v ← instantiateLevelMVars (← getLevel type)
+          if v.hasMVar then
+            -- TODO
+            trace[Meta.debug] "checkCtorArgLevel, {v} <= {u}"
+          else unless u.geq v do
+            let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter"
+            let localDecl ← getFVarLocalDecl ctorArg
+            unless localDecl.userName.hasMacroScopes do
+              msg := msg ++ m!" '{ctorArg}'"
+            msg := msg ++ m!" has type{indentExpr type}"
+            msg := msg ++ m!"\nat universe level{indentD v}"
+            msg := msg ++ m!"\nit must be smaller than or equal to the inductive datatype universe level{indentD u}"
+            withCtorRef views ctor.name <| throwError msg
 
 private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State MetaM Unit := do
   indTypes.forM fun indType => do
@@ -602,7 +622,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
           if inferLevel then
             updateResultingUniverse numParams (← levelMVarToParam indTypes)
           else
-            checkResultingUniverses numParams indTypes
+            checkResultingUniverses views numParams indTypes
             levelMVarToParam indTypes
         let usedLevelNames := collectLevelParamsInInductive indTypes
         match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
diff --git a/tests/lean/ctorUnivTooBig.lean b/tests/lean/ctorUnivTooBig.lean
new file mode 100644
index 0000000000..3be8e882c1
--- /dev/null
+++ b/tests/lean/ctorUnivTooBig.lean
@@ -0,0 +1,17 @@
+inductive Bla : Type u where
+  | nil  : Bla
+  | cons : (α : Type u) → (a : α) → Bla → Bla
+
+inductive Foo : Type where
+  | leaf
+  | mk (α : Type) (a : α)
+  | mk₂
+
+inductive Foo' : Type u where
+  | leaf
+  | mk : Sort (max u v) → a → Foo'
+  | mk₂
+
+inductive Boo : Type u where
+  | nil  : Boo
+  | cons : (α : Sort u) → (a : α) → Boo → Boo
diff --git a/tests/lean/ctorUnivTooBig.lean.expected.out b/tests/lean/ctorUnivTooBig.lean.expected.out
new file mode 100644
index 0000000000..7d0b120183
--- /dev/null
+++ b/tests/lean/ctorUnivTooBig.lean.expected.out
@@ -0,0 +1,18 @@
+ctorUnivTooBig.lean:3:2-3:45: error: invalid universe level in constructor 'Bla.cons', parameter 'α' has type
+  Type u
+at universe level
+  u+2
+it must be smaller than or equal to the inductive datatype universe level
+  u+1
+ctorUnivTooBig.lean:7:2-7:25: error: invalid universe level in constructor 'Foo.mk', parameter 'α' has type
+  Type
+at universe level
+  2
+it must be smaller than or equal to the inductive datatype universe level
+  1
+ctorUnivTooBig.lean:12:2-12:34: error: invalid universe level in constructor 'Foo'.mk', parameter has type
+  Sort (max u v)
+at universe level
+  (max u v)+1
+it must be smaller than or equal to the inductive datatype universe level
+  u+1