It appears, as far as I can tell, that GHC can't move a forall past an -> with coerce. I was playing around with the MonadTrans instance for Codensity, wanting (essentially) to write lift = coerce (>>=) This is legal: instance MonadTrans Codensity where lift = frob frob :: forall m a . Monad m => m a -> Codensity m a frob = coerce (blah (Mag (>>=)) :: m a -> Mag2 m a) newtype Mag m a = Mag (forall b . m a -> (a -> m b) -> m b) newtype Mag2 m a = Mag2 (forall b . (a -> m b) -> m b) blah :: Mag m a -> m a -> Mag2 m a blah (Mag p) q = Mag2 (p q) The problem is that there doesn't *seem* to be a way to implement blah as a coercion. GHC doesn't recognize that Mag m a has the same representation as m a -> Mag2 m a The essential difference, as far as I can see, is that the `forall b` is shifted across `m a ->`. It seems that this really shouldn't be an issue, because 1. b is not free in `m a` 2. Type lambdas all compile away Would it be worth trying to extend the Coercible mechanism to deal with these kinds of situations? Or is there already some way to do it that I've missed? David
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!
Richard
On Oct 19, 2015, at 5:02 PM, David Feuer
It appears, as far as I can tell, that GHC can't move a forall past an -> with coerce. I was playing around with the MonadTrans instance for Codensity, wanting (essentially) to write
lift = coerce (>>=)
This is legal:
instance MonadTrans Codensity where lift = frob frob :: forall m a . Monad m => m a -> Codensity m a frob = coerce (blah (Mag (>>=)) :: m a -> Mag2 m a) newtype Mag m a = Mag (forall b . m a -> (a -> m b) -> m b) newtype Mag2 m a = Mag2 (forall b . (a -> m b) -> m b) blah :: Mag m a -> m a -> Mag2 m a blah (Mag p) q = Mag2 (p q)
The problem is that there doesn't *seem* to be a way to implement blah as a coercion. GHC doesn't recognize that
Mag m a
has the same representation as
m a -> Mag2 m a
The essential difference, as far as I can see, is that the `forall b` is shifted across `m a ->`. It seems that this really shouldn't be an issue, because
1. b is not free in `m a` 2. Type lambdas all compile away
Would it be worth trying to extend the Coercible mechanism to deal with these kinds of situations? Or is there already some way to do it that I've missed?
David _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
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
participants (3)
-
David Feuer -
Joachim Breitner -
Richard Eisenberg