type checker takes O(~1.5^recursion_limit) time to reject simple-ish code

[comex]

Found when trying to port my old type system Brainfuck interpreter to use associated types. Reduced case:

#![recursion_limit="10"]
use std::marker::PhantomData;

struct Nil;
struct Cons<A, B>(PhantomData<A>, PhantomData<B>);
struct BFPlus;

trait BF {
    type NewState: ?Sized;
}

// +
impl<U, OtherInsns, NewState>
    BF for (U, Cons<BFPlus, OtherInsns>)
    where (U, OtherInsns): BF<NewState=NewState> {
    type NewState = ();
}

fn main() {
    let insns = Nil;
    let state = Nil;


    fn print_bf<State, Insns, NewState>(state: State, insns: Insns)
        where (State, Insns): BF<NewState=NewState> {
    }
    print_bf(state, insns);
}

I don't really understand what's going on, but as written, rustc outputs:

error[E0275]: overflow evaluating the requirement `<(_, _) as BF>::NewState`
  --> xx-iloop.rs:27:5
   |
27 |     print_bf(state, insns);
   |     ^^^^^^^^
   |
   = help: consider adding a `#![recursion_limit="20"]` attribute to your crate
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, _>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, _>>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, _>>>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, _>>>>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, _>>>>>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, _>>>>>>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, _>>>>>>>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, _>>>>>>>>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, _>>>>>>>>>)`
   = note: required because of the requirements on the impl of `BF` for `(_, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, Cons<BFPlus, _>>>>>>>>>>)`
   = note: required by `main::print_bf`

However, increasing the recursion_limit dramatically increases the time it takes to report the error.

Note that writing the impl more normally as

impl<U, OtherInsns>
    BF for (U, Cons<BFPlus, OtherInsns>)
    where (U, OtherInsns): BF {
    type NewState = <(U, OtherInsns) as BF>::NewState;
}

fails instantly even with a high recursion limit. But I don't see why it should fail at all: the impl is sane enough, implementing BF for a larger type based on its implementation for a smaller type.

[eddyb]

@comex This is a classical induction problem: the compiler cannot reason, ahead of time, that there isn't an impl for an arbitrarily large tuple where NewState matches.

Although, in this case... did you mean type NewState = NewState;? If so, this is specifically a limitation of the current implementation w.r.t type parameters which are only constrained by associated types.

[comex]

I guess has to do with the order of considering constraints. It shouldn't have to go hunting for such an impl, because Insns is forced to be Nil by the parameter. Actually, if I add an explicit type parameter to print_bf, it fails immediately:

print_bf::<_, Nil, _>(state, insns);

produces

error[E0277]: the trait bound `(_, Nil): BF` is not satisfied

[eddyb]

cc @nikomatsakis

[ishitatsuyuki]

Duplicate of #38528?

[ishitatsuyuki]

Not resolved in #48296, the battle continues...