A bit unrelated, but the other day I noticed Rust also has higher rank *constraints* (e.g. for<'a> &'a T: Send) but only for lifetimes, not types. AFAIK, even Haskell doesn't have this, although you can emulate it
people have been working on in GrTT - which integrates some of their fancy graded modal stuff with dependent type systems… not sure if that is useful at all for first class module systems.