I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive. With these you can learn about the equality of the types of elements of an STRef when you go to testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b) I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/ With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a). This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values. Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down. -Edward