Our paper "Contextual Modal Type Theory with Polymorphic Context" is accepted for ESOP'23, woohoo! You can read the preprint from arxiv: https://arxiv.org/abs/1801.09225v2