<div dir="auto">+1</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Aug 13, 2019, 7:32 PM Andrew Lelechenko <<a href="mailto:andrew.lelechenko@gmail.com">andrew.lelechenko@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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" rel="noreferrer">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>