{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiev6tqyni3m5gs4opt6vef3qsy2kftzj5cxqxk3d7yvm7aqumxu4i",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mncghhxnwcc2"
  },
  "path": "/t/serokell-s-work-on-ghc-dependent-types-part-5/14184#post_5",
  "publishedAt": "2026-06-02T09:39:17.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "Correct!\n\n  * 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.\n\n  * 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.\n\n\n\n\nSo 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`.",
  "title": "Serokell’s Work on GHC: Dependent Types, Part 5"
}