[GHC] #14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code
GHC
ghc-devs at haskell.org
Sat Jan 5 21:27:54 UTC 2019
#14579: GeneralizedNewtypeDeriving produces ambiguously-kinded code
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.10.1
Component: Compiler (Type | Version: 8.2.2
checker) |
Resolution: | Keywords: deriving
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | deriving/should_compile/T14579{a}
Blocked By: 12045 | Blocking:
Related Tickets: | Differential Rev(s): Phab:D4264,
Wiki Page: | Phab:D5229
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
When writing comment:12, I was originally hopeful that we could scrap all
of commit 649e777211fe08432900093002547d7358f92d82—that is, that we could
avoid generating any explicit kind signatures and exclusively use visible
kind application. Alas, this is not the case. Consider this tortuous
example:
{{{#!hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
module Bug where
import Data.Kind
import Data.Proxy
-- type P :: forall {k} {t :: k}. Proxy t
type P = 'Proxy
-- type Wat :: forall a. Proxy a -> *
newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
deriving Eq
-- type Wat2 :: forall {a}. Proxy a -> *
type Wat2 = Wat
-- type Glurp :: * -> *
newtype Glurp a = MkGlurp (Wat2 (P :: Proxy a))
deriving Eq
}}}
This compiles with GHC 8.6.3. However, if I try to switch
`GeneralizedNewtypeDeriving` over to using exclusively visible kind
applications, then the code that it generates no longer compiles:
{{{
$ ghc/inplace/bin/ghc-stage2 Bug.hs -ddump-deriv
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
==================== 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.Maybe.Maybe a_a1wk
-> GHC.Maybe.Maybe a_a1wk -> GHC.Types.Bool)
@(Bug.Wat @a_a1wk x_a210
-> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool)
((GHC.Classes.==) @(GHC.Maybe.Maybe a_a1wk)) ::
Bug.Wat @a_a1wk x_a210 -> Bug.Wat @a_a1wk x_a210 ->
GHC.Types.Bool
(GHC.Classes./=)
= GHC.Prim.coerce
@(GHC.Maybe.Maybe a_a1wk
-> GHC.Maybe.Maybe a_a1wk -> GHC.Types.Bool)
@(Bug.Wat @a_a1wk x_a210
-> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool)
((GHC.Classes./=) @(GHC.Maybe.Maybe a_a1wk)) ::
Bug.Wat @a_a1wk x_a210 -> Bug.Wat @a_a1wk x_a210 ->
GHC.Types.Bool
instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where
(GHC.Classes.==)
= GHC.Prim.coerce
@(Bug.Wat2 Bug.P -> Bug.Wat2 Bug.P -> GHC.Types.Bool)
@(Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool)
((GHC.Classes.==) @(Bug.Wat2 Bug.P)) ::
Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool
(GHC.Classes./=)
= GHC.Prim.coerce
@(Bug.Wat2 Bug.P -> Bug.Wat2 Bug.P -> GHC.Types.Bool)
@(Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool)
((GHC.Classes./=) @(Bug.Wat2 Bug.P)) ::
Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool
Derived type family instances:
Bug.hs:21: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:21:12-13
• In the expression:
GHC.Prim.coerce
@(Wat2 P -> Wat2 P -> Bool)
@(Glurp a -> Glurp a -> Bool)
((==) @(Wat2 P)) ::
Glurp a -> Glurp a -> Bool
In an equation for ‘==’:
(==)
= GHC.Prim.coerce
@(Wat2 P -> Wat2 P -> Bool)
@(Glurp a -> Glurp a -> Bool)
((==) @(Wat2 P)) ::
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:21:12)
|
21 | deriving Eq
| ^^
Bug.hs:21: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:21:12-13
• In the expression:
GHC.Prim.coerce
@(Wat2 P -> Wat2 P -> Bool)
@(Glurp a -> Glurp a -> Bool)
((/=) @(Wat2 P)) ::
Glurp a -> Glurp a -> Bool
In an equation for ‘/=’:
(/=)
= GHC.Prim.coerce
@(Wat2 P -> Wat2 P -> Bool)
@(Glurp a -> Glurp a -> Bool)
((/=) @(Wat2 P)) ::
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:21:12)
|
21 | deriving Eq
| ^^
}}}
Ambiguity once again rears its ugly head. You might be tempted to think
that we could sprinkle `@a` somewhere in `Wat2 P` to resolve the
ambiguity, but this is impossible, as all of the type variable binders in
`Wat2` and `P` are inferred, making them unavailable for visible kind
application. The only way out of this mess is to surround `P` with an
explicit kind signature (i.e., `(P :: Proxy a)`).
That being said, visible kind application will help us quite a bit, as we
can avoid generating explicit kind signatures whenever a tycon only has
specified or required type variable binders in its kind. But we'll still
need to keep around the hack in commit
649e777211fe08432900093002547d7358f92d82 in the event that there are any
inferred type variables.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14579#comment:20>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list