13 Aug
2019
13 Aug
'19
7:32 p.m.
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