rust-lang / rust

Empowering everyone to build reliable and efficient software.
https://www.rust-lang.org
Other
98.11k stars 12.69k forks source link

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

Open comex opened 7 years ago

comex commented 7 years ago

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 commented 7 years ago

@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 commented 7 years ago

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 commented 7 years ago

cc @nikomatsakis

ishitatsuyuki commented 6 years ago

Duplicate of #38528?

ishitatsuyuki commented 6 years ago

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