Why is it bad? Implicit integer conversions are generally bad because they can produce unexpected behavior at runtime and obstruct what’s really happening, but that doesn’t seem to be what’s happening here.
Never is a standard type in many languages and is at the bottom of the type hierarchy because it’s a subtype of every type. Never isn’t implicitly converted any more than `&’a A` is “implicitly converted” into a `&’b B`, where `’a` subsumes `’b`. There’s no runtime conversion because there will never be an instance of never—it represents the value of a computation that never completes by definition.
I think what you mean to say is that implicit runtime conversions are bad, not that all subtyping is bad.
Never is a standard type in many languages and is at the bottom of the type hierarchy because it’s a subtype of every type. Never isn’t implicitly converted any more than `&’a A` is “implicitly converted” into a `&’b B`, where `’a` subsumes `’b`. There’s no runtime conversion because there will never be an instance of never—it represents the value of a computation that never completes by definition.
I think what you mean to say is that implicit runtime conversions are bad, not that all subtyping is bad.