is_basis has wonky type

Stream: general

[Kevin Buzzard]

is_basis : Π {ι : Type u_1} (R : Type u_3) {M : Type u_5}, (ι → M) → Π [_inst_1 : ring R] [_inst_2 : add_comm_group M] [_inst_5 : module R M], Prop

Is that OK? We ask for a type R, and then much later on we ask for the ring structure on R. I would have had the map iota -> M at the very end, and indeed the definition could probably easily be "fixed" by moving the variable order around in linear_algebra.basis. But does it matter?

[Eric Wieser]

If we care about this, a linter might be a good idea

[Eric Wieser]

It's very hard to know what order your variables are going to end up in without inserting #check all the time

[Eric Wieser]

I guess as a concrete example of a problem with that definition, (set_of (is_basis R) : set M) doesn't work without adding a lambda

[Mario Carneiro]

I don't think it matters. Certainly we haven't been very consistent about any particular ordering, although it's fairly common to have all the types and then all the instances and then other stuff

[Mario Carneiro]

Actually it does matter a bit in this case since the function is an explicit argument, which means if you use is_basis unapplied then R is inferred but not ring R

[Mario Carneiro]

I think we should at least keep typeclasses and implicit type arguments before explicit arguments

[Yury G. Kudryashov]

Unless we have (R : Type*) [ring R]