From 94d2a3ef86306ea79498482adeb3138f2ebd8328 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 May 2022 18:30:53 -0700 Subject: [PATCH] feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures --- src/Lean/Elab/Inductive.lean | 75 ++++++++++++------- src/Lean/Elab/Structure.lean | 9 ++- tests/lean/inductiveUnivErrorMsg.lean | 7 ++ .../inductiveUnivErrorMsg.lean.expected.out | 14 ++++ tests/lean/univInference.lean.expected.out | 14 +++- 5 files changed, 91 insertions(+), 28 deletions(-) create mode 100644 tests/lean/inductiveUnivErrorMsg.lean create mode 100644 tests/lean/inductiveUnivErrorMsg.lean.expected.out diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 5764bbb7f1..cc57da414f 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -415,33 +415,60 @@ def mkResultUniverse (us : Array Level) (rOffset : Nat) : Level := else r.normalize + /-- + Auxiliary function for `updateResultingUniverse` + `accLevel u r rOffset` add `u` to state if it is not already there and + it is different from the resulting universe level `r+rOffset`. + + + If `u` is a `max`, then its components are recursively processed. + If `u` is a `succ` and `rOffset > 0`, we process the `u`s child using `rOffset-1`. + + This method is used to infer the resulting universe level of an inductive datatype. + -/ +def accLevel (u : Level) (r : Level) (rOffset : Nat) : OptionT (StateT (Array Level) Id) Unit := do + go u rOffset +where + go (u : Level) (rOffset : Nat) : OptionT (StateT (Array Level) Id) Unit := do + match u, rOffset with + | Level.max u v _, rOffset => go u rOffset; go v rOffset + | Level.imax u v _, rOffset => go u rOffset; go v rOffset + | Level.zero _, _ => return () + | Level.succ u _, rOffset+1 => go u rOffset + | u, rOffset => + if rOffset == 0 && u == r then + return () + else if r.occurs u then + failure + else if rOffset > 0 then + failure + else if (← get).contains u then + return () + else + modify fun us => us.push u + /-- Auxiliary function for `updateResultingUniverse` - `accLevelAtCtor u r rOffset` add `u` to state if it is not already there and + `accLevelAtCtor ctor ctorParam r rOffset` add `u` (`ctorParam`'s universe) to state if it is not already there and it is different from the resulting universe level `r+rOffset`. - If `u` is a `max`, then its components are recursively processed. - If `u` is a `succ` and `rOffset > 0`, we process the `u`s child using `rOffset-1`. - - This method is used to infer the resulting universe level of an inductive datatype. + See `accLevel`. -/ -def accLevelAtCtor (u : Level) (r : Level) (rOffset : Nat) : StateRefT (Array Level) TermElabM Unit := do - match u, rOffset with - | Level.max u v _, rOffset => accLevelAtCtor u r rOffset; accLevelAtCtor v r rOffset - | Level.imax u v _, rOffset => accLevelAtCtor u r rOffset; accLevelAtCtor v r rOffset - | Level.zero _, _ => return () - | Level.succ u _, rOffset+1 => accLevelAtCtor u r rOffset - | u, rOffset => - if rOffset == 0 && u == r then - return () - else if r.occurs u then - throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly" - else if rOffset > 0 then - throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly" - else if (← get).contains u then - return () - else - modify fun us => us.push u +def accLevelAtCtor (ctor : Constructor) (ctorParam : Expr) (r : Level) (rOffset : Nat) : StateRefT (Array Level) TermElabM Unit := do + let type ← inferType ctorParam + let u ← instantiateLevelMVars (← getLevel type) + match (← modifyGet fun s => accLevel u r rOffset |>.run |>.run s) with + | some _ => pure () + | none => + let typeType ← inferType type + let mut msg := m!"failed to compute resulting universe level of inductive datatype, constructor '{ctor.name}' has type{indentExpr ctor.type}\nparameter" + let localDecl ← getFVarLocalDecl ctorParam + unless localDecl.userName.hasMacroScopes do + msg := msg ++ m!" '{ctorParam}'" + msg := msg ++ m!" has type{indentD m!"{type} : {typeType}"}\ninductive type resulting type{indentExpr (mkSort (r.addOffset rOffset))}" + if r.isMVar then + msg := msg ++ "\nrecall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level" + throwError msg /-- Execute `k` using the `Syntax` reference associated with constructor `ctorName`. @@ -463,9 +490,7 @@ where withCtorRef views ctor.name do forallTelescopeReducing ctor.type fun ctorParams _ => for ctorParam in ctorParams[numParams:] do - let type ← inferType ctorParam - let u ← instantiateLevelMVars (← getLevel type) - accLevelAtCtor u r rOffset + accLevelAtCtor ctor ctorParam r rOffset private def updateResultingUniverse (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) := do let r ← getResultingUniverse indTypes diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 888abf061f..f4ecfac2f0 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -623,7 +623,14 @@ where let type ← inferType info.fvar let u ← getLevel type let u ← instantiateLevelMVars u - accLevelAtCtor u r rOffset + match (← modifyGet fun s => accLevel u r rOffset |>.run |>.run s) with + | some _ => pure () + | none => + let typeType ← inferType type + let mut msg := m!"failed to compute resulting universe level of structure, field '{info.declName}' has type{indentD m!"{type} : {typeType}"}\nstructure resulting type{indentExpr (mkSort (r.addOffset rOffset))}" + if r.isMVar then + msg := msg ++ "\nrecall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the structure resulting universe level" + throwError msg private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type : Expr) : TermElabM Expr := do let r ← getResultUniverse type diff --git a/tests/lean/inductiveUnivErrorMsg.lean b/tests/lean/inductiveUnivErrorMsg.lean new file mode 100644 index 0000000000..6eb27f2c3f --- /dev/null +++ b/tests/lean/inductiveUnivErrorMsg.lean @@ -0,0 +1,7 @@ +inductive Bar +| foobar : Foo → Bar +| somelist : List Bar → Bar + +inductive Bar2 +| foobar : (x : Foo) → Bar2 +| somelist : List Bar2 → Bar2 diff --git a/tests/lean/inductiveUnivErrorMsg.lean.expected.out b/tests/lean/inductiveUnivErrorMsg.lean.expected.out new file mode 100644 index 0000000000..ebbe2704eb --- /dev/null +++ b/tests/lean/inductiveUnivErrorMsg.lean.expected.out @@ -0,0 +1,14 @@ +inductiveUnivErrorMsg.lean:2:0-2:20: error: failed to compute resulting universe level of inductive datatype, constructor 'Bar.foobar' has type + {Foo : Sort u_1} → Foo → Bar +parameter has type + Foo : Sort u_1 +inductive type resulting type + Type ?u +recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level +inductiveUnivErrorMsg.lean:6:0-6:27: error: failed to compute resulting universe level of inductive datatype, constructor 'Bar2.foobar' has type + {Foo : Sort u_1} → Foo → Bar2 +parameter 'x' has type + Foo : Sort u_1 +inductive type resulting type + Type ?u +recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level diff --git a/tests/lean/univInference.lean.expected.out b/tests/lean/univInference.lean.expected.out index ad85bbc6a5..5b76915466 100644 --- a/tests/lean/univInference.lean.expected.out +++ b/tests/lean/univInference.lean.expected.out @@ -1,8 +1,18 @@ -univInference.lean:25:0-27:9: error: failed to compute resulting universe level of inductive datatype, provide universe explicitly +univInference.lean:25:0-27:9: error: failed to compute resulting universe level of structure, field 'Struct.S4.a' has type + α : Sort u +structure resulting type + Type ?u +recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the structure resulting universe level S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1)) univInference.lean:45:0-46:17: error: 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' max u v -univInference.lean:65:2-65:22: error: failed to compute resulting universe level of inductive datatype, provide universe explicitly +univInference.lean:65:2-65:22: error: failed to compute resulting universe level of inductive datatype, constructor 'Induct.S4.mk' has type + {α : Sort u} → {β : Sort v} → α → β → S4 α β +parameter 'a' has type + α : Sort u +inductive type resulting type + Type ?u +recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level univInference.lean:73:0-74:22: error: 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' max u v univInference.lean:81:0-82:22: error: 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'