Skip to content

GeneralizedNewtypeDeriving produces ambiguously-kinded code

This program //should// compile:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Data.Proxy

newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
  deriving Eq

newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))
  deriving Eq

After all, it //should// produce this Eq (Glurp a) instance, which compiles without issue:

instance Eq a => Eq (Glurp a) where
  (==) = coerce @(Wat ('Proxy :: Proxy a) -> Wat ('Proxy :: Proxy a) -> Bool)
                @(Glurp a                 -> Glurp a                 -> Bool)
                (==)

But despite my wishful thinking, GHC does not actually do this. In fact, the code that GHC tries to generate for an Eq (Glurp a) instance is completely wrong:

$ /opt/ghc/8.2.2/bin/ghci -ddump-deriv 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 )

==================== Derived instances ====================
Derived class instances:
  instance forall a (x :: Data.Proxy.Proxy a).
           GHC.Classes.Eq a =>
           GHC.Classes.Eq (Bug.Wat x) where
    (GHC.Classes.==)
      = GHC.Prim.coerce
          @(GHC.Base.Maybe a_a2wE -> GHC.Base.Maybe a_a2wE -> GHC.Types.Bool)
          @(Bug.Wat x_a2wF -> Bug.Wat x_a2wF -> GHC.Types.Bool)
          (GHC.Classes.==)
    (GHC.Classes./=)
      = GHC.Prim.coerce
          @(GHC.Base.Maybe a_a2wE -> GHC.Base.Maybe a_a2wE -> GHC.Types.Bool)
          @(Bug.Wat x_a2wF -> Bug.Wat x_a2wF -> GHC.Types.Bool)
          (GHC.Classes./=)
  
  instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where
    (GHC.Classes.==)
      = GHC.Prim.coerce
          @(Bug.Wat Data.Proxy.Proxy
            -> Bug.Wat Data.Proxy.Proxy -> GHC.Types.Bool)
          @(Bug.Glurp a_a1vT -> Bug.Glurp a_a1vT -> GHC.Types.Bool)
          (GHC.Classes.==)
    (GHC.Classes./=)
      = GHC.Prim.coerce
          @(Bug.Wat Data.Proxy.Proxy
            -> Bug.Wat Data.Proxy.Proxy -> GHC.Types.Bool)
          @(Bug.Glurp a_a1vT -> Bug.Glurp a_a1vT -> GHC.Types.Bool)
          (GHC.Classes./=)
  

Derived type family instances:



Bug.hs:12:12: error:
    • Couldn't match representation of type ‘a0’ with that of ‘a’
        arising from a use of ‘GHC.Prim.coerce’
      ‘a’ is a rigid type variable bound by
        the instance declaration at Bug.hs:12:12-13
    • In the expression:
        GHC.Prim.coerce
          @(Wat Proxy -> Wat Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (==)
      In an equation for ‘==’:
          (==)
            = GHC.Prim.coerce
                @(Wat Proxy -> Wat Proxy -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                (==)
      When typechecking the code for ‘==’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘Eq (Glurp a)’
    • Relevant bindings include
        (==) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:12:12)
   |
12 |   deriving Eq
   |            ^^

Bug.hs:12:12: error:
    • Could not deduce (Eq a0) arising from a use of ‘==’
      from the context: Eq a
        bound by the instance declaration at Bug.hs:12:12-13
      The type variable ‘a0’ is ambiguous
      These potential instances exist:
        instance forall k (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’
        instance Eq Ordering -- Defined in ‘GHC.Classes’
        instance Eq Integer
          -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’
        ...plus 25 others
        ...plus 9 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the third argument of ‘GHC.Prim.coerce’, namely ‘(==)’
      In the expression:
        GHC.Prim.coerce
          @(Wat Proxy -> Wat Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (==)
      In an equation for ‘==’:
          (==)
            = GHC.Prim.coerce
                @(Wat Proxy -> Wat Proxy -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                (==)
      When typechecking the code for ‘==’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
   |
12 |   deriving Eq
   |            ^^

Bug.hs:12:12: error:
    • Couldn't match representation of type ‘a1’ with that of ‘a’
        arising from a use of ‘GHC.Prim.coerce’
      ‘a’ is a rigid type variable bound by
        the instance declaration at Bug.hs:12:12-13
    • In the expression:
        GHC.Prim.coerce
          @(Wat Proxy -> Wat Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (/=)
      In an equation for ‘/=’:
          (/=)
            = GHC.Prim.coerce
                @(Wat Proxy -> Wat Proxy -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                (/=)
      When typechecking the code for ‘/=’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘Eq (Glurp a)’
    • Relevant bindings include
        (/=) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:12:12)
   |
12 |   deriving Eq
   |            ^^

Bug.hs:12:12: error:
    • Could not deduce (Eq a1) arising from a use of ‘/=’
      from the context: Eq a
        bound by the instance declaration at Bug.hs:12:12-13
      The type variable ‘a1’ is ambiguous
      These potential instances exist:
        instance forall k (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’
        instance Eq Ordering -- Defined in ‘GHC.Classes’
        instance Eq Integer
          -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’
        ...plus 25 others
        ...plus 9 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the third argument of ‘GHC.Prim.coerce’, namely ‘(/=)’
      In the expression:
        GHC.Prim.coerce
          @(Wat Proxy -> Wat Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (/=)
      In an equation for ‘/=’:
          (/=)
            = GHC.Prim.coerce
                @(Wat Proxy -> Wat Proxy -> Bool)
                @(Glurp a -> Glurp a -> Bool)
                (/=)
      When typechecking the code for ‘/=’
        in a derived instance for ‘Eq (Glurp a)’:
        To see the code I am typechecking, use -ddump-deriv
   |
12 |   deriving Eq
   |            ^^

Yikes. To see what went wrong, let's zoom in a particular part of the -ddump-deriv output (cleaned up a bit for presentation purposes):

  instance Eq a => Eq (Glurp a) where
    (==)
      = coerce
          @(Wat 'Proxy -> Wat 'Proxy -> Bool)
          @(Glurp a -> Glurp a -> Bool)
          (==)

Notice that it's Wat 'Proxy, and not Wat ('Proxy :: Proxy a)! And no, that's not just a result of GHC omitting the kind information—you will see the exact same thing if you compile with -fprint-explicit-kinds. What's going on here?

As it turns out, the types inside of those visible type applications aren't Types, but rather HsType GhcRns (i.e., source syntax). So what is happening is that GHC is literally producing @(Wat 'Proxy -> Wat 'Proxy -> Bool) //as source syntax//, not as a Type. This means that 'Proxy has an underspecified kind, resulting in the numerous The type variable ‘a0’ is ambiguous errors you see 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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information