Idris has implicit parameters: https://idris2.readthedocs.io/en/latest/tutorial/miscellany....

As does Lean: https://lean-lang.org/lean4/doc/implicit.html

Would yours look different from those, or is it the same idea?

Thanks for the pointers. I'll read the details of these languages for inspiration.

To be clear, I'm not inventing anything here, I found out about implicits from scala.

Ah cool, I didn't realize Scala has them too!

I believe the Scala creators invented implicits, as an alternative to type classes that fit more naturally with an OOP language. They were later shown to be equivalent to type classes.

I love this. I too will never get around to this, but I’d definitely join you!

(I think propagating context up should be fine, but requires functions specialisation by call site).