feat: produces an error if the declaration body contains a universe p…

…arameter that does not occur in the declaration type nor is explicitly provided

closes leanprover#898

RELEASES.md

@@ -1,6 +1,26 @@
 Unreleased
 ---------
 
+* Lean now generates an error if the body of a declaration body contains a universe parameter that does not occur in the declaration type, nor is an explicit parameter.
+  Examples:
+  ```lean
+  /-
+  The following declaration now produces an error because `PUnit` is universe polymorphic,
+  but the universe parameter does not occur in the function type `Nat → Nat`
+  -/
+  def f (n : Nat) : Nat :=
+    let aux (_ : PUnit) : Nat := n + 1
+    aux ⟨⟩
+
+  /-
+  The following declaration is accepted because the universe parameter was explicitly provided in the
+  function signature.
+  -/
+  def g.{u} (n : Nat) : Nat :=
+    let aux (_ : PUnit.{u}) : Nat := n + 1
+    aux ⟨⟩
+  ```
+
 * Add `subst_vars` tactic.
 
 * [Fix `autoParam` in structure fields lost in multiple inheritance.](https://github.com/leanprover/lean4/issues/1158).

src/Lean/Elab/MutualDef.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Parser.Term
 import Lean.Meta.Closure
 import Lean.Meta.Check
+import Lean.PrettyPrinter.Delaborator.Options
 import Lean.Elab.Command
 import Lean.Elab.Match
 import Lean.Elab.DefView
@@ -720,6 +721,45 @@ def eraseAuxDiscr (e : Expr) : CoreM Expr := do
         return TransformStep.visit e
     | e => return TransformStep.visit e
 
+partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs : Array PreDefinition) : TermElabM Unit :=
+  unless (← MonadLog.hasErrors) do
+    -- We do not report this kind of error if the declaration already contains errors
+    let mut sTypes : CollectLevelParams.State := {}
+    let mut sValues : CollectLevelParams.State := {}
+    for preDef in preDefs do
+      sTypes  := collectLevelParams sTypes preDef.type
+      sValues := collectLevelParams sValues preDef.value
+    if sValues.params.all fun u => sTypes.params.contains u || allUserLevelNames.contains u then
+      -- If all universe level occurring in values also occur in types or explicitly provided universes, then everything is fine
+      -- and we just return
+      return ()
+    let checkPreDef (preDef : PreDefinition) : TermElabM Unit :=
+      -- Otherwise, we try to produce an error message containing the expression with the offending universe
+      let rec visitLevel (u : Level) : ReaderT Expr TermElabM Unit := do
+        match u with
+        | .succ u _ => visitLevel u
+        | .imax u v _ | .max u v _ => visitLevel u; visitLevel v
+        | .param n _ =>
+          unless sTypes.visitedLevel.contains u || allUserLevelNames.contains n do
+            let parent ← withOptions (fun o => pp.universes.set o true) do addMessageContext m!"{indentExpr (← read)}"
+            let body ← withOptions (fun o => pp.letVarTypes.setIfNotSet (pp.funBinderTypes.setIfNotSet o true) true) do addMessageContext m!"{indentExpr preDef.value}"
+            throwError "invalid occurrence of universe level '{u}' at '{preDef.declName}', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression{parent}\nat declaration body{body}"
+        | _ => pure ()
+      let rec visit (e : Expr) : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit := do
+        checkCache { val := e : ExprStructEq } fun _ => do
+          match e with
+          | .forallE n d b c | .lam n d b c => visit d e; withLocalDecl n c.binderInfo d fun x => visit (b.instantiate1 x) e
+          | .letE n t v b _  => visit t e; visit v e; withLetDecl n t v fun x => visit (b.instantiate1 x) e
+          | .app ..        => e.withApp fun f args => do visit f e; args.forM fun arg => visit arg e
+          | .mdata _ b _   => visit b e
+          | .proj _ _ b _  => visit b e
+          | .sort u _      => visitLevel u (← read)
+          | .const _ us _  => us.forM (visitLevel · (← read))
+          | _              => pure ()
+      visit preDef.value preDef.value |>.run {}
+    for preDef in preDefs do
+      checkPreDef preDef
+
 def elabMutualDef (vars : Array Expr) (views : Array DefView) (hints : TerminationHints) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv go
@@ -753,6 +793,7 @@ where
             return preDef
           else
             return { preDef with value := (← eraseAuxDiscr preDef.value) }
+        checkForHiddenUnivLevels allUserLevelNames preDefs
         addPreDefinitions preDefs hints
         processDeriving headers
 

tests/lean/holeErrors.lean

@@ -1,11 +1,11 @@
 --
 
-def f1 := id
+def f1.{u} := id.{u}
 
 def f2 : _ := id
 
-def f3 :=
-let x := id;
+def f3.{u} :=
+let x := id.{u};
 x
 
 def f4 (x) := x
@@ -15,6 +15,6 @@ def f5 (x : _) := x
 def f6 :=
 fun x => x
 
-def f7 :=
-let rec x := id;
+def f7.{u} :=
+let rec x := id.{u};
 10

tests/lean/holeErrors.lean.expected.out

@@ -1,24 +1,24 @@
-holeErrors.lean:3:7-3:12: error: failed to infer definition type
-holeErrors.lean:3:10-3:12: error: don't know how to synthesize implicit argument
+holeErrors.lean:3:11-3:20: error: failed to infer definition type
+holeErrors.lean:3:14-3:20: error: don't know how to synthesize implicit argument
   @id ?m
 context:
-⊢ Sort u_1
+⊢ Sort u
 holeErrors.lean:5:9-5:10: error: failed to infer definition type
 when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
-holeErrors.lean:8:9-8:11: error: don't know how to synthesize implicit argument
+holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
+holeErrors.lean:8:9-8:15: error: don't know how to synthesize implicit argument
   @id ?m
 context:
-⊢ Sort u_1
-holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
-holeErrors.lean:7:7-9:1: error: failed to infer definition type
+⊢ Sort u
+holeErrors.lean:7:11-9:1: error: failed to infer definition type
 holeErrors.lean:11:11-11:15: error: failed to infer definition type
 holeErrors.lean:11:8-11:9: error: failed to infer binder type
 holeErrors.lean:13:12-13:13: error: failed to infer binder type
 holeErrors.lean:13:15-13:19: error: failed to infer definition type
 holeErrors.lean:16:4-16:5: error: failed to infer binder type
 holeErrors.lean:15:7-16:10: error: failed to infer definition type
-holeErrors.lean:19:13-19:15: error: don't know how to synthesize implicit argument
+holeErrors.lean:19:13-19:19: error: don't know how to synthesize implicit argument
   @id ?m
 context:
-⊢ Sort u_1
+⊢ Sort u
 holeErrors.lean:19:8-19:9: error: failed to infer 'let rec' declaration type