Skip to content

Make sameNat and sameSymbol proxy-polymorphic

Motivation

Currently base:GHC.TypeNats.sameNat is implemented as follows:

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat x y
 | natVal x == natVal y = Just (unsafeCoerce Refl)
 | otherwise = Nothing

One cannot directly apply sameNat to a value of type Foo (a :: Nat), but has to bind a and construct Proxy :: Proxy a first. While not terribly inconvenient, it would be so much better to apply sameNat to Foo a directly.

The same shortcoming cripples base:GHC.TypeLits.sameSymbol.

Proposal

I propose to change types to

sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol :: (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

It does not require any changes in the implementation, because natVal and symbolVal are already "proxy-polymorphic":

natVal :: forall n proxy. KnownNat n => proxy n -> Natural
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String

Discussion in the mail list: https://mail.haskell.org/pipermail/libraries/2019-August/029847.html

Edited by Bodigrim
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information