[GHC] #14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code

13 Dec 2017

      #14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
  (Type checker)                     |
           Keywords:  deriving       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This program //should// compile:

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

 {{{#!hs
 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):

 {{{#!hs
   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 `Type`s, but rather `HsType GhcRn`s (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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14579
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)