Do Self Types make the Calculus of Inductive Constructions obsolete?
I'm not an expert in this work, but it seems to me that the major current issue is a lack of SN proof, even with restrictions. These proofs are notoriously tricky though, even when the calculus is correct, so I'd give it a little time. The work is certainly very promising.

One thing to note is that these restrictions are actually quite non-trivial to express, which is a large part of the complexity of the formulation of the inductive families in the CIC. The real selling point of an approach like this would be to concisely formulate these conditions.

It's been a somewhat longstanding open problem to have a dependently typed language which is


Consistent/Normalizing
Can express all the type families from Coq (or even Agda)
Allows for a simple expression of recursion over these families
Simple or has a small number of core constructions ($\Pi,\Sigma,\mu$).


One such attempt that I know of is the Altenkirch &amp; al $\Pi\Sigma$ language, which similarly lacks a full meta-theoretical study (and also isn't consistent without further restrictions).