Maybe it has "brutal practical cost", I don't know, but even most high-level languages don't have set-theoretic type systems. Perhaps because the approach is relatively new and most popular languages are old.