GitLab

In 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:

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

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

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

Trac metadata

Trac field	Value
Version	8.2.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture