Fin as a coercion?

Stream: mathlib4

[Yury G. Kudryashov]

I think about adding a scoped instance

namespace NatCoeSort

scoped instance : CoeSort Nat Type where coe := Fin

It works with variables but doesn't allow one to write Matrix 2 2 Int. I can add an OfNat instance but Lean won't unfold it during parsing.

[Yury G. Kudryashov]

What should I do? Abandon this idea? Make the OfNat instance reducible and hope that Lean can see through it?

[Yury G. Kudryashov]

I do not suggest that we start writing i : n in random parts of the library. The suggested applications are arguments of the definitions like docs#Matrix and docs#MultilinearMap, where we build most of the theory about a type with a [Fintype] instance (BTW, should it be FinType?) but in most cases we apply it to Fin n.

[Jireh Loreaux]

I worry about abuse of this (like the one you mentioned), especially because throughout the matrix library we have variables like {n : Type _} [Fintype n], where i : n does make sense. Therefore I expect such abuse to be a bit hard for reviewers to catch at a glance. If it's also hard to get working, my opinion would be to abandon it.