<div dir="ltr">+1 on all of the above, I generally find my proxy code is nicest when i'm polymoprophic over the prox :) <br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Aug 14, 2019 at 12:45 PM Eric Mertens <<a href="mailto:emertens@gmail.com">emertens@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">While we’re fixing that, let’s also fix sameSymbol.<br>
<br>
> On Aug 13, 2019, at 4:32 PM, Andrew Lelechenko <<a href="mailto:andrew.lelechenko@gmail.com" target="_blank">andrew.lelechenko@gmail.com</a>> wrote:<br>
> <br>
> Hi all,<br>
> <br>
> Currently base:GHC.TypeNats.sameNat is implemented as follows:<br>
> <br>
> sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)<br>
> sameNat x y<br>
>  | natVal x == natVal y = Just (unsafeCoerce Refl)<br>
>  | otherwise = Nothing<br>
> <br>
> There are applications, when more flexibility is desirable. I propose to change sameNat's type to <br>
> <br>
> sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)<br>
> <br>
> It does not require any changes in the implementation, because natVal is already "proxy-polymorphic":<br>
> <br>
> natVal :: forall n proxy. KnownNat n => proxy n -> Natural<br>
> <br>
> Best regards,<br>
> Andrew<br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>