_analyzed.pil output files can't be run again

[georgwiese]

I would expect this to work:

$ cargo run pil test_data/asm/book/hello_world.asm -o output -f -i 0
...
Writing output/hello_world_analyzed.pil.
...
$ cargo run pil output/hello_world_analyzed.pil -o output -f -i 0
Analyzing PIL and computing constraints...
Error analyzing PIL file:
error: Inferred type scheme for symbol std::btree::internal::array_split_pivot does not match the declared type.
Inferred: let<T: Add + FromLiteral + Mul> std::btree::internal::array_split_pivot: T[], int -> (T[], T, T[])
Declared: let<T> std::btree::internal::array_split_pivot: T[], int -> (T[], T, T[])
    ┌─ /Users/georg/coding/powdr/output/hello_world_analyzed.pil:125:59
    │  
125 │       let<T> array_split_pivot: T[], int -> (T[], T, T[]) = |arr, i| {
    │ ╭───────────────────────────────────────────────────────────^
126 │ │         let left: T[] = std::array::sub_array::<T>(arr, 0_int, i);
127 │ │         let right: T[] = std::array::sub_array::<T>(arr, i + 1_int, std::array::len::<T>(arr) - i - 1_int);
128 │ │         (left, arr[i], right)
129 │ │     };
    │ ╰─────^

thread 'main' panicked at cli/src/main.rs:700:32:
called `Result::unwrap()` on an `Err` value: ["Inferred type scheme for symbol std::btree::internal::array_split_pivot does not match the declared type.\nInferred: let<T: Add + FromLiteral + Mul> std::btree::internal::array_split_pivot: T[], int -> (T[], T, T[])\nDeclared: let<T> std::btree::internal::array_split_pivot: T[], int -> (T[], T, T[]) at /Users/georg/coding/powdr/output/hello_world_analyzed.pil:10417-10638"]
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

The file is just the printed Analyzed<T>.

[chriseth]

The function is declared as let<T> array_split_pivot: ...., so it is a generic symbol with explicit type. This means that its type cannot be changed by the way it is used (this is different for symbols without type, where the type is determined both from its value and the way it is used). The type checker should take a look at the value of the function and re-check that the type determined from that matches the declared type. I don't see where the type bounds should come from in that definition.

One difference between the two commands is that the first one runs in "asm mode" while the second one runs in "pil mode", but since the type checker only kicks in after the asm to pil transformation, that shouldn't make a big difference.

[gzanitti]

I have been looking into this.

First of all, this is a reduced version of the problem. The type_vars were changed to simplify the substitutions:

#[test]
fn release_type_var() {
    // If we remove pow_ext, the error disappears.
    let input = "
    namespace std::array;
        let<T> len: T[] -> int = [];
        let<G> new: int, (int -> G) -> G[] = |length, f| std::utils::fold::<G, G[]>(length, f, [], |acc, e| acc + [e]);
        let<N> sub_array: N[], int, int -> N[] = |arr, start, l| std::array::new::<N>(l, |i| arr[start + i]);
    namespace std::btree::internal;
        let<T> array_split: T[], int -> (T[], T[]) = |arr, l| {
            let left: T[] = std::array::sub_array::<T>(arr, 0_int, l);
            let right: T[] = std::array::sub_array::<T>(arr, l, std::array::len::<T>(arr) - l);
            (left, right)
        };
    namespace std::math::fp2;
        enum Fp2<L> {
            Fp2(L, L),
        }
        let<T: Add + FromLiteral + Mul> pow_ext: std::math::fp2::Fp2<T>, int -> std::math::fp2::Fp2<T> = |x, i| match i {
            0 => std::math::fp2::Fp2::Fp2::<T>(1, 0),
            1 => x,
            _ => {
                std::math::fp2::square_ext::<T>(std::math::fp2::Fp2::Fp2::<T>(i, 0))
            },
        };
        let<S: Add + FromLiteral + Mul> square_ext: std::math::fp2::Fp2<S> -> std::math::fp2::Fp2<S> = |a| match a {
            std::math::fp2::Fp2::Fp2(a0, a1) => std::math::fp2::Fp2::Fp2::<S>(a0 * a0 + 11 * a1 * a1, 2 * a1 * a0),
        };

    namespace std::utils;
        let<P, Z> fold: int, (int -> P), Z, (Z, P -> Z) -> Z = |length, f, initial, folder| if length <= 0_int { initial } else { folder(std::utils::fold::<P, Z>(length - 1_int, f, initial, folder), f(length - 1_int)) };
    ";

    type_check(input, &[]);
}

if we remove pow_ext, the error disappears.

The problem seems to be that we store all the substitutions of T against the same key T (string), so when we go to look for the bounds of T, the program should look for the substitution such that it gets the T from array_split, but since it also processes pow_ext, the subs return this T (i.e: the Txxx that leads to the T in pow_ext), so the array_split bonds fail.
I tried to separate them instantiated new typeschemes, but so far every attempt has broken something else.

The same problem could be created by the BUILTIN_SCHEMES, all defined on a T that is added to the substitutions.

As a side note, I also believe that these parameters:

powdr/pil-analyzer/src/type_inference.rs

Line 539 in 83c5894

.unify_types(requested.clone(), inferred.clone())

should be inverted (otherwise, every duplicated requested will be overwritten). But this alone doesn't fix the problem.

I'll keep looking for the solution, just dropping by to update (ofc, ideas are welcome).