Notation classes require Type

Stream: lean4

[Edward van de Meent]

I ran into an obstruction caused by the current (possibly unintentional) design of notation classes in core.
I'm defining a universe polymorphic inductive type for which i'd like to implement an instance of HAppend. However, my type lives in Sort (max (u + 1) v), and the fact that the class only takes Type x arguments means that i need to implemement two instances, one for the case where v is 0, and another for the case where v is 1+w for some w. Not only do i need to duplicate instances, it also means that i have to duplicate lemmas which make use of these instances!

To fix this, i'd like to propose to change all notation typeclasses to use Sort u.
What do people think? Any unforseen consequences?

[Yaël Dillies]

You can try, but I had tried back in Lean 3 (for exactly the same reason) and performance was poor

[Edward van de Meent]

so... after doing some preliminary experiments, i get errors like the following:

error: application type mismatch
  @HSub.hSub Nat
argument
  Nat
has type
  Type : Type 1
but is expected to have type
  Prop : Type

which seems to suggest that the kernel has builtin universe values for some of these classes?

[Edward van de Meent]

or maybe elaboration has trouble recognizing that the universe level changed?

[Aaron Liu]

Some Nat expr methods hardcode the universe level

[Aaron Liu]

Like docs#Lean.Nat.mkInstHSub, for example

[Edward van de Meent]

still, it surprises me that this would cause errors in these non-meta positions

[Aaron Liu]

What do you mean "non-meta position"?

[Edward van de Meent]

as in, the places of these errors seem to me like they should not need any special case meta handling

[Aaron Liu]

huh

[Edward van de Meent]

for example at docs#Nat.succ_le_succ the kernel complains about hAdd not being provided a correct level

[Aaron Liu]

maybe something about whnf

[Aaron Liu]

are you sure it was the kernel

[Aaron Liu]

and not the elaborator

[Edward van de Meent]

yea, the error started with (kernel)

[Edward van de Meent]

(i'm trying to build the current version right now, so i can't try things atm, but i will check again later)

[Edward van de Meent]

the specific error:

(kernel) application type mismatch
  @hAdd Nat
argument has type
  Type
but function has type
  {α β : Prop} → {γ : @outParam Prop} → [self : @HAdd α β γ] → α → β → γ

[Aaron Liu]

The expression for Nat.succ_le_succ contains a random n + 1 even though everywhere else it occurs it occurs as n.succ

[Aaron Liu]

I have no idea why this is, but I suspect if you fix all the nat expr builders it will not error

[Aaron Liu]

theorem Nat.succ_le_succ : ∀ {n m : Nat},
  @LE.le.{0} Nat instLENat n m → @LE.le.{0} Nat instLENat (Nat.succ n) (Nat.succ m) :=
fun {n m : Nat} (x : @LE.le.{0} Nat instLENat n m) =>
  let funType : {m : Nat} → @LE.le.{0} Nat instLENat n m → Prop := fun {m : Nat} (x : @LE.le.{0} Nat instLENat n m) =>
    @LE.le.{0} Nat instLENat (Nat.succ n) (Nat.succ m);
  @Nat.le.brecOn n (fun {m : Nat} (x : @LE.le.{0} Nat instLENat n m) => @funType m x) m x
    fun {m : Nat} (x : @LE.le.{0} Nat instLENat n m)
      (x_1 : @Nat.le.below n (fun {m : Nat} (x : @LE.le.{0} Nat instLENat n m) => @funType m x) m x) =>
    @Nat.succ_le_succ.match_1_1✝ n funType
      (fun (m : Nat) (x : @LE.le.{0} Nat instLENat n m)
          (h_below : @Nat.le.below n (fun {m : Nat} (x : @LE.le.{0} Nat instLENat n m) => @funType m x) m x) =>
        @LE.le.{0} Nat instLENat (Nat.succ n) (Nat.succ m))
      m x x_1 (fun (_ : Unit) => @Nat.le.refl (Nat.succ n))
      fun (m : Nat) (h : Nat.le n m)
        (h_1 : @Nat.le.below n (fun {m : Nat} (x : @LE.le.{0} Nat instLENat n m) => @funType m x) m h)
        (a : @funType m h) =>
      @Nat.le.step (Nat.succ n)
        (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
          (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
        a

[Floris van Doorn]

Edward van de Meent said:

I ran into an obstruction caused by the current (possibly unintentional) design of notation classes in core.

These design decisions are very intentional. They were different in Lean 2, at it caused universe issues.
Operations like Prod used to have type Sort u -> Sort v -> Sort (max 1 u v). One issue with that is that if you know that A \times B : Type and A : Type, you still don't know the type of B. That is the reason we now have Prod and PProd.

I don't expect you'll convince anyone from the Core team to change the sort of the notation classes. I think the more important question is why you have a type that lives in Sort (max (u + 1) v. Why don't just bump that up to Type (max u v)?

[Robert Maxton]

You can't always. Certainly I've lost entire weeks to Mathlib's Type bias for exactly this reason -- usually coupled with some other class that requires things be exactly the same universe level.