`&` 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?

[mtzguido]

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

Potentially they could, but non-dependent tuples are usually better behaved for type inference, due to having simpler (and more efficient) unification constraints, so we usually use the non-dependent kind when possible. Also, if we were to have subtyping on datatype parameters, we could definitely make (nat, X) a subtype of (int, X), but for a dependent tuple this is not necessarily the case: X could be a function defined only on nat.

[chandradeepdey]

Thanks!