Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?
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 nobrainer, 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 ddumpderiv
to figure out what code is being generated:
$ /opt/ghc/8.2.2/bin/ghci Bug.hs ddumpderiv
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
 ^
Uhoh. 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 