Niko Matsakis

First, a nit-pick: > If an impl passes the orphan rules, we know that it doesn't have a coherence issue with any impls outside of this crate. So we only...

> Of course the philosophical arguments Aaron made about the difficulty of determining 'the most specific proof' & the goal of making the internal logic language as simple as possible...

@aturon > Can you elaborate a bit on what you had in mind with using "or" rules? I was just saying that, instead of supporting goals like `A; B` we...

> This may be what you were getting at, but it doesn't seem like the decision tree strategy and the negative fact check strategy are at odds. Agreed, although it...

@withoutboats > First, #39 will land giving us the overlap check. I'm going to modify this to, when impls overlap, instead of erroring, follow up with queries to determine if...

@withoutboats Yeah, I have to think about this -- I am trying to figure out if this implies that lowering cannot be separated cleanly from proving or not. I...well, I...

This is where we select the next goal to pursue: https://github.com/rust-lang-nursery/chalk/blob/fa1837ed99260f01f1ad5f1978cc88644f06c9ed/chalk-slg/src/logic.rs#L369-L376 Right now, the SLG solver doesn't really know anything about the content of the domain goals, so we'd probably...

We discussed this some [on Zulip](https://rust-lang.zulipchat.com/#narrow/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection). The rough design we are thinking of is as follows: - Extend the `InferenceTable` trait, or else add a new `SelectionOps` trait - It...

The basic idea then is to add a few sorts of domain goals: - `RevealMode` - `Overrides[Id](P0: Trait)` -- where `Id` is the identity of an associated type value. We...

As @sunjay pointed out on Zulip, an obvious first step is: Extend the parser to support `default type Foo = Bar` inside of an impl; that should be a flag...