Stream: t-compiler/help

Topic: trait bounds for projected type

Nathan Corbyn (Jun 30 2019 at 20:54, on Zulip):

I've run into a situation where I'm trying to prove something along the lines of this: for some type T, <T as Future>::Output == U where U: Try. I know how to prove both <T as Future>::Output and where U: Try separately using InferCtxt::predicate_may_hold, but I don't know how to construct an obligation for both.

Nathan Corbyn (Jun 30 2019 at 20:56, on Zulip):

Does anyone have any ideas about how I could go about doing this?

davidtwco (Jul 09 2019 at 08:16, on Zulip):

I've also ran into situations where this would be useful, anyone have any ideas?

Nathan Corbyn (Jul 09 2019 at 20:14, on Zulip):

I’ve made some attempts at this by including the TraitPredicate in the param_env of the Obligation with both the TraitPredicate and ProjectionPredicate referencing the same type variable but none of them have worked

Nathan Corbyn (Jul 09 2019 at 20:14, on Zulip):

cc @WG-traits

Last update: Sep 18 2020 at 21:15UTC