function coercions in the stdlib

Stream: lean4

[Jason Gross]

Is there a reason the standard library doesn't have coercion instances such as

instance CoeArr {α β α' β'} [Coe α' α] [Coe β β'] : Coe (α → β) (α' → β') := { coe := λ f a => coe (f (coe a)) }

?

[Mario Carneiro]

I personally think it's better to be explicit about such things; it's also more work to unravel the coercions in simp or what have you

[Mario Carneiro]

Plus instances like this are an easy way to accidentally sneak transitivity into a typeclass that isn't supposed to be transitive

[Mario Carneiro]

(this is an issue that has bit us before in mathlib)

[Jason Gross]

I'd be fine with replacing Coe with CoeTC in all the places, and then the transitivity issue isn't a problem...