[Haskell-cafe] Eta Reduction

[Niklas Haas]

On Wed, 2 Apr 2014 14:25:55 -0700, John Lato <jwlato at gmail.com> wrote:
> On Apr 2, 2014 4:32 PM, "Niklas Haas" <haskell at nand.wakku.to> wrote:
> >
> > On Wed, 2 Apr 2014 09:51:46 -0400, Edward Kmett <ekmett at gmail.com> wrote:
> > > We're not storing the instance as a slot in the constructor, so this
> isn't.
> > >
> > > data Foo a where
> > >    Foo :: Seq a => Int -> a -> Foo a
> > >
> > > or equivalently
> > >
> > > data Foo a = Seq a => Foo !Int !a
> >
> > Why not? Say we define Seq to something like
> >
> > > type family Seq (a :: *) :: Constraint where
> > >   Seq (a -> b) = 1 ~ 0
> > >   Seq t = ()
> >
> > What would be the drawback in this scenario?
> 
> I think that would be acceptable if we posit the existence of a valid Seq a
> dictionary.  I think that would be possible for all builtin types and
> anything defined via data.  But what about e.g.
> 
>   newtype F = F (forall x. Show x => x-> String)

Oh, fair point; this particular F apparently doesn't break it but if you
remove the Show x constraint, it does.

Actually, is that a bug in GHC?

> λ newtype F = F (forall x. Show x => x -> String)
> λ F undefined `seq` ()
> ()
> λ undefined `seq` ()
> *** Exception: Prelude.undefined

I'm not sure how to interpret this output.