I stand by my non-response in that I’m not about to get involved in a detailed discussion here. But I just wanted to point out that with:
(soundness and principality); Leo says they do, but no one else knows
I think soundness is generally accepted as not really an issue – they basically elaborate into existing OCaml constructs. It is on principality, and more generally on similar properties of the inference itself where things are less clear.