feat: infer Prop for inductive/structure when defining syntacti…

…c subsingletons (#5517)

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`.

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. The motivation for
this restriction is that every inductive type starts with a zero
constructors and each constructor starts with zero fields, and
stubbed-out types shouldn't be `Prop`.

Thanks to @arthur-adjedj for the investigation in #2695 and to @digama0
for formulating the heuristic.

Closes #2690

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,31 @@ where
           for ctorParam in ctorParams[numParams:] do
             accLevelAtCtor ctor ctorParam r rOffset
 
+/--
+Decides whether the inductive type should be `Prop`-valued when the universe is not given
+and when the universe inference algorithm `collectUniverses` determines
+that the inductive type could naturally be `Prop`-valued.
+Recall: the natural universe level is the mimimum universe level for all the types of all the constructor parameters.
+
+Heuristic:
+- We want `Prop` when each inductive type is a syntactic subsingleton.
+  That's to say, when each inductive type has at most one constructor.
+  Such types carry no data anyway.
+- Exception: if no inductive type has any constructors, these are likely stubbed-out declarations,
+  so we prefer `Type` instead.
+- Exception: if each constructor has no parameters, then these are likely partially-written enumerations,
+  so we prefer `Type` instead.
+-/
+private def isPropCandidate (numParams : Nat) (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 cparams ← forallTelescopeReducing ctor.type fun ctorParams _ => pure (ctorParams.size - numParams)
+      unless cparams == 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 +545,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 numParams indTypes)
   assignLevelMVar r.mvarId! rNew
   indTypes.mapM fun indType => do
     let type ← instantiateMVars indType.type

src/Lean/Elab/Structure.lean

@@ -632,14 +632,27 @@ 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
 
+/--
+Decides whether the structure should be `Prop`-valued when the universe is not given
+and when the universe inference algorithm `collectUniversesFromFields` determines
+that the inductive type could naturally be `Prop`-valued.
+
+See `Lean.Elab.Command.isPropCandidate` for an explanation.
+Specialized to structures, the heuristic is that we prefer a `Prop` instead of a `Type` structure
+when it could be a syntactic subsingleton.
+Exception: no-field structures are `Type` since they are likely stubbed-out declarations.
+-/
+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/1074b.lean

@@ -1,4 +1,4 @@
-inductive Term
+inductive Term : Type
 | id: Term -> Term
 
 inductive Brx: Term -> Prop

tests/lean/etaStructIssue.lean

@@ -1,4 +1,4 @@
-inductive E where
+inductive E : Type where
   | mk : E → E
 
 inductive F : E → Prop

tests/lean/run/1074a.lean

@@ -1,4 +1,4 @@
-inductive Term
+inductive Term : Type
 | id2: Term -> Term -> Term
 
 inductive Brx: Term -> Prop

tests/lean/run/2690.lean

@@ -0,0 +1,111 @@
+/-!
+# `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 constructor parameters. Type.
+-/
+inductive I2 where
+  | a
+/-- info: I2 : Type -/
+#guard_msgs in #check I2
+
+inductive I2' (_ : Nat) where
+  | a
+/-- info: I2' : Nat → 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'