In case anyone's still interested, Atze Dijkstra and I have come up with an alternative approach to implementing this which requires changing much fewer moving parts. The idea is to internally regard `type MySyn a = T[_, a, _]` as `type MySyn w1 w2 a = T[w1, a, w2]`, recording in `SynTyCon` that we'll need to synthesize 2 wildcard argument; then, during typechecking of occurrences, `MySyn` gets expanded into `MySyn _ _`. This is basically a simplified version of what languages with implicit parameters do -- in Agda syntax, we'd have MySyn : {w1 : Type} {w2 : Type} (a : Type) -> Type and the application `MySyn A` is short-hand for `MySyn {w1 = _} {w2 = _} A`. Of course, for a robust implementation, we can't just put all these implicit parameters up front, because they can form a telescope with other parameters; but, because type synonym applications need to be saturated anyway, I think even that could be implemented without complicated impredicativity decisions, simply by storing a bit more than just a single natural number as the extra info in `SynTyCon`.