# Type level programming: Dealing with ambiguous type error

**URL:** <https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828>\
**Category:** Learn\
**Created:** [March 19, 2026, 8:35am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828 "2026-03-19T08:35:41Z")\
**Posts on this page:** 13\
**Page:** 1

<div class="post-metadata">

**Author:** ![AriFordsham](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/arifordsham/32/979_2.png) [@AriFordsham](https://discourse.haskell.org/u/AriFordsham)\
**Post date:** [March 19, 2026, 8:35am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/1 "2026-03-19T08:35:41Z")

</div>

I’m trying to use the [`vec` package](https://hackage.haskell.org/package/vec) 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.

The following code doesn’t compile:

```haskell
import Data.Type.Nat
import Data.Vec.Lazy as Vec (Vec (..))

data ArithBlock (n :: Nat) (m :: Nat) where

eval :: ArithBlock n m -> Vec (Plus n x) Int -> Vec (Plus m x) Int
eval = undefined

```

The error:

```haskell
• Couldn't match type: Plus n x0
                 with: Plus n x
  Expected: ArithBlock n m
            -> Vec (Plus n x) Int -> Vec (Plus m x) Int
    Actual: ArithBlock n m
            -> Vec (Plus n x0) Int -> Vec (Plus m x0) Int
  Note: ‘Plus’ is a non-injective type family.
  The type variable ‘x0’ is ambiguous
• In the ambiguity check for ‘eval’
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  In the type signature:
    eval :: ArithBlock n m -> Vec (Plus n x) Int -> Vec (Plus m x) Int

```

Note that `vec` uses the [`fin` package](https://hackage.haskell.org/package/fin) 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)

I’m guessing the answer involves threading through a singleton for `x`, is there any way to avoid this?

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [March 19, 2026, 8:46am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/2 "2026-03-19T08:46:38Z")

</div>

The simple solution is to make x a required type argument. You can also try your luck at enabling AllowAmbiguousTypes, but maybe you’ll get an ambiguity error when you try to use eval anyway.

I do think `Plus n` (given one argument) should be injective. Perhaps you can find some other way to define it which the compiler can understand. For example a typeclass with functional dependencies.

---

<div class="post-metadata">

**Author:** ![AriFordsham](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/arifordsham/32/979_2.png) [@AriFordsham](https://discourse.haskell.org/u/AriFordsham)\
**Post date:** [March 19, 2026, 9:04am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/3 "2026-03-19T09:04:20Z")

</div>

`AllowAmbiguousTypes` will just push the logical problem elsewhere. A required type argument won’t help because `x` is highly dynamic.

There seems to be two possible approaches here:

1. Somehow get the compiler to understand the relationship between `m`, `n` and `x` in the way that it can work here. This is my preferece, but I’m open to the fact that it might not be possible.

2. Thread through a singleton for `x`. This is complicated by the fact that it is not trivial to know what `x` is at any given point. I think I will try implementing an algorithm that passes `x` in the dumb-list version of my machine.

---

<div class="post-metadata">

**Author:** ![Leary](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/leary/32/4348_2.png) [@Leary](https://discourse.haskell.org/u/Leary)\
**Post date:** [March 19, 2026, 9:33am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/4 "2026-03-19T09:33:44Z")

</div>

People have traditionally solved this problem by passing `proxy x` arguments, but `RequiredTypeArguments` is the upgrade that makes such runtime proxies obsolete in recent GHCs.

It’s not clear to me exactly why you’re writing this approach off; dynamacy shouldn’t pose an issue. I suggest you try it and let us know what roadblocks you hit.

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [March 19, 2026, 9:34am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/5 "2026-03-19T09:34:53Z")

</div>

> [@AriFordsham](#):
>
> `AllowAmbiguousTypes` will just push the logical problem elsewhere.

Not 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:

```haskell
{-# LANGUAGE AllowAmbiguousTypes, TypeFamilies, DataKinds, RequiredTypeArguments #-}

data Nat = Z | S Nat

type family Plus x y where
  Plus Z x = x
  Plus (S x) y = S (Plus x y)

data Proxy a = Proxy

foo :: forall x y -> Proxy (Plus x z) -> Proxy (Plus y z)
foo _ _ Proxy = Proxy

bar = foo (S (S Z)) (S Z) Proxy -- not ambiguous

```

---

<div class="post-metadata">

**Author:** ![AriFordsham](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/arifordsham/32/979_2.png) [@AriFordsham](https://discourse.haskell.org/u/AriFordsham)\
**Post date:** [March 19, 2026, 11:49am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/6 "2026-03-19T11:49:12Z")

</div>

> [@jaror](#):
>
> If all the `ArithBlocks` have constants as arguments

This is not the case

---

<div class="post-metadata">

**Author:** ![AriFordsham](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/arifordsham/32/979_2.png) [@AriFordsham](https://discourse.haskell.org/u/AriFordsham)\
**Post date:** [April 13, 2026, 7:33am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/7 "2026-04-13T07:33:37Z")

</div>

Thanks all, indeed `Proxy`s unblocked me here.

I will be avoiding `RequiredTypeArguments` for now; I tried them briefly and the behaviour around the scoping of names seemed wierd.

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [April 13, 2026, 8:08am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/8 "2026-04-13T08:08:43Z")

</div>

> [@AriFordsham](#):
>
> I tried them briefly and the behaviour around the scoping of names seemed wierd.

Interesting, for me the scoping makes more sense than for example ScopedTypeVariables. What strangeness did you encounter?

---

<div class="post-metadata">

**Author:** ![AriFordsham](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/arifordsham/32/979_2.png) [@AriFordsham](https://discourse.haskell.org/u/AriFordsham)\
**Post date:** [April 13, 2026, 9:10am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/9 "2026-04-13T09:10:23Z")

</div>

I didn’t narrow it down to something specific, but I dropped it as being trouble compared to `Proxy` for not much gain.

I expect my code to compile warning-free. When using variables introduced by `forall n ->`, I found trying to juggle the variables introduced in the type signature and in the pattern match, with type applications/inline type signatures, I seemed to always have either an undeclared or an unused variable. Something like, a function wouldn’t compile without a variable being included in `forall n.`, but when I did include it, I got an unused type variable warning. I just gave up and switched to proxies.

Having said that, there is a feature of `RequiredTypeArguments` that I do like. Until now, the only way to go from `type (or data kind) -> term` was with a typeclass. this has the disadvantage of a) unwieldly syntax (for this use case) and b) It doesn’t support closed classes. By RTA allows me to pattern-match on types in function syntax, which is nice. So I may well come back to them someday and settle my differences properly.

---

<div class="post-metadata">

**Author:** ![george.fst](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/george.fst/32/4933_2.png) [@george.fst](https://discourse.haskell.org/u/george.fst)\
**Post date:** [April 13, 2026, 9:48am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/10 "2026-04-13T09:48:57Z")

</div>

> [@AriFordsham](#):
>
> Having said that, there is a feature of `RequiredTypeArguments` that I do like. Until now, the only way to go from `type (or data kind) -> term` was with a typeclass. this has the disadvantage of a) unwieldly syntax (for this use case) and b) It doesn’t support closed classes. By RTA allows me to pattern-match on types in function syntax, which is nice.

Could you give an example of what you mean here? It sounds like you’re saying it’s possible to do something like this:

```hs
f :: forall (a :: Type) -> Int
f Int = 0
f Bool = 1

```

But that gives an error:

```haskell
• Couldn't match expected type ‘a’ with actual type ‘Int’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      f :: forall a -> Int
• In the pattern: Int
  In an equation for ‘f’: f Int = 0

```

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [April 14, 2026, 7:19am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/11 "2026-04-14T07:19:46Z")

</div>

Right, `RequiredTypeArguments` _doesn’t_ allow you to do that. It’s just syntax. What _will_ allow you to do that is `foreach`. I’ve no idea how long through the development pipeline that is. And in the meantime, the library feature that supports this functionality is singletons (whether with the `singletons` package specifically, or with the general notion).

[EDIT: corrected `forall ->` to `foreach`]

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [April 14, 2026, 7:27am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/12 "2026-04-14T07:27:15Z")

</div>

> [@tomjaguarpaw](#):
>
> What _will_ allow you to do that is `forall ->`.

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.

What you would be able to do with full dependent types is create a data type and map that to the type level:

```haskell
data MyType = TInt | TBool

typeOfMyType :: MyType -> Type
typeOfMyType TInt = Int
typeOfMyType TBool = Bool

negateLike :: foreach (t :: MyType) -> typeOfMyType t -> typeOfMyType t
negateLike TInt x = -x
negateLike TBool x = not x

```

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [April 14, 2026, 8:08am UTC](https://discourse.haskell.org/t/type-level-programming-dealing-with-ambiguous-type-error/13828/13 "2026-04-14T08:08:33Z")

</div>

> [@jaror](#):
>
> 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.

Sorry, I meant `foreach`, not `forall ->`. (`forall ->` _is_ `RequiredTypeArguments`!) Does that resolve the confusion?

I 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.

You can see a little more in the [Dependent Products section of the Serokell Dependent Types roadmap](https://ghc.serokell.io/dh).

EDIT: I see from your edit that it was a conceptual example of using `foreach` in a future version of GHC. In the meantime

~~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:

```haskell
{-# LANGUAGE GHC2024 #-}

import Data.Kind

data SMyType t where
  STInt :: SMyType Int
  STBool :: SMyType Bool

negateLike :: forall (t :: Type). SMyType t -> t -> t
negateLike STInt x = -x
negateLike STBool x = not x

```