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):

forget about the questions, i'm answering them myself

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):

niko already answered this on the issue

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):

(else I can find someone else to adopt, or adopt myself)

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: Nov 12 2019 at 17:00UTC