{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreic2psv2cplo4nvwb4642dyfaxyv3o3frwax7ko5jvfvgizqgbynmi",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mhfnoa2evbr2"
  },
  "path": "/t/type-level-programming-dealing-with-ambiguous-type-error/13828#post_1",
  "publishedAt": "2026-03-19T08:35:41.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "vec package",
    "fin package"
  ],
  "textContent": "I’m trying to use the vec package to implement a stack machine: Instructions are tagged with the number of their parmeters and return values, and the evaluator pops the parameters off the `Vec` stack, evaluates the instruction, and pushes the return values back.\n\nThe following code doesn’t compile:\n\n\n    import Data.Type.Nat\n    import Data.Vec.Lazy  as Vec (Vec (..))\n\n    data ArithBlock (n :: Nat) (m :: Nat) where\n\n    eval :: ArithBlock n m -> Vec (Plus n x) Int -> Vec (Plus m x) Int\n    eval = undefined\n\n\nThe error:\n\n\n    • Couldn't match type: Plus n x0\n                     with: Plus n x\n      Expected: ArithBlock n m\n                -> Vec (Plus n x) Int -> Vec (Plus m x) Int\n        Actual: ArithBlock n m\n                -> Vec (Plus n x0) Int -> Vec (Plus m x0) Int\n      Note: ‘Plus’ is a non-injective type family.\n      The type variable ‘x0’ is ambiguous\n    • In the ambiguity check for ‘eval’\n      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\n      In the type signature:\n        eval :: ArithBlock n m -> Vec (Plus n x) Int -> Vec (Plus m x) Int\n\n\nNote that `vec` uses the fin package for Natural numbers, which uses a Peano encoding, instead of GHC’s built-in literals. But ultimately I beleive they support the same set of operations (besides for GHC builtins getting better arithmetic logic via typechecker plugins, which I am trying to avoid)\n\nI’m guessing the answer involves threading through a singleton for `x`, is there any way to avoid this?",
  "title": "Type level programming: Dealing with ambiguous type error"
}