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