However, I think I figured out how to make it work. Here are some somewhat brief notes on how the system looks and an outline of the correctness proofs. The key is that asserting that everything is simply-typed from the get-go lets us be fairly reckless with carrying out some crazy hereditary substitutions that are not generally going to be fully dependently well-typed (because we at least know they will all normalize, thanks to the simple types), and just check, after the dust settles, that all the indices match up.
As a consequence the system has Πs powerful enough to abstract over even cyclically dependent collections of free unification variables that arise from examples like the one I posted here.
