#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