Type level programming: Dealing with ambiguous type error

Learn
1

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?

2

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.

3

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.

4

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.

5

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:

{-# 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
6

This is not the case