fix : only default to Prop for structures

leanprover · Mar 11, 2024 · 41b7323 · 41b7323
1 parent cf7551e
commit 41b7323
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
@@ -420,13 +420,13 @@ where
   levelMVarToParam' (type : Expr) : TermElabM Expr := do
     Term.levelMVarToParam type (except := fun mvarId => univToInfer? == some mvarId)
 
-def mkResultUniverse (us : Array Level) (rOffset : Nat) : Level :=
+def mkResultUniverse (us : Array Level) (rOffset : Nat) (defaultLevel : Level) : Level :=
   if us.isEmpty && rOffset == 0 then
-    levelOne
+    defaultLevel
   else
     let r := Level.mkNaryMax us.toList
-    if rOffset == 0 && !r.isZero && !r.isNeverZero then
-      mkLevelMax r levelOne |>.normalize
+    if rOffset == 0 && !r.isZero && !r.isNeverZero && !defaultLevel.isZero then
+      mkLevelMax r defaultLevel |>.normalize
     else
       r.normalize
 
@@ -447,6 +447,7 @@ where
   go (u : Level) (rOffset : Nat) : OptionT (StateT (Array Level) Id) Unit := do
     match u, rOffset with
     | .max u v,  rOffset   => go u rOffset; go v rOffset
+    | .zero,     _         => return ()
     | .imax u v, rOffset   => go u rOffset; go v rOffset
     | .succ u,   rOffset+1 => go u rOffset
     | u,         rOffset   =>
@@ -514,7 +515,7 @@ private def updateResultingUniverse (views : Array InductiveView) (numParams : N
     throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly: {r}"
   let us ← collectUniverses views r rOffset numParams indTypes
   trace[Elab.inductive] "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
-  let rNew := mkResultUniverse us rOffset
+  let rNew := mkResultUniverse us rOffset levelOne
   assignLevelMVar r.mvarId! rNew
   indTypes.mapM fun indType => do
     let type ← instantiateMVars indType.type

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
@@ -647,7 +647,7 @@ private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type :
   match r with
   | Level.mvar mvarId =>
     let us ← collectUniversesFromFields r rOffset fieldInfos
-    let rNew := mkResultUniverse us rOffset
+    let rNew := mkResultUniverse us rOffset levelZero
     assignLevelMVar mvarId rNew
     instantiateMVars type
   | _ => throwError "failed to compute resulting universe level of structure, provide universe explicitly"