Implement unification of const abstract impls

[JulianKnodt]

If two impls cover the entire set of possibilities:

i.e.

impl TraitName for Struct<true> {}
impl TraitName for Struct<false> {}

Then it would be expected that:

... <const N: usize> ... where Struct<{N > 1}>: TraitName {

Should compile.
This allows for such by generating a pseudo-impl for conditions which are exhaustive.

Since these impls will never be instantiated as is, it is fine to have a fake impl.

For now, this checks for a single bool condition, and whether both bool implementations are present.

Not sure who to r?but cc @BoxyUwU
Addresses rust-lang/project-const-generics#26

[rustbot]

r? @oli-obk

(rustbot has picked a reviewer for you, use r? to override)

[oli-obk]

I think you should not select any candidates in assemble_candidates_from_unified_impls, and instead of bailing out successfully here, actually go into confirmation. Confirmation can then generate obligations for all the variants of the enum/bool

[JulianKnodt]

So what you're saying is instead of 1 single fake candidates, generate a new obligation that looks for all candidates of the variants?

[oli-obk]

I think you'll still want one candidate, so that we first look for a single generic impl with the existing candidates, and if that fails, we process your new candidate in confirmation by requiring an obligation per variant

[JulianKnodt]

@oli-obk I've implemented a very sketchy version of what I think you're asking for. If this is the general idea, I'll clean it up and make it a bit more general, but please let me know if this is generally what you're thinking of.

[oli-obk]

I was hoping we could insert it unconditionally if the candidates list is empty after

rust/compiler/rustc_trait_selection/src/traits/select/candidate_assembly.rs

Lines 329 to 333 in dd12cd6

	// Auto implementations have lower priority, so we only
	// consider triggering a default if there is no other impl that can apply.
	if candidates.vec.is_empty() {
	self.assemble_candidates_from_auto_impls(obligation, &mut candidates);
	}

Did you try that?

[oli-obk]

I've been giving this scheme some thought. Instead of generating all possible variants and proving them, maybe we could let the trait solver handle such "questions". Basically you are asking the trait solver whether

• Type<X>: Trait can be satisfied (where X is a constant)
• which is basically for<const X: bool> Type<X>: Trait
• which gets turned into something like Type<PlaceholderConst>: Trait
• which we could then treat differently from Type<ParamConst> or Type<true> or Type<false>

When we try to prove that, we could add some special handling for that case that essentially makes a query to list all possible impls for Type<_> even if normally it would avoid trying to match inference vars against possible impls. Once we got the list of all impls that match (for bools there should be either one (a generic one) or two (one true and one false)). I'm not sure this works out, but we should probably explore it before going with a feature that just lists all values. Especially because the listing would get annoying for enums with values

[JulianKnodt]

I think this makes sense, as extending this to enums is also a pain. There are also cases which are inductive such as 0usize, and N.saturating_sub(1). Where would that kind of impl go?

As a counterpoint, this PR was meant to be a small part of this larger feature, but I think most use cases would be for bools and not enums with many variants.

[oli-obk]

I think most use cases would be for bools and not enums with many variants.

I'm not worried about enums with many variants. I was mainly thinking about an impl for None and one for Some(T).

I get that this is supposed to be a minimal impl, but I don't know if we should land a minimal impl if we are sure it's going to get removed entirely and replaced by a rewrite (fwiw: I don't think we are sure yet, but I also don't know if anyone'll have the capacity to work on my explorative alternative proposed above).

[JulianKnodt]

I can definitely make something which can have more cases added, but I am not entirely sure how to add something like that without explicit checks for certain traits. I've mostly been able to follow the trait selection documentation, since it mostly exists for candidate assembly, but beyond that point there isn't much.

Would it require building or refactoring a large part of the existing obligation system?

[oli-obk]

i don't believe so. but i also don't know how to implement it exactly. this would be more exploratory work.

we could do a sync session on eploring the existing implementation and coming up with more concrete ideas.

[bors]

☔ The latest upstream changes (presumably #105070) made this pull request unmergeable. Please resolve the merge conflicts.

[JulianKnodt]

@oli-obk this is the closest thing to what I think you want. For an exhaustive impl, it will add obligations for each implementation for a specific const, rather than exhaustively search for all of them. I didn't add ADTs yet, because I'm not entirely sure how to construct them from valtrees, but it's easy to fill in later.

[oli-obk]

For an exhaustive impl, it will add obligations for each implementation for a specific const, rather than exhaustively search for all of them

This is still the design you basically had originally. You are still iterating over the possible values of bool and i8.

[JulianKnodt]

For that, what I could do is push an additional candidate in assemble_candidates_from_impls, where I explicitly replace the predicate's Const that is either Unevaluated | Param with a PlaceholderConst, and then handle it similarly in confirm_impl_candidate as to how I'm handling consts currently in confirm_exhaustive_candidate. Ultimately the functionality will be the same (it will still have to exhaustively check types), but it will just be in the same function as the existing user specified impls. Is that more what you're thinking?

Ultimately, I don't think that checking exhaustively can be avoided, as ultimately there will need to be some check to see it is actually generic over all values.

[oli-obk]

My issue with this approach is that it creates a second exhaustiveness checker that

a) works very differently from the one we have (pattern exhaustiveness collects all patterns and fills out a matrix with the patterns that are there).
b) doesn't clearly allow us to migrate to a scheme that will reuse (or at least share code with) pattern exhaustiveness in the future
c) is "good enough", so if it lands, there is little incentive to remove all of it and create a better version in the future
d) can be emulated with specialization, so I don't think it's useful to have a new very unstable feature just for convenience

I'd be ok without reusing pattern exhaustiveness checking in an initial MVP that we can land, but the approach should be designed in a way that works as if we were using it.

I am very aware how painful that design would be to implement in the old solver, and I don't know how to implement it in the new solver without doing a deep dive myself.

Since it has been lost in the discussion and wasn't very well explained to begin with, I'll try to explain the high level steps that I think should be done, without exactly knowing how the steps can be done currently (they likely need some extra work, or may only work in the new solver)

if you have an predicate of the form SomeStruct<C>: Trait to prove, replace the const generic params with inference variables: SomeStruct<?42c>: Trait. Then ask the trait solver to collect all candidates that match that predicate. Now you got a list of impls or where bounds or other candidates. This means you are in a situation similar to pattern exhaustiveness checking. Only instead of patterns like Foo(BAR) you have types like SomeStruct<BAR>, or even SomeStruct<Some(BAZ)>. I don't know yet how to generalize exhaustiveness checking to allow you to plug in these types, but I'm sure we could figure that out. But we don't have to initially, we can just do a cheap version that works for booleans and field-less enums similarly to how you did it. Instead of creating obligations for all variants and proving them, you create a list of all the variants that the constant's type has, and then you remove all variants that were found. If there are no variants left, success, we are exhaustive, otherwise you can now report a single error similar to exhaustiveness checking informing the user about which variants are still missing.

[bors]

☔ The latest upstream changes (presumably #113393) made this pull request unmergeable. Please resolve the merge conflicts.

[lcnr]

I'd be ok without reusing pattern exhaustiveness checking in an initial MVP that we can land, but the approach should be designed in a way that works as if we were using it.

saw this PR because of #113393. Even when using pattern exhaustiveness checking and while being unstable, I would prefer to not currently experiment on this.

Having a kind of working, but not not-appropriate for stabilization, impl here will end up causing issues or conflict in the future. Having something that kinda works makes it harder to rework the surrounding code because we don't want to unnecessarily break peoples projects, even if unstable. It also causes bad vibes™ in the community if we do break it. This has happened when adding ConstEvaluatable checks for all constants while working towards the min_const_generics stabilization. From what I can tell we also have this issue with specialization and const_trait_impls.

There are a lot of subtle details here: e.g. should impl Trait<true> for u32 and impl<T> Trait<false> for T should allow us to assume for<const B: bool> u32: Trait<B> and how do we check that? This also interacts with how and whether we will consider the following impl to constrain const N: usize and therefore be valid: impl<const N: usize> Trait for Struct<{ Some(N) }>. I do not want to stabilize anything here until at least stabilizing generic_const_exprs, as the design of that will interact with this.

Any such involved changes to the type system should also require a t-types FCP before being landed, even if unstably.

[JulianKnodt]

@oli-obk ah, I finally understand what you're saying.
I agree with a) and b), and I'll continue to revise this PR until it's a version which reuses the existing exhaustiveness checker, in the old solver. I have no idea how the new solver works, but I'll cross that bridge if need be for this.
Whether c) is good or bad strongly depends on how forward thinking this feature should be, so I will defer to your judgement and try to make it adaptable for future checking. d) I strongly disagree with, as I find specialization to be a beast on its own, and its necessary to pull in significant type-fu to get things to compile, and they are difficult to transfer across library boundaries (but that's a personal preference on my end).

@lcnr I'll try to make this a more suitable version using exhaustiveness checking, but it seems that the methodology is not the issue, but that there are many unanswered questions about types. I'm not sure if this is a satisfying enough answer, but I think that this feature could be restricted to a subset of types, where the implementor must be a Adt, and have one or more const parameters. I view this as a common use case, and the other is inductive logic but I don't intend to handle that yet. Further down the line, more generic types could be considered, but I think there is a clear immediate use, and it's more murky how to handle much more complex types. I realize that reasoning looks a lot like min_const_generics and const_generics... which I hope is alright for this.

Since I don't understand all the minutiae of generic_const_exprs, I agree that this would have to be gated behind that (not sure if you meant stabilize as in merge or as in stable). My understanding of what you mean by constraining const N: usize in that specific case is that there may be an overlapping impl (i.e. impl Trait for Struct<2>) and thus N need not equal 2, but if it is the most conservative and prevents overlapping impls, is there an issue with that approach?

[bors]

☔ The latest upstream changes (presumably #114134) made this pull request unmergeable. Please resolve the merge conflicts.

[bors]

☔ The latest upstream changes (presumably #114781) made this pull request unmergeable. Please resolve the merge conflicts.

[tranquillity-codes]

Ping from triage, @JulianKnodt any updates on resolving the conflicts? Thanks

[JulianKnodt]

@tranquillity-codes
It's been a long time since I added this change, I also added a change to another repo which was created to mimic the trait solver, but that has gotten no reviews. Will this PR be reviewed if it's simply rebased?

[the8472]

Looks like it has been marked as waiting-for-author since #104803 (comment)

[compiler-errors]

I'm gonna go ahead and close this.

I think T-types is not really free at the moment to take on any major new const generic features, since we're busy working on revamping the base support for const generics (Boxy is leading all that wonderful work!). This PR has sat in an unresolved state for quite some time (sorry about that from the types side!), so I don't want to give the impression that this PR is still open for review sake.