& produces dependent tuples instead of ordinary ones if the constituents are named

[chandradeepdey]

let this_is_a_pair (a: nat) (b: nat) : nat * nat = a, b

let this_is_a_pair' (a: nat) (b: nat) : a': nat * b': nat = a, b

let this_is_a_pair'' (a: nat) (b: nat) : nat & nat = a, b

[@@expect_failure]
let this_is_not_a_pair (a: nat) (b: nat) : a': nat & b' : nat = a, b

let this_is_a_dpair (a: nat) (b: nat) : a': nat & b' : nat = (|a, b|)

[mtzguido]

This is intentional :). & has always been the syntax for dependent tuples and, since around 2019 or so I think, it was extended to also represent normal pairs when there is no name for the left component. You can always use * or tuple2 to refer to normal tuples.

See also PR #2816 for a quirk with refinements, which we should probably revive.

[chandradeepdey]

Ah, thanks!

Btw, what is the rationale behind having separate “independent” tuples? Why can’t every tuple be a dependent tuple?