universe level not normalized in DecidableLT

Stream: lean4

[Jovan Gerbscheid]

When working on the @[to_dual] attribute, I ran into the problem that DecidableLT has type Sort (max 1 (u+1)). The way it gets pretty printed varies:

import Lean
open Lean

-- DecidableLT.{u} (α : Type u) [LT α] : Type u
#check DecidableLT

-- (α : Type u) → [inst : LT α] → Type (max 0 u)
run_meta logInfo m! "{(← getConstInfo ``DecidableLT).type}"

This is an issue because I want to define the dual DecidableGT/DecidableLT', but that one does live in the expected Type u.

I wrote a program to find more occurences of this

code

import Batteries
open Lean Meta
unsafe def findUnivs (e : Expr) : CoreM Unit :=
  let rec visitUnivs (u : Level) : CoreM Unit := do
    match u with
    | .max (.succ .zero) (.succ u)
    | .max (.succ u) (.succ .zero) => throwError "{u}"
    | .max u v
    | .imax u v => visitUnivs u; visitUnivs v
    | .succ u => visitUnivs u
    | _ => return
  let rec visit (e : Expr) : (StateT (PtrSet Expr) CoreM) Unit := do
    if (← get).contains e then
      return
    else
      match e with
      | .app f a         => visit f; visit a
      | .mdata _ b       => visit b
      | .proj _ _ b      => visit b
      | .letE _ t v b _  => visit t; visit v; visit b
      | .lam _ d b _     => visit d; visit b
      | .forallE _ d b _ => visit d; visit b
      | .const _ us      => liftM <| us.forM visitUnivs
      | .sort u          => liftM (visitUnivs u)
      | _                => return
  visit e |>.run' mkPtrSet
@[noinline]
def foo := unsafe findUnivs
namespace Batteries.Tactic.Lint
/-- A linter for commutativity lemmas that are marked simp. -/
@[env_linter]
def myLinter : Linter where
  noErrorsFound := "No error found"
  errorsFound := "Error found"
  test := fun declName => do
    let cinfo ← getConstInfo declName
    let type := cinfo.type
    _ ← unsafe findUnivs type
    return none
end Batteries.Tactic.Lint
universe u
abbrev DecidableLT' (α : Type u) [LT α] := DecidableRel (LT.lt : α → α → Prop)
#lint only myLinter in all

And here are the bad declarations it found in Lean/Batteries:

-- Batteries.Data.BinomialHeap.Basic
#check Batteries.BinomialHeap

-- Batteries.Data.PairingHeap
#check Batteries.PairingHeap

-- Init.Core
#check @Subtype.instDecidableEq

-- Init.Data.Array.Lemmas
#check @Array.swapAt!.eq_1

-- Init.Data.Array.QSort
#check @Array.qpartition.loop.eq_def✝

-- Init.Data.Vector.Lemmas
#check @Vector.insertIdx!.eq_1
#check @Vector.eraseIdx!.eq_1

-- Init.Prelude
#check NonemptyType
#check DecidableLT
#check DecidableLE

-- Init.WF
#check PSigma.skipLeft

-- Lean.Data.HashSet
#check HashSetBucket
#check HashSet

-- Lean.Data.SSet
#check SSet

[Eric Wieser]

Just to take #check out of the picture, inferType also reports the "clean" universe:

import Lean
import Qq
open Lean Qq

-- (α : Type u) → [inst : LT α] → Type u
run_meta do
  let u : Level := .param `u
  let e := q(@DecidableLT.{u})
  logInfo m!"{← Meta.inferType e}"