[Bug][move-compiler-v2] recursive function type parameter checks are a little too conservative

[brmataptos]

🐛 Bug

Following https://github.com/aptos-labs/aptos-core/pull/12360, cyclic instantiation checks are mostly right (so #12072 has been closed) but seem to have one remaining subtle problem.

The first test case in third_party/move/move-compiler-v2/tests/cyclic-instantiation-checker/v1-tests/complex_1.exp is not quite correct, as the code shifts type parameters around while traversing a recursive loop, but the types don't grow without bound.

Unless I'm wrong, the types go:

c<T1, T2> -> d<T2> -> b<u64, T2> -> c<M::S<T2>, bool> -> d<bool> -> b<u64, bool> -> c<M::S<bool>, bool> -> ...

so it stabilizes without growing much.

We could modify the error message to be more vague about why we prohibit it or ignore it for now (as obscure), but eventually should probably fix it, but it is probably nontrivial (will require some iteration and/or reasoning about the recursive type expression).

[fEst1ck]

I see. Suppose we found f<T_1, T_2, ...> (T_1, T_2, are type variables) calling f<S_1, S_2, ...> (S_1, S_2, are types possibly containing the type variables). We currently use a heuristic that if any S_i properly contains any T_i, we consider it will lead to cyclic instantiations; and this is causing false positives like the one above.

The fix: Construct a graph with nodes T_1, T_2, ...., edge T_i contains T iff S_i == T, edge T_i properly contains T iff S_i properly contains T. We then check if there is loop in the graph from T_i to itself, where at least one edge is a properly contains.

[zzjas]

Encountered the same error while building the fuzzer. Here's the code in case it can be used as a test case in the future:

module 0xCAFE::Module0 {
    struct HasCopyDrop has copy, drop {}

    struct C2<T1: drop, phantom T2: copy> has copy, drop, store {}

    fun m1<T1: copy+drop, T2: copy>(x: T1) {
        m2<C2<HasCopyDrop, T2>, HasCopyDrop>(C2{});
    }
    fun m2<T3: copy+drop, T4: copy>(x: T3): T3 {
        m1<T3, T4>(x);
        x
    }
}