{
"$type": "site.standard.document",
"bskyPostRef": {
"cid": "bafyreiceyc5rcbomhciqnnmuz4c55w24odc6ojs5xgp6r43bunfslluiiq",
"uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mi6viosstfc2"
},
"path": "/t/history-of-dh-dependent-types-in-haskell-contributions/11242?page=2#post_25",
"publishedAt": "2026-03-29T02:01:15.000Z",
"site": "https://discourse.haskell.org",
"textContent": "Here’s a probably stupid idea I had for unification:\n\nUse a type family that would redirect the term specific things. E.g.\n\n\n data HsTerm s p =\n -- Variations of\n HsVar/HsTyVar\n HsOverLit, HsLit/HsTyLit\n HsApp/HsAppTy\n HsAppType/HsAppKindTy\n OpApp/HsOpTy\n HsPar/HsParTy\n ExplicitTuple/HsExplicitTupleTy\n ExplicitList/HsExplicitListTy\n ExprWithTySig/HsKindSig\n HsUntypedSplice/HsSpliceTy\n HsHole/HsWildCardTy\n HsForAll/HsForAllTy\n HsQual/HsQualTy\n HsFunArr/HsFunTy\n -- The redirect\n HsExprType !(XHsExprType s p) (ExprType s p)\n\n data TermParam = Ty | Ex | Unknown -- like this to avoid name collisions in GHC, qualified imports would probably be used.\n\n type family ExprType where\n ExprType Ty = OtherHsType\n ExprType Ex = OtherHsExpr\n ExprType Unknown= DataCannotHappen\n type HsExpr = HsTerm Ex\n type HsType = HsTerm Ty\n\n\nWhere `OtherHsType` and `OtherHsExpr` contain fields not mentioned above. I mainly propose this as with `PatternSynonyms`, I don’t think it’s a breaking change.\n\n(Sorry for the formatting, I’ll change it when I’m at my computer)",
"title": "History of DH (Dependent Types in Haskell) contributions"
}