why dubious?

Stream: mathlib4

[Jireh Loreaux]

in mathlib#588, the following is marked as a dubious translation, but I don't understand why. I assume it has something to do with the _aux_param.

/- warning: sum.bind -> Sum.bind is a dubious translation:
lean 3 declaration is
  forall {e : Type.{v}} {α : Type.{u_1}} {β : Type.{u_2}}, (Sum.{v u_1} e α) -> (α -> (Sum.{v u_2} e β)) -> (Sum.{v u_2} e β)
but is expected to have type
  forall {e : Type.{v}} {α : Type.{_aux_param_0}} {β : Type.{_aux_param_1}}, (Sum.{v _aux_param_0} e α) -> (α -> (Sum.{v _aux_param_1} e β)) -> (Sum.{v _aux_param_1} e β)
Case conversion may be inaccurate. Consider using '#align sum.bind Sum.bindₓ'. -/

[Jireh Loreaux]

Should I just ₓ it?

[Scott Morrison]

I would not ₓ something like this, and just presume I know better than mathport...

[Mario Carneiro]

To answer the universe question specifically, no that's not the issue. (It was too annoying to make sure the universes were instantiated to use the same names, but it's actually matching modulo universe names behind the scenes, so you can find/replace _aux_param_0 -> u_1 and _aux_param_1 -> u_2 in the above)

[Scott Morrison]

So what is dubious about this translation?

[Mario Carneiro]

no idea, looks like a bug

[Kevin Buzzard]

Looks like this just came up again here.

[Kevin Buzzard]

And looks like it's been solved there too. It might actually be a dubious translation because the order of the universes might have changed