Misleading `Type` delaborator

Stream: lean4

[Eric Wieser]

This caught me by surprise:

-- for convenience, not part of the issue
import Qq.Macro
open Qq

run_cmd do
  let u := mkLevelParam `u
  let v := mkLevelParam `v
  let t1 : Expr := q(Sort (max (u+1) (v+1)))
  let t2 : Expr := q(Sort ((max u v)+1))
  Lean.logInfo m!"({t1} == {t2}) = {t1 == t2}"
-- (Type (max u v) == Type (max u v)) = false

My mental model was that delaborators should round trip up to Expr equality, not just to defeq; is this a reasonable model?

[Kyle Miller]

Ah, this is from the fact that the delaborator uses docs#Lean.Level.dec to decide whether to pretty print using Type or Sort.

I'm not sure there's a firm policy on universe levels for the pretty printer. It seems like it would be very hard to guarantee universe level equality when round tripping.

At least for expressions, I think it's the case that pretty printing yields equal expressions, modulo universe levels.