From 8649483b416ec9d919c380d657ceedf8184ed527 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jun 2022 19:41:40 -0700 Subject: [PATCH] feat: produces an error if the declaration body contains a universe parameter that does not occur in the declaration type nor is explicitly provided closes #898 --- RELEASES.md | 20 ++++++++++++ src/Lean/Elab/MutualDef.lean | 41 +++++++++++++++++++++++++ tests/lean/holeErrors.lean | 10 +++--- tests/lean/holeErrors.lean.expected.out | 18 +++++------ 4 files changed, 75 insertions(+), 14 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index 9ed9131a637a..3e2f112b8289 100644 --- a/RELEASES.md +++ b/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). diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 91915e195243..8d3b27b8397f 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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 diff --git a/tests/lean/holeErrors.lean b/tests/lean/holeErrors.lean index 5d5e5f23915f..e6969e64608d 100644 --- a/tests/lean/holeErrors.lean +++ b/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 diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out index d88cb4e3f166..b2c86aab8943 100644 --- a/tests/lean/holeErrors.lean.expected.out +++ b/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