> the presence of an implicit conversion rule `T -> T?` amounts to the observation that `T <: T?`, where <: is the subtyping relation
Not necessarily, because you might consider it acceptable for the implicit conversion to change the memory layout in this sense.
> I don't think any languages allow this
Plenty do, e.g. Rust's Option works that way.
> in any case disallowing nullability for unboxed types amounts to the observation that `P !<: P?`, where !<: is "does not subtype"
Saying the same thing with fancier words doesn't explain anything. The point is you can't simply treat non-nullable as a subtype of nullable in general, because this case exists.
Not necessarily, because you might consider it acceptable for the implicit conversion to change the memory layout in this sense.
> I don't think any languages allow this
Plenty do, e.g. Rust's Option works that way.
> in any case disallowing nullability for unboxed types amounts to the observation that `P !<: P?`, where !<: is "does not subtype"
Saying the same thing with fancier words doesn't explain anything. The point is you can't simply treat non-nullable as a subtype of nullable in general, because this case exists.