It's also not clear that an h-m type system is what people want. For example, checking json inputs in gleam will always either be awkward or behind a "marshaller for me but not for thee" sort of inside-ball stuff, and the interface with other members of the beam ecosystem will be poor. It is possible to build a set theoretic type system without these problems, but I don't see these cases being handled by elixir's type system, either.