Type level programming: Dealing with ambiguous type error

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:

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