fix : only default to Prop for structures

Author: arthur-adjedj

src/Lean/Elab/Inductive.lean

@@ -419,13 +419,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
 
@@ -446,6 +446,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   =>
@@ -513,7 +514,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

src/Lean/Elab/Structure.lean

@@ -644,7 +644,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"