StreamingIterator code panics with "zipping things of mixed type"

[mikeyhew]

The following program panics with the error message "zipping things of mixed type", after outputting a = '?0, b = Array3<i32>.

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::Item<'a>;
    type IntoIter = S;
}

struct i32 {}
struct usize {}

struct Ref<'a, T> {}

struct Array3<T> {_1: T, _2: T, _3: T}

struct Array3IntoIter<T> {
    array: Array3<T>,
    index: usize
}

impl<T> StreamingIterator for Array3IntoIter<T> {
    type Item<'a> = Ref<'a, T>;
}

impl<T> IntoStreamingIterator for Array3<T> {
    type Item<'a> = Ref<'a, T>;
    type IntoIter = Array3IntoIter<T>;
}

// goal: Array3<i32>: IntoStreamingIterator

output including backtrace

$ RUST_BACKTRACE=1 cargo run -- --program=streaming_iterator.chalk --goal='Array3<i32>: IntoStreamingIterator'
    Finished dev [unoptimized + debuginfo] target(s) in 0.0 secs
     Running `target/debug/chalki --program=streaming_iterator.chalk '--goal=Array3<i32>: IntoStreamingIterator'`
a = '?0, b = Array3<i32>
thread 'main' panicked at 'zipping things of mixed kind', src/zip.rs:260:16
stack backtrace:
   0: std::sys::imp::backtrace::tracing::imp::unwind_backtrace
             at src/libstd/sys/unix/backtrace/tracing/gcc_s.rs:49
   1: std::sys_common::backtrace::_print
             at src/libstd/sys_common/backtrace.rs:69
   2: std::panicking::default_hook::{{closure}}
             at src/libstd/sys_common/backtrace.rs:58
             at src/libstd/panicking.rs:381
   3: std::panicking::default_hook
             at src/libstd/panicking.rs:397
   4: std::panicking::begin_panic
             at src/libstd/panicking.rs:577
   5: std::panicking::begin_panic
             at /Users/travis/build/rust-lang/rust/src/libstd/panicking.rs:538
   6: <chalk::ir::ParameterKind<T, L> as chalk::zip::Zip>::zip_with
             at src/zip.rs:260
   7: <[T] as chalk::zip::Zip>::zip_with
             at src/zip.rs:83
   8: <alloc::vec::Vec<T> as chalk::zip::Zip>::zip_with
             at src/zip.rs:72
   9: <chalk::ir::UnselectedProjectionTy as chalk::zip::Zip>::zip_with
             at src/zip.rs:155
  10: <chalk::ir::UnselectedNormalize as chalk::zip::Zip>::zip_with
             at src/zip.rs:155
  11: <chalk::ir::DomainGoal as chalk::zip::Zip>::zip_with
             at src/zip.rs:189
  12: <T as chalk::ir::could_match::CouldMatch<T>>::could_match
             at src/ir/could_match.rs:12
  13: <T as chalk::ir::could_match::CouldMatch<T>>::could_match
             at src/ir/could_match.rs:53
  14: chalk::solve::recursive::Solver::solve_new_subgoal::{{closure}}
             at src/solve/recursive/mod.rs:232
  15: <core::iter::Filter<I, P> as core::iter::iterator::Iterator>::next
             at /Users/travis/build/rust-lang/rust/src/libcore/iter/mod.rs:1221
  16: <core::iter::Cloned<I> as core::iter::iterator::Iterator>::next
             at /Users/travis/build/rust-lang/rust/src/libcore/iter/mod.rs:443
  17: <alloc::vec::Vec<T> as alloc::vec::SpecExtend<T, I>>::from_iter
             at /Users/travis/build/rust-lang/rust/src/liballoc/vec.rs:1802
  18: <alloc::vec::Vec<T> as core::iter::traits::FromIterator<T>>::from_iter
             at /Users/travis/build/rust-lang/rust/src/liballoc/vec.rs:1715
  19: core::iter::iterator::Iterator::collect
             at /Users/travis/build/rust-lang/rust/src/libcore/iter/iterator.rs:1298
  20: chalk::solve::recursive::Solver::solve_new_subgoal
             at src/solve/recursive/mod.rs:228
  21: chalk::solve::recursive::Solver::solve_reduced_goal
             at src/solve/recursive/mod.rs:162
  22: chalk::solve::recursive::fulfill::Fulfill::prove
             at src/solve/recursive/fulfill.rs:195
  23: chalk::solve::recursive::fulfill::Fulfill::fulfill
             at src/solve/recursive/fulfill.rs:290
  24: chalk::solve::recursive::fulfill::Fulfill::solve
             at src/solve/recursive/fulfill.rs:337
  25: chalk::solve::recursive::Solver::solve_via_implication
             at src/solve/recursive/mod.rs:376
  26: chalk::solve::recursive::Solver::solve_from_clauses
             at src/solve/recursive/mod.rs:337
  27: chalk::solve::recursive::Solver::solve_new_subgoal
             at src/solve/recursive/mod.rs:236
  28: chalk::solve::recursive::Solver::solve_reduced_goal
             at src/solve/recursive/mod.rs:162
  29: chalk::solve::recursive::fulfill::Fulfill::prove
             at src/solve/recursive/fulfill.rs:195
  30: chalk::solve::recursive::fulfill::Fulfill::fulfill
             at src/solve/recursive/fulfill.rs:290
  31: chalk::solve::recursive::fulfill::Fulfill::solve
             at src/solve/recursive/fulfill.rs:337
  32: chalk::solve::recursive::Solver::solve_via_implication
             at src/solve/recursive/mod.rs:376
  33: chalk::solve::recursive::Solver::solve_from_clauses
             at src/solve/recursive/mod.rs:337
  34: chalk::solve::recursive::Solver::solve_new_subgoal
             at src/solve/recursive/mod.rs:236
  35: chalk::solve::recursive::Solver::solve_reduced_goal
             at src/solve/recursive/mod.rs:162
  36: chalk::solve::recursive::fulfill::Fulfill::prove
             at src/solve/recursive/fulfill.rs:195
  37: chalk::solve::recursive::fulfill::Fulfill::fulfill
             at src/solve/recursive/fulfill.rs:290
  38: chalk::solve::recursive::fulfill::Fulfill::solve
             at src/solve/recursive/fulfill.rs:337
  39: chalk::solve::recursive::Solver::solve_canonical_goal
             at src/solve/recursive/mod.rs:108
  40: chalk::solve::infer::InferenceTable::universe_of_unbound_var
             at src/solve/recursive/mod.rs:96
  41: chalk::solve::infer::unify::OccursCheck::new
             at src/solve/mod.rs:228
  42: chalki::goal
             at src/bin/chalki.rs:231
  43: chalki::run::{{closure}}
             at src/bin/chalki.rs:125
  44: chalk::ir::tls::set_current_program::{{closure}}
             at ./src/ir/tls.rs:23
  45: <std::thread::local::LocalKey<T>>::try_with
             at /Users/travis/build/rust-lang/rust/src/libstd/thread/local.rs:377
  46: <std::thread::local::LocalKey<T>>::with
             at /Users/travis/build/rust-lang/rust/src/libstd/thread/local.rs:288
  47: chalk::ir::tls::set_current_program
             at ./src/ir/tls.rs:21
  48: chalki::run
             at src/bin/chalki.rs:123
  49: chalki::main
             at ./<quick_main macros>:4
  50: panic_unwind::dwarf::eh::read_encoded_pointer
             at src/libpanic_unwind/lib.rs:99
  51: <std::rand::reader::ReaderRng<R> as rand::Rng>::fill_bytes
             at src/libstd/panicking.rs:459
             at src/libstd/panic.rs:361
             at src/libstd/rt.rs:59
  52: chalki::main

[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