unused universe parameter

Stream: mathlib4

[Yury G. Kudryashov]

In !4#2312, I get an "unused universe parameter 'w'" error. Is it a linter that can be disabled?

[Yury G. Kudryashov]

The unused param is here on purpose: it says where to ULift the morphisms in a category.

[Kevin Buzzard]

Can you use it? I mean, add a .{w} or something?

[Yury G. Kudryashov]

Lean fails to compile the definition.

[Matthew Ballard]

I pushed a hacky "fix". (Sadly, I don't have a gif of me doing air quotes to go with this message.)

[Matthew Ballard]

Ability to toggle this error would be nice

[Yury G. Kudryashov]

Do you want to take over this PR? It has 1 "unused argument" linter error left.

[Matthew Ballard]

I can look at it again this evening. But I should get some official sanction for the “fix”

[Yury G. Kudryashov]

This will be given by a reviewer.

[Reid Barton]

It should have a porting note

[Matthew Ballard]

It is ready for review.

[Adam Topaz]

This is quite a hack...

def UliftHom.{w} (C : Type u) : Type u :=
  let _ := ULift.{w} C
  C

Is there really no way around this?

[Adam Topaz]

Do we not have some way to turn off the unused universe parameter linter?

[Matthew Ballard]

No it is in core

[Matthew Ballard]

But others will know better than me

[Adam Topaz]

sigh

[Adam Topaz]

I might be misunderstanding, but it seems that this is hardcoded and not a linter? Here is where this check is coming from:
https://github.com/leanprover/lean4/blob/cce2d3500e64ea0bfd56c46688e7aaeb1c4cb548/src/Lean/Elab/DeclUtil.lean#L77

[Matthew Ballard]

That is my understanding also

[Eric Wieser]

Is this worth opening a lean 4 issue about?

[Eric Wieser]

Then we have something to reference in a comment next to the hack

[Matthew Ballard]

Issue #2116