Another useful property we could test here when we fix the issue about is_subtype_of and non-fully-static types is that a non-fully-static type never participates in subtyping. (This assumes that we add Type::is_fully_static so we can check this predicate.)

Added as a task in #14524

I find the macro fairly hard to read. What I understand is that their primary benefit is to reduce the repetition of creating the cached db and dereferencing it.

• How much faster is reusing the db over creating a new database?
• Have you considered adding a snapshot method to the database instead of locking it? Databases are thread safe and can be shared (for as long as you don't update the db with a &mut Db reference

        pub fn snapshot(&self) -> Self {
            Self {
                storage: self.storage.clone(),
                files: self.files.snapshot(),
                system: self.system.clone(),
                vendored: self.vendored.clone(),
                events: Arc::clone(&self.events),
            }
        }

A test then becomes

    #[test]
    #[quickcheck_macros::quickcheck]
    fn equivalent_to_is_reflexive2(t: crate::types::tests::Ty) -> bool {
        let db = get_cached_db();
        let t = t.into_type(&db);
        t.is_equivalent_to(&db, t)
    }

Which I don't find too bad

How much faster is reusing the db over creating a new database?

Three orders of magnitude. It's essential. I found some bugs only after I added this optimization.

• Have you considered adding a snapshot method to the database instead of locking it

I have not. Would the benefit be to get rid of the let db = &*db;, or do you think that would be faster?

I find the macro fairly hard to read

Because macros are hard to read, or because this particular macro is hard to read? 😄

I don't disagree, but it's also not like we're hiding lots of complexity in there. It's really just a boilerplate-reduction macro. I personally care much more about the readability of the individual tests. The macro is ugly, yes. But I won't have to read the macro code again when writing new tests.

A test then becomes [...] Which I don't find too bad

Well, you picked the easiest example there ;-). With just one type and no logical implication. Did you see the macro-vs-non-macro comparison in the PR description? Or this example, which has three types:

#[quickcheck]
fn subtype_of_is_transitive(s: Ty, t: Ty, u: Ty) -> bool {
    let db = get_cached_db();
    let db = &*db;
    let s = s.into_type(db);
    let t = t.into_type(db);
    let u = u.into_type(db);

    !(s.is_subtype_of(db, t) && t.is_subtype_of(db, u)) || s.is_subtype_of(db, u)
}

type_property_test!(
    subtype_of_is_transitive,
    db,
    (s, t, u),
    s.is_subtype_of(db, t) && t.is_subtype_of(db, u) => s.is_subtype_of(db, u)
);

their primary benefit is to reduce the repetition of creating the cached db and dereferencing it

It also removes the necessity for lots of let t = t.into_type(db); lines, and allows us to write logical implications using premise => conclusion instead of !(premise) || (conclusion).

Let me know what you think. I'm going to be okay if we remove it again 😄.

I have not. Would the benefit be to get rid of the let db = &*db;, or do you think that would be faster?

It would allow you to remove the mutex guard and the deref (you still need to use &db when calling any function)

Because macros are hard to read, or because this particular macro is hard to read? 😄

It's somewhat both. I had to expand the macro to understand what the different parts map to. Like what's up with the (s, t, u)? which part is even the assertion? Some extra documentation might help.

Did you see the macro-vs-non-macro comparison in the PR description? Or this example, which has three types:

I admit, I did not! I see how it simplifies the code a bit, but it doesn't significantly reduce the number of lines.

Could we implement into_type for tuples so that you can keep writing (s, t, u) = (s, t, u).into_types(db)?

It also removes the necessity for lots of let t = t.into_type(db); lines, and allows us to write logical implications using premise => conclusion instead of !(premise) || (conclusion).

I do like that. Maybe we can limit the macro part to just that?

I'm not opposed to keeping the macros. I just had to expand them, and I still spent about 5 minutes trying to figure out what was going on. But I'm also not sure if it's worth it if you spend more time on it.

Like what's up with the (s, t, u)? which part is even the assertion?

These are valid concerns. I now pushed another commit where I change the syntax to the following:

type_property_test!(
    subtype_of_implies_assignable_to, db,
    forall types s, t. s.is_subtype_of(db, t) => s.is_assignable_to(db, t)
);

The intention is that it reads like a mathematical property ∀ S, T. ….

I also simplified the macro definition (only two clauses instead of four), clarified the variable names and added some documentation.

I kind of like how this looks, and would merge it for now. I'm happy to revisit it though if I get more feedback on it (from you or others).

It would allow you to remove the mutex guard and the deref (you still need to use &db when calling any function)

I'll note it down as a task for me (low priority), thanks.

Thanks. I like this much more!