Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

implement `is_coinductive` chalk callback #55096

Closed
nikomatsakis opened this issue Oct 15, 2018 · 3 comments
Closed

implement `is_coinductive` chalk callback #55096

nikomatsakis opened this issue Oct 15, 2018 · 3 comments

Comments

@nikomatsakis
Copy link
Contributor

@nikomatsakis nikomatsakis commented Oct 15, 2018

The chalk integrate includes a is_coinductive callback that indicates whether a particular goal is co-inductive:

/// True if this is a coinductive goal -- e.g., proving an auto trait.
fn is_coinductive(&self, _goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> bool {
unimplemented!()
}

A co-inductive goal is one of the following (see the corresponding chalk code for a kind of reference):

The existing trait solver doesn't have this notion of "well-formed trait goals" -- but it does have code related to testing about auto-traits that gives a few clues as to how to do the first step.

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

@nikomatsakis nikomatsakis commented Oct 29, 2018

Mentoring instructions

Looking at the chalk implementation, we want this function to match on goals that are:

  • domain goals of "auto traits" (test with trait_is_auto)
  • domain goals for "trait well-formedness conditions" (this variant)
  • quantified goals that meet the coinductive criteria -- in chalk, we only match forall goals, but actually I imagine the same is true for exist goals (though rust never really uses those...)

This function is given a "canonical goal", so the first step is that we want to just look at the canonical value (e.g., goal.value). It's fine to just skip past the canonical binders here because the stuff we care about (e.g., the trait name) is not something you can quantify over (i.e., you can't write forall<trait T> { Implemented(u32: T) }). So just match on goal.value and look for the various cases enumerated above, something like:

fn is_coinductive(&self, goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> bool {
  let mut goal = &goal.value;
  loop {
    match goal {
      GoalKind::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => return true,
      GoalKind::DomainGoal(DomainGoal::Implemented(trait_predicate) => {
          return self.tcx.trait_is_auto(trait_predicate.def_id),
      }
      GoalKind::Quantified(_, bound_goal) => goal = bound_goal.skip_binder(),
      _ => return false,
    }
  }
}
@sunjay

This comment has been minimized.

Copy link
Member

@sunjay sunjay commented Oct 29, 2018

Hello I'd like to work on this!

scalexm added a commit to scalexm/rust that referenced this issue Nov 23, 2018
scalexm added a commit to scalexm/rust that referenced this issue Nov 24, 2018
scalexm added a commit to scalexm/rust that referenced this issue Nov 24, 2018
scalexm added a commit to scalexm/rust that referenced this issue Nov 24, 2018
scalexm added a commit to scalexm/rust that referenced this issue Nov 28, 2018
@sunjay sunjay removed their assignment Nov 28, 2018
@sunjay

This comment has been minimized.

Copy link
Member

@sunjay sunjay commented Nov 28, 2018

I see that @scalexm is working on this right now. Sorry I haven't been around. I'll let them finish it since they have already started. My apologies again and thanks for picking up my slack! :)

scalexm added a commit to scalexm/rust that referenced this issue Nov 30, 2018
scalexm added a commit to scalexm/rust that referenced this issue Nov 30, 2018
scalexm added a commit to scalexm/rust that referenced this issue Dec 8, 2018
scalexm added a commit to scalexm/rust that referenced this issue Dec 20, 2018
@bors bors closed this in 9b87f59 Dec 27, 2018
Dylan-DPC added a commit to Dylan-DPC/rust that referenced this issue Jan 5, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.