# Moving forall with coerce

Joachim Breitner mail at joachim-breitner.de
Tue Oct 20 11:09:24 UTC 2015

```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

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 at joachim-breitner.de • http://www.joachim-breitner.de/
Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0xF0FBF51F
Debian Developer: nomeata at debian.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part