Skip to content

trait solver hangs for recursively expanding coinductive cycles #13

Open
@lcnr

Description

@lcnr
#![feature(rustc_attrs)]

#[rustc_coinductive]
trait Trait {}

struct W<T>(T);

impl<T, U> Trait for W<(W<T>, W<U>)>
where
    W<T>: Trait,
    W<U>: Trait,
{
}

fn impls<T: Trait>() {}

fn main() {
    impls::<W<_>>();
}

this hangs in the new solver.

we start with a coinductive cycle of length 1 and 2 nested goals, then the next cycle is of length 2 with 4 nested goals, then length 3 with 8 nested goals. This is an example which should result in overflow while only slowly growing the recursion depth.

i think we generally want some general "overflow counter" in the search graph. For this to be sound wrt to caching hitting that limit may have to be fatal or we include the steps taken in the query response 🤷 we will figure it out

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions