ICE: negative subgoal had delayed_subgoals

[lcnr]

#[test]
fn depth_not_on_stack() {
    test! {
        program {
            #[coinductive]
            trait A {}
            #[coinductive]
            trait B {}
            #[coinductive]
            trait C {}
            #[coinductive]
            trait D {}
            #[coinductive]
            trait E {}

            impl<T> A for () 
            where
                T: B,
            {}
            impl<T> A for ()
            where
                T: E
            {}

            impl<T> B for ()
            where
                T: C,
                T: E,
            {}
            impl<T> C for ()
            where
                T: D,
                T: B,
            {}
            impl<T> D for ()
            where
                T: C
            {}
            impl<T> E for ()
            where
                T: D
            {}
        }

        goal {
            exists<T> {
                T: A
            }
        } yields[SolverChoice::slg(10, None)] {
            expect![["Unique; for<?U0> { substitution [?0 := ^0.0] }"]]
        } yields[SolverChoice::recursive_default()] {
            expect![["Unique; for<?U0> { substitution [?0 := ^0.0] }"]]
        }
    }
}

results in

--- test::cycle::depth_not_on_stack stdout ----
program {
    #[coinductive] trait A {} #[coinductive] trait B {} #[coinductive] trait C
    {} #[coinductive] trait D {} #[coinductive] trait E {} impl < T > A for()
    where T : B, {} impl < T > A for() where T : E {} impl < T > B for() where
    T : C, T : E, {} impl < T > C for() where T : D, T : B, {} impl < T > D
    for() where T : C {} impl < T > E for() where T : D {}
}
thread 'test::cycle::depth_not_on_stack' panicked at 'Negative subgoal had delayed_subgoals', /home/lcnr/chalk/chalk-engine/src/logic.rs:725:21

Found this while trying to get a test for the following buggy proof tree:

• A
  • candidate 1:
    • B
      • C
        • D (d has depth 2)
          • C
        • B (depth 0)
      • E
        • D (from cache with depth 2, even though the depth should be 0)
        • ok (incorrectly moved to global cache)
      • FALSE
  • candidate 2:
    • E (ok)

[lcnr]

is the issue that the impls have unbound generic parameters :sweat_smile: didn't notice that i wrote impl<T> Trait for ()

[lcnr]

no, it is not :sweat_smile: this also causes the same panic:

#[test]
fn depth_not_on_stack() {
    test! {
        program {
            #[coinductive]
            trait A {}
            #[coinductive]
            trait B {}
            #[coinductive]
            trait C {}
            #[coinductive]
            trait D {}
            #[coinductive]
            trait E {}

            impl<T> A for T
            where
                T: B,
            {}
            impl<T> A for T
            where
                T: E
            {}

            impl<T> B for T
            where
                T: C,
                T: E,
            {}
            impl<T> C for T
            where
                T: D,
                T: B,
            {}
            impl<T> D for T
            where
                T: C
            {}
            impl<T> E for T
            where
                T: D
            {}
        }

        goal {
            exists<T> {
                T: A
            }
        } yields[SolverChoice::slg(10, None)] {
            expect![["Unique; for<?U0> { substitution [?0 := ^0.0] }"]]
        } yields[SolverChoice::recursive_default()] {
            expect![["Unique; for<?U0> { substitution [?0 := ^0.0] }"]]
        }
    }
}