[GHC] #11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced

12 Jan 2016

      #11416: GHC mistakenly believes datatype with type synonym in its type can't be
eta-reduced
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I uncovered this when playing around with `-XTypeInType`:

 {{{#!hs
 {-# 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:

 {{{#!hs
 {-# 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11416
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler