Hi all,

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

There are applications, when more flexibility is desirable. I propose to change sameNat's type to

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

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

natVal :: forall n proxy. KnownNat n => proxy n -> Natural

Best regards,
Andrew
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries