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

Opened by comex at 2024-12-21 05:02:42

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.

@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.
Eduard-Mihai Burtescu at 2017-03-08 14:01:22
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
```
comex at 2017-03-08 19:42:18
cc @nikomatsakis
Eduard-Mihai Burtescu at 2017-03-08 19:51:30
Duplicate of #38528?
Tatsuyuki Ishi at 2018-02-18 13:08:57
Not resolved in #48296, the battle continues...
Tatsuyuki Ishi at 2018-02-26 09:27:58