Type constraints for right-hand operand of shift operators

[blp]

The following program:

input relation X(x: bit<16>, y: bit<16>)
output relation Y(x: bit<16>, y: bit<16>, z: bit<16>)
Y(x, y, x << y) :- X(x, y).

yields the following compiler error that I don't expect (with release v1.2.3 and earlier releases):

error: /home/blp/nerpa/nerpa/ofp4/test.dl:3.6-3.7: Unsatisfiable bit-width constraint '16 = 0' in
expected type: bit<16>
actual type: bit<32>
in
expression 'y'
Y(x, y, x << y) :- X(x, y).
     ^

I can fix it by casting y to u32 in the shift expression, like this:

Y(x, y, x << (y as u32)) :- X(x, y).

I would prefer that << (and presumably >>) accept any integer type as its right-hand operand.

[mihaibudiu]

Probably any unsigned integer type only could work. Signed values introduce additional complications.

[blp]

That's reasonable.

[blp]

If #1159 gets merged, and this bug gets fixed, then the documentation added by the PR should be updated as well.