Opened 23 months ago

Closed 23 months ago

Last modified 22 months ago

#11416 closed bug (fixed)

GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1772
Wiki Page:

Description

I uncovered this when playing around with -XTypeInType:

{-# LANGUAGE DeriveFunctor, TypeInType #-}
module CantEtaReduce1 where

import Data.Kind

type ConstantT a b = a
newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor

This fails because it thinks that you can't reduce the last type variable of T, since it mentions another type variable (f):

    • Cannot eta-reduce to an instance of form
        instance (...) => Functor (T f)
    • In the newtype declaration for ‘T

But it should be able to, since ConstantT * f reduces to *, and the equivalent declaration newtype T (f :: * -> *) (a :: *) = ... eta-reduces just fine.

I marked this as appearing in GHC 8.1 since you need -XTypeInType to have kind synonyms, but this can also happen in earlier GHC versions with data families:

{-# LANGUAGE DeriveFunctor, PolyKinds, TypeFamilies #-}
module CantEtaReduce2 where

type ConstantT a b = a
data family T (f :: * -> *) (a :: *)
newtype instance T f (ConstantT a f) = T (f a) deriving Functor

I believe the fix will be to apply coreView with precision to parts of the code which typecheck deriving statements so that these type synonyms are peeled off.

Change History (6)

comment:1 Changed 23 months ago by RyanGlScott

Differential Rev(s): Phab:D1772
Status: newpatch

comment:2 Changed 23 months ago by Ben Gamari <ben@…>

In 165ae440/ghc:

Expand type/kind synonyms in TyVars before deriving-related typechecking

Before, it was possible to have a datatypes such as

```
type ConstantT a b = a
newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor

data family TFam (f :: * -> *) (a :: *)
newtype instance TFam f (ConstantT a f) = TFam (f a) deriving Functor
```

fail to eta-reduce because either (1) a TyVar had a kind synonym that
mentioned another TyVar, or (2) an instantiated type was itself a type
synonym that mentioned another TyVar. A little bit of tweaking to
`expandTypeSynonyms` and applying it before the eta-reduction check in
the `deriving` machinery is sufficient to fix this.

Fixes #11416.

Test Plan: ./validate

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: simonpj

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1772

GHC Trac Issues: #11416

comment:3 Changed 23 months ago by thomie

Milestone: 8.0.1
Status: patchmerge
Version: 8.18.0.1-rc1

comment:4 Changed 23 months ago by bgamari

Resolution: fixed
Status: mergeclosed

This was merged to ghc-8.0 as 20f848b0e9020355340f3f0f2311d2f3d9aceb7c.

comment:5 Changed 22 months ago by RyanGlScott

Hm, there's another tricky case that I hadn't previously considered:

type ConstT a b = a
data family Fam a b
data instance Fam (ConstT a b) b = Fam b deriving Functor

Currently, the eta-reduction check rejects this. Should it?

On on hand, the b in ConstT a b will go away if you expand the ConstT type synonym, so one could argue this is no different from data instance Fam a b = Fam b deriving Functor (which is accepted).

On the other hand, if you consider what the derived instance would look like:

instance Functor (Fam (ConstT a b)) where ...

This feels a bit off, because now the instance head is mentioning an eta-reduced type variable! But it does typecheck if you type it in manually...

comment:6 Changed 22 months ago by simonpj

Maybe. If you type it in manually you'll get a spuriously polymorphic instance, which will result in some uses of Any. I think the same will happen if you allow this data instance. Perhaps it's no more than using exactTyCoVarsofType in eta_reduce in tcDataFamInstDecl.

You'd need to make sure you quantify over the tyvar anyway; but I think that will happen.

I don't feel strongly. It would be good to document it.

Crumbs if I had a pound for every hour I've spent on GeneralisedNewtypeDeriving I'd be a rich man.

Thanks for digging into this

Note: See TracTickets for help on using tickets.