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