{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreihj42hdq3vorncw66g4qxgpkxpwlfvgmnfwt7e2ukk7mrlh7wwmmm",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mippzasa3nc2"
  },
  "path": "/t/type-equality-in-gadt-typefamily-context/13876#post_8",
  "publishedAt": "2026-04-05T01:28:16.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "this comment",
    "an issue",
    "@True"
  ],
  "textContent": "A follow-up on my prior comment.\n\n### `Data.Type.Equality.==`\n\nThe reason for its weird implementation is discussed in this comment.\n\nRather than simplifying it, the better course of action should be to use/provide:\n\n\n    equal :: a :~: b -> (a == b) :~: True\n    equal Refl = unsafeCoerce (Refl @True)\n\n\n### `apart`\n\nI didn’t do enough testing. There’s no issue with this primitive in principle, but in practice the `GHC.TypeLits.decide*` functions don’t actually provide legitimate inequalities. `apart` refuses to be fooled and explodes.\n\nThis can be fixed, so I’ve made an issue of it.",
  "title": "Type equality in GADT/TypeFamily context"
}