Stream: t-compiler

Topic: #57893 coherence and traits


Ariel Ben-Yehuda (Jun 26 2019 at 19:45, on Zulip):

hi @RalfJung

Ariel Ben-Yehuda (Jun 26 2019 at 19:46, on Zulip):

what do you mean by "assuming coherence" exactly

Ariel Ben-Yehuda (Jun 26 2019 at 19:46, on Zulip):

It seems like a basic rule of Rust that we want to keep that it is possible to follow impls. e.g., with IntoIterator, you really want typeck to be able to assume that <T as IntoIterator>::Item = U := T: Iterator, <T as Iterator>::Item = U.

Wesley Wiser (Jun 26 2019 at 20:34, on Zulip):

(pinging @RalfJ so he sees this ^)

RalfJ (Jun 26 2019 at 20:53, on Zulip):

It seems like a basic rule of Rust that we want to keep that it is possible to follow impls. e.g., with IntoIterator, you really want typeck to be able to assume that <T as IntoIterator>::Item = U := T: Iterator, <T as Iterator>::Item = U.

that's exactly what I mean by "exploiting coherence"

RalfJ (Jun 26 2019 at 20:53, on Zulip):

it's very useful and very subtle and makes analysis very complicated

RalfJ (Jun 26 2019 at 20:53, on Zulip):

which is why I wrote

But there's likely already tons of code out there that exploits this.

RalfJ (Jun 26 2019 at 20:53, on Zulip):

so this is likely a moot point

RalfJ (Jun 26 2019 at 20:54, on Zulip):

but if this were pre-1.0 I would argue fiercly against doing what we are doing ;)

RalfJ (Jun 26 2019 at 20:55, on Zulip):

@Ariel Ben-Yehuda @Ariel Ben-Yehuda (also keep pinging me, I have t-compiler muted because there is too much traffic and Zulip does not support unmuting just one topic in a stream)
(also who is the real ariel?^^)

centril (Jun 26 2019 at 21:03, on Zulip):

Haskell does allow something similar:

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}

class Object t u where
  type Output t u :: *

instance Object t u where
  type Output t u = u

foo :: Output t u -> u
foo x = x
Ariel Ben-Yehuda (Jun 26 2019 at 21:20, on Zulip):

@RalfJ
I accidentally created a new zulip account. Probably a github vs. google login problem.

Ariel Ben-Yehuda (Jun 26 2019 at 21:21, on Zulip):

it's very useful and very subtle and makes analysis very complicated

I think it's hard to work with associated types without this

Ariel Ben-Yehuda (Jun 26 2019 at 21:23, on Zulip):

unless there is some restricted version of this rule that works, I don't see how you could use associated types in a generic context otherwise

RalfJ (Jun 26 2019 at 21:24, on Zulip):

you just have to state the assumptions you are making?

Ariel Ben-Yehuda (Jun 26 2019 at 21:24, on Zulip):

on the function?

RalfJ (Jun 26 2019 at 21:24, on Zulip):

we would have stabilized equality constraints much sooner in that alternative universe ;)

Ariel Ben-Yehuda (Jun 26 2019 at 21:24, on Zulip):

but then you can't use "new" associated types

RalfJ (Jun 26 2019 at 21:25, on Zulip):

@centril wait doesnt haskell also have a flag to allow overlapping instances...?

Ariel Ben-Yehuda (Jun 26 2019 at 21:25, on Zulip):

consider that T: Sized is a bound

RalfJ (Jun 26 2019 at 21:25, on Zulip):

@Ariel Ben-Yehuda not sure what you mean

Ariel Ben-Yehuda (Jun 26 2019 at 21:25, on Zulip):

I mean, suppose you have a function that takes a generic T

centril (Jun 26 2019 at 21:25, on Zulip):

@RalfJ Yeah but don't ever use it

Ariel Ben-Yehuda (Jun 26 2019 at 21:25, on Zulip):

it needs to be able to evaluate <Vec<T> as IntoIterator>::Item

Ariel Ben-Yehuda (Jun 26 2019 at 21:26, on Zulip):

or <slice::Iter<'a, T> as IntoIterator>::Item

RalfJ (Jun 26 2019 at 21:26, on Zulip):

that's an opaque type at that point

Ariel Ben-Yehuda (Jun 26 2019 at 21:26, on Zulip):

if you couldn't do <Vec<T> as IntoIterator>::Item = T, then IntoIterator wouldn't be very useful

Ariel Ben-Yehuda (Jun 26 2019 at 21:26, on Zulip):

I mean, for a generic T: Sized

RalfJ (Jun 26 2019 at 21:27, on Zulip):

then add that as a where clause

Ariel Ben-Yehuda (Jun 26 2019 at 21:27, on Zulip):

every function that takes a T: Sized also needs a <Vec<T> as IntoIterator>::Item = T where-clause?

RalfJ (Jun 26 2019 at 21:27, on Zulip):

(that's what someone else suggested in the thread, basically interpret our current scheme as adding all those where clauses implicitly)

Ariel Ben-Yehuda (Jun 26 2019 at 21:27, on Zulip):

I suppose you'll also want a Vec<Option<T>> as IntoIterator>::Item = Option<T>

Ariel Ben-Yehuda (Jun 26 2019 at 21:28, on Zulip):

that would be a very complicated family of where-clauses

RalfJ (Jun 26 2019 at 21:28, on Zulip):

hm I see, you are saying that constraint would have to bubble up way beyond the code that actually does the iteration

Ariel Ben-Yehuda (Jun 26 2019 at 21:28, on Zulip):

I mean, if you couldn't reduce it to "where all the impls in this crate hold"

Ariel Ben-Yehuda (Jun 26 2019 at 21:29, on Zulip):

which is the state we have today :-)

RalfJ (Jun 26 2019 at 21:31, on Zulip):

so maybe this is less practical than I thought...

Ariel Ben-Yehuda (Jun 26 2019 at 21:31, on Zulip):

I mean, you could prohibit associated types in structs

Ariel Ben-Yehuda (Jun 26 2019 at 21:31, on Zulip):

*in item fields

RalfJ (Jun 26 2019 at 21:31, on Zulip):

but the alternative seems to be to consider the implicit impl Trait for dyn Trait a real impl in terms of coherence, which would reject plenty of generic impls

Ariel Ben-Yehuda (Jun 26 2019 at 21:32, on Zulip):

but the alternative seems to be to consider the implicit impl Trait for dyn Trait a real impl in terms of coherence, which would reject plenty of generic impls

or do "impl priority" where it only holds if there is no other impl, or some hack like that

Ariel Ben-Yehuda (Jun 26 2019 at 21:32, on Zulip):

I prefer having to specify explicitly whether a trait is object-safe to not having associated types in struct fields

Ariel Ben-Yehuda (Jun 26 2019 at 21:32, on Zulip):

even from a blank-slate POV

Ariel Ben-Yehuda (Jun 26 2019 at 21:33, on Zulip):

(not that "having to specify explicitly whether a trait is object-safe" is a good idea)

RalfJ (Jun 26 2019 at 21:33, on Zulip):

or do "impl priority" where it only holds if there is no other impl, or some hack like that

this needs chalk and a proof or I dont believe it to be sound^^

RalfJ (Jun 26 2019 at 21:33, on Zulip):

(not that "having to specify explicitly whether a trait is object-safe" is a good idea)

that's actually a great idea

Ariel Ben-Yehuda (Jun 26 2019 at 21:33, on Zulip):

@RalfJ
the most basic form would be having a dyn Trait be non-object-safe if it has a blanket impl

RalfJ (Jun 26 2019 at 21:34, on Zulip):

also in terms of semver where today you can accidentally break rev dependencies by changing a trait from obj-safe to not-obj-safe

RalfJ (Jun 26 2019 at 21:34, on Zulip):

I have seen people asking for an explicit annotation like that before

Ariel Ben-Yehuda (Jun 26 2019 at 21:34, on Zulip):

that might be the solution area

RalfJ (Jun 26 2019 at 21:34, on Zulip):

I prefer having to specify explicitly whether a trait is object-safe to not having associated types in struct fields

why would struct fields be special here?

Ariel Ben-Yehuda (Jun 26 2019 at 21:34, on Zulip):

why would struct fields be special here?

if item fields don't have associated types, you "sort of don't need associated types"

Ariel Ben-Yehuda (Jun 26 2019 at 21:35, on Zulip):

you could stay in the pre-1.0 world where everything was type parameters and HRTBs

Ariel Ben-Yehuda (Jun 26 2019 at 21:35, on Zulip):

and a bit of inference magic

RalfJ (Jun 26 2019 at 21:35, on Zulip):

that sounds... surprising?

Ariel Ben-Yehuda (Jun 26 2019 at 21:36, on Zulip):

I mean, when you have a trait Foo { type Assoc; }, you can translate it to trait Foo {}. trait Foo2<Assoc>; "forall<T> T: Foo -> exists U. T: Foo2<U>"

Ariel Ben-Yehuda (Jun 26 2019 at 21:37, on Zulip):

i.e., just give up on associated type uniqueness

RalfJ (Jun 26 2019 at 21:37, on Zulip):

but didnt you just argue above that that would be awful for e.g. <Vec<T> as IntoIterator>::Item?

Ariel Ben-Yehuda (Jun 26 2019 at 21:37, on Zulip):

I mean, in that place, type inference can pick the impl associated type

Ariel Ben-Yehuda (Jun 26 2019 at 21:37, on Zulip):

and it does not matter whether there is any other impl

Ariel Ben-Yehuda (Jun 26 2019 at 21:38, on Zulip):

(you also need to move all trait-items to the "most detailed" trait)

Ariel Ben-Yehuda (Jun 26 2019 at 21:38, on Zulip):

(or parameterize them or something)

Ariel Ben-Yehuda (Jun 26 2019 at 21:39, on Zulip):

that was what rust did before 1.0

Ariel Ben-Yehuda (Jun 26 2019 at 21:39, on Zulip):

and I think this is basically Haskell without TypeFamilies

Ariel Ben-Yehuda (Jun 26 2019 at 21:39, on Zulip):

which is a language that you can do things in

Ariel Ben-Yehuda (Jun 26 2019 at 21:40, on Zulip):

and the main problem is basically "putting associated types in structs"

RalfJ (Jun 26 2019 at 21:42, on Zulip):

and it does not matter whether there is any other impl

oh I see... the case that wouldn't work though is fn foo<T>(t: <T as Iterator>::Item) -> <T as IntoIterator>::Item where T: Iterator + IntoIterator

RalfJ (Jun 26 2019 at 21:42, on Zulip):

because then you dont know which impl it is

RalfJ (Jun 26 2019 at 21:42, on Zulip):

so maybe we can just rule out that kind of "expoitingcoherence"? or does your other example in the issue show that that's not enough?

Ariel Ben-Yehuda (Jun 26 2019 at 21:43, on Zulip):

because then you dont know which impl it is

sure, and in that case you'll need an extra equality clause

Ariel Ben-Yehuda (Jun 26 2019 at 21:43, on Zulip):

so maybe we can just rule out that kind of "expoitingcoherence"? or does your other example in the issue show that that's not enough?

I think that once you have associated types in struct fields, you need full coherence

Ariel Ben-Yehuda (Jun 26 2019 at 21:44, on Zulip):

or a struct could require you to "commit" to all of the types of its fields, but that would be ugly

Ariel Ben-Yehuda (Jun 26 2019 at 21:45, on Zulip):

so yea I think T-lang should come up with the solution for #57893

centril (Jun 26 2019 at 21:46, on Zulip):

@Ariel Ben-Yehuda by "coherence" do you mean "every different valid typing derivation of a program leads to a resulting program that has the same dynamic semantics" or do you mean canonicity (global uniqueness)? I assume the latter

Ariel Ben-Yehuda (Jun 26 2019 at 21:46, on Zulip):

I mean unique associated type resolution

Ariel Ben-Yehuda (Jun 26 2019 at 21:47, on Zulip):

for every concrete associated trait-ref <Foo as Bar>::Baz, there is exactly 1 way to resolve it

centril (Jun 26 2019 at 21:48, on Zulip):

@Ariel Ben-Yehuda I'll need to digest your example on the issue tomorrow then... too tired now ^^

centril (Jun 26 2019 at 21:50, on Zulip):

@Ariel Ben-Yehuda Anyways, we've booked a lang team meeting for #57893 on the 11th of July; there's an entry on the lang team calendar if you want to join (which would be great)

Ariel Ben-Yehuda (Jun 26 2019 at 21:50, on Zulip):

which time is that?

Ariel Ben-Yehuda (Jun 26 2019 at 21:51, on Zulip):

(btw, if we treat methods as associated trait-refs, that description of coherence explains why incoherent marker traits are not a problem - still every ATR resolves in exactly 1 way)

centril (Jun 26 2019 at 21:54, on Zulip):

@Ariel Ben-Yehuda 21:00 CEST I believe (summer time is tricky... check the calendar :D )

Ariel Ben-Yehuda (Jun 26 2019 at 21:55, on Zulip):

it says 15:00 boston time, which is indeed 21:00 CEST

centril (Jun 27 2019 at 08:06, on Zulip):

@Ariel Ben-Yehuda so looking at your example, adding where dyn Object<U, Output = T>: Object<U, Output = T>, to iso1 solves nothing; A constraint where dyn Object<U, Output = T>: Object<U, Output = V>, on transmute_m would solve things but to do that you'd need to look inside transmute_m which would be very ungreat in terms of the phase separation of the current compiler

centril (Jun 27 2019 at 08:12, on Zulip):

@RalfJ @Ariel Ben-Yehuda Oh but interestingly, if we add X: Object<U, Output = V> to iso2 we make transmute_m not type check. This assumption can be deduced purely from the signature of iso2 so we do not have to ruin phase separation

centril (Jun 27 2019 at 08:24, on Zulip):

From what I can tell this comes down to a question of increased compile-times + a-more-trusted-analysis (adding new proof obligations when derivations from coherence are made) vs. giving up on some sound code and losing out on completeness (object safety taking blanket impls into account)

RalfJ (Jun 27 2019 at 09:13, on Zulip):

Yeah iso2 is the "bad" one there I think

centril (Jun 27 2019 at 09:16, on Zulip):

@RalfJ In the sense that it is not requiring things it should from its callers (which really makes transmute_m the bit that would stop type checking)

RalfJ (Jun 27 2019 at 09:20, on Zulip):

yes

Ariel Ben-Yehuda (Jun 28 2019 at 16:53, on Zulip):

@RalfJ @centril do you have a principled rule?

I think we have 4 classes of options for fixing things here:
1. Making the blanket impl a coherence violation, which might have bad back-compat consequences, and is somewhat hard to implement in the compiler today (because of the dyn Trait+AnySetOfSubtraits problem, and also the for<'a> dyn Trait<'a> problem, unless we already modified coherence such that it is eqty to dyn Trait<'a> in coherence).
2. Making iso_1 be illegal in its current form ("requiring it to have an extra where-clause"). In Chalk terms, the rule iso_1 uses is the <dyn Object<U, Output=T> as Object<U, Output=T>>::Output = T :-, the ObjectCandidate in rustc terms.
I think it is possible to allow the ObjectCandidate rule only if there are no potentially-conflicting impls. One way of doing it would be to make Trait non-object-safe (in Rust terms), using the coherence conflict as the justificataion.
3. Making iso_2 be illegal in its current form ("requiring it to have an extra where-clause"). In Chalk terms, the rule iso_2 uses is <T as Object<U>>::Output = V := U: Mark, <U as Mark>::Output = V. This is very similar to the rule that allows you to work with IntoIterator, so I don't think it is a good idea to get rid of it, unless you have a principled exception in mind.
4. Making transmute_m illegal. ~~I can't think of a way of doing this that doesn't also make iso_1 directly illegal.
~~ Actually, if we consider the "object impl" to be an implied bound on the object ADT, then the equivalent of 2. would prohibit transmute_m rather than iso_1, because iso_1 would get what it needs through an implied bound and not need the ObjectCandidate.

How do your ideas fit in this mold?

Ariel Ben-Yehuda (Jun 28 2019 at 16:56, on Zulip):

@RalfJung @centril

so I think what you wrote is basically a variant of 3., except it would add an "implicit" X: Object<U, Output = V> bound to iso_2 to make it "work again". Do you have a principled way of doing it?

Ariel Ben-Yehuda (Jun 28 2019 at 16:56, on Zulip):

@RalfJ

RalfJ (Jun 28 2019 at 16:59, on Zulip):

I'm afraid I dont have anything principled to say here

RalfJ (Jun 28 2019 at 16:59, on Zulip):

I have an intuition from thinking about modelling traits in lambda-rust, but we haven't modeled them yet

RalfJ (Jun 28 2019 at 16:59, on Zulip):

and I know nothing about how rustc/chalk actually implements all the trait rules

Ariel Ben-Yehuda (Jun 28 2019 at 16:59, on Zulip):

sure, I think the precise modeling of trait objects is important here

RalfJ (Jun 28 2019 at 17:00, on Zulip):

absolutely

RalfJ (Jun 28 2019 at 17:00, on Zulip):

every time some knocks on derek's door that's one of the projects he is proposing ;)

RalfJ (Jun 28 2019 at 17:01, on Zulip):

but so far people picked other projects

RalfJ (Jun 28 2019 at 17:01, on Zulip):

my intuition here is that iso_2 is sneakily hiding an assumption that it is making... iso_1 seems perfectly fine to me, after all it specifically asked for this associated type

centril (Jun 28 2019 at 17:03, on Zulip):

All I can say is... we need to steal Stephanie Weirich, Richard Eisenberg, and more Haskell folks ;)

centril (Jun 28 2019 at 17:04, on Zulip):

@Ariel Ben-Yehuda so I think mine (our?) thinking is that we do 4. by adding an implicit V == <X as Object<U>>::Output eq-constraint

Ariel Ben-Yehuda (Jun 28 2019 at 17:04, on Zulip):

@centril I consider it a form of 3.

Ariel Ben-Yehuda (Jun 28 2019 at 17:04, on Zulip):

or of 2

Ariel Ben-Yehuda (Jun 28 2019 at 17:05, on Zulip):

actually, forbidding you from proving WF(dyn Object<U, Output=T>) would be a form of 4. that might not be 2.

centril (Jun 28 2019 at 17:05, on Zulip):

Well it revolves around iso2; I agree with @RalfJ that iso2 is not properly propagating its assumption

Ariel Ben-Yehuda (Jun 28 2019 at 17:06, on Zulip):

because 2 would get WF(dyn Object<U, Output=T>) as an assumption, and therefore it wouldn't need to prove it

RalfJ (Jun 28 2019 at 17:08, on Zulip):

what happened to the idea that one can do #[dyn] trait { ... } and doing so makes coherence consider the implicit impl, thereby ruling out the blanket impl in your example?

centril (Jun 28 2019 at 17:08, on Zulip):

@Ariel Ben-Yehuda as for "how do we do this"... I'm thinking that "when we assume a blanket impl in a signature we also add a constraint for that assumption to said signature"

RalfJ (Jun 28 2019 at 17:08, on Zulip):

i guess that would be a variant of 1)

centril (Jun 28 2019 at 17:08, on Zulip):

but that might be awfully hand-wavy

Ariel Ben-Yehuda (Jun 28 2019 at 17:09, on Zulip):

@RalfJ that's 1.

Ariel Ben-Yehuda (Jun 28 2019 at 17:10, on Zulip):

@centril but you don't assume the blanket impl in the signature

Ariel Ben-Yehuda (Jun 28 2019 at 17:11, on Zulip):

I suppose we might ask the Chalk people @scalexm

centril (Jun 28 2019 at 17:13, on Zulip):

Then I don't get how:

fn iso_2<X: ?Sized, U, V>(data: Data<X, U>) -> V
where
    U: Mark<Output = V>,
{
    // similarly, this shouldn't "see" the trait-object impl.
    data.data
}

can type-check

centril (Jun 28 2019 at 17:13, on Zulip):

Removing:

impl<T: ?Sized, U: Mark<Output = V>, V> Object<U> for T {
    type Output = V;
}

makes fn iso2 not type-check

centril (Jun 28 2019 at 17:15, on Zulip):

This notably does not rely on the body of iso2; if you replace it with panic!() and remove either U: Mark<Output = V> or the blanket impl it won't type check

Ariel Ben-Yehuda (Jun 28 2019 at 17:16, on Zulip):

Yea it requires an X: Object<U> bound

Ariel Ben-Yehuda (Jun 28 2019 at 17:17, on Zulip):

and because of a weird rustc limitation, a X: Object<U> requires you to specify V

Ariel Ben-Yehuda (Jun 28 2019 at 17:17, on Zulip):

but perhaps that rustc limitation could be formalized

Ariel Ben-Yehuda (Jun 28 2019 at 17:18, on Zulip):

but in an implied bounds setting, iso_2 would compile and the X: Object<U> bound would be passed to the caller

Ariel Ben-Yehuda (Jun 28 2019 at 17:18, on Zulip):

(in fact, today, transmute_m already has to prove X: Object<U>)

centril (Jun 28 2019 at 17:19, on Zulip):

Propagating these assumed un-propagated constraints may however be expensive... I would suggest that we try the various 1-4 strategies, @craterbot and @rust-timer build them and see what falls out

Ariel Ben-Yehuda (Jun 28 2019 at 17:37, on Zulip):

so I'm still thinking whether there is a way to abuse the absence of coherence

Ariel Ben-Yehuda (Jun 28 2019 at 17:39, on Zulip):

or rather, of figuring out a sound/allows-all-the-code-we-want-compiling--to-compile rule, or why we don't want such a rule

Ariel Ben-Yehuda (Jun 28 2019 at 17:39, on Zulip):

of course, the general boogeyman of these would be specialization

Ariel Ben-Yehuda (Jun 28 2019 at 17:39, on Zulip):

but we still have no idea when specialization is sound, so I'll rather not try to rely on it

Ariel Ben-Yehuda (Jun 28 2019 at 20:46, on Zulip):

So I think I found a hole in my naïve attempt to implement @RalfJ's suggestion: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=dc1bdbf5d59a3dba86fa3c9ece8556fc

Ariel Ben-Yehuda (Jun 28 2019 at 20:47, on Zulip):

there's no way to see Object in the signature of iso_2, because it gets wrapped in the HidingPlace

centril (Jun 28 2019 at 20:48, on Zulip):

Thanks :sweat_smile: I'll read it tomorrow

RalfJ (Jun 28 2019 at 20:49, on Zulip):

iso_2 still stops type-checking without the blanket impl though

Ariel Ben-Yehuda (Jun 28 2019 at 20:53, on Zulip):

@RalfJ sure it does

Ariel Ben-Yehuda (Jun 28 2019 at 20:53, on Zulip):

but what can you do with it?

Ariel Ben-Yehuda (Jun 28 2019 at 20:54, on Zulip):

I mean, you don't want type inference to depend on function bodies

Ariel Ben-Yehuda (Jun 28 2019 at 20:54, on Zulip):

*function signatures to depend on function bodies

RalfJ (Jun 28 2019 at 20:55, on Zulip):

it doesnt have to -- but (and I think I said that in the issue) it would have to basically aggressively collect all the facts that the body might use and add them to the "signature"

Ariel Ben-Yehuda (Jun 28 2019 at 20:55, on Zulip):

That means that type inference depends on function bodies

RalfJ (Jun 28 2019 at 20:55, on Zulip):

I have no idea if that is even remotely practical

Ariel Ben-Yehuda (Jun 28 2019 at 20:55, on Zulip):

and I expect it to have weird effects with things like IntoIterator

RalfJ (Jun 28 2019 at 20:55, on Zulip):

hu, how that?

Ariel Ben-Yehuda (Jun 28 2019 at 20:56, on Zulip):

I mean, to see whether iso_2 typechecks, you have to see the body of iso_2

Ariel Ben-Yehuda (Jun 28 2019 at 20:56, on Zulip):

plus, you can make iso_2 a trait function

Ariel Ben-Yehuda (Jun 28 2019 at 20:56, on Zulip):

so you can't do "naive" propagation

RalfJ (Jun 28 2019 at 20:56, on Zulip):

I said none of that

RalfJ (Jun 28 2019 at 20:56, on Zulip):

I said collect all facts it might use

RalfJ (Jun 28 2019 at 20:56, on Zulip):

without knowing what it actually does use

RalfJ (Jun 28 2019 at 20:57, on Zulip):

basically going forward from the where clauses we got, what are all the things we can deduce? these all become part of the "signature"

RalfJ (Jun 28 2019 at 20:57, on Zulip):

and again, I have no idea if that's even remotely practical ;)

centril (Jun 28 2019 at 20:58, on Zulip):

That feels like it could blow up very easily in terms of compile times ^^

Ariel Ben-Yehuda (Jun 28 2019 at 20:58, on Zulip):

I mean, if you go by the "might use" idea, you can notice that you have a coherence violation

Ariel Ben-Yehuda (Jun 28 2019 at 20:58, on Zulip):

everything "might use" a coherence violation

Ariel Ben-Yehuda (Jun 28 2019 at 20:58, on Zulip):

which means that code with a coherence violation does not compile

centril (Jun 28 2019 at 20:58, on Zulip):

@Ariel Ben-Yehuda

That means that type inference depends on function bodies

I'm not opposed to this :slight_smile:

centril (Jun 28 2019 at 20:58, on Zulip):

I know everyone else is tho

Ariel Ben-Yehuda (Jun 28 2019 at 20:59, on Zulip):

I'm not opposed to this

This doesn't scale to traits. Suppose you have

trait Iso2 {
fn iso_2<X: ?Sized, U, V, D>(data: D) -> V
    where U: Mark<Output=V>, D: HidingPlace<X, U>;
}

impl Iso2 for MyIso2 {
    ...
}

trait TransmuteM {
fn transmute_m<T, U, V, I: Iso2>(data: T) -> V
    where U: Mark<Output=V>;
}

impl TransmuteM for MyTransmuteM {
fn transmute_m<T, U, V, I: Iso2>(data: T) -> V
    where U: Mark<Output=V> { /* ... */ }
}
centril (Jun 28 2019 at 21:02, on Zulip):

(Is there anything in particular that Rust has that Haskell doesn't here apart from type based dispatch with methods?)

centril (Jun 28 2019 at 21:02, on Zulip):

(Given that Haskell does have global type inference)

Ariel Ben-Yehuda (Jun 28 2019 at 21:02, on Zulip):

The problem here is not global type inference

Ariel Ben-Yehuda (Jun 28 2019 at 21:02, on Zulip):

I don't think typeclasses in haskell have type inference

Ariel Ben-Yehuda (Jun 28 2019 at 21:02, on Zulip):

TransmuteM would be a typeclass in Haskell

centril (Jun 28 2019 at 21:04, on Zulip):

@Ariel Ben-Yehuda type class definitions and instance heads do not; functions certainly do infer type class constraints in Haskell

Ariel Ben-Yehuda (Jun 28 2019 at 21:04, on Zulip):

@centril sure, but here what you want is for the constraint on the body of MyIso2 to somehow transfer to the typeclass definition for the trait Iso2

centril (Jun 28 2019 at 21:05, on Zulip):

I'll need to look at your newest example more carefully tomorrow and get back to you :slight_smile:

Ariel Ben-Yehuda (Jun 28 2019 at 21:06, on Zulip):

ok

Ariel Ben-Yehuda (Jun 29 2019 at 17:36, on Zulip):

And my next obstacle to iso-2-blaming: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=b96e34ea38383adabe1850d049e9e9b0

Ariel Ben-Yehuda (Jun 29 2019 at 17:36, on Zulip):

which "hides" the evidence for Mark by using MarkWitness

Ariel Ben-Yehuda (Jun 29 2019 at 17:44, on Zulip):

in that place, Iso2Observer::observe uses the ImplCandidate (to normalize the result of get_data). However, I don't see a way of forcing it to propagate its requirement without breaking IntoIterator

Ariel Ben-Yehuda (Jun 29 2019 at 17:45, on Zulip):

aka, while allowing it to use things like <Vec<U> as IntoIterator>

scalexm (Jul 03 2019 at 16:51, on Zulip):

@Ariel Ben-Yehuda I’ve not exactly followed the solutions you have in mind so far, but to me there are basically two realistic solutions:

Is that right? Are there any problems with, e.g. the second approach?

Ariel Ben-Yehuda (Jul 03 2019 at 16:52, on Zulip):

@scalexm

I'm not sure the coherence solution is too bad

scalexm (Jul 03 2019 at 16:52, on Zulip):

(Other than breaking compatibility of course)

Ariel Ben-Yehuda (Jul 03 2019 at 16:52, on Zulip):

I'm not sure people are abusing things sufficiently badly that we have a coherence problem

scalexm (Jul 03 2019 at 16:52, on Zulip):

What are you calling « coherence solution »?

Ariel Ben-Yehuda (Jul 03 2019 at 16:53, on Zulip):

making the bad impl illegal

Ariel Ben-Yehuda (Jul 03 2019 at 16:53, on Zulip):

I mean, we have an unsoundness, everything is going to break compatibility

scalexm (Jul 03 2019 at 16:53, on Zulip):

Right

scalexm (Jul 03 2019 at 16:54, on Zulip):

So you prefer « making the impl illegal » rather than « making it illegal to use the trait as a trait object »

Ariel Ben-Yehuda (Jul 03 2019 at 16:55, on Zulip):

I'm not sure

Ariel Ben-Yehuda (Jul 03 2019 at 16:56, on Zulip):

this feels like a lang-design question that might need some thought

Ariel Ben-Yehuda (Jul 03 2019 at 16:56, on Zulip):

@scalexm BTW, how can we do impl precedence?

scalexm (Jul 03 2019 at 16:57, on Zulip):

@Ariel Ben-Yehuda I don’t know :)

scalexm (Jul 03 2019 at 16:57, on Zulip):

But if it were possible, it would presumably break less code?

Ariel Ben-Yehuda (Jul 03 2019 at 16:57, on Zulip):

I'm not sure

Ariel Ben-Yehuda (Jul 03 2019 at 16:57, on Zulip):

it feels like any real way of doing it would manage to break some code

Ariel Ben-Yehuda (Jul 03 2019 at 16:58, on Zulip):

what with it being a fairly-big change and all

scalexm (Jul 03 2019 at 16:58, on Zulip):

Yes

Ariel Ben-Yehuda (Jul 03 2019 at 16:58, on Zulip):

and we're still not sure that preventing the trait from being "object-safe" would break things

Ariel Ben-Yehuda (Jul 03 2019 at 16:58, on Zulip):

my actual idea for non-object-safety was uglier but more permitting

Ariel Ben-Yehuda (Jul 03 2019 at 16:59, on Zulip):

you make the ObjectCandidate not apply when an ImplCandidate can "possibly" match

Ariel Ben-Yehuda (Jul 03 2019 at 16:59, on Zulip):

i.e., basically add negative bounds to the object candidate

scalexm (Jul 03 2019 at 17:00, on Zulip):

I see

Last update: Nov 16 2019 at 01:00UTC