[GHC] #11732: Deriving Generic1 interacts poorly with TypeInType
GHC
ghc-devs at haskell.org
Sat Mar 26 21:57:16 UTC 2016
#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:/compiler/typecheck/TcGenGenerics.hs#l482
here] for the code).
As a result, GHC only has knowledge of the `tyConTyVars`
[http://git.haskell.org/ghc.git/blob/9f73e46c0f34b8b5e8318e6b488b7dade7db68e3:/compiler/typecheck/TcGenGenerics.hs#l384
on the LHS] and
[http://git.haskell.org/ghc.git/blob/9f73e46c0f34b8b5e8318e6b488b7dade7db68e3:/compiler/typecheck/TcGenGenerics.hs#l539
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
More information about the ghc-tickets
mailing list