Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,386
    • Issues 4,386
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 371
    • Merge Requests 371
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #14728

Closed
Open
Opened Jan 27, 2018 by Ryan Scott@RyanGlScottMaintainer

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
Assignee
Assign to
8.4.1
Milestone
8.4.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#14728