{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreieyn6hscojsz44hdl35b3u4twfubqf7tzht72venvth4iixkigo7i",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mhfufdxwxoh2"
  },
  "path": "/t/type-level-programming-dealing-with-ambiguous-type-error/13828#post_5",
  "publishedAt": "2026-03-19T09:34:53.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "AriFordsham:\n\n> `AllowAmbiguousTypes` will just push the logical problem elsewhere.\n\nNot necessarily. If all the `ArithBlocks` have constants as arguments (e.g. `ArithBlock (S (S Z)) (S Z)`) then GHC can infer the ambiguous `x` without issues. Here’s a simplified example of that:\n\n\n    {-# LANGUAGE AllowAmbiguousTypes, TypeFamilies, DataKinds, RequiredTypeArguments #-}\n\n    data Nat = Z | S Nat\n\n    type family Plus x y where\n      Plus Z x = x\n      Plus (S x) y = S (Plus x y)\n\n    data Proxy a = Proxy\n\n    foo :: forall x y -> Proxy (Plus x z) -> Proxy (Plus y z)\n    foo _ _ Proxy = Proxy\n\n    bar = foo (S (S Z)) (S Z) Proxy -- not ambiguous\n",
  "title": "Type level programming: Dealing with ambiguous type error"
}