[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