testEquality compares two keys for equality that possibly have a different type, but it doesn't allow comparing Key s Int and Key s Maybe by producing a proof HRefl
-- this definition to go into Data.Type.Equality
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
testHEquality :: Key s a -> Key s b -> Maybe (a :~~: b)
Consider adding it when it when they get added to base.
testEqualitycompares two keys for equality that possibly have a different type, but it doesn't allow comparingKey s IntandKey s Maybeby producing a proofHReflConsider adding it when it when they get added to base.