[GHC] #14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code
GHC
ghc-devs at haskell.org
Wed Dec 13 16:02:55 UTC 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
More information about the ghc-tickets
mailing list