Why are type variables in `IsTrans α r` explicit?

Stream: mathlib4

[Kim Morrison]

It seems to me they ought to be implicit, as α is determined by r.

It is occasionally convenient that we can write e.g. IsTrans α (· ≤ ·). However we can still write IsTrans (α := α) (· ≤ ·) when this occurs

[Kim Morrison]

I started having a look at the fallout, but have other things that need to get done more urgently.

[Kim Morrison]

If anyone is interested in this, you could take a look at branch#algebra_classes_implicit and see if you can finish fixing things!

[Yaël Dillies]

I'm not sure making them implicit is a good thing since r is most often some polymorphic relation

[Kim Morrison]

Well, most often in the code it is actually some variable, e.g. r. It's true that IsTrans α (· ≤ ·) occurs frequently, but it is far from exclusive.

[Kim Morrison]

I'm not particularly bothered either way. I noticed this because it interacted badly with something on lean#4814, but this can /shouldbe fixed independently.