Universe lint & `Ulift`

Stream: mathlib4

[Arien Malec]

I'm getting a "bad universe levels lint for ported code for Mathlib.Control.ULift` mathlib4#638

It's quite possible that the fix is to go through and set explicit universe annotations in all the ULift references & also possible that this is a false positive and I'm not clear on which...

[Arien Malec]

If I make all the references to ULift.up into ULift.up.{u} will that solve the lint?

[Mario Carneiro]

do you have a MWE? (Use #lint to run the linter yourself at the end of a file.)

[Arien Malec]

linting reveals zero issues with the code as is...

[Arien Malec]

I'll call runLinter explicitly.

[Arien Malec]

I believe the #mwe would be:

namespace ULift

variable {α : Type u} {β : Type v}

/-- Functorial action. -/
protected def map (f : α → β) (a : ULift α) : ULift β :=
  ULift.up (f a.down)

/-- Embedding of pure values. -/
@[simp]
protected def pure : α → ULift α :=
  up

/-- Applicative sequencing. -/
protected def seq {α β} (f : ULift (α → β)) (x : Unit → ULift α) : ULift β :=
  ULift.up (f.down (x ()).

/-- Monadic bind. -/
protected def bind (a : ULift α) (f : α → ULift β) : ULift β :=
  f a.down


instance : Monad ULift where
  map := @ULift.map
  pure := @ULift.pure
  seq := @ULift.seq
  bind := @ULift.bind

end ULift

[Arien Malec]

Again with runLinter locally lints pass.

[Arien Malec]

only happens in CI

[Mario Carneiro]

try #lint at the bottom of the file

[Mario Carneiro]

you have a syntax error on the seq definition

[Arien Malec]

At the end of the file.

[Mario Carneiro]

this shows the error:

import Std.Tactic.Lint
instance instMonadULift : Monad ULift.{u, v} := sorry
#lint checkUnivs

/- The `checkUnivs` linter reports:
THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS.  -/
-- Mathlib.Test
#check instMonadULift /- universes [u, v] only occur together. -/

[Arien Malec]

seq as defined typechecks...

The code as ported through mathlib3port was

/-- Applicative sequencing. -/
protected def seq (f : PLift (α → β)) (x : PLift α) : PLift β :=
  PLift.up (f.down x.down)

but this didn't match the type signature of seq so I added the explicit Unit → ULift α to match the signature and adjusted the call to fit.

[Mario Carneiro]

I didn't compile it but the seq you wrote above has unbalanced parentheses and a trailing dot

[Arien Malec]

Oops, cut n paste issue -- corrected above.

[Arien Malec]

Adding .up.{u} throughout removes the linting errors.

[Mario Carneiro]

Fixed on std4 master. Merge with mathlib4 master and then lake update on your branch to clear the CI error on your branch @Arien Malec

[Arien Malec]

Lints are breaking now...

[Arien Malec]

whole build breaks...

[Scott Morrison]

I merged master and it seems to compile fine, so I pushed.

[Scott Morrison]

and then merged.