{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreifkyqoabqcuwv5waldwrhphticlpth5oum57xjc4zbf4gpvkufpq4",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjs7dnz3nap2"
  },
  "path": "/t/lawvere-theories/13944#post_10",
  "publishedAt": "2026-04-18T19:23:49.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "ashokkimmel:\n\n>\n>     type Stuck :: Peano\n>     type family Stuck where\n>\n>\n> This is an irreducible type family, but it’s still technically valid. It also is not an instance of Prop.\n\nInteresting. Is that the type-level equivalent to a function declaration without a function body? Does the kind `Peano` also contain an infinity type like `infinity = Succ infinity`? Apparently under `UndecidableInstances` one can write such a type family. Your `Stuck` example is more unnerving, though, because it does not require an obviously dangerous language extension. Thanks for showing it!",
  "title": "Lawvere theories"
}