Set-theoretic type connectives with their native support for union, intersection, and negation have the potential to capture the idioms of dynamically typed languages like Erlang. We investigate whether this theoretical expressiveness translates into practice: does the resulting type solver remain tractable on real-world code? Can the type system reflect the programmer’s intention even though no principal types exist? And does it actually detect or avoid errors in real codebases? This paper reports on our experience on applying Etylizer, a set-theoretic type checker for Erlang, to its own implementation. We test whether the type system can express the patterns arising in a non-trivial Erlang codebase. In addition, we present a systematic comparison of design tradeoffs between Etylizer, eqWAlizer, and Dialyzer, examining how each tool handles exhaustiveness, function overloading, numeric precision, gradual typing, and occurrence typing. Our findings suggest that set-theoretic types are expressive enough to capture Erlang programmers’ intentions: intersection types and automatic exhaustiveness checking provide clear advantages, and the approach is not in conflict with Erlang’s let-it-crash idiom. Although the type system lacks principal types, types can be refined as needed through annotations. Scalability for typechecking is largely addressed, and in the cases where it remains an issue, less expressive tools face similar limitations.