failure to infer that a type is a pair

[oskgo]

The following code fails even though it should be possible to infer that x is a tuple:

op foo ['a]: ('a -> bool) -> 'a -> bool.

op bar = foo (fun x => x.`1 = x.`2) (true, true).

Adding a type annotation makes this succeed:

op bar = foo (fun (x: _ * _) => x.`1 = x.`2) (true, true).

[fdupress]

Unfortunately, we can't infer that it's a pair: the projectors are generic in the size of the tuple.

You can fix it for pairs by using fst and snd instead of the generic projectors.

[oskgo]

EasyCrypt cannot infer the size of the tuple from the (true, true) input? This also fails if you reorder the inputs of foo btw.

[fdupress]

Yes, our type inference is simpler that it needs to be.
It is also not used to inform operator selection, which could be where it fails in this instance. (It tries to select which projection operator should be used, and stops when it can't even tell that the input is not a tuple.)

[strub]

Superseded by #630

As François said, we are not even using a bidirectional type-checker.