I only skimmed the paper, but how do holes in the type system differ from e.g. `!` in Rust or `never` in TypeScript?