#11732: Deriving Generic1 interacts poorly with TypeInType -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType, | Generics Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:6 goldfire]:
Before blindly trying this, though, I'd love someone (Ryan, it seems) who understands Generics to consider what this instantiation check is really trying to do, and why it (previously) avoided looking at kinds. And why it makes sense to look at dependency, as I've proposed here. I've no real clue what's going on, and when I deleted `isKind` (which was what was used previously) I just reached for the closest thing, which was visibility.
As I noted [https://ghc.haskell.org/trac/ghc/ticket/11732?replyto=6#comment:1 here], the reason why `gen_Generic_binds` seems to need the instantiation check at the moment is a matter of implementation practicality. Deriving `Generic(1)` is different from any other derived classes in that in generates a type family instance (`Rep`/`Rep1`), so it needs to be able to faithfully reproduce the the same type as what the user provides. GHC's current mechanism for retrieving the type is by examining the `TyCon` (see [http://git.haskell.org/ghc.git/blob/9f73e46c0f34b8b5e8318e6b488b7dade7db68e3... here] for the code). As a result, GHC only has knowledge of the `tyConTyVars` [http://git.haskell.org/ghc.git/blob/9f73e46c0f34b8b5e8318e6b488b7dade7db68e3... on the LHS] and [http://git.haskell.org/ghc.git/blob/9f73e46c0f34b8b5e8318e6b488b7dade7db68e3... on the RHS] of the derived `Rep(1)` instance. If any of those type variables were to be instantiated to a concrete type, it would result in an apparent mismatch between the instance head and the generated `Rep(1)` instance (the subject of ticket #5939), e.g., {{{#!hs data T a b c = T a b c deriving instance Generic (T a Bool c) ==> instance Generic (T a Bool c) where type Rep (T a b c) = a :*: b :*: c -- wrong? }}} But interestingly, it's possible to have this kind of mismatch with clever use of `-XTypeInType`. There's the example in the ticket description, plus this: {{{ λ> :set -XDeriveGeneric -XTypeInType -ddump-deriv λ> import Data.Proxy λ> data P (a :: k) = P (Proxy k) deriving Generic1 ==================== Derived instances ==================== Derived instances: instance GHC.Generics.Generic1 Ghci3.P where GHC.Generics.from1 (Ghci3.P g1_a2b8) = GHC.Generics.M1 (GHC.Generics.M1 (GHC.Generics.M1 (GHC.Generics.K1 g1_a2b8))) GHC.Generics.to1 (GHC.Generics.M1 (GHC.Generics.M1 (GHC.Generics.M1 g1_a2b9))) = Ghci3.P (GHC.Generics.unK1 g1_a2b9) GHC.Generics representation types: type GHC.Generics.Rep1 Ghci3.P = GHC.Generics.D1 ('GHC.Generics.MetaData "P" "Ghci3" "interactive" 'GHC.Types.False) (GHC.Generics.C1 ('GHC.Generics.MetaCons "P" 'GHC.Generics.PrefixI 'GHC.Types.False) (GHC.Generics.S1 ('GHC.Generics.MetaSel 'GHC.Base.Nothing 'GHC.Generics.NoSourceUnpackedness 'GHC.Generics.NoSourceStrictness 'GHC.Generics.DecidedLazy) (GHC.Generics.Rec0 (Data.Proxy.Proxy k_a2b7)))) λ> :kind! Rep1 P Rep1 P :: * -> * = D1 ('MetaData "P" "Ghci3" "interactive" 'False) (C1 ('MetaCons "P" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Proxy *)))) }}} Notice how the generated `Rep1 P` instance mentions kind `k_a2b7` when it should be `*`. This probably shouldn't typecheck, but it does... So we really have two issues here: 1. `gen_Generic_binds` doesn't do any type variable substitution in the generated `Rep1` instance. 2. A `deriving Generic1` clause might instantiate more type variables than what would be desirable in a generated `Generic1` instance. Fixing (1) might be doable with some `Type`-related subtitution sorcery. Fixing (2) requires figuring out when a substitution is "undesirable". * In #5939, Pedro [https://ghc.haskell.org/trac/ghc/ticket/5939#comment:2 decided] to make an instantiation of a //type// variable in a `Generic(1)` instance was bad, even in the presence of `-XStandaloneDeriving`. Kinds were excluded from this discussion since, at the time, you couldn't put kinds at the type level. * Alternatively, we could be ultra-permissive and allow //any// type variables to be instantiated when deriving `Generic(1)`, both standalone and using a `deriving` clause. This should be sound (I think) if (1) gets fixed. * You [https://ghc.haskell.org/trac/ghc/ticket/11732?replyto=6#comment:2 proposed] a scheme wherein instantiating type/kind variables in a `Generic(1)` instance is OK with `-XStandaloneDeriving`, but not with just a `deriving` clause. I'd be fine with any approach. But if we picked the first or last option, now that types and kinds are merged, we'd have to figure out a better distinction between what type variables are and aren't allowed to be instantiated in such an instance. Your suggestion of only checking dependent type variables would only be feasible with the third option, I believe, because combining that check with the first option would cause [https://ghc.haskell.org/trac/ghc/ticket/5939#comment:1 this program] to be erroneously accepted. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11732#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler