Your description of a monad comprehension in Idris reminds me of computation expressions in F#[1]. Looks like I have one more programming language to dive into!
[1] https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...
[1] https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...