structure sometimes makes a Type not a Prop.

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Structures which should be Props (because all their fields are Props) sometimes come out as Types and Lean needs to be explicitly told that they are Props.

Steps to Reproduce

structure foo (α : Type) where
  h : ∀ a : α, a = a

#check foo Nat -- Type?!

structure foo' (α : Type) : Prop where
  h : ∀ a : α, a = a

#check foo' Nat -- Prop, as expected

Expected behavior:

foo α : Prop

Actual behavior:

foo α : Type

Versions

This bug has existed since Lean 3 and the community has been using the obvious workaround for years ("when you randomly notice an instance of this, typically because a new user is confused on Zulip, just tell the structure that it's a Prop explicitly")

[Output of lean --version in the folder that the issue occured in]

Lean (version 4.2.0-rc1, commit a62d2fd, Release)

[OS version]

Ubuntu 22.04

Impact

Very minor, occasionally confusing, little more than annoying once you know about it.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[arthur-adjedj]

Looking into the related implementation, this seems to be an intended design decision and not a bug. In particular, some classes such as Decidable and IsNeutral make use of the fact that the universe infered is Type. This issue probably deserves to be tagged as an RFC.

[digama0]

Decidable would not infer Prop type, and it's not a structure in the first place. IsNeutral can and should be a Prop.

Looking into the related implementation, this seems to be an intended design decision and not a bug.

I don't see how you can read intentionality into that uncommented code. Certainly this is the function that would need to be changed and it does not do what is suggested in this issue, but there is no indication that this is a deliberate design or that it is not written in this way to avoid a certain other issue.

[arthur-adjedj]

I first experimented with having the same rules apply to both inductives and inductives (it was also easier to do so since they shared the same bit of code), IsNeutral is composed with an Option here, hence the need to either have it in Type, or lift the universe it. I didn't experiment further down that path, but assumed other such issues would come up.

I don't see how you can read intentionality into that uncommented code.

That bit of code seems to have been made with the purpose of making things live in Type as a fallback. If it didn't, the code could simply be Level.mkNaryMax us.toList |>.normalize here, hence why I assumed it was a thought out decision.

[digama0]

Things should live in Type as a fallback. But the fallback doesn't need to be taken if there is <= 1 constructor and all the constructor arguments are Props or recursive, since then it would be a large eliminating type even if it lived in Prop.

[arthur-adjedj]

That was my reasoning as well, but that would change not only the type of structures, but also of a lot of inductives, so I'm hesitant on doing that.

[digama0]

IsNeutral is composed with an Option here, hence the need to either have it in Type, or lift the universe it. I didn't experiment further down that path, but assumed some other issues would come up.

I'm inclined to lift the universe using Nonempty there. The impact is relatively minimal, but it is sufficiently unrelated to the PR that it might be worth doing separately.