Serokell’s Work on GHC: Dependent Types, Part 5

Correct!

• If your module is compiled with NoListTuplePuns, then (Int, Bool) :: Tuple2 Type Type, and the Tuple type family maps it to Tuple2 Int Bool. That’s the intended usage.

• But that’s not all. If you compile with ListTuplePuns, then (Int, Bool) :: Type, because it already is Tuple2 Int Bool, and then applying Tuple is identity.

So the Tuple type family works regardless of (No)ListTuplePuns. Now that I’ve spelled this out, it’s also occurred to me that this means Tuple is idempotent, i.e. forall x. Tuple (Tuple x) = Tuple x.