StreamingIterator code panics with "zipping things of mixed type" about chalk

[mikeyhew]

I just realized, the a = '?0, b = Array3<i32> that was output is from a println!() statement I added to figure out what was going on (and then subsequently forgot about). This diff shows exactly what it's printing out:

diff --git a/src/zip.rs b/src/zip.rs
index 9f1f92e..b9398ff 100644
--- a/src/zip.rs
+++ b/src/zip.rs
@@ -256,6 +256,7 @@ impl<T: Zip, L: Zip> Zip for ParameterKind<T, L> {
                 Zip::zip_with(zipper, a, b),
             (&ParameterKind::Ty(_), _) |
             (&ParameterKind::Lifetime(_), _) => {
+                println!("a = {:?}, b = {:?}", a, b);
                 panic!("zipping things of mixed kind")
             }
         }

[nikomatsakis]

That is indeed a bug, though it may be that the bug is in the input. Chalk doesn't do that much sanity checking just now.

[scalexm]

I think that this is indeed a bug (I encountered it as well), which seems to occur when dealing with higher kinded associated types. The fix I guess is just to change the panic! message into a

return Err(NoSolution);

[nikomatsakis]

That sounds suspicious to me! Is it possible to reduce the test case at all?

[nikomatsakis]

I don't actually get this result:

Mr-Darcy. target/debug/chalki --program=$HOME/tmp/foo.chalk --goal='Array3<i32>: IntoStreamingIterator'
Unique; substitution [], lifetime constraints []

Mr-Darcy. target/debug/chalki --program=$HOME/tmp/foo.chalk --goal='Array3<i32>: IntoStreamingIterator' --solver slg
Unique; substitution [], lifetime constraints []

[lqd]

I've had this error before and I think — that is to say, if I've bisected correctly :) — that it was recently fixed by removing the fallback clauses: c92c25d

[scalexm]

The bug at the origin of this issue was still there though, but was fixed in #82.

[mikeyhew]

Since this issue has been closed, I tested out the above code with the current version of chalk, and indeed it no longer panics. Instead, it outputs "error: trait impl for "IntoStreamingIterator" does not meet well-formedness requirements".

Does anyone know why it is not well-formed, and what would need to be changed to make it well-formed?

[scalexm]

The recursive solver has some problems with projection types, try with the option --solver slg, it will work if you replace unselected projections (e.g. S::Item<'a>) with explicit projections (e.g. <S as StreamingInterator>::Item<'a>). However, it seems like there is still a bug with unselected projections.

[mikeyhew]

@scalexm no dice. The following two examples both produce the same well-formedness error message, even with --solver slg.

trait StreamingIterator {
    type Item<'a>;
}

trait IntoStreamingIterator where Self::IntoIter: StreamingIterator {
    type Item<'a>;
    type IntoIter;
}

impl<S> IntoStreamingIterator for S where S: StreamingIterator {
    type Item<'a> = <S as StreamingIterator>::Item<'a>;
    type IntoIter = S;
}

trait StreamingIterator {
    type Item<'a>;
}

trait IntoStreamingIterator where Self::IntoIter: StreamingIterator {
    type IntoIter;
}

impl<S> IntoStreamingIterator for S where S: StreamingIterator {
    type IntoIter = S;
}

[scalexm]

There's still Self::IntoIter which should be changed to <Self as IntoStreamingIterator>::IntoIter. So forgetting about the bug with unselected projections which does give a zipping things of mixed kind panic and which I'm currently fixing, unselected projections only work if you explicitly add an InScope assumption, for example:

if (InScope(IntoStreamingIterator)) {
    /* inside here you can use `MyType::IntoIter` without explicitly writing
        `<MyType as IntoStreamingIterator>::IntoIter` */
}

However, since well-formedness requirements are enforced during lowering (i.e. the program is loading, you cannot write any goal), one cannot use InScope during this phase unless it is explicitly written in the where clauses. This is a limitation indeed, I think we should add some InScope rules during lowering anyway, and this should be a separate issue.

[mikeyhew]

@scalexm good point, I replaced Self::IntoIter with the explicit version and it worked