The proposed type system for Elixir doesn't run into Girard's paradox because it doesn't allow for impredicative polymorphism, which is where the paradox arises. The type system is based on set-theoretic types and includes a top type (the term() type), but it doesn't allow for types to be quantified over all types. As for adding features like dependent types or higher-order polymorphism, these would increase the type system's complexity and could potentially lead to issues like Girard's paradox. The authors don't discuss adding such features, so it's unclear how difficult it would be.