I couldn't find out if this was expected behavior for type in impl trait. Maybe someone can complement my knowledge on this unstable feature. 'Existential values' in particular are not discussed in the feature RFC or other documents I could turn up. However given a strong analogue to associated types, I'm assuming this code compiles, unintentionally.
mod b {
pub trait PtrSize {
const PtrSize: u16;
}
struct A;
impl PtrSize for A {
const PtrSize: u16 = core::mem::size_of::<usize>() as u16;
}
pub type Platform = impl PtrSize;
fn _internal() -> Platform {
A
}
}
fn main() {
let _: [u8; <b::Platform as b:: PtrSize>::PtrSize as usize] = [0; 8];
}
I expected to see this happen: The code fails to compile. The impl does not mention any bound or constraint on the value of the associated constant. The constant is thus not part of the explicit interface of the existential type Platform. It should be invalid to depend on the value of this constant in the manner within type equivalence checking. Compare this to the equivalent code of associated types:
mod a {
pub trait Iterator {
type Item;
}
struct A;
impl Iterator for A {
type Item = u8;
}
pub type T = impl Iterator;
fn _internal() -> T {
A
}
}
fn main() {
let _: <a::T as Iterator>::Item = 0u8;
/*
error[E0308]: mismatched types
--> src/main.rs:40:42
|
14 | pub type T = impl Iterator;
| ------------- the expected opaque type
...
40 | let _: <a::T as a::Iterator>::Item = 0u8;
| --------------------------- ^^^ expected associated type, found `u8`
| |
| expected due to this
|
= note: expected associated type `<T as a::Iterator>::Item`
found type `u8`
= help: consider constraining the associated type `<T as a::Iterator>::Item` to `u8` or calling a method that returns `<T as a::Iterator>::Item`
*/
}
Instead, this happened: the code compiles on some platforms, and fails type checking on others.
Meta
version: 1.75.0-nightly
(2023-11-06 189d6c71f3bb6c52113b)
Addendum
Besides the issue, it turns up a very peculiar question: should we have an 'impl'-like feature for constants outright? In particular in reference to a long-standing problem with SemVer / stability of const and const fn. The following doesn't 100% relate to the issue itself but explains my thoughts of reasoning on the differences between associated / constant type vs. value treatment by the compiler.
One could make the case that each constant declaration is akin to constraining the value type to a singleton value, in the form of a common canonical type for each particular comparable value. An existential value would instead treat this as a new type instead of the canonical one. (Still with an implied bound that allows those types in the constructor of arrays etc, let's not stretch it too far). Now the question is whether one could and should utilize the existing declaration to decide.
It's not quite clear what const fn is then doing under this analogy. Sure, functions are just relations of input values to output values but traits do not work as an analoge. Rust's type instances are for a single Self type and tuples are very ad-hoc for this equivalence.
const A: usize = const { B + C };
This would be solving a very complicated type equivalence, where B and C are known, and together determine the type of the result. The case of overflow can be covered by there not necessarily existing an instance of the mentioned operation families. Let's use as a notational framework the idea that operations are traits taking N additional arguments, and with an associated Output type. Then some canonical internal type (let's call it Termination) is utilized to denote the success operations by (not) providing an instance of the operation traits for it.
// Notational equivalence to the above.
type A = <Termination as Plus<B, C>>::Output;
Under the combined type-analogy, code blocks are just transitive closure of type resolution. And now obviously each of these results could be made existential instead. Note that const-fn declarations are just code blocks and thus, under this analogy, just transitive type resolution. Does this match our usual privacy intuition? It's usually that the body of a function is an implementation detail but here is clearly gets made into a public part of the declaration. That's a little more formalism around the above mentioned long-standing SemVer problem.
Aside: All said, I don't think it's possible, feasible, or desired to change any of the existing semantics of
const fn. What would it even be like to it into an 'existential' form? Keep in mind that even other constant declarations must not be able to observe the specific value of the result then. This includes failure to resolve further which would ruin the transitive translation of blocks. Unless the existential function result comes with its own set of additional guarantees.Maybe the surrounding scope should be able to observe the body? In a similar manner as const-computation in generic type parameters is allowed / declared as an input dependency? It seems cumbersome and that there should be some cute syntax just waiting to be discovered.
Isn't there some fundamental connection to different type equivalence and Extensional type theory here? (Or is it impredicative?)