class is Type not Prop

Stream: lean4

[Kevin Buzzard]

Am I right in thinking that

class IsAddRightCancel (A : Type u) [Add A] where
  add_right_cancel (a b c : A) : a + b = c + b → a = c

variable (A : Type) [Add A]
#check IsAddRightCancel A -- Type

should really be a Prop? I think that Lean 3 made it a Type as well. You can explicitly tell it otherwise and it works:

class IsAddRightCancel' (A : Type u) [Add A] : Prop :=
  add_right_cancel (a b c : A) : a + b = c + b → a = c

#check IsAddRightCancel' A -- Prop

Beginners who don't know about this trick in Lean 3 sometimes accidentally make Types instead of Props this way.

[Mario Carneiro]

Should we use mathlib4 issues to build up wishlist features like this that can plausibly be implemented in mathlib instead of lean 4?

[Mario Carneiro]

(in this case, I mean defaulting classes whose members are propositions to Prop instead of Type*)

[Mario Carneiro]

From the type theory point of view, you have to specify the target type and for a class like this it will work for Prop or any Type v

[Mario Carneiro]

It has to do with the fact that it's an inductive type, it's underdetermined in the same way as the type nat is not determined in this recursive definition:

meta def foo : nat := foo

[Mac]

Why should it be a Prop rather than a Type? What benefits does that provide?

[Mac]

Given that it defaults to and instance of Type and most utility classes in Lean deal with instances of Type, It would seem most logical to keep it that way unless there is a compelling reason it should be a Prop.

[Kevin Buzzard]

My instinct is that type-valued typeclasses are far more prone to causing diamond issues but I don't know if that would be the case here

[Mario Carneiro]

Unless it makes the projections noncomputable, it is generally better to have a Prop than a Type when there is only one inhabitant because you get proof irrelevance, meaning that diamond issues go away entirely