## Stream: wg-traits

### Topic: dyn and impl trait support chalk#218

Keith Yeung (May 03 2019 at 10:26, on Zulip):

starting this thread here for the work on https://github.com/rust-lang/chalk/issues/218

Keith Yeung (May 03 2019 at 10:35, on Zulip):

first things first, where is the specification for dyn and impl trait?

Keith Yeung (May 03 2019 at 10:35, on Zulip):

i'd like to know which positions we're supposed to support this new syntax

Keith Yeung (May 03 2019 at 11:51, on Zulip):

(deleted)

Keith Yeung (May 03 2019 at 12:18, on Zulip):

Keith Yeung (May 03 2019 at 17:55, on Zulip):

@nikomatsakis In the issue, you said that the chalk parser should create new `Ty` enum variants with a field containing `Vec<InlineBound>`, but in the chalk IR, you have `Vec<QuantifiedWhereClause>` instead. Which one should be the correct one to use?

nikomatsakis (May 03 2019 at 18:21, on Zulip):

@Keith Yeung nice

nikomatsakis (May 03 2019 at 18:21, on Zulip):

mmm let me see

Keith Yeung (May 03 2019 at 18:22, on Zulip):

as far i can see, the difference between them is whether it supports the "forall" syntax or not

nikomatsakis (May 03 2019 at 18:25, on Zulip):

@Keith Yeung ah. We do want that.

nikomatsakis (May 03 2019 at 18:25, on Zulip):

In other words, these are legal types. `dyn for<'a> Output<'a>`

nikomatsakis (May 03 2019 at 18:25, on Zulip):

`impl for<'a> Output<'a>` :)

Keith Yeung (May 03 2019 at 18:29, on Zulip):

gotcha, so we should use `QuantifiedWhereClause` instead

Keith Yeung (May 03 2019 at 18:29, on Zulip):

or wait, what's the difference between `QuantifiedWhereClause` and `QuantifiedInlineBound`?

Keith Yeung (May 03 2019 at 18:32, on Zulip):

it looks to me the better one is `QuantifiedInlineBound` instead

nikomatsakis (May 03 2019 at 18:34, on Zulip):

it looks to me the better one is `QuantifiedInlineBound` instead

correct

scalexm (May 03 2019 at 20:07, on Zulip):

@Keith Yeung a suggestion from @nikomatsakis was to get rid of `QuantifiedInlineBound` and instead have `Binder<QuantifiedWhereClause>` where the binder would bind an existential `^Self`. It would be cool if we were able to do that, but I remember having tried and it was not as easy at it sounded

nikomatsakis (May 03 2019 at 20:21, on Zulip):

@scalexm I think I meant to do it in the lowering, not necessarily in the AST

nikomatsakis (May 03 2019 at 20:21, on Zulip):

i.e., in chalk-ir

scalexm (May 03 2019 at 20:21, on Zulip):

@nikomatsakis yes

scalexm (May 03 2019 at 20:22, on Zulip):

Ah ok we’re still only talking about syntax

scalexm (May 03 2019 at 20:23, on Zulip):

Still good to keep this in mind for when we proceed onto implementing dyn traits lowering :)

Keith Yeung (May 04 2019 at 13:14, on Zulip):

hmm, looks like i still need some clarification on how "forall" is supported

Keith Yeung (May 04 2019 at 13:15, on Zulip):

given we have `impl for<'a> Foo<'a>`, is this supposed to work? `impl for<'a> Foo<'a> + Bar<'a>`

Keith Yeung (May 04 2019 at 13:16, on Zulip):

or is it supposed to be something like `impl for<'a> Foo<'a> + for<'b> Bar<'b>`

Keith Yeung (May 04 2019 at 13:16, on Zulip):

i'm inclined to believe that the former is the version of quantified types that we'd like to support, and if so, then the grammar is a bit different and I'll need to account for it

centril (May 04 2019 at 13:19, on Zulip):

@Keith Yeung `impl dyn for<'a> Foo<'a> + for<'b> Bar<'b> { ... }`makes things easier to understand :slight_smile:

Keith Yeung (May 04 2019 at 13:20, on Zulip):

i'm not talking about the difficulty of understanding it, i want to know what exactly we'd like to support

centril (May 04 2019 at 13:23, on Zulip):

@Keith Yeung we don't allow 1) `for<'a> (Foo<'a> + Bar<'a>)` in Rust atm. However, using 2) `∀ x. [P(x) ∧ Q(x)] ≡ [∀ x. P(x)] ∧ [∀ x. Q(x)]` you get 3) `(for<'a> Foo<'a>) + (for<'a> Bar<'a>)` which is equivalent to 1)

Keith Yeung (May 04 2019 at 13:25, on Zulip):

ok, so the latter is what we'd like to have instead

centril (May 04 2019 at 13:25, on Zulip):

@Keith Yeung yeah we need to support:
1) `dyn (for<'a> Foo<'a>) + (for<'a> Bar<'a>)`
2) `impl (for<'a> Foo<'a>) + (for<'a> Bar<'a>)`
3) `T: (for<'a> Foo<'a>) + (for<'a> Bar<'a>)`

centril (May 04 2019 at 13:26, on Zulip):

since rustc does

Keith Yeung (May 04 2019 at 14:15, on Zulip):

so, i found quite a lot of convenience traits and methods that allow me to lower AST types into chalk IR types

Keith Yeung (May 04 2019 at 14:20, on Zulip):

first, let's be clear about what we want to lower: `ast::Ty::Dyn(Vec<QuantifiedInlineBound>)` into `chalk_ir::Ty::Dyn(Vec<QuantifiedWhereClause>)`

Keith Yeung (May 04 2019 at 14:20, on Zulip):

there's already a `LowerQuantifiedInlineBound` trait which provides me with a method to lower the `Vec<ast::QuantifiedInlineBound>` into a `Vec<rust_ir::QuantifiedInlineBound>`

Keith Yeung (May 04 2019 at 14:20, on Zulip):

what's left then is to convert that result into a `Vec<chalk_ir::QuantifiedWhereClause>`, which the `IntoWhereClauses` trait also provides me convenience methods for

Keith Yeung (May 04 2019 at 14:20, on Zulip):

the problem here now is that `into_where_clauses` accepts an additional `self_ty` parameter, and I'm trying to figure out what to put there

Keith Yeung (May 04 2019 at 14:22, on Zulip):

my educated guess is `chalk_ir::Ty::BoundVar(binders.len())` where `binders` is the binders for each `QuantifiedInlineBound` in the vector, because that's the de Bruijn index that describes the anonymous self type that an `impl/dyn Trait` has

Keith Yeung (May 04 2019 at 14:22, on Zulip):

can somebody confirm that this is the case?

Keith Yeung (May 04 2019 at 16:31, on Zulip):

Note that these types introduce a level of binder -- this is so that you can represent the (unknown) Self type with a debruijn variable. i.e., something like dyn Foo<Bar> would wind up represented as

Dyn(^0: Foo<Bar>`)

where ^0 represents "debruijn variable with depth 0.

Keith Yeung (May 04 2019 at 16:31, on Zulip):

Keith Yeung (May 04 2019 at 16:32, on Zulip):

at this point then, i'm onto extending `chalk-solve`, but as niko said in the issue, it's blocked on chalk#216

Keith Yeung (May 04 2019 at 16:33, on Zulip):

oh? it just got merged yesterday

Keith Yeung (May 05 2019 at 07:04, on Zulip):

error[E0004]: non-exhaustive patterns: `(&Dyn(_), &Apply(_))`, `(&Opaque(_), &Apply(_))`, `(&Dyn(_), &Dyn(_))` and 11 more not covered
--> chalk-solve\src\infer\unify.rs:107:15
|
107 | match (a, b) {
| ^^^^^^ patterns `(&Dyn(_), &Apply(_))`, `(&Opaque(_), &Apply(_))`, `(&Dyn(_), &Dyn(_))` and 11 more not covered

error[E0004]: non-exhaustive patterns: `(&Dyn(_), &Apply(_))`, `(&Opaque(_), &Apply(_))`, `(&Dyn(_), &Dyn(_))` and 9 more not covered
--> chalk-solve\src\solve\slg.rs:364:15
|
364 | match (new, current) {
| ^^^^^^^^^^^^^^ patterns `(&Dyn(_), &Apply(_))`, `(&Opaque(_), &Apply(_))`, `(&Dyn(_), &Dyn(_))` and 9 more not covered

error[E0004]: non-exhaustive patterns: `(&Dyn(_), _)` and `(&Opaque(_), _)` not covered
--> chalk-solve\src\solve\slg\aggregate.rs:171:15
|
171 | match (ty0, ty1) {
| ^^^^^^^^^^ patterns `(&Dyn(_), _)` and `(&Opaque(_), _)` not covered

error[E0004]: non-exhaustive patterns: `(&Dyn(_), &Apply(_))`, `(&Opaque(_), &Apply(_))`, `(&Dyn(_), &Dyn(_))` and 11 more not covered
--> chalk-solve\src\solve\slg\resolvent.rs:340:15
|
340 | match (answer, pending) {
| ^^^^^^^^^^^^^^^^^ patterns `(&Dyn(_), &Apply(_))`, `(&Opaque(_), &Apply(_))`, `(&Dyn(_), &Dyn(_))` and 11 more not covered

error[E0004]: non-exhaustive patterns: `&Dyn(_)` and `&Opaque(_)` not covered
--> chalk-solve\src\wf.rs:56:15
|
56 | match self {
| ^^^^ patterns `&Dyn(_)` and `&Opaque(_)` not covered

error: aborting due to 5 previous errors

Keith Yeung (May 05 2019 at 07:05, on Zulip):

these are the remaining compile time errors that i have to solve

nikomatsakis (May 06 2019 at 17:08, on Zulip):

seems like you're making good progress :)

Keith Yeung (May 06 2019 at 17:31, on Zulip):

@nikomatsakis I actually do need some help on `chalk-solve`, precisely because I'm not sure how the general direction should look like

Keith Yeung (May 06 2019 at 17:32, on Zulip):

the compiler errors give me a hint, but i don't think it's enough for my theoretical understanding of how a goal with a `impl/dyn trait` should be solved

Keith Yeung (May 06 2019 at 17:33, on Zulip):

let me try and see what components of the solver needs work... `unify`, `slg`, `aggregate`, `resolvent` and `wf`

nikomatsakis (May 06 2019 at 17:37, on Zulip):

@Keith Yeung is there a PR?

nikomatsakis (May 06 2019 at 17:37, on Zulip):

maybe you can leave pointers into places that you have questions?

Keith Yeung (May 06 2019 at 18:02, on Zulip):

no there isn't yet; i'll make one this evening when i get back home

Keith Yeung (May 08 2019 at 07:16, on Zulip):

here's a PR https://github.com/rust-lang/chalk/pull/226

Keith Yeung (May 08 2019 at 07:16, on Zulip):

it's still not ready yet; i'll need some eyes here to ensure everything's fiine

Keith Yeung (May 20 2019 at 18:05, on Zulip):

@nikomatsakis so i'm really not sure what I should do for the chalk solver in order to support `dyn Trait` and `impl Trait`, there are no mentoring instructions written up for this and going by the compiler errors doesn't really tell me what each module is doing

nikomatsakis (May 28 2019 at 19:57, on Zulip):

@Keith Yeung ok, I'll try to give you some feedback on this this week

Keith Yeung (Jun 03 2019 at 20:22, on Zulip):

@nikomatsakis I saw that you've left review comments on the draft PR i created, however I'd still need some guidance on how we should support dyn and impl Trait on the solver

nikomatsakis (Sep 23 2019 at 21:13, on Zulip):

@Keith Yeung ping :wave: -- sorry for the big hiatus, you still interested in maintaining the PR?

nikomatsakis (Sep 23 2019 at 21:13, on Zulip):

I'm going to leave some comments today, so let me know

nikomatsakis (Sep 23 2019 at 21:13, on Zulip):

Keith Yeung (Sep 23 2019 at 21:14, on Zulip):

sure, i still have some time nowadays for it

Keith Yeung (Sep 23 2019 at 21:15, on Zulip):

i think i just need to understand how the solver works

nikomatsakis (Sep 23 2019 at 21:16, on Zulip):

OK

nikomatsakis (Sep 23 2019 at 21:16, on Zulip):

actually you don't

nikomatsakis (Sep 23 2019 at 21:16, on Zulip):

that is, I think all the required changes are "outside" the 'core solver'

nikomatsakis (Sep 23 2019 at 21:16, on Zulip):

I guess it depends on what you mean by "the solver"

nikomatsakis (Sep 23 2019 at 21:17, on Zulip):

anyway let me write a comment up

nikomatsakis (Sep 23 2019 at 21:50, on Zulip):

@Keith Yeung wrote a comment here -- not sure if it's gonna be a bit too opaque to make sense to you, so feel free to drop questions (probably here is better, but if you put them on GH, just make sure to `@` me)

Keith Yeung (Sep 23 2019 at 21:58, on Zulip):

ok, will read it when i find the time

Keith Yeung (Sep 23 2019 at 22:55, on Zulip):

so, aside from `clauses.rs` in the solver that I have to update, there is also `wf.rs`, `resolvent.rs`, `env_elaborator.rs`, `unify.rs` and `aggregate.rs` that requires me to handle the additional `Ty::Dyn` and `Ty::Opaque` cases

Keith Yeung (Sep 23 2019 at 22:56, on Zulip):

i'll also need to know what these files in the solver do in order to know how to handle them appropriately

nikomatsakis (Sep 25 2019 at 12:39, on Zulip):

OK, I plan to put more time into traits stuff on Friday, so I can leave further instructions then. Ping me @Keith Yeung if you have any questions on the stuff so far, or you get done early -- if I get some spare cycles i'll try to leave some more notes.

Keith Yeung (Sep 30 2019 at 17:27, on Zulip):

@nikomatsakis Ok, I just pushed a commit that extends `clauses.rs` to generate additional program clauses for impl and dyn Trait

nikomatsakis (Sep 30 2019 at 17:34, on Zulip):

cool

Keith Yeung (Sep 30 2019 at 17:35, on Zulip):

now we just need to fix the remaining files where we need to handle the additional variants for impl and dyn Trait

nikomatsakis (Sep 30 2019 at 17:56, on Zulip):

@Keith Yeung take a look at this comment -- does it make sense to you?

Keith Yeung (Sep 30 2019 at 18:25, on Zulip):

ah, so it looks like that i was generating the wrong clauses

Keith Yeung (Sep 30 2019 at 18:26, on Zulip):

i thought we wanted an implication

Keith Yeung (Sep 30 2019 at 18:26, on Zulip):

i'm not exactly understanding what the binders do

nikomatsakis (Sep 30 2019 at 19:10, on Zulip):

@Keith Yeung in general?

nikomatsakis (Sep 30 2019 at 19:10, on Zulip):

or in this specific case?

Keith Yeung (Sep 30 2019 at 19:10, on Zulip):

Both I suppose

nikomatsakis (Sep 30 2019 at 19:11, on Zulip):

are you familiar with debruijn indices?

nikomatsakis (Sep 30 2019 at 19:11, on Zulip):

(they're just a representation technique, but it's relevant here)

nikomatsakis (Sep 30 2019 at 19:11, on Zulip):

at a high-level, a `Binder<T>` represents some kind of, well, binder -- i.e., it creates a variable, but the purpose of that variable depends on the surrounding context

nikomatsakis (Sep 30 2019 at 19:11, on Zulip):

e.g., if you have a chalk goal like `forall<T> { Implemented(T: Trait) }`

nikomatsakis (Sep 30 2019 at 19:12, on Zulip):

that `<T> { ... }` (without the `forall`) is represented using a `Binder`

nikomatsakis (Sep 30 2019 at 19:12, on Zulip):

the `Binder` itself is embedded in a context that indicates whether it's a `forall`, `exists`, or something else

nikomatsakis (Sep 30 2019 at 20:09, on Zulip):

does that help, @Keith Yeung ?

Keith Yeung (Sep 30 2019 at 23:15, on Zulip):

sorry, was away for a while

Keith Yeung (Sep 30 2019 at 23:16, on Zulip):

so in that comment, you said that we should call `Subst::apply`, and that would mean that we're filling in the variables in the binder by giving it the appropriate context?

nikomatsakis (Oct 01 2019 at 00:00, on Zulip):

@Keith Yeung right.

nikomatsakis (Oct 01 2019 at 00:00, on Zulip):

And in this case, we're storing a type like `dyn Foo` as (kind of) `dyn<X> { X: Foo }`

nikomatsakis (Oct 01 2019 at 00:01, on Zulip):

and so we are substituting here the `dyn Foo` type itself for `X` to get our final clauses:

nikomatsakis (Oct 01 2019 at 00:01, on Zulip):

`dyn Foo: Foo`

Keith Yeung (Oct 01 2019 at 00:02, on Zulip):

ok, so i just force-pushed an amended commit that should resolve the comment you made

Keith Yeung (Oct 01 2019 at 00:02, on Zulip):

there is another place in the `clauses.rs` file where i have to handle `Ty::Opaque | Ty::Dyn`, and it's in `match_ty`

Keith Yeung (Oct 01 2019 at 00:04, on Zulip):

(i'm also wondering if I should just create a new method called `instantiate` on `Binder` altogether...)

nikomatsakis (Oct 01 2019 at 00:07, on Zulip):

yeah, seems good -- I like operating on the bindder itself, I don't like accessing the `value` field directly

nikomatsakis (Oct 01 2019 at 00:08, on Zulip):

@Keith Yeung I'd call it `substitute`, perhaps

nikomatsakis (Oct 01 2019 at 00:08, on Zulip):

I feel like there used to be such a method but it was removed for being unused

nikomatsakis (Oct 01 2019 at 00:08, on Zulip):

bsaically the same as this existing method, for a `Binders<T: Fold>`:

```impl QuantifiedTy {
pub fn substitute(&self, parameters: &[Parameter]) -> Ty {
assert_eq!(self.num_binders, parameters.len());
Subst::apply(parameters, &self.ty)
}
}
```
nikomatsakis (Oct 01 2019 at 00:09, on Zulip):

(really, `QuantifiedTy` is just a "specialized" form of binders)

Keith Yeung (Oct 01 2019 at 01:04, on Zulip):

are program clauses "facts" that you provide to the datafrog engine btw?

Keith Yeung (Oct 03 2019 at 18:18, on Zulip):

@nikomatsakis I think we're awaiting for your review and next steps after implementing the logic for generating program clauses in the solver

nikomatsakis (Oct 03 2019 at 18:20, on Zulip):

@Keith Yeung yep, on my list for tomorrow!

nikomatsakis (Oct 03 2019 at 18:21, on Zulip):

or maybe later today if I get lucky :)

nikomatsakis (Oct 04 2019 at 18:24, on Zulip):

@Keith Yeung comment

Keith Yeung (Oct 04 2019 at 18:25, on Zulip):

gotcha, will go over them when i have time

Keith Yeung (Oct 04 2019 at 21:03, on Zulip):

@nikomatsakis one additional thing, I want to make sure that my code here is correct: https://github.com/rust-lang/chalk/pull/226/files#diff-a66f74f4c8a6a7a1342ab7c62c3ae8a4R281

Keith Yeung (Oct 04 2019 at 21:04, on Zulip):

this is not part of the clause "lowering" code i believe

Keith Yeung (Oct 04 2019 at 21:05, on Zulip):

but is part of the `match_ty` function

Keith Yeung (Oct 04 2019 at 21:07, on Zulip):

actually, this commit would be the change that i'd like someone to review: https://github.com/rust-lang/chalk/pull/226/commits/0a53a25e5343f2982d9e988e8226aa081c41ca41

nikomatsakis (Oct 04 2019 at 21:11, on Zulip):

nikomatsakis one additional thing, I want to make sure that my code here is correct: https://github.com/rust-lang/chalk/pull/226/files#diff-a66f74f4c8a6a7a1342ab7c62c3ae8a4R281

@Keith Yeung that code is not wrong but also not necessary. The `match_ty` code is kind of poorly named, but it is only used for various 'internals' chalk goals like `IsLocal` and so forth, which will never be part of a `dyn` type. That said, if it were to be used from new places, then the code would be right I think, and those clauses will get screened out eventually.

nikomatsakis (Oct 04 2019 at 21:11, on Zulip):

It might be nice to remove it but instead to add an assertion or something that the clauses aren't relevant

Keith Yeung (Oct 04 2019 at 21:12, on Zulip):

hmm, so similar to another case where it does nothing, or panicks

nikomatsakis (Oct 04 2019 at 21:13, on Zulip):

(at worst, a `debug_assertion!` could be used to instantiate the clauses but assert that `could_match` is false)

nikomatsakis (Oct 04 2019 at 21:13, on Zulip):

or maybe at best :)

nikomatsakis (Oct 04 2019 at 21:13, on Zulip):

that seems ok

nikomatsakis (Oct 04 2019 at 21:13, on Zulip):

I'd say `debug_assertion!` because it's non trivial in complexity

nikomatsakis (Oct 04 2019 at 21:14, on Zulip):

I guess that `match_ty` would need another argument, the `env_clause` we are trying to solve

nikomatsakis (Oct 04 2019 at 21:14, on Zulip):

or rather the `goal`

nikomatsakis (Oct 04 2019 at 21:14, on Zulip):

then you'd do something like this

nikomatsakis (Oct 04 2019 at 21:15, on Zulip):
```debug_assert!(
qwc
.substitute(&[ty.clone().cast()])
.iter()
.all(|c| !c.could_match(goal))
);
```
Keith Yeung (Oct 06 2019 at 08:07, on Zulip):

@nikomatsakis ok, i'm down to one last compile error, and it's in `unify.rs`

Keith Yeung (Oct 06 2019 at 08:08, on Zulip):

two cases are still missing from your comment: `(Ty::Apply, Ty::Dyn)` and `(Ty::Apply, Ty::Opaque)`

Keith Yeung (Oct 06 2019 at 08:08, on Zulip):

i'm not sure how i should unify these types with `Ty::Apply`

Keith Yeung (Oct 07 2019 at 17:30, on Zulip):

my guess is that since `Apply` is about type constructors, it may just be sufficient if we can prove that the `Apply` type implements all of the traits that `Opaque` requires?

Keith Yeung (Oct 07 2019 at 17:32, on Zulip):

i would think that there shouldn't be any solution for unifying `Dyn` and `Apply`, since `Dyn` specifically refers to a trait object, and no `Apply` type represents a trait object

nikomatsakis (Oct 14 2019 at 09:19, on Zulip):

i would think that there shouldn't be any solution for unifying `Dyn` and `Apply`, since `Dyn` specifically refers to a trait object, and no `Apply` type represents a trait object

@Keith Yeung sorry for not responding to these more promptly, I forgot I hadn't answered. I went ahead and pushed some commits to your branch to fix the unification cases. This was correct.

nikomatsakis (Oct 14 2019 at 09:20, on Zulip):

I also pushed a few minor fixes and the branch builds now!

nikomatsakis (Oct 14 2019 at 09:20, on Zulip):

I was thinking that man we really need to get this code landed.

nikomatsakis (Oct 14 2019 at 09:20, on Zulip):

(I was attempting some other refactorings and realized I would stomp all over your branch.)

nikomatsakis (Oct 14 2019 at 09:37, on Zulip):

I was reading the diff and I would say at this point the main thing that's missing is tests -- although when I tried to add one, I immediately got some panics. =) I'm inclined to land the branch first and address adding tests and fixing bugs next

nikomatsakis (Oct 14 2019 at 10:42, on Zulip):

@Keith Yeung ok I merged the existing PR. I also created a list of some tests.

Keith Yeung (Oct 14 2019 at 17:34, on Zulip):

what kind of tests do you have in mind?

nikomatsakis (Oct 15 2019 at 00:48, on Zulip):

@Keith Yeung I added a list to the top of this issue -- but let me make a branch with some examples

nikomatsakis (Oct 15 2019 at 00:52, on Zulip):

@Keith Yeung a sample test (which fails) is on this branch -- it panics in unification because we need to write a routine for unifying `QuantifiedWhereClauses`

nikomatsakis (Oct 15 2019 at 00:52, on Zulip):

similar I imagine to `unify_forall_tys`

nikomatsakis (Oct 21 2019 at 14:33, on Zulip):

@Keith Yeung did you see the above notes :point_up: ?

Keith Yeung (Oct 21 2019 at 17:45, on Zulip):

sorry, i was busying with other stuff

Keith Yeung (Oct 21 2019 at 17:45, on Zulip):

it does look like there's some work left on the implementation itself before it can properly be used

Keith Yeung (Oct 21 2019 at 17:46, on Zulip):

i'm not 100% familiar with the macro syntax in your branch, but I can familiarize myself with it after some reading

Keith Yeung (Nov 01 2019 at 23:58, on Zulip):

@nikomatsakis ok so I was able to look further into this last night, and the problem that i think i'm encountering right now is the elimination of the 2 binders on the Opaque/Dyn types

Keith Yeung (Nov 02 2019 at 00:00, on Zulip):

i currently made it so that the code checks for arity of the outer binder, ensuring that it is 1 (which represents the self-type)

Keith Yeung (Nov 02 2019 at 00:00, on Zulip):

and if not, panic with an error message

Keith Yeung (Nov 02 2019 at 00:05, on Zulip):

then i create a new universe and construct two placeholder types, and substitute them into both arguments that gets passed in, which removes the outer binder

Keith Yeung (Nov 02 2019 at 00:05, on Zulip):

i have doubts on whether this is the correct approach, because I felt like i should've created two new variables on the universe instead of creating placeholder types

nikomatsakis (Nov 04 2019 at 19:02, on Zulip):

@Keith Yeung hmm so good questions :) let me circle back to you on this

nikomatsakis (Nov 04 2019 at 21:33, on Zulip):

OK so @Keith Yeung we have to equate the `dyn` and `impl` types...

nikomatsakis (Nov 04 2019 at 21:34, on Zulip):

I think that in the particular case of the `Self` binder

nikomatsakis (Nov 04 2019 at 21:34, on Zulip):

we can take a simpler approach

nikomatsakis (Nov 04 2019 at 21:34, on Zulip):

precisely because we know there is exactly one parameter

nikomatsakis (Nov 04 2019 at 22:18, on Zulip):

oh, huh.

nikomatsakis (Nov 04 2019 at 22:19, on Zulip):

reading the existing unification logic...I ... feel like there is a bug here

nikomatsakis (Nov 04 2019 at 22:20, on Zulip):

...yep...

nikomatsakis (Nov 04 2019 at 22:33, on Zulip):

@Keith Yeung I wrote up in detail what needs to be done as chalk#275

nikomatsakis (Nov 11 2019 at 20:53, on Zulip):

btw @Keith Yeung -- have you had a chance to take a look at this? if not, I might take a swing at it later on

Keith Yeung (Nov 11 2019 at 20:54, on Zulip):

not really, i've only looked briefly at the issue

Keith Yeung (Nov 11 2019 at 20:54, on Zulip):

not so much into the code

Last update: Aug 13 2020 at 09:15UTC