{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreie335si65fob7nh357ngxrkoaajcjzfwmz7jgx6wyl7xqj4tglngm",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjh4ao3zkvo2"
  },
  "path": "/t/type-level-programming-dealing-with-ambiguous-type-error/13828#post_13",
  "publishedAt": "2026-04-14T08:08:33.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "Dependent Products section of the Serokell Dependent Types roadmap"
  ],
  "textContent": "jaror:\n\n> No, matching on types is not (and should not be) possible even with full dependent types like in Agda. I hope this is not a planned feature.\n\nSorry, I meant `foreach`, not `forall ->`. (`forall ->` _is_ `RequiredTypeArguments`!) Does that resolve the confusion?\n\nI believe “`foreach`” corresponds to a “Pi-type” or “dependent product” in dependent type theory, and should be possible in Agda, as far as I know. In Haskell it boils down to something like passing `Typeable` or the singleton for the type in question.\n\nYou can see a little more in the Dependent Products section of the Serokell Dependent Types roadmap.\n\nEDIT: I see from your edit that it was a conceptual example of using `foreach` in a future version of GHC. In the meantime\n\n~~I’m not sure whether your example was supposed to be literal or conceptual but~~ here’s a literal version that uses a hand-written singleton:\n\n\n    {-# LANGUAGE GHC2024 #-}\n\n    import Data.Kind\n\n    data SMyType t where\n      STInt :: SMyType Int\n      STBool :: SMyType Bool\n\n    negateLike :: forall (t :: Type). SMyType t -> t -> t\n    negateLike STInt x = -x\n    negateLike STBool x = not x\n",
  "title": "Type level programming: Dealing with ambiguous type error"
}