Considering detours on a couple of topics I've had on the list for a long time that 3 reminds me of. Specifically related to (1) implicits and (2) block structure syntax.
Conversation
Re. implicits, it might also be interesting to look into Agda's instance arguments, and the fork of OCaml that implements the modular implicits proposal. Along with the paper, I think there are a few blog posts floating around on the things those might let you do.
1
1
Would be interesting to compare the instance resolution algorithms - apparently Scala's instance resolution has subtleties that can make things confusing - ie. you are not sure what instance is being used, which Modular Implicits were intending to improve on.
Not sure how Agda's instance arguments compare on that front though. 🤔 agda.readthedocs.io/en/latest/lang
1