Hi David, Am Montag, den 19.10.2015, 18:06 -0400 schrieb Richard Eisenberg:
Just to be clear, the Codensity bit (which I don't know) is a red herring here. What you want is this:
newtype A m a = MkA (forall b. m a -> (a -> m b) -> m b) newtype B (m :: * -> *) a = MkB (forall b. (a -> m b) -> m b)
foo :: A m a -> (m a -> B m a) foo = coerce
On one level, this is perfectly reasonable. These two types do seem to have the same runtime representation. But in thinking about how the types work out, it's all less clear. In particular, this seems to require impredicativity, as we'll be solving a Coercible constraint over forall-types. I think we'll have to sort out impredicativity, in general, before we can start to tackle something like this.
But I haven't thought very deeply about it, and perhaps there's a way forward I haven't seen.
Interesting example!
JFTR, note that the solver can handle forall’s in a very limited way, namely coercing between two forall’ed types works: instance (forall a. Coercible t1 t2) => Coercible (forall a. t1) (forall a. t2) but you need something more powerful. Also note that once class join the party, things become less coercible. This might work: > newtype A = A (forall x. Int -> [x] -> x) > newtype B = B (Int -> forall x. [x] -> x) > :t coerce :: A -> B (although it currently does not), but this will not > newtype A = A (forall x. Show x => Int -> [x] -> x) > newtype B = B (Int -> forall x. Show x => [x] -> x) > coerce :: A -> B as the order of the Int and the show instance would be different in the representation. Not sure how much that implementation detail should pervade the user space. OTOH, coercible is already quite implementation-specific, and of course we want to be able to coerce as much as possible. Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0xF0FBF51F Debian Developer: nomeata@debian.org