Type level programming: Dealing with ambiguous type error

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.

The following code doesn’t compile:

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:

• 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 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?