I thought of this, but the problem is that Data.Type.Equality is
Trustworthy, while Data.Type.Coercion is unsafe. Therefore, you can't
define the superclass in a Safe module.
The solution to this would be to have Data.Type.Equality export
TestCoercion but not testCoercion, and have a a default implementation
(with DefaultSignatures) that requires TestEquality and just turns the
equality into a coercion.
Another option is to include testCoercion, but not Coercion, and use the
fact that Coercion is a Category here:
toId :: Category p => (a :~: b) -> p a b
toId Refl = id
And then testCoercion a b = fmap toId $ testEquality a b
On Tue, Dec 4, 2018, 19:50 Edward Kmett You actually would need both types for full generality. Both provide
useful power under different circumstances. Another thing I noticed when working on this is that TestEquality is
missing TestCoercion as a superclass at present. This means you can't use
the latter as merely a weaker TestEquality constraint, but have to plumb
both independently. This feels wrong. Everything that can support
TestEquality should be able to support TestCoercion. I do at least want the TestCoercion instances. -Edward On Tue, Dec 4, 2018 at 7:46 AM Andrew Martin Given that each comes at the cost of the other, if I had to choose
between which of these two STRef features I could have, I would pick being
able to use it to recover equality over being able to lift newtype
coercions through it. The former is increases expressivity while the latter
accomplishes something that is achievable by simply using less newtypes in
APIs where the need for this arises (not that I've ever actually needed to
coerce an STRef in this way, but it would be interesting to hear from
anyone who has needed this). On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett Mostly because it means I wind up needing another construction to make
it all go and can't just kick it all upstream. ;) -Edward On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg Why is it unfortunate? This looks like desired behavior to me. That is:
I think these reference types should allow coercions between
representationally equal types. Of course, that means that TestEquality is
out. Richard On Dec 2, 2018, at 5:04 PM, Edward Kmett On Sun, Dec 2, 2018 at 7:55 PM David Feuer Unfortunately, testEquality for STRef is not at all safe, for reasons
we've previously discussed in another context. testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b) let x = [1, 2]
foo :: STRef s [Int] <- newSTRef x
let bar :: STRef s (ZipList Int) = coerce foo
case testEquality foo bar of UH-OH I suspect testCoercion actually will work here. You could patch up the problem by giving STRef (and perhaps MutVar#) a
stricter role signature: type role STRef nominal nominal That might not break enough code to worry about; I'm not sure. That is rather unfortunate, as it means most if not all of these would
be limited to TestCoercion. -Edward On Sun, Dec 2, 2018, 7:16 PM Edward Kmett 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
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries --
-Andrew Thaddeus Martin _______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries