## #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

Differential Rev(s): | → Phab:D1772 |
---|---|

Status: | new → patch |

### comment:2 Changed 23 months ago by

### comment:3 Changed 23 months ago by

Milestone: | → 8.0.1 |
---|---|

Status: | patch → merge |

Version: | 8.1 → 8.0.1-rc1 |

### comment:4 Changed 23 months ago by

Resolution: | → fixed |
---|---|

Status: | merge → closed |

This was merged to `ghc-8.0`

as 20f848b0e9020355340f3f0f2311d2f3d9aceb7c.

### comment:5 Changed 22 months ago by

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

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.

In 165ae440/ghc: