Moving forall with coerce

[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!

Richard

On Oct 19, 2015, at 5:02 PM, David Feuer <david.feuer at gmail.com> wrote:

> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs