Compilation help: type equality again?

[anon80458984]

pub trait Has<T1> {
    fn get(&self) -> &T1;}

pub struct C1<T1> {
    c1: T1,}

impl<T1> Has<T1> for C1<T1> {
    fn get(&self) -> &T1 {
        &self.c1}}

pub struct C2<T1, T2> {
    c1: T1,
    c2: T2,}

impl<T1, T2> Has<T1> for C2<T1, T2> {
    fn get(&self) -> &T1 {
        &self.c1}}

impl<T1, T2> Has<T2> for C2<T1, T2> {
    fn get(&self) -> &T1 {
        &self.c2}}

What is the simplest way to make this work? In the case of T1 == T2, I don't care which is returned (as long as it does not cause Rust UB).

[anon80458984]

I have something like this, which compiles & runs, but I am uncomfortable with not knowing whether type inference (for the Index#) will always succeed when there is a unique solution. Is there any standard that guarantees this will work (when the types are different), or is there some mysterious limit where type checking will just give up:

pub struct Index0 {}
pub struct Index1 {}
pub struct Index2 {}
pub struct Index3 {}
pub struct Index4 {}
pub struct Index5 {}
pub struct Index6 {}
pub struct Index7 {}
pub struct Index8 {}

pub trait Has<T, Loc> {
    fn get(&self) -> &T;}

pub struct Row2<T0, T1> {
    c0: T0,
    c1: T1,}

impl<T0, T1> Row2<T0, T1> {
    pub fn new(c0: T0, c1: T1) -> Row2<T0, T1> {
        Row2 { c0, c1}}}

impl<T0, T1> Has<T0, Index0> for Row2<T0, T1> {
    fn get(&self) -> &T0 {
        &self.c0}}

impl<T0, T1> Has<T1, Index1> for Row2<T0, T1> {
    fn get(&self) -> &T1 {
        &self.c1}}

fn stuff<L0, L1, X: Has<i64, L0> + Has<i32, L1>>(x: X) -> i64 {
    (&x as &dyn Has<i64, L0>).get() + (*(&x as &Has<i32, L1>).get() as i64)}

#[test]
fn test_00() {
    let x = Row2::<i64, i32>::new(1, 2);
    let y = stuff(x);
    println!("ans: {:?}", y);}

[ambiso]

Specialization might help with this, but I'm not yet sure how.

Negative trait bounds would probably solve this, but Rust doesn't implement them.
It could look something like this

impl<T1: !Has<T2>, T2: !Has<T1>> Has<T1> for C2<T1, T2> {
    fn get(&self) -> &T1 {
        &self.c1
    }
}

impl<T1: !Has<T2>, T2: !Has<T1> Has<T2> for C2<T1, T2> {
    fn get(&self) -> &T2 {
        &self.c2
    }
}

Also note that the type of get in impl Has<T2> for C2 is incorrect. It would also probably help others if you formatted your code (using cargo fmt for example).

[ambiso]

This should unify fine - you can even elide the types at the callsite:

(&x as &dyn Has<_, L0>).get() + (*(&x as &dyn Has<_, L1>).get() as i64)

Note the _ underscores

[anon80458984]

@ambiso

Negative trait bounds would probably solve this, but Rust doesn't implement them.

I agree with this statement. I think there is a logical reason that type checking can not support negative traits, but I do not know what reason is.

@ambiso

Specialization might help with this, but I'm not yet sure how.

I also agree with this statement; in particular something called min_specialization, but I have not figured out how to use it yet.

[anon80458984]

@ambiso

This should unify fine - you can even elide the types at the callsite:

(&x as &dyn Has<_, L0>).get() + (*(&x as &dyn Has<_, L1>).get() as i64)

I would actually prefer to write x.get::<i64>() + (x.get::<i32>() as i64) but have not yet figured out how to do that.

[ambiso]

Yeah, I'm not sure it's (supposed to be) possible.

This unfortunately doesn't work either:

struct True;
struct False;

trait Bool {}
impl Bool for True {}
impl Bool for False {}

trait IsNotEq<T2> {
    type Eq: Bool;
}

impl<T1, T2> IsNotEq<T2> for T1 {
    type Eq = True;
}

impl<T> IsNotEq<T> for T {
    type Eq = False;
}

[Yandros]

What should <&'a str as IsNotEq<&'b str>>::Eq yield? The compiler is unable to yield a consistent answer to the "is 'a equal to 'b" problem when dealing with trait solving (it's a complete separate part from borrow checking, which is the one part of the language able to consistently reason about lifetimes).

• And if the answer is incosistent, then you can trick the language into transmuting True into False and vice versa, that is, the language showcases type-related unsoundness, there. Hence why specialization was reduced to min_specialization, which denies such potentially ambiguous cases. The sad thing is that : 'static bounds on each type appearing on that snippet avoids the unsoundness issue (same reason why Any : 'static, by the way), but for some reason it doesn't help with the compilation

---

Anyhoo, here is a neat trick to help with the OP:

pub
trait Has<T1, Direction = ()> {
    fn get (self: &'_ Self)
      -> &'_ T1
    ;
}

#[allow(nonstandard_style)]
pub
mod Direction {
    pub enum Left {}
    pub enum Right {}
}

pub
struct C1<T1> {
    c1: T1,
}

impl<T1> Has<T1> for C1<T1> {
    fn get (self: &'_ C1<T1>)
      -> &'_ T1
    {
        &self.c1
    }
}

pub
struct C2<T1, T2> {
    c1: T1,
    c2: T2,
}

impl<T1, T2> Has<T1, Direction::Left>
    for C2<T1, T2>
{
    fn get (self: &'_ C2<T1, T2>)
      -> &'_ T1
    {
        &self.c1
    }
}

impl<T1, T2> Has<T2, Direction::Right>
    for C2<T1, T2>
{
    fn get (self: &'_ C2<T1, T2>)
      -> &'_ T2
    {
        &self.c2
    }
}

fn _with_basic<T1, T2> (c: C2<T1, T2>)
{
    let _: &T1 = c.get();
    let _: &T2 = c.get();
}

fn _with_equal<T> (c: C2<T, T>)
{
    // let _: &T = c.get(); // Error, type annotations needed
    let _: &T = Has::<_, Direction::Left>::get(&c);
}

• Playground

Note that the type annotation ambiguity can be palliated by adding an inherent impl on C2<T, T>:

impl<T> C2<T, T> {
    fn get (self: &'_ C2<T, T>)
      -> &'_ T
    {
        Has::<_, Direction::Left>::get(self)
    }
}

That way, when T1 == T2, C2<T1, T2> will showcase an inherent impl that shall shadow the one from the trait, dodging the ambiguity (and thus using the impl from there, which I've arbitrarily chosen to pick from the left). And if we considern back the T1 = &'a str, T2 = &'b str kind of situation, then, well, depending on whether 'a is considered equal to 'b or not, there shall be ambiguity and a compilation error or not, which is not unsound and gives a chance to the programmer to disambiguate.

[anon80458984]

I think I am missing something basic. Is there a benefit of Left, Right vs Index0, Index1 ? In particular, I end up building something like:

pub struct Row9<T0, T1, T2, T3, T4, T5, T6, T7, T8>(T0, T1, T2, T3, T4, T5, T6, T7, T8);

impl<T0, T1, T2, T3, T4, T5, T6, T7, T8> Row9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
    fn mget<T, Index: 'static>(&self) -> &T
    where
        Self: Has<T, Index>,
    {
        (self as &dyn Has<T, Index>).get()}}

impl<T0, T1, T2, T3, T4, T5, T6, T7, T8> Row9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
    pub fn new(
        c0: T0,
        c1: T1,
        c2: T2,
        c3: T3,
        c4: T4,
        c5: T5,
        c6: T6,
        c7: T7,
        c8: T8,
    ) -> Row9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
        Row9(c0, c1, c2, c3, c4, c5, c6, c7, c8)}}

impl<T0, T1, T2, T3, T4, T5, T6, T7, T8> Has<T0, Index0>
    for Row9<T0, T1, T2, T3, T4, T5, T6, T7, T8>
{
    fn get(&self) -> &T0 {
        &self.0}}

impl<T0, T1, T2, T3, T4, T5, T6, T7, T8> Has<T1, Index1>
    for Row9<T0, T1, T2, T3, T4, T5, T6, T7, T8>
{
    fn get(&self) -> &T1 {
        &self.1}}

[Yandros]

Sorry, missed the post with your Indexes. So you're right, it's really the same solution

If you have that many indices, by the way, you could even go and use:

enum Index<const N: usize> {}

to write Index<0>, Index<1>, and so on. This could have the advantage to let you write some (other) trait with a get_nth::<3>(row)

[anon80458984]

Thanks for clarifying. One thing I am still uncomfortable with this solution -- is Rust's type checker inference guaranteed to run to completion, or is there some level of complexity where the type inference engine goes:

• maximum recursion level reached
• I give up
• user needs to specify more info

in which case, this solution breaks down

[Yandros]

I'm not knowledgeable enough of the actual compiler internals to answer that (most of my knowledge is empirical ), but these inference / trait solving problems look like existential logic-based solving problems; in practice they are impressively powerful and good at solving this kind of problems, although in theory they are "too expressive" / powerful (Turing complete) which makes them generally undecidable / there exist inputs that will make the trait solver "try to loop indefinitely" (which, for the sake of user feedback, will probably hit a hard-coded recursion limit in the compiler (which thus means that rather than Turing complete, there are legitimately correct code inputs that trigger a compiler error; off the top of my head I'd say that already if you nest a type too much (e.g., Option<Option<… 260 times … <()>> … >) you can hit these hard-coded errors)).

• This whole blog post is a very interesting read as a whole, and has a dedicated section where it talks about trait solving / unification, which seems impressively relevant here:

  @https://sdleffler.github.io/RustTypeSystemTuringComplete/#type-level-smallfuck-in-rust

  Type-Level Smallfuck in Rust

  Rust has a feature called traits. Traits are a way of doing compile-time static
  dispatch, and can also be used to do runtime dispatch (although in practice that's
  rarely useful.) I will assume here that the reader knows what traits are in Rust
  and has used them a fair amount. To implement Smallfuck, we'll be relying on a
  particular feature of traits known as associated types.

  Trait resolution and unification

  In Rust, in order to call a trait method or resolve an associated type, the compiler
  must go through a process called trait resolution. In order to resolve a trait,
  the compiler has to look for an impl which unifies with the types involved.
  Unification is a
  process for solving equations between types. If there is no solution, we say that
  unification has failed. Here's an example:

  trait Foo<B> {
     type Associated;
  }
  
  
  impl<B> Foo<B> for u16 {
      type Associated = bool;
  }
  
  
  impl Foo<u64> for u8 {
      type Associated = String;
  }
  

  This is a very contrived example, but it will serve a point. In order to resolve
  a reference to an associated type (e.g. <F as Foo<T>>::Associated), the Rust
  compiler has to search for an impl which matches F and T correctly. Let's
  say that we have F == u16 and T == u64. What if the compiler tries the
  second impl, of Foo<u64> for u8? Then it will immediately find that F does
  not match u8 -- so, it's not the impl we're looking for. What if it tries the
  first? Then we have F == u16, which is true, so all good. Now we have to match
  T == B. And here's where the magic happens.

  The Rust compiler unifies
  F with B. Since B is a type variable -- not a concrete type, like String
  or u64 -- its value is free to be assigned. So now B is replaced with u64,
  and going through with the substitution of B => u64, we now have an impl of
  Foo<u64> for u16 which is valid. Unification is a fairly simple procedure: it
  takes in a type (term) which may have variables, and every time it runs into a place where
  a variable that hasn't yet been assigned is matched against any other term, the
  variable is assigned to that term (even if the other term is a variable!) Then,
  any time that variable is come across while unifying the same term, it's replaced
  with its assigned value, and instead unification tries to unify the assigned value
  against the other term.

  The output of unification is a "substitution" - a mapping of variables to terms,
  such that when you take the terms you were trying to unify and replace all the
  variables mentioned in the substitution with the terms they're mapped to, you end
  up with two identical terms. Here's a standalone example of unification, trying
  to unify Foo<X, Bar<u16, Z> with Foo<Baz, Y>:

  Foo<X, Bar<u16, Z>> == Foo<Baz, Y>
  

  First we check the heads of the terms - we get Foo vs. Foo, which checks out.
  So we haven't failed to unify yet. If we had, say, Foo == Bar, then unification
  would fail. Next, we decompose this into two subproblems. We know Foo<A, B> == Foo<C, D>
  if and only if A == C and B == D:

  X == Baz, Bar<u16, Z> == Y
  

  We've now solved a variable -- X has a clearly defined value, Baz. So we can
  now add to our substitution, [X -> Baz]. Then, we apply that substitution to the
  second term, Bar<u16, Z> == Y. Since there are no occurrences of X in there,
  nothing happens, and we're left with the same term. And then we have a solution
  for Y. So our final substitution looks like [X -> Baz, Y -> Bar<u16, Z>]. Let's
  observe what happens when we apply that to the original equation we wanted to check:

  Foo<X, Bar<u16, Z>> == Foo<Baz, Y> [X -> Baz, Y -> Bar<u16, Z>]
  

  Becomes:

  Foo<Baz, Bar<u16, Z>> == Foo<Baz, Bar<u16, Z>>
  

  Which is obviously true. The two terms are now equal! So what's an example of
  unification failing? Let's try:

  Foo<Bar, X> == Foo<X, Baz>
  

  Which breaks down into two equations:

  Bar == X, X == Baz
  

  So we solve the first equation, obtaining the substitution [X -> Bar]. Applying
  this to X == Baz yields Bar == Baz, which is clearly false. So our unification
  has failed -- there isn't a solution.

  Unification is such a useful process that there actually exists a programming
  language, Prolog, which describes programs
  through logical terms, and execution is unification of terms. So that seems suspicious.
  If you have a Turing-complete language, Prolog, which is based off of unification,
  then it seems straightforward that Rust's trait resolution -- which works by attempting
  to unify trait impls until it finds the one which works -- might be Turing-complete
  as well.

---

In practice, for your use case, I'd say that solving these type inference problems (inferring the Index{…} types) is trivial for it to solve, and that thus the only limitation you will hit is when you have duplicated types which make the solutions non-unique, and thus require disambiguation.

[2e71828]

@anon80458984

is Rust's type checker inference guaranteed to run to completion

There are recursion limits in place for the type checker, but they can be raised with the #![recursion_limit = "..."] directive. Without the limit, though, you still can’t ensure the compilation will complete because the trait solver is Turing-complete all on its own. (cf Appendix A of my Master's thesis)