More GND + role inference woes

classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

More GND + role inference woes

Ben Gamari
Edward Kmett <ekmett at gmail.com> writes:

> If this forced me to write those instances by hand, I could accept
> that as a tax for correctness. It means you can't GND any of the
> HasFoo dictionaries that lens builds, but meh.
>
Am I correct in assuming that Bind, R1, R2, R3, and R4 are the
problematic instances in linear? With recent GHC I get the errors below.

Cheers,

- Ben


    src/Linear/Affine.hs:112:34:
        Could not coerce from ?f (f a)? to ?f (Point f a)?
          because ?f (f a)? and ?f (Point f a)? are different types.
          arising from the coercion of the method ?join? from type
                       ?forall a. f (f a) -> f a? to type
                       ?forall a. Point f (Point f a) -> Point f a?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (Bind (Point f))
   
    src/Linear/Affine.hs:112:58:
        Could not coerce from ?g (f x)? to ?g (Point f x)?
          because ?g (f x)? and ?g (Point f x)? are different types.
          arising from the coercion of the method ?core? from type
                       ?forall a.
                        ((forall (g :: * -> *) x.
                          Functor g =>
                          (x -> g x) -> f x -> g (f x))
                         -> a)
                        -> f a?
                       to type
                       ?forall a.
                        ((forall (g :: * -> *) x.
                          Functor g =>
                          (x -> g x) -> Point f x -> g (Point f x))
                         -> a)
                        -> Point f a?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (Core (Point f))
   
    src/Linear/Affine.hs:112:64:
        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
          arising from the coercion of the method ?_x? from type
                       ?forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)?
                       to type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (a -> f a) -> Point f a -> f (Point f a)?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (R1 (Point f))
   
    src/Linear/Affine.hs:112:68:
        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
          arising from the coercion of the method ?_xy? from type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (V2 a -> f (V2 a)) -> f a -> f (f a)?
                       to type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (V2 a -> f (V2 a)) -> Point f a -> f (Point f a)?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (R2 (Point f))
   
    src/Linear/Affine.hs:112:68:
        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
          arising from the coercion of the method ?_y? from type
                       ?forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)?
                       to type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (a -> f a) -> Point f a -> f (Point f a)?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (R2 (Point f))
   
    src/Linear/Affine.hs:112:72:
        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
          arising from the coercion of the method ?_xyz? from type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (V3 a -> f (V3 a)) -> f a -> f (f a)?
                       to type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (V3 a -> f (V3 a)) -> Point f a -> f (Point f a)?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (R3 (Point f))
   
    src/Linear/Affine.hs:112:72:
        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
          arising from the coercion of the method ?_z? from type
                       ?forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)?
                       to type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (a -> f a) -> Point f a -> f (Point f a)?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (R3 (Point f))
   
    src/Linear/Affine.hs:112:76:
        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
          arising from the coercion of the method ?_xyzw? from type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (V4 a -> f (V4 a)) -> f a -> f (f a)?
                       to type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (V4 a -> f (V4 a)) -> Point f a -> f (Point f a)?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (R4 (Point f))
   
    src/Linear/Affine.hs:112:76:
        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
          arising from the coercion of the method ?_w? from type
                       ?forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)?
                       to type
                       ?forall a (f :: * -> *).
                        Functor f =>
                        (a -> f a) -> Point f a -> f (Point f a)?
        Possible fix:
          use a standalone 'deriving instance' declaration,
            so you can specify the instance context yourself
        When deriving the instance for (R4 (Point f))
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 489 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131214/62f365fe/attachment.sig>

Reply | Threaded
Open this post in threaded view
|

More GND + role inference woes

Richard Eisenberg-2
Yes, I believe that's right. As far as I can figure out, these classes really *are* problematic, in that if we allowed GeneralizedNewtypeDeriving for them, there would be a way to subvert the type system. To make these derivable, we would need to be able to restrict various type parameters from taking on values that take a nominal argument. Without the ability to restrict the values in this way, there could be trouble.

Richard

On Dec 14, 2013, at 4:52 PM, Ben Gamari wrote:

> Edward Kmett <ekmett at gmail.com> writes:
>
>> If this forced me to write those instances by hand, I could accept
>> that as a tax for correctness. It means you can't GND any of the
>> HasFoo dictionaries that lens builds, but meh.
>>
> Am I correct in assuming that Bind, R1, R2, R3, and R4 are the
> problematic instances in linear? With recent GHC I get the errors below.
>
> Cheers,
>
> - Ben
>
>
>    src/Linear/Affine.hs:112:34:
>        Could not coerce from ?f (f a)? to ?f (Point f a)?
>          because ?f (f a)? and ?f (Point f a)? are different types.
>          arising from the coercion of the method ?join? from type
>                       ?forall a. f (f a) -> f a? to type
>                       ?forall a. Point f (Point f a) -> Point f a?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (Bind (Point f))
>
>    src/Linear/Affine.hs:112:58:
>        Could not coerce from ?g (f x)? to ?g (Point f x)?
>          because ?g (f x)? and ?g (Point f x)? are different types.
>          arising from the coercion of the method ?core? from type
>                       ?forall a.
>                        ((forall (g :: * -> *) x.
>                          Functor g =>
>                          (x -> g x) -> f x -> g (f x))
>                         -> a)
>                        -> f a?
>                       to type
>                       ?forall a.
>                        ((forall (g :: * -> *) x.
>                          Functor g =>
>                          (x -> g x) -> Point f x -> g (Point f x))
>                         -> a)
>                        -> Point f a?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (Core (Point f))
>
>    src/Linear/Affine.hs:112:64:
>        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
>          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
>          arising from the coercion of the method ?_x? from type
>                       ?forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)?
>                       to type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (a -> f a) -> Point f a -> f (Point f a)?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (R1 (Point f))
>
>    src/Linear/Affine.hs:112:68:
>        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
>          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
>          arising from the coercion of the method ?_xy? from type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (V2 a -> f (V2 a)) -> f a -> f (f a)?
>                       to type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (V2 a -> f (V2 a)) -> Point f a -> f (Point f a)?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (R2 (Point f))
>
>    src/Linear/Affine.hs:112:68:
>        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
>          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
>          arising from the coercion of the method ?_y? from type
>                       ?forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)?
>                       to type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (a -> f a) -> Point f a -> f (Point f a)?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (R2 (Point f))
>
>    src/Linear/Affine.hs:112:72:
>        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
>          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
>          arising from the coercion of the method ?_xyz? from type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (V3 a -> f (V3 a)) -> f a -> f (f a)?
>                       to type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (V3 a -> f (V3 a)) -> Point f a -> f (Point f a)?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (R3 (Point f))
>
>    src/Linear/Affine.hs:112:72:
>        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
>          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
>          arising from the coercion of the method ?_z? from type
>                       ?forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)?
>                       to type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (a -> f a) -> Point f a -> f (Point f a)?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (R3 (Point f))
>
>    src/Linear/Affine.hs:112:76:
>        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
>          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
>          arising from the coercion of the method ?_xyzw? from type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (V4 a -> f (V4 a)) -> f a -> f (f a)?
>                       to type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (V4 a -> f (V4 a)) -> Point f a -> f (Point f a)?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (R4 (Point f))
>
>    src/Linear/Affine.hs:112:76:
>        Could not coerce from ?f1 (f a)? to ?f1 (Point f a)?
>          because ?f1 (f a)? and ?f1 (Point f a)? are different types.
>          arising from the coercion of the method ?_w? from type
>                       ?forall a (f :: * -> *). Functor f => (a -> f a) -> f a -> f (f a)?
>                       to type
>                       ?forall a (f :: * -> *).
>                        Functor f =>
>                        (a -> f a) -> Point f a -> f (Point f a)?
>        Possible fix:
>          use a standalone 'deriving instance' declaration,
>            so you can specify the instance context yourself
>        When deriving the instance for (R4 (Point f))


Reply | Threaded
Open this post in threaded view
|

More GND + role inference woes

Ben Gamari
Richard Eisenberg <eir at cis.upenn.edu> writes:

> Yes, I believe that's right. As far as I can figure out, these classes
> really *are* problematic, in that if we allowed
> GeneralizedNewtypeDeriving for them, there would be a way to subvert
> the type system. To make these derivable, we would need to be able to
> restrict various type parameters from taking on values that take a
> nominal argument. Without the ability to restrict the values in this
> way, there could be trouble.
>
I suppose it's unlikely that the roles mechanism will be extended to
allow for such restriction?

Cheers,

- Ben

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 489 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131214/f1fc0ca3/attachment-0001.sig>

Reply | Threaded
Open this post in threaded view
|

More GND + role inference woes

Richard Eisenberg-2


On Dec 14, 2013, at 7:59 PM, Ben Gamari wrote:
>
> I suppose it's unlikely that the roles mechanism will be extended to
> allow for such restriction?

Very unlikely in the short term. As more use cases for such a feature filter in and the community demands the feature, there's no strong technical reason it can't be done. We believe that doing this would add quite a bit more complexity within GHC and doesn't have the right payoff-to-complexity ratio, for now.

Richard

Reply | Threaded
Open this post in threaded view
|

More GND + role inference woes

Edward Kmett-2
In reply to this post by Ben Gamari
Correct. With 7.8 we'll need to hand-implement those instances rather than
derive them.


On Sat, Dec 14, 2013 at 7:59 PM, Ben Gamari <bgamari.foss at gmail.com> wrote:

> Richard Eisenberg <eir at cis.upenn.edu> writes:
>
> > Yes, I believe that's right. As far as I can figure out, these classes
> > really *are* problematic, in that if we allowed
> > GeneralizedNewtypeDeriving for them, there would be a way to subvert
> > the type system. To make these derivable, we would need to be able to
> > restrict various type parameters from taking on values that take a
> > nominal argument. Without the ability to restrict the values in this
> > way, there could be trouble.
> >
> I suppose it's unlikely that the roles mechanism will be extended to
> allow for such restriction?
>
> Cheers,
>
> - Ben
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131215/da35cb7e/attachment.html>

Reply | Threaded
Open this post in threaded view
|

More GND + role inference woes

Simon Peyton Jones
So I think we are agreed that what is currently implemented is the right thing; and that it?s expressive enough for now.

There?s a lot of interesting stuff in this thread that it would be a shame to lose.  It would be great if the wiki page on roles could cover this stuff: https://ghc.haskell.org/trac/ghc/wiki/Roles

Specifically,

?         the way that GND is implemented (as described in the attached email) by looking at the method types, is manifestly non-obvious (since we missed it for ages)

?         Richard?s observations about the things it still doesn?t do are interesting

?         Some poster-child examples for where the simple roles we have are insufficiently expressive and a sketch of how it could be extended if necessary (I agree with Richard?s assessment that it?s not worth it right now).

Richard, you are the obvious person to do this, if you have time. Maybe just pointers to the right places would do.

Simon

From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Edward Kmett
Sent: 15 December 2013 09:28
To: Ben Gamari
Cc: ghc-devs
Subject: Re: More GND + role inference woes

Correct. With 7.8 we'll need to hand-implement those instances rather than derive them.

On Sat, Dec 14, 2013 at 7:59 PM, Ben Gamari <bgamari.foss at gmail.com<mailto:bgamari.foss at gmail.com>> wrote:
Richard Eisenberg <eir at cis.upenn.edu<mailto:eir at cis.upenn.edu>> writes:

> Yes, I believe that's right. As far as I can figure out, these classes
> really *are* problematic, in that if we allowed
> GeneralizedNewtypeDeriving for them, there would be a way to subvert
> the type system. To make these derivable, we would need to be able to
> restrict various type parameters from taking on values that take a
> nominal argument. Without the ability to restrict the values in this
> way, there could be trouble.
>
I suppose it's unlikely that the roles mechanism will be extended to
allow for such restriction?

Cheers,

- Ben

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131231/8b4b105f/attachment-0001.html>
-------------- next part --------------
An embedded message was scrubbed...
From: Simon Peyton-Jones <simonpj at microsoft.com>
Subject: RE: More GND + role inference woes
Date: Wed, 16 Oct 2013 13:28:28 +0000
Size: 48528
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131231/8b4b105f/attachment-0002.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Richard Eisenberg <eir at cis.upenn.edu>
Subject: Re: More GND + role inference woes
Date: Sun, 15 Dec 2013 01:06:08 +0000
Size: 4517
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131231/8b4b105f/attachment-0003.mht>