Expected type of arguments not (always?) useds

[mtzguido]

This works fine:

fn use_nat (x : nat) { () }
fn call_nat () { use_nat 42; }

But,

fn use_nat (x : nat & nat) { () }
fn call_nat () { use_nat (42, 1); }

Gives:

- Ill-typed term: FStar.Pervasives.Native.Mktuple2 #int #nat 42 1
- Expected a term of type nat & nat
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.
- Also see: /home/guido/r/kuiper/main/inst/lib/fstar/ulib/Prims.fst:161.28-183.79
- Raised within Tactics.refl_core_check_term
F*
- This query failed:
- forall (i: Prims.int) (x: Prims.unit).
    Prims.trivial <==> Prims.equals #Prims.bool (i >= 0) true
F*

Likely since we've elaborated the tuple without regard for the expected type.

It is even the case when it's not the last argument.

fn use_nat (x : nat & nat) () { () }

fn call_nat () { use_nat (42, 1) (); }

- Ill-typed term: use_nat (FStar.Pervasives.Native.Mktuple2 #int #nat 42 1)
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.
- Also see: /home/guido/r/kuiper/main/inst/lib/fstar/ulib/Prims.fst:161.28-183.79
- Raised within Tactics.refl_tc_term
F*
- This query failed:
- forall (i: Prims.int) (x: Prims.unit).
    Prims.trivial <==> Prims.equals #Prims.bool (i >= 0) true

Note that, somehow, in the last two cases the second type was inferred to be nat... unsure why.