Extract a type from an explicit instance argument

Stream: new members

[cognivore]

I often find myself writing code like:

inductive I (T : Type) [Monad M] ...

It unwraps implicitly into I T M inst_monad.

Given concrete X, I can't call I X, because it needs a monad. So I need to write @I X Y my, where my captures monad instance for Y. I'm ok with it, but my intuition is that I can somehow write I (T : Type) (m : Monad M) and call I somehow in such way that Y is "inferred" from my?..

[Kevin Buzzard]

Just to clarify, is this Lean 4?

[Kevin Buzzard]

Why don't you make M explicit?