diff --git a/text/0195-associated-items.md b/text/0195-associated-items.md index 0a76c63d5fc..c17018b580e 100644 --- a/text/0195-associated-items.md +++ b/text/0195-associated-items.md @@ -882,6 +882,7 @@ trait Foo { type Output1; type Output2; lifetime 'a; + const C: bool; ... } ``` @@ -894,6 +895,7 @@ T: Foo T: Foo T: Foo T: Foo>(t: T) // this is valid fn consume_obj(t: Box>) // this is NOT valid // but this IS valid: -fn consume_obj(t: Box::N] = [0u8; ::N + ::N]; - let x: [u8; ::N + 1] = [0u8; 1 + ::N]; - // Still not allowed. - let x: [u8; ::N + 1] = [0u8; ::N + 1]; - // Workaround for the expression above. - const N_PLUS_1: usize = ::N + 1; - let x: [u8; N_PLUS_1] = [0u8; N_PLUS_1]; - // Neither of the following are allowed. - const ALIAS_N_PLUS_1: usize = N_PLUS_1; - let x: [u8; N_PLUS_1] = [0u8; ALIAS_N_PLUS_1]; - const ALIAS_N: usize = ::N; - let x: [u8; ::N] = [0u8; ALIAS_N]; - ``` +If the value of an associated const depends on a type parameter (including +`Self`), it cannot be used in a constant expression. This restriction will +almost certainly be lifted in the future, but this raises questions outside the +scope of this RFC. # Staging @@ -1471,97 +1414,31 @@ on implementation concerns, which are not yet clear. ## Generic associated consts in match patterns It seems desirable to allow constants that depend on type parameters in match -patterns, but it's not clear how to do so. - -Looking at the `HasVar` example above, one possibility would be to simply treat -the first, forbidden match expression as syntactic sugar for the second, allowed -match expression that uses a pattern guard. This is simple to implement because -one can simply ignore the constant when performing exhaustiveness and -reachability checks. Unfortunately, this approach blurs the difference between -match patterns (which provide strict checks) and pattern guards (which are just -useful syntactic sugar), and it does not increase the expressiveness of the -language. - -An alternative would be to allow `where` clauses to place constraints on -associated consts. If an associated const is known to be equal/unequal to some -other value (or in the case of integers, inside/outside a given range), this can -inform exhaustiveness and reachability checks. But this requires more design and -implementation work, and more syntax. +patterns, but it's not clear how to do so while still checking exhaustiveness +and reachability of the match arms. Most likely this requires new forms of +where clause, to constrain associated constant values. For now, we simply defer the question. ## Generic associated consts in array sizes -The above solution for type-checking array sizes is somewhat unsatisfactory. In -particular, it is counter-intuitive that neither of the following will type -check: +It would be useful to be able to use trait-associated constants in generic code. ```rust // Shouldn't this be OK? const ALIAS_N: usize = ::N; let x: [u8; ::N] = [0u8; ALIAS_N]; -// This is likely to yield an embarrassing error message such as: -// "couldn't prove that `::N + 1` is equal to `::N + 1`" -let x: [u8; ::N + 1] = [0u8; ::N + 1]; -``` - -A function like this is especially affected: - -```rust -trait HasN { - const N: usize; -} -fn foo() -> [u8; ::N + 1] { - // Can't be verified to be correct for the return type, and can't use the - // intermediate const workaround due to scoping issues. - [0u8; ::N + 1] -} +// Or... +let x: [u8; T::N + 1] = [0u8; T::N + 1]; ``` -This can be worked around with type-level naturals that use associated consts to -produce array sizes, but this is syntactically a bit inelegant. +However, this causes some problems. What should we do with the following case in +type checking, where we need to prove that a generic is valid for any `T`? ```rust -// Assume that `TypeAdd` and `One` are from a type-level naturals or similar -// library, and that `NAsTypeNatN` provides some way of translating the `N` -// on a `HasN` to a type compatible with that library. -trait HasN { - const N: usize; - type TypeNatN; -} -fn foo() -> [u8; TypeAdd<::TypeNatN, One>::AsUsize] { - // Because the type `TypeAdd<::TypeNatN, One>` can be verified to be - // equal to itself in type checking, we know that the associated const - // `AsUsize` below must be the same item as the `AsUsize` mentioned in the - // return type above. - [0u8; TypeAdd<::NAsTypeNat, One>::AsUsize] -} +let x: [u8; T::N + T::N] = [0u8; 2 * T::N]; ``` -There are a variety of possible ways to address the above issues, including: - - - Implementing smarter handling of consts that are just aliases of other - constant items. - - Allowing `where` clauses to constrain some associated constants to be equal, - to other expressions, and using this information in type checking. - - Adding normalization with little or no awareness of arithmetic (e.g. allowing - expressions that are exactly the same to be considered equal, or using only - a very basic understanding of which operations are commutative and/or - associative). - - Adding new syntax and/or new capability to plugins to allow type-level - naturals to be used with more ergonomic and clear syntax. - - Implementing a dependent type system that provides built-in semantics for - integer arithmetic at the type level, rather than implementing this in an - external or standard library. - - Using a full-fledged SMT solver. - - Some other creative solutions not on this list. - -While there are many ways to improve on the current design, and many of these -approaches are not mutually exclusive, much more work is needed to investigate -and implement a self-consistent, effective, and ideally intuitive set of -solutions. - -Though admittedly not very satisfying at the moment, the current approach has -the advantage of being (arguably) a good minimalist design, allowing associated -consts to be used for array sizes in generic code now, but also allowing for any -of a number of improved systems to be implemented later. +We would like to handle at least some obvious cases (e.g. proving that +`T::N == T::N`), but without trying to prove arbitrary statements about +arithmetic. The question of how to do this is deferred.