feat: infer Prop for inductive/structure when defining syntactic subsingletons

A `Prop`-valued inductive type is a syntactic subsingleton if it has at most one constructor and all the arguments to the constructor are in `Prop`. Such types have large elimination, so they could be defined in `Type` or `Prop` without any trouble, though users tend to expect that such types define a `Prop` and need to learn to insert `: Prop` manually.

Currently, the default universe for types is `Type`. This PR adds a heuristic: if a type is a syntactic subsingleton with exactly one constructor, and the constructor has at least one parameter, then the `inductive` command will prefer creating a `Prop` instead of a `Type`. For `structure`, we ask for at least one field.

More generally, for mutual inductives, each type needs to be a syntactic subsingleton, at least one type must have one constructor, and at least one constructor must have at least one parameter.

Thanks to @arthur-adjedj for the investigation in leanprover#2695.

Closes leanprover#2690

Author: kmill

src/Lean/Elab/Inductive.lean

@@ -425,9 +425,9 @@ 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) (preferProp : Bool) : Level :=
   if us.isEmpty && rOffset == 0 then
-    levelOne
+    if preferProp then levelZero else levelOne
   else
     let r := Level.mkNaryMax us.toList
     if rOffset == 0 && !r.isZero && !r.isNeverZero then
@@ -512,6 +512,22 @@ where
           for ctorParam in ctorParams[numParams:] do
             accLevelAtCtor ctor ctorParam r rOffset
 
+/--
+Heuristic: we prefer a `Prop` over `Type` if the inductive type could be a syntactic subsingleton.
+However, we prefer `Type` in the following cases:
+- if there are no constructors
+- if each constructor has no parameters
+-/
+private def isPropCandidate (indTypes : List InductiveType) : MetaM Bool := do
+  unless indTypes.foldl (fun n indType => max n indType.ctors.length) 0 == 1 do
+    return false
+  for indType in indTypes do
+    for ctor in indType.ctors do
+      let nparams ← forallTelescopeReducing ctor.type fun ctorParams _ => pure ctorParams.size
+      unless nparams == 0 do
+        return true
+  return false
+
 private def updateResultingUniverse (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) := do
   let r ← getResultingUniverse indTypes
   let rOffset : Nat   := r.getOffset
@@ -520,7 +536,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 (← isPropCandidate indTypes)
   assignLevelMVar r.mvarId! rNew
   indTypes.mapM fun indType => do
     let type ← instantiateMVars indType.type

src/Lean/Elab/Structure.lean

@@ -632,14 +632,21 @@ where
           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
 
+/--
+Heuristic: we prefer a `Prop` instead of a `Type` structure when it could be a syntactic subsingleton.
+However, if there are no fields, we prefer `Type`.
+-/
+private def isPropCandidate (fieldInfos : Array StructFieldInfo) : Bool :=
+  !fieldInfos.isEmpty
+
 private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type : Expr) : TermElabM Expr := do
   let r ← getResultUniverse type
   let rOffset : Nat   := r.getOffset
   let r       : Level := r.getLevelOffset
   match r with
   | Level.mvar mvarId =>
     let us ← collectUniversesFromFields r rOffset fieldInfos
-    let rNew := mkResultUniverse us rOffset
+    let rNew := mkResultUniverse us rOffset (isPropCandidate fieldInfos)
     assignLevelMVar mvarId rNew
     instantiateMVars type
   | _ => throwError "failed to compute resulting universe level of structure, provide universe explicitly"

tests/lean/run/2690.lean

@@ -0,0 +1,106 @@
+/-!
+# `Prop`-valued `inductive`/`structure` by default
+
+When the inductive types are syntactic subsingletons and could be `Prop`,
+they may as well be `Prop`.
+
+Issue: https://github.com/leanprover/lean4/issues/2690
+-/
+
+/-!
+Subsingleton, but no constructors. Type.
+-/
+inductive I0 where
+/-- info: I0 : Type -/
+#guard_msgs in #check I0
+
+/-!
+One constructor, has a Prop parameter. Prop.
+-/
+inductive I1 where
+  | a (h : True)
+/-- info: I1 : Prop -/
+#guard_msgs in #check I1
+
+/-!
+One constructor, no parameters. Type.
+-/
+inductive I2 where
+  | a
+/-- info: I2 : Type -/
+#guard_msgs in #check I2
+
+/-!
+Two constructors. Type
+-/
+inductive I3 where
+  | a | b
+/-- info: I3 : Type -/
+#guard_msgs in #check I3
+
+/-!
+Mutually inductives, both syntactic subsingletons,
+even if one doesn't have a constructor,
+and one has no parameters.
+-/
+mutual
+inductive C1 where
+inductive C2 where
+  | a (h : True)
+inductive C3 where
+  | b
+end
+/-- info: C1 : Prop -/
+#guard_msgs in #check C1
+/-- info: C2 : Prop -/
+#guard_msgs in #check C2
+/-- info: C3 : Prop -/
+#guard_msgs in #check C3
+
+/-!
+Type parameter (promoted from index), still Prop.
+-/
+inductive D : Nat → Sort _ where
+  | a (h : n = n) : D n
+/-- info: D : Nat → Prop -/
+#guard_msgs in #check D
+
+/-!
+Structure with no fields, Type.
+-/
+structure S1 where
+/-- info: S1 : Type -/
+#guard_msgs in #check S1
+
+/-!
+Structure with a Prop field, Prop.
+-/
+structure S2 where
+  h : True
+/-- info: S2 : Prop -/
+#guard_msgs in #check S2
+
+/-!
+Structure with parameter and a Prop field, Prop.
+-/
+structure S3 (α : Type) where
+  h : ∀ a : α, a = a
+/-- info: S3 (α : Type) : Prop -/
+#guard_msgs in #check S3
+
+/-!
+Verify: `Decidable` is a `Type`.
+-/
+class inductive Decidable' (p : Prop) where
+  | isFalse (h : Not p) : Decidable' p
+  | isTrue (h : p) : Decidable' p
+/-- info: Decidable' (p : Prop) : Type -/
+#guard_msgs in #check Decidable'
+
+/-!
+Verify: `WellFounded` is a `Prop`.
+-/
+inductive WellFounded' {α : Sort u} (r : α → α → Prop) where
+  | intro (h : ∀ a, Acc r a) : WellFounded' r
+/-- info: WellFounded'.{u} {α : Sort u} (r : α → α → Prop) : Prop -/
+#guard_msgs in #check WellFounded'