How to create a type generic structure with tuples?

Stream: lean4

[Anders Christiansen Sørby]

Trying to create a generic structure which contains a Type u x Type u : Type (u +1) tuple

structure S (T : Type u) : Type u where
  values : (T,T)

Leads to this error

[Lean 4] [E] type expected
failed to synthesize instance
  CoeSort (Type u × Type u) ?m.406

But doing this works

inductive Pair (α : Type u) (β : Type v)
| mk : α → β → Pair α β

structure S (T : Type u) : Type u where
  values : Pair T T

What is special about using tuples ( , ) contra Prod?

[Marcus Rossel]

(T, T) is not the notation for the product type. T \x T is the correct notation.

[Marcus Rossel]

The error message complains that it doesn't know how to turn a tuple of type Type u × Type u into a type (?m.406).

[Adam Topaz]

Note: You would use \x to write that product symbol.

[Anders Christiansen Sørby]

Ok, thanks. Is there a special reason why the (T, T) syntax can't be used for types?

[Adam Topaz]

Like Marcus mentioned, we use (a,b) for a term of type A \x B where a : A and b : B. This is more in line with the usual notation from mathematics.

[Reid Barton]

It can be used, it defines a pair of types.

[Anders Christiansen Sørby]

Oh, that is true it is ambiguous with first class types