Preventing types from unifying

Question

Given this wrapper around integers:

newtype MyProxy a = MyProxy Int

mkProxy :: Int -> MyProxy a
mkProxy a = MyProxy a

addProxy :: MyProxy a -> MyProxy a -> MyProxy  a
addProxy (MyProxy a1) (MyProxy a2) = MyProxy $ a1+a2

I can perform the following:

a = mkProxy 1
b = mkProxy 2
c = addProxy a b

because the phantom parameters will be unified. But I want to prevent this unification and cause a type error on line c.

The ST monad uses rank2 types to achieve a similar effect. I could probably do something similar by changing the type of addProxy. But I specifically do not want to do this. I want to annotate the a type variable somehow to prevent it from unifying on the addProxy call.

Is this possible in Haskell? Is there a reason why such an option would be dangerous?

---

Edit:

Let me elaborate on a partial solution (requiring -XScopedTypeVariables). I can rewrite the code above as:

c :: forall a1 a2. MyProxy a1
c = addProxy a b
    where
        a = mkProxy 1 :: MyProxy a1
        b = mkProxy 2 :: MyProxy a2

This correctly causes a type error on c because a1 and a2 cannot be unified. But this has two drawbacks: a and b cannot be defined at the top level; and you must explicitly specify the resulting type of mkProxy.

Is it possible to fix these drawbacks?

Answer 1

No you can't, at least not without specifying something more to mkProxy.

The way the ST monad works is by requiring the escaping computation to generate something of type forall s. ST s a which prevents s from appearing free in a.

In your case however, you're doing two identical computations so generating a different type for each could be used to do evil things. For example, if mkInt 1 generated different types each time it was called,

class Evil a b c | a, b -> c where
  foo :: a -> b -> c

let x = mkProxy 1 in foo x x

Would be different than

 foo (mkProxy 1) (mkProxy 1)

and we've lost some very nice properties in our code.

We can however do some extra leg work and make the fact that a and b can't unify explicit

 {-# LANGUAGE DataKinds #-}

 data Nat = S Nat | Z
 data Proxy (n :: Nat) a = Proxy a

 based :: a -> Proxy Z a
 based = Proxy

 fresh :: Proxy n a -> a -> Proxy (S n) a
 fresh (Proxy _) a = Proxy a

So now you need to do something like

a = based 1

b = fresh a 2

Answer 2

I would think that existential type variables would be suitable for this. Basically, two existential type variables created independently won't unify. In the following test fails to typecheck because it can't unify the type variables of the two MyProxys.

{-# LANGUAGE ExistentialQuantification #-}

newtype MyProxy a = MyProxy Int

data Exists f = forall a. Exists (f a)

mkProxy :: Int -> Exists MyProxy
mkProxy a = Exists (MyProxy a)

addProxy :: MyProxy a -> MyProxy a -> MyProxy a
addProxy (MyProxy a1) (MyProxy a2) = MyProxy $ a1+a2

test :: Exists MyProxy -> Exists MyProxy -> Exists MyProxy
test (Exists a) (Exists b) = Exists (addProxy a b)