Specifying a universe parameter for an instance?

Stream: lean4

[Tanner Swett]

I've defined a structure Monoid.{u} which is a monoid at universe level u. If I want to define a coercion from Monoid.{u} to Type u, I can do this:

universe u
instance : CoeSort Monoid.{u} (Type u) where
  coe := Monoid.Elem

But how do I forego the universe u declaration there and specify the universe parameter explicitly? I've tried placing various numbers of .{u}s in various places, and I've also tried to find documentation on how to do it, but I haven't found anything that works yet.

[Kyle Miller]

Have you tried not including universe u and leaving everything else the same?

[Tanner Swett]

Yeah. That gives the error unknown universe level 'u' at both occurrences of u there.

[Kyle Miller]

Ok, I take it you're disabling auto-implicits?

[Kyle Miller]

I'm not at Lean at the moment, but if you want to be explicit about the universe variables, I believe it's instance {u} : CoeSort Monoid.{u} (Type u) or instance {u} instCoeSortMonoid : CoeSort Monoid.{u} (Type u) (i.e., you might need to name the instance for it to parse correctly)

[Tanner Swett]

Aha! Neither one of those exactly worked, but I took your second suggestion and rearranged it and that worked:

instance instCoeSortMonoidType.{u} : CoeSort Monoid.{u} (Type u) where
  coe := Monoid.Elem

[Tanner Swett]

And yeah, I do have auto-implicits off.

Actually, the above declaration gives a linter warning since I'm not using instCoeSortMonoidType anywhere else, so I did this to suppress the warning:

set_option linter.unusedVariables false in
instance instCoeSortMonoidType.{u} : CoeSort Monoid.{u} (Type u) where
  coe := Monoid.Elem

Not the prettiest thing ever, but I'll stick with it until I grow to hate it :big_smile:

[Eric Wieser]

What's the exact linter message you get without the suppression?

[Tanner Swett]

It's

unused variable `instCoeSortMonoidType` [linter.unusedVariables]

[Scott Morrison]

That seems wrong?