[GHC] #14728: Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?

[GHC]

#14728: Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
  (Type checker)                     |
           Keywords:  deriving,      |  Operating System:  Unknown/Multiple
  TypeFamilies                       |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 In Phab:D2636, I implemented this ability to use
 `GeneralizedNewtypeDeriving` to derive instances of type classes with
 associated type families. At the time, I thought the implementation was a
 no-brainer, but now I'm starting to have second thoughts. To explain what
 I mean, consider this program:

 {{{#!hs
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Functor.Identity
 import Data.Kind

 class C (a :: Type) where
   type T a (x :: a) :: Type

 instance C () where
   type T () '() = Bool

 deriving instance C (Identity a)
 }}}

 Quite to my surprise, this typechecks. Let's consult `-ddump-deriv` to
 figure out what code is being generated:

 {{{
 $ /opt/ghc/8.2.2/bin/ghci Bug.hs -ddump-deriv
 GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 ==================== Derived instances ====================
 Derived class instances:
   instance Bug.C (Data.Functor.Identity.Identity a) where


 Derived type family instances:
   type Bug.T (Data.Functor.Identity.Identity a1_a1M3) x_a1M5 = Bug.T
                                                                  a1_a1M3
 x_a1M5
 }}}

 Hm... OK. Since GHC was able to generate this code, surely we should be
 able to write it ourselves, right?

 {{{#!hs
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Functor.Identity
 import Data.Kind

 class C (a :: Type) where
   type T a (x :: a) :: Type

 instance C () where
   type T () '() = Bool

 -- deriving instance C (Identity a)

 instance C (Identity a) where
   type T (Identity a) x = T a x
 }}}
 {{{
 $ /opt/ghc/8.2.2/bin/ghci Bug.hs
 GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:19:31: error:
     • Occurs check: cannot construct the infinite kind: a ~ Identity a
     • In the second argument of ‘T’, namely ‘x’
       In the type ‘T a x’
       In the type instance declaration for ‘T’
    |
 19 |   type T (Identity a) x = T a x
    |                               ^
 }}}

 Uh-oh. GHC gets quite angry when we try to type this in ourselves, which
 isn't a good sign. This raises the question: just what is GHC doing in the
 previous version of the program? I tried to answer that question by seeing
 if `T (Identity a) x` could ever reduce:

 {{{#!hs
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Functor.Identity
 import Data.Kind

 class C (a :: Type) where
   type T a (x :: a) :: Type

 instance C () where
   type T () '() = Bool

 deriving instance C (Identity a)

 f :: T (Identity ()) ('Identity '())
 f = True
 }}}

 And lo and behold, you get:

 {{{
 $ /opt/ghc/8.2.2/bin/ghci Bug.hs
 GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:19:5: error:
     • Couldn't match type ‘T () ('Identity '())’ with ‘Bool’
       Expected type: T (Identity ()) ('Identity '())
         Actual type: Bool
     • In the expression: True
       In an equation for ‘f’: f = True
    |
 19 | f = True
    |     ^^^^
 }}}

 It appears that `T (Identity ()) ('Identity '())` reduced to `T ()
 ('Identity '())`. At that point, it becomes stuck. (Perhaps it's for the
 best that it's the case—if `T () ('Identity '())` managed to reduce, who
 knows what kind of mischief GHC could get itself into.)

 But all of this leads me to wonder: is something broken in the
 implementation of this feature, or is `GeneralizedNewtypeDeriving` simply
 not sound with respect to associated type families? I certainly hope that
 it's not the latter, as it's quite a useful feature. But at the same time,
 it's hard to reconcile that usefulness with the strange behavior above.

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