Make sameNat proxy-polymorphic

[Carter Schonwald]

+1 on all of the above, I generally find my proxy code is nicest when i'm
polymoprophic over the prox :)

On Wed, Aug 14, 2019 at 12:45 PM Eric Mertens <emertens at gmail.com> wrote:

> 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
>
> _______________________________________________
> 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/20190815/53623c53/attachment.html>