Make sameNat proxy-polymorphic

[Eric Mertens]

While we’re fixing that, let’s also fix sameSymbol.

> On Aug 13, 2019, at 4:32 PM, Andrew Lelechenko <andrew.lelechenko at gmail.com> wrote:
> 
> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries