Skip to content

Commit

Permalink
start of a fix for rust-lang#727
Browse files Browse the repository at this point in the history
  • Loading branch information
nikomatsakis committed Mar 10, 2022
1 parent f470f2f commit f979cd1
Show file tree
Hide file tree
Showing 5 changed files with 181 additions and 24 deletions.
7 changes: 5 additions & 2 deletions chalk-recursive/src/combine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ use tracing::debug;
use chalk_ir::interner::Interner;
use chalk_ir::{ClausePriority, DomainGoal, GenericArg};

#[tracing::instrument(level = "Debug", skip(interner))]
pub(super) fn with_priorities<I: Interner>(
interner: I,
domain_goal: &DomainGoal<I>,
Expand All @@ -12,7 +13,7 @@ pub(super) fn with_priorities<I: Interner>(
b: Solution<I>,
prio_b: ClausePriority,
) -> (Solution<I>, ClausePriority) {
match (prio_a, prio_b, a, b) {
let result = match (prio_a, prio_b, a, b) {
(ClausePriority::High, ClausePriority::Low, higher, lower)
| (ClausePriority::Low, ClausePriority::High, lower, higher) => {
// if we have a high-priority solution and a low-priority solution,
Expand All @@ -34,7 +35,9 @@ pub(super) fn with_priorities<I: Interner>(
}
}
(_, _, a, b) => (a.combine(b, interner), prio_a),
}
};
debug!(?result, "combined result");
result
}

fn calculate_inputs<I: Interner>(
Expand Down
7 changes: 2 additions & 5 deletions chalk-recursive/src/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -154,11 +154,6 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
for program_clause in clauses {
debug_span!("solve_from_clauses", clause = ?program_clause);

// If we have a completely ambiguous answer, it's not going to get better, so stop
if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) {
return Ok(Solution::Ambig(Guidance::Unknown));
}

let ProgramClauseData(implication) = program_clause.data(self.interner());
let infer = infer.clone();
let subst = subst.clone();
Expand Down Expand Up @@ -187,8 +182,10 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
}

if let Some((s, _)) = cur_solution {
debug!("solve_from_clauses: result = {:?}", s);
Ok(s)
} else {
debug!("solve_from_clauses: error");
Err(NoSolution)
}
}
Expand Down
57 changes: 40 additions & 17 deletions chalk-solve/src/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -44,30 +44,43 @@ impl<I: Interner> Solution<I> {
/// There are multiple candidate solutions, which may or may not agree on
/// the values for existential variables; attempt to combine them. This
/// operation does not depend on the order of its arguments.
//
// This actually isn't as precise as it could be, in two ways:
//
// a. It might be that while there are multiple distinct candidates, they
// all agree about *some things*. To be maximally precise, we would
// compute the intersection of what they agree on. It's not clear though
// that this is actually what we want Rust's inference to do, and it's
// certainly not what it does today.
//
// b. There might also be an ambiguous candidate and a successful candidate,
// both with the same refined-goal. In that case, we could probably claim
// success, since if the conditions of the ambiguous candidate were met,
// we know the success would apply. Example: `?0: Clone` yields ambiguous
// candidate `Option<?0>: Clone` and successful candidate `Option<?0>:
// Clone`.
//
// But you get the idea.
///
/// This actually isn't as precise as it could be, in two ways:
///
/// a. It might be that while there are multiple distinct candidates, they
/// all agree about *some things*. To be maximally precise, we would
/// compute the intersection of what they agree on. It's not clear though
/// that this is actually what we want Rust's inference to do, and it's
/// certainly not what it does today.
///
/// b. There might also be an ambiguous candidate and a successful candidate,
/// both with the same refined-goal. In that case, we could probably claim
/// success, since if the conditions of the ambiguous candidate were met,
/// we know the success would apply. Example: `?0: Clone` yields ambiguous
/// candidate `Option<?0>: Clone` and successful candidate `Option<?0>:
/// Clone`.
///
/// But you get the idea.
pub fn combine(self, other: Solution<I>, interner: I) -> Solution<I> {
use self::Guidance::*;

if self == other {
return self;
}

// Special case hack: if one solution is "true" without any constraints,
// that is always the combined result.
//
// This is not as general as it could be: ideally, if we had one solution
// that is Unique with a simpler substitution than the other one, or region constraints
// which are a subset, we'd combine them.
if self.is_trivial_and_always_true(interner) {
return self;
}
if other.is_trivial_and_always_true(interner) {
return other;
}

debug!(
"combine {} with {}",
self.display(interner),
Expand All @@ -88,6 +101,16 @@ impl<I: Interner> Solution<I> {
Solution::Ambig(guidance)
}

fn is_trivial_and_always_true(&self, interner: I) -> bool {
match self {
Solution::Unique(constrained_subst) => {
constrained_subst.value.subst.is_identity_subst(interner)
&& constrained_subst.value.constraints.is_empty(interner)
}
Solution::Ambig(_) => false,
}
}

/// View this solution purely in terms of type inference guidance
pub fn into_guidance(self) -> Guidance<I> {
match self {
Expand Down
133 changes: 133 additions & 0 deletions tests/test/ambiguity_issue_727.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,133 @@
use super::*;

#[test]
fn issue_727_1() {
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
expect![["Unique"]]
} yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
expect![["Unique"]]
}
);
}

#[test]
fn issue_727_2() {
test!(
program {
#[non_enumerable] #[object_safe]
trait Database {}

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

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

struct HelloWorldStorage {}

impl QueryGroup for HelloWorldStorage {
type DynDb = dyn HasQueryGroup<HelloWorldStorage> + 'static;
}
}

goal {
forall<T> {
if (FromEnv(T: HasQueryGroup<HelloWorldStorage>)) {
T: Database
}
}
} yields[SolverChoice::slg_default()] {
expect![["Unique"]]
} yields[SolverChoice::recursive_default()] {
expect![["Unique"]]
}
);
}

#[test]
fn issue_727_3() {
test!(
program {
#[non_enumerable]
trait Database {}

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

struct HelloWorldStorage {}

impl Database for HelloWorldStorage { }
}

goal {
forall<T, S> {
if (FromEnv(HelloWorldStorage: HasQueryGroup<T>); FromEnv(HelloWorldStorage: HasQueryGroup<S>)) {
HelloWorldStorage: Database
}
}
} yields[SolverChoice::slg_default()] {
expect![["Unique"]]
} yields[SolverChoice::recursive_default()] {
expect![["Unique"]]
}
);
}
1 change: 1 addition & 0 deletions tests/test/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -404,6 +404,7 @@ fn solve_aggregated(
expected.assert_eq(head);
}

mod ambiguity_issue_727;
mod arrays;
mod auto_traits;
mod closures;
Expand Down

0 comments on commit f979cd1

Please sign in to comment.