Type of some division expressions is ambiguous and the default interpretation is bad

[marcoeilers]

Gobra frequently generates permission amounts like 1 / 4000 / 2 for SCION code by @jcp19. These are intended to be a fractional permission 1/4000 divided by two, i.e., the permission value 1/8000. Instead, they are apparently parsed as an integer division 1 \ 4000, which is zero, which is then the numerator in the fractional permission 0 / 2. This is bad because a) it's not the intended meaning, and b) there is no way to pretty-print it so that the parser returns the intended meaning.

[marcoeilers]

Similar problem: 0 / 1 < 1 / 2 can be parsed as two integer divisions, in which case it's false, or two perm divisions, in which case it's true.

[jcp19]

A possible fix for this would be to allow the syntax Perm(x, y) to stand unambiguously for the perm amount x/y. While this does not solve the fact that / is ambiguous, it introduces syntax that allows us to be precise when we need to

[marcoeilers]

Fixed in PR #855 by modifying type priorities: Whenever possible, every division will be interpreted as a Perm-typed division. Users can force a different interpretation by using the \ operator in the division.