"Could not infer a type for parameter..." error should be removed

[kfcripps]

I am curious why the source code at testdata/p4_16_errors_outputs/methodArgDontcare.p4 is not expected to compile. In my opinion, this error should not have been added by #3901 (#3808 was actually fixed by the "argument cannot have type..." error), but maybe I am missing something.

[kfcripps]

I also find it interesting that the following does compile:

extern E {
    E();
    void f<T>(in T arg);
}

control c() {
    E() e;
    apply {
        e.f<_>(0);
    }
}

control proto();
package top(proto p);
top(c()) main;

while the mentioned test case does not. Seems to me like they should both exhibit the same behavior.

[kfcripps]

@fruffy @jafingerhut From the Perspective of the P4-16 spec, do you think the error message makes sense?

And is there a reason for the inconsistency between the two mentioned code snippets, or should they exhibit the same behavior?

[fruffy]

@jnfoster

I also find it interesting that the following does compile:

extern E {
    E();
    void f<T>(in T arg);
}

control c() {
    E() e;
    apply {
        e.f<_>(0);
    }
}

control proto();
package top(proto p);
top(c()) main;

while the mentioned test case does not. Seems to me like they should both exhibit the same behavior.

Can you provide more reasoning why you believe this should not compile? Because it is a Type_InfInt?

https://p4.org/p4-spec/docs/P4-16-working-spec.html#sec-invocations is indeed underspecified as to what types are allowed here. I believe the decisions are made as a mix of these two restrictions:

The “don't care” identifier (_) can only be used for an out function/method argument, when the value of returned in that argument is ignored by subsequent computations. When used in generic functions or methods, the compiler may reject the program if it is unable to infer a type for the don't care argument.

The types header, header_union, enum, struct, extern, parser, control, and package can only be used in type declarations, where they introduce a new name for the type. The type can subsequently be referred to using this identifier.

[jafingerhut]

@kfcripps My apologies, but I do not have a good enough understanding of what the P4 language spec says (or doesn't say) about type checking of code like this.

[kfcripps]

Can you provide more reasoning why you believe this should not compile? Because it is a Type_InfInt?

@fruffy I do not know whether it should or should not compile (well, testdata/p4_16_errors/methodArgDontcare.p4 successfully compiled before #3901, and my first question is about whether this change was intentional or not).

My second point is that I would expect both snippets to either compile or not compile. Ultimately, they are the same: In testdata/p4_16_errors/methodArgDontcare.p4 (copied below for reference), we are providing the arg type in the extern instantiation, and in the other case, we are providing it in the method call. If we can infer the type in the latter case, then why not the former?

extern E<T> {
    E();
    void f(in T arg);
}

control c() {
    E<_>() e;
    apply {
        e.f(0);
    }
}

control proto();
package top(proto p);

top(c()) main;

[jnfoster]

The specification doesn't really commit to what the compiler may or may not do when it comes to inferring type arguments given as _.

I understand the intuition behind wanting the two examples to behave the same. But if type inference is being done in a local manner, they could well be different.

• For the case where the type variable T is on the entire extern, a local analysis might try to resolve the _ from the types of the arguments to the constructor. But in the case of the E extern, T does not appear in the type signature to the constructor. So it cannot use local information to resolve the _.
• For the case where the type variable T is on the method, T is the type of the parameter to the method, so it might be able to resolve the _ from the type of the argument to the method.

In fact, this is what Petr4 does... Petr4's type inference algorithm is based on "local type inference", which is also known as "bidirectional type inference" in the literature.

So when the T is on the entire extern, the type checker fails with an error because it cannot determine a type to substitute for the _, as discussed above.

But when the T is on the method f, the type checker correctly infers that the type argument, namely _, and the argument to the function, namely 0, must have the same type, namely int. However, it then produces an error because parameters of type int must be directionless. It would succeed if 0 were replaced with any of 1w0, 8w0, 16w0, etc.

One could argue that type inference should not be local. Instead it should some consider the whole program, or at least an entire scope. But this quickly gets tricky -- the compiler needs to wait to type check the constructor until it analyzes all of the ways the methods might be used. And what if the extern is supplied to another control that invokes some of its methods. Should those method invocations affect how type arguments to the constructor are resolved? It's hard to know where to draw the line. So some in the programming languages community, including yours truly, now feel that local approaches to type inference may be better -- they are simpler to describe and implement, and can arguably be more predictable for programmers (if, in certain cases, more limited).

[jnfoster]

By the way, I think p4c is wrong to accept the version with the _ on the f method, because it rejects this program.

extern E {
    E();
    void f(in int arg);
}

control c() {
    E() e;
    apply {
        e.f(0);
    }
}

control proto();
package top(proto p);
top(c()) main;

with the following error:

dc2.p4(3): [--Werror=type-error] error: arg: parameters with type int must be directionless
    void f(in int arg);
                  ^^^
dc2.p4(3)
    void f(in int arg);
              ^^^

That is, I believe Petr4 is more consistent in applying the rules about int, implicit casts, etc.