Make sameNat proxy-polymorphic

[chessai .]

+1

On Tue, Aug 13, 2019, 7: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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20190813/dfe0d8bb/attachment.html>