Type mismatch in salsa-generated code

[lnicola]

CC #8961

pub trait Database {}

pub trait QueryGroup: Sized {
    type DynDb: ?Sized + Database + HasQueryGroup<Self>;
}

pub trait HasQueryGroup<G>: Database
where
    G: QueryGroup,
{
}

trait HelloWorld: HasQueryGroup<HelloWorldStorage> {
    fn length(&self);
}

struct HelloWorldStorage;
impl QueryGroup for HelloWorldStorage {
    type DynDb = dyn HelloWorld;
}

fn __shim(_db: &(dyn HelloWorld + '_)) {}

impl<DB> HelloWorld for DB
where
    DB: Database,
    DB: HasQueryGroup<HelloWorldStorage>,
{
    fn length(&self) {
        __shim(self); // Expected &dyn HelloWorld, got &DB
    }
}

[lnicola]

Updated with a self-contained repro, but it's still pretty convoluted. And I could swear I've done this before 😕.

[flodiebold]

Thanks for the minimization -- I looked into this a bit and it looks like a Chalk problem where it on the one hand correctly determines that DB: Database from the environment, but then it also tries to use QueryGroup::DynDb: Database to prove the same thing and gets an ambiguous result from that, so the whole thing is ambiguous. In another case I looked at (one of the few that weren't inside Salsa-generated code) it was similar, but while trying to prove DB: Sized. We'll probably need a Chalk reproduction.

[iDawer]

I did log with CHALK_DEBUG=info CHALK_PRINT=1 issue_9990.log but it does not give the full program dump 🤔 (Is this possible?)

So I wrote it by myself, not sure it reflects ra's vision of the example precisely:

#[test]
fn coerce_ra_issue_9990() {
    test!(
        program {
            #[object_safe]
            #[lang(sized)]
            trait Sized {}
            #[object_safe]
            #[lang(unsize)]
            trait Unsize<T> {}
            #[object_safe]
            #[lang(coerce_unsized)]
            trait CoerceUnsized<T> {}

            impl<T, U> CoerceUnsized<&'static U> for &'static T where T: Unsize<U> {}

            #[object_safe]
            trait Database {}

            #[object_safe]
            trait QueryGroup
            where
                Self: Sized,
            {
                type DynDb: Database + HasQueryGroup<Self>;
            }

            #[object_safe]
            trait HasQueryGroup<G>
            where
                Self: Database,
                G: QueryGroup,
                G: Sized,
            { }

            #[object_safe]
            trait HelloWorld
            where
                Self: HasQueryGroup<HelloWorldStorage>,
            { }

            struct HelloWorldStorage {}

            impl QueryGroup for HelloWorldStorage {
                type DynDb = dyn HelloWorld + 'static;
            }
            impl<DB> HelloWorld for DB
            where
                DB: Database,
                DB: HasQueryGroup<HelloWorldStorage>,
                DB: Sized,
            { }
        }

        goal {
            exists<T> {
                if (FromEnv(T: Database); FromEnv(T: HasQueryGroup<HelloWorldStorage>); FromEnv(T: Sized)) {
                    &'static T: CoerceUnsized<&'static dyn HelloWorld + 'static>
                }
            }
        } yields {
            "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: !1_0: 'static }]"
        }
    );
}

(Note: ra marks all traits #[object_safe], seems not relevant here.)

This test fails with Ambiguous; no inference guidance. Changing the quantifier to forall fixes it.

Hmm, after some playing I'm even more in doubt of it's precision: removing DB: Database bound from the original rust example makes ra stop complaining, but removing that plus FromEnv(T: Database) from the Chalk program has no effect, the test is still failing.

[lnicola]

Note: ra marks all traits #[object_safe], seems not relevant here.

Well, that's not really surprising: https://github.com/rust-analyzer/rust-analyzer/blob/ae36af2bd43906ddb1eeff96d76754f012c0a2c7/crates/hir_ty/src/chalk_db.rs#L288-L291

[flodiebold]

I think the example can be simplified further by getting rid of CoerceUnsized; just trying to solve T: HelloWorld should be enough to reproduce it.

[iDawer]

just trying to solve T: HelloWorld should be enough to reproduce it.

simplified

test!(
    program {
        #[upstream]
        #[non_enumerable]
        #[lang(sized)]
        trait Sized {}

        #[non_enumerable]
        #[object_safe]
        trait Database {}

        #[non_enumerable]
        trait QueryGroup
        where
            Self: Sized,
        {
            type DynDb: Database + HasQueryGroup<Self>;
        }

        #[non_enumerable]
        #[object_safe]
        trait HasQueryGroup<G>
        where
            Self: Database,
            G: QueryGroup,
            G: Sized,
        { }

        #[non_enumerable]
        #[object_safe]
        trait HelloWorld
        where
            Self: HasQueryGroup<HelloWorldStorage>,
        { }

        struct HelloWorldStorage {}

        impl QueryGroup for HelloWorldStorage {
            type DynDb = dyn HelloWorld + 'static;
        }
        impl<DB> HelloWorld for DB
        where
            DB: Database,
            DB: HasQueryGroup<HelloWorldStorage>,
            DB: Sized,
        { }
    }

    goal {
        exists<T> {
            if (FromEnv(T: Database); FromEnv(T: HasQueryGroup<HelloWorldStorage>); FromEnv(T: Sized)) {
                T: HelloWorld
            }
        }
    } yields[SolverChoice::slg_default()] { // fails: "Ambiguous; no inference guidance"
        "Unique"
    } yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
        "Unique"
    }

    goal {
        exists<T> {
            if (FromEnv(T: Database); FromEnv(T: HasQueryGroup<HelloWorldStorage>); FromEnv(T: Sized)) {
                T: Database
            }
        }
    } yields[SolverChoice::slg_default()] { // ok
        "Unique"
    } yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
        "Unique"
    }

    goal {
        exists<T> {
            if (FromEnv(T: Database); FromEnv(T: HasQueryGroup<HelloWorldStorage>); FromEnv(T: Sized)) {
                HelloWorldStorage: Sized
            }
        }
    } yields[SolverChoice::slg_default()] { // ok
        "Unique"
    } yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
        "Unique"
    }
);

[iDawer]

Also the queries differ. Chalk test's query looks like this:

[tests/test/mod.rs:266] &peeled_goal = UCanonical {
    canonical: Canonical {
        value: InEnvironment {
            environment: Env([
                for<> FromEnv(^1.0: Database),
                for<> FromEnv(^1.0: HasQueryGroup<HelloWorldStorage>),
                for<> FromEnv(^1.0: Sized)
            ]),
            goal: Implemented(^0.0: HelloWorld),
        },
        binders: [U0 with kind type],
    },
    universes: 1,
}

But the RA query uses !0_1:

UCanonical {
    canonical: Canonical {
        value: InEnvironment { 
            environment: Env([
                for<> FromEnv(!0_1: Database), 
                for<> FromEnv(!0_1: HasQueryGroup<HelloWorldStorage<[]>>), 
                for<> FromEnv(!0_1: Sized)
            ]), 
            goal: Implemented((&'static !0_1): CoerceUnsized<(&'static dyn for<type> [for<> Implemented(^1.0: HelloWorld)] + 'static)>) 
        }, 
        binders: [],
    }, 
    universes: 1,
}

Is this query correct? In for<> FromEnv(!0_1: Database) the !0_1 placeholder is not defined in the innermost binder.

[flodiebold]

Yes, the test doesn't match the Rust code -- the equivalent of a type parameter DB would be a forall<DB>, not exists.

You can simplify the Rust version further as well by turning

fn __shim(_db: &(dyn HelloWorld + '_)) {}

into something like

fn __shim<T: HelloWorld>(_db: &T) {}

. I think it should still fail, and get rid of the CoerceUnsized involvement.

[iDawer]

fn __shim<T: HelloWorld>(_db: &T) {}

analysis-stats shows no mismatch with that 🤔 .

Ok, this is closer now:

test!(
    program {
        #[upstream] #[non_enumerable] #[lang(sized)]
        trait Sized {}

        #[non_enumerable] #[object_safe]
        trait Database {}

        #[non_enumerable]
        trait QueryGroup
        where
            Self: Sized,
        {
            type DynDb: Database + HasQueryGroup<Self>;
        }

        #[non_enumerable] #[object_safe]
        trait HasQueryGroup<G>
        where
            Self: Database,
            G: QueryGroup,
            G: Sized,
        { }

        #[non_enumerable] #[object_safe]
        trait HelloWorld
        where
            Self: HasQueryGroup<HelloWorldStorage>,
        { }

        struct HelloWorldStorage {}

        impl QueryGroup for HelloWorldStorage {
            type DynDb = dyn HelloWorld + 'static;
        }
        impl<DB> HelloWorld for DB
        where
            DB: Database,
            DB: HasQueryGroup<HelloWorldStorage>,
            DB: Sized,
        { }
    }

    goal {
        forall<T> {
            if (FromEnv(T: Database); FromEnv(T: HasQueryGroup<HelloWorldStorage>); FromEnv(T: Sized)) {
                T: HelloWorld
            }
        }
    } yields[SolverChoice::slg_default()] { // ok
        "Unique"
    } yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
        "Unique"
    }
);

The query lowers to this:

[tests/test/mod.rs:266] &peeled_goal = UCanonical {
    canonical: Canonical {
        value: InEnvironment {
            environment: Env([
                for<> FromEnv(!1_0: Database),
                for<> FromEnv(!1_0: HasQueryGroup<HelloWorldStorage>),
                for<> FromEnv(!1_0: Sized)
            ]),
            goal: Implemented(!1_0: HelloWorld),
        },
        binders: [],
    },
    universes: 2,
}

Removing DB: Database, bound and FromEnv(T: Database); makes the test pass just like the Rust code. The same behavior shows &'static T: CoerceUnsized<&'static dyn HelloWorld + 'static> query.

In logs both solvers report cycles but SLG does the job. Do we hit limitations/bug in recursive solver here? As a workaround we could switch to the SLG solver when the recursive failed.

[flodiebold]

analysis-stats shows no mismatch with that

Ah well, failed obligations from type parameters don't lead to mismatches...

[flodiebold]

In logs both solvers report cycles but SLG does the job. Do we hit limitations/bug in recursive solver here? As a workaround we could switch to the SLG solver when the recursive failed.

Bug yes, I don't see any reason why it should be a limitation. I would rather investigate the actual problem than involve the SLG solver, which would just lead to failures in even more obscure cases (and also probably greatly slow down inference). I think the next step would be to report this to the Chalk team so they're aware of it (and maybe someone will look into it).