How do I efficiently add existentially typed safe money values?

I wrote a toy library that uses dependent types to represent money with its currency in the type signature:

data Currency = CHF | EUR | PLN | USD
  deriving stock (Bounded, Enum, Eq, Read, Show)

data CurrencyWitness (c :: Currency) where
  CHFWitness :: CurrencyWitness CHF
  EURWitness :: CurrencyWitness EUR
  PLNWitness :: CurrencyWitness PLN
  USDWitness :: CurrencyWitness USD

deriving stock instance Eq (CurrencyWitness c)
deriving stock instance Show (CurrencyWitness c)


data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(CurrencyWitness currency)
  , moneyAmount :: !representation
  }
  deriving stock (Eq, Show)

add :: (Num r) => Money c r -> Money c r -> Money c r
add (Money witness1 amount1) (Money _ amount2) =
  Money witness1 (amount1 + amount2)

data SomeMoney r where
  SomeMoney :: Money c r -> SomeMoney r

How can I now write addSomeMoney :: (Num r) => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r) that safely adds money only if they are of the same currency? You can imagine that this might be needed in a situation where users provide money arguments, so we can't check their currency at compile time.

My best approach is:

addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c' _)) = case (c, c') of
  (CHFWitness, CHFWitness) -> Just . SomeMoney $ add m m'
  (PLNWitness, PLNWitness) -> Just . SomeMoney $ add m m'
  -- ...
  (_, _) -> Nothing

This approach has the drawback that it is cumbersome to write, repetitive, and becomes faulty when I add a new currency as the compiler won't warn me that that case is not handled.

addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c _)) = _

doesn't work. GHC complains about duplicate c: Conlicting definitions of 'c'.

A completely "type safe" approach is possible, but we have to write some boilerplate.

We start from the OP's code, mostly verbatim. We only add a few extensions, enable warnings (which should more properly be done elsewhere, but let's keep this simply) and import Data.Typeable.

(I haven't checked if some extensions can be removed)

{-# LANGUAGE GADTs, DerivingStrategies, KindSignatures,
    StandaloneDeriving, DataKinds, RankNTypes, 
    TypeApplications, ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}
   
import Data.Typeable

data Currency = CHF | EUR | PLN | USD
  deriving stock (Bounded, Enum, Eq, Read, Show)

data CurrencyWitness (c :: Currency) where
  CHFWitness :: CurrencyWitness 'CHF
  EURWitness :: CurrencyWitness 'EUR
  PLNWitness :: CurrencyWitness 'PLN
  USDWitness :: CurrencyWitness 'USD

deriving stock instance Eq (CurrencyWitness c)
deriving stock instance Show (CurrencyWitness c)

data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(CurrencyWitness currency)
  , moneyAmount :: !representation
  }
  deriving stock (Eq, Show)

add :: (Num r) => Money c r -> Money c r -> Money c r
add (Money witness1 amount1) (Money _ amount2) =
  Money witness1 (amount1 + amount2)

data SomeMoney r where
  SomeMoney :: Money c r -> SomeMoney r

Now the new part.

We first "prove" that any currency type c satisfies the Typeable constraint. This is trivial to do, but requires some boilerplate.

Importantly, adding new currencies will trigger a non-exhaustive patter matching warning, so it is reasonably easy to keep it in sync.

withTypeableCurrency :: CurrencyWitness c -> (Typeable c => a) -> a
withTypeableCurrency CHFWitness x = x
withTypeableCurrency EURWitness x = x
withTypeableCurrency PLNWitness x = x
withTypeableCurrency USDWitness x = x

Then, the currency-adding function. We invoke withTypeableCurrency to put two Typeable constraints in scope. Then we leverage eqT to check if the two currency types are the same. In the affirmative case, we do not get a boring True boolean, but a convenient Refl which allows the compiler to identify the types. The rest is then easy.

addSomeMoney :: (Num r) => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)
addSomeMoney (SomeMoney (m1@(Money (c1 :: CurrencyWitness tc1) _)))
             (SomeMoney (m2@(Money (c2 :: CurrencyWitness tc2) _))) =
  withTypeableCurrency c1 $
  withTypeableCurrency c2 $
  case eqT @tc1 @tc2 of
    Just Refl -> Just . SomeMoney $ add m1 m2
    Nothing   -> Nothing  -- not the same type of currency

The advantage of this approach is that the boilerplate is confined within withTypeableCurrency, and does not have to be repeated in each function dealing with SomeMoney like addSomeMoney, subtractSomeMoney, etc.

---

Update: some of the boilerplate can be removed exploiting the singletons package and some Template Haskell.

{-# LANGUAGE GADTs, DerivingStrategies, KindSignatures,
    StandaloneDeriving, DataKinds, RankNTypes, TypeApplications,
    ScopedTypeVariables, TemplateHaskell, EmptyCase, TypeFamilies,
    UndecidableInstances, TypeSynonymInstances, InstanceSigs #-}

import Data.Singletons.Decide
import Data.Singletons.TH

$(singletons [d|
  data Currency = CHF | EUR | PLN | USD
    deriving (Eq, Read, Show, Bounded)
  |])
-- This automatically creates the equivalent of
--    data SCurrency :: Currency -> Type where
--       SCHF :: SCurrency 'CHF
--       SEUR :: SCurrency 'EUR
--       SPLN :: SCurrency 'PLN
--       SUSD :: SCurrency 'USD
-- and some helper stuff.

-- singletons does not like deriving Enum, so we move it here.
deriving stock instance Enum Currency

-- singletons does not create this for some reason.
deriving stock instance Eq (SCurrency c)

data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(SCurrency currency)
  , moneyAmount :: !representation
  }
  deriving stock (Eq, Show)

add :: (Num r) => Money c r -> Money c r -> Money c r
add (Money witness1 amount1) (Money _ amount2) =
  Money witness1 (amount1 + amount2)

data SomeMoney r where
  SomeMoney :: Money c r -> SomeMoney r

The key function is even simpler, exploiting %~.

addSomeMoney :: (Num r) => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)
addSomeMoney (SomeMoney m1@(Money c1 _))
             (SomeMoney m2@(Money c2 _)) =
  -- Check for singleton equality.
  case c1 %~ c2 of
    Proved    Refl -> Just . SomeMoney $ add m1 m2
    Disproved _    -> Nothing