Been thinking recently: Could variable captures be considered as coeffects?
(\x => \y => x) : a -> b -> a
(\x => \y =(x)=> x) : a -> b -> a
(\y => x) : error!
(\y =(x)=> x) : b -(a)-> b
Kind of reminds me of capture lists in C++ 🤔
Conversation
Also reminds me of how you can index data types with the context when making well-typed interpreters in dependently typed languages. See: docs.idris-lang.org/en/latest/tuto