abby: add test DSL docs

[khyperia]

For context: see rust-lang/project-assumptions-on-binders#8 but there's been several more-specific issues filed since then, so, yeah.

r? @BoxyUwU

I forget if there's any abby tracking issue for writing docs? I don't think so. Anyway, there ought to be docs for this lil wonky nugget of a macro, so, I wrote some words.

I wasn't particularly careful about being extremely precise with my wording/terminology choices while writing this, so feel free to nitpick if something isn't technically correct. Hopefully is at least comprehensible/understandable though.

[tshepang]

these entries exist for renamed filenames to avoid broken links... yours should not need an entry since it's entirely new

View changes since the review

[BoxyUwU]

rust-lang/project-assumptions-on-binders#9 was a thing until I closed it the other day 😆

[BoxyUwU]

we elaborate them? :o

View changes since the review

[khyperia]

to be honest I don't actually know the technical word here, was kind of just hoping that the english word of elaboration is the same as the technical word. Like, for example, whatever is happening here:

trait Trait {
    type Assoc;
}

core::test_binder_constraints! {
    impl<T: Trait> {
        forall<'a> {
            for<> T::Assoc: 'a
        } expect {
            or {
                for<'b> T::Assoc: 'b,
                for<> T::Assoc: 'static,
            }
        }
    }
}

core::test_binder_constraints! {
    impl<T: Trait> {
        forall<'a> {
            predicates T::Assoc: 'a
        } expect {
            or {
                for<'b> T::Assoc: 'b,
                for<> T::Assoc: 'static,
                T: 'static // <-- new!
            }
        }
    }
}

[BoxyUwU]

hmm

[BoxyUwU]

I guess the vibes feel slightly off 🤔 we evaluate the goals and that gives us a list of region constraints that need to hold for the goal to hold. I wouldn't call that elaboration in casual coversation especailly since we have the separate term "elaboration" for things like turning T: Trait into T: Trait + Super and whatnot

[BoxyUwU]

I would maybe say like, "and as such are later evaluated resulting in a pile of region constraints and whatnot"

[bit-aloo]

The dsl is only available under assumptions-on-binders right? Is test_binder_constraints a subfeature of the parent abby feature?

Other than that, the doc was pretty intuitive and easy to follow. Thanks!

View changes since this review

[khyperia]

The dsl is only available under assumptions-on-binders right? Is test_binder_constraints a subfeature of the parent abby feature?

technically not! this technically passes:

//@ check-pass
#![feature(test_binder_constraints)]
core::test_binder_constraints! {
    impl<'a: 'b, 'b> {
        predicates 'a: 'b
    }
}

I believe that the only thing that -Zassumptions-on-binders does relative to the test framework is for the top-level default impl handling to use InferCtxtInner::solver_region_constraint_storage rather than InferCtxtInner::region_constraint_storage (as well as changes where predicates constraints get registered to). The test framework itself is hardcoded to use new-style constraints though.

So, yeah, while it is probably not particularly useful to use the test framework without -Zassumptions-on-binders, I haven't wired it to require it since we might change up flags in the future, change up features, and updating the test framework might get weird, or people might not realize the test framework doesn't actually depend on it. For example, if old and new style constraint storage merge, the flag would be significantly more useless for the test framework.