I remember a Luca Cardelli paper that explores a language with "type:type" and it contains a sentence roughly expressing: "even if the type system is not satisfying as a logic, it offers interesting possibilities for programming"