Comment by kibwen
6 hours ago
Let's avoid using the term "subtyping", which as you say is irrelevant here. The reason you need diverging functions to satisfy arbitrary type obligations (i.e. to coerce to any other type) is because otherwise anything as simple as `let x = Some(42); x.unwrap();` just completely fails to compile, because `unwrap` is internally just:
fn unwrap<T>(t: Option<T>) -> T {
match t {
Some(foo) => foo,
None => panic!()
}
}
...and this function couldn't otherwise typecheck because it doesn't return a `T` in the `None` branch. You need coercion here.
No you don’t need coercion. You only need polymorphism. The type of `panic!()` could be an arbitrary U, which unifies just fine with the type T here.
Generally languages with such polymorphism have a never type only because they don’t also support impredicative polymorphism.
And then once you have `fn foo<T>() -> T`, what do you write in the body that allows it to typecheck?