Remove the instantiation check when deriving Generic(1)

Previously, deriving `Generic(1)` bailed out when attempting to
instantiate visible type parameters (#5939), but this instantiation
check was quite fragile and doesn't interact well with `-XTypeInType`.
It has been decided that `Generic(1)` shouldn't be subjected to this
check anyway, so it has been removed, and `gen_Generic_binds`'s
machinery has been updated to substitute the type variables in a
generated `Rep`/`Rep1` instance with the user-supplied type arguments.

In addition, this also refactors `Condition` in `TcDeriv` a bit. Namely,
since we no longer need `tc_args` to check any conditions, the `[Type]`
component of `Condition` has been removed.

Fixes #11732.

Test Plan: ./validate

Reviewers: goldfire, kosmikus, simonpj, bgamari, austin

Reviewed By: simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2061

GHC Trac Issues: #5939, #11732

9 files changed, 249 insertions, 113 deletions

diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 90d981600d..f579748797 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -705,6 +705,55 @@ an instance   $df :: forall (x:*->*). Functor x => Functor (P * (x:*->*))
 and similarly for C.  Notice the modified kind of x, both at binding
 and occurrence sites.
 
+This can lead to some surprising results when *visible* kind binder is
+unified (in contrast to the above examples, in which only non-visible kind
+binders were considered). Consider this example from Trac #11732:
+
+    data T k (a :: k) = MkT deriving Functor
+
+Since unification yields k:=*, this results in a generated instance of:
+
+    instance Functor (T *) where ...
+
+which looks odd at first glance, since one might expect the instance head
+to be of the form Functor (T k). Indeed, one could envision an alternative
+generated instance of:
+
+    instance (k ~ *) => Functor (T k) where
+
+But this does not typecheck as the result of a -XTypeInType design decision:
+kind equalities are not allowed to be bound in types, only terms. But in
+essence, the two instance declarations are entirely equivalent, since even
+though (T k) matches any kind k, the only possibly value for k is *, since
+anything else is ill-typed. As a result, we can just as comfortably use (T *).
+
+Another way of thinking about is: deriving clauses often infer constraints.
+For example:
+
+    data S a = S a deriving Eq
+
+infers an (Eq a) constraint in the derived instance. By analogy, when we
+are deriving Functor, we might infer an equality constraint (e.g., k ~ *).
+The only distinction is that GHC instantiates equality constraints directly
+during the deriving process.
+
+Another quirk of this design choice manifests when typeclasses have visible
+kind parameters. Consider this code (also from Trac #11732):
+
+    class Cat k (cat :: k -> k -> *) where
+      catId   :: cat a a
+      catComp :: cat b c -> cat a b -> cat a c
+
+    instance Cat * (->) where
+      catId   = id
+      catComp = (.)
+
+    newtype Fun a b = Fun (a -> b) deriving (Cat k)
+
+Even though we requested an derived instance of the form (Cat k Fun), the
+kind unification will actually generate (Cat * Fun) (i.e., the same thing as if
+the user wrote deriving (Cat *)).
+
 Note [Eta-reducing type synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 One can instantiate a type in a data family instance with a type synonym that
@@ -857,7 +906,7 @@ mkDataTypeEqn :: DynFlags
 
 mkDataTypeEqn dflags overlap_mode tvs cls cls_tys
               tycon tc_args rep_tc rep_tc_args mtheta
-  = case checkSideConditions dflags mtheta cls cls_tys rep_tc rep_tc_args of
+  = case checkSideConditions dflags mtheta cls cls_tys rep_tc of
         -- NB: pass the *representation* tycon to checkSideConditions
         NonDerivableClass   msg -> bale_out (nonStdErr cls $$ msg)
         DerivableClassError msg -> bale_out msg
@@ -1098,11 +1147,11 @@ data DerivStatus = CanDerive                 -- Standard class, can derive
 -- to generate code for, such as Eq, Ord, Ix, etc.
 
 checkSideConditions :: DynFlags -> DerivContext -> Class -> [TcType]
-                    -> TyCon -> [Type] -- tycon and its parameters
+                    -> TyCon -- tycon
                     -> DerivStatus
-checkSideConditions dflags mtheta cls cls_tys rep_tc rep_tc_args
+checkSideConditions dflags mtheta cls cls_tys rep_tc
   | Just cond <- sideConditions mtheta cls
-  = case (cond (dflags, rep_tc, rep_tc_args)) of
+  = case (cond (dflags, rep_tc)) of
         NotValid err -> DerivableClassError err  -- Class-specific error
         IsValid  | null cls_tys -> CanDerive     -- All derivable classes are unary, so
                                                  -- cls_tys (the type args other than last)
@@ -1189,11 +1238,8 @@ canDeriveAnyClass dflags _tycon clas
 typeToTypeKind :: Kind
 typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
 
-type Condition = (DynFlags, TyCon, [Type]) -> Validity
-        -- first Bool is whether or not we are allowed to derive Data and Typeable
-        -- second Bool is whether or not we are allowed to derive Functor
+type Condition = (DynFlags, TyCon) -> Validity
         -- TyCon is the *representation* tycon if the data type is an indexed one
-        -- [Type] are the type arguments to the (representation) TyCon
         -- Nothing => OK
 
 orCond :: Condition -> Condition -> Condition
@@ -1216,7 +1262,7 @@ cond_stdOK (Just _) _ _
   = IsValid     -- Don't check these conservative conditions for
                 -- standalone deriving; just generate the code
                 -- and let the typechecker handle the result
-cond_stdOK Nothing permissive (_, rep_tc, _)
+cond_stdOK Nothing permissive (_, rep_tc)
   | null data_cons
   , not permissive      = NotValid (no_cons_why rep_tc $$ suggestion)
   | not (null con_whys) = NotValid (vcat con_whys $$ suggestion)
@@ -1240,10 +1286,10 @@ no_cons_why rep_tc = quotes (pprSourceTyCon rep_tc) <+>
                      text "must have at least one data constructor"
 
 cond_RepresentableOk :: Condition
-cond_RepresentableOk (dflags, tc, tc_args) = canDoGenerics dflags tc tc_args
+cond_RepresentableOk (_, tc) = canDoGenerics tc
 
 cond_Representable1Ok :: Condition
-cond_Representable1Ok (dflags, tc, tc_args) = canDoGenerics1 dflags tc tc_args
+cond_Representable1Ok (_, tc) = canDoGenerics1 tc
 
 cond_enumOrProduct :: Class -> Condition
 cond_enumOrProduct cls = cond_isEnumeration `orCond`
@@ -1252,7 +1298,7 @@ cond_enumOrProduct cls = cond_isEnumeration `orCond`
 cond_args :: Class -> Condition
 -- For some classes (eg Eq, Ord) we allow unlifted arg types
 -- by generating specialised code.  For others (eg Data) we don't.
-cond_args cls (_, tc, _)
+cond_args cls (_, tc)
   = case bad_args of
       []     -> IsValid
       (ty:_) -> NotValid (hang (text "Don't know how to derive" <+> quotes (ppr cls))
@@ -1276,7 +1322,7 @@ cond_args cls (_, tc, _)
 
 
 cond_isEnumeration :: Condition
-cond_isEnumeration (_, rep_tc, _)
+cond_isEnumeration (_, rep_tc)
   | isEnumerationTyCon rep_tc = IsValid
   | otherwise                 = NotValid why
   where
@@ -1286,7 +1332,7 @@ cond_isEnumeration (_, rep_tc, _)
                   -- See Note [Enumeration types] in TyCon
 
 cond_isProduct :: Condition
-cond_isProduct (_, rep_tc, _)
+cond_isProduct (_, rep_tc)
   | isProductTyCon rep_tc = IsValid
   | otherwise             = NotValid why
   where
@@ -1300,7 +1346,7 @@ cond_functorOK :: Bool -> Bool -> Condition
 --            (c) don't use argument in the wrong place, e.g. data T a = T (X a a)
 --            (d) optionally: don't use function types
 --            (e) no "stupid context" on data type
-cond_functorOK allowFunctions allowExQuantifiedLastTyVar (_, rep_tc, _)
+cond_functorOK allowFunctions allowExQuantifiedLastTyVar (_, rep_tc)
   | null tc_tvs
   = NotValid (text "Data type" <+> quotes (ppr rep_tc)
               <+> text "must have some type parameters")
@@ -1348,7 +1394,7 @@ cond_functorOK allowFunctions allowExQuantifiedLastTyVar (_, rep_tc, _)
     wrong_arg   = text "must use the type variable only as the last argument of a data type"
 
 checkFlag :: LangExt.Extension -> Condition
-checkFlag flag (dflags, _, _)
+checkFlag flag (dflags, _)
   | xopt flag dflags = IsValid
   | otherwise        = NotValid why
   where
@@ -1443,7 +1489,6 @@ Here there *is* no argument field, but we must nevertheless generate
 a context for the Data instances:
         instance Typable a => Data (T a) where ...
 
-
 ************************************************************************
 *                                                                      *
                 Deriving newtypes
@@ -1482,7 +1527,7 @@ mkNewTypeEqn dflags overlap_mode tvs
             , ds_overlap = overlap_mode
             , ds_newtype = Just rep_inst_ty }
   | otherwise
-  = case checkSideConditions dflags mtheta cls cls_tys rep_tycon rep_tc_args of
+  = case checkSideConditions dflags mtheta cls cls_tys rep_tycon of
       -- Error with standard class
       DerivableClassError msg
         | might_derive_via_coercible -> bale_out (msg $$ suggest_gnd)
@@ -2088,7 +2133,10 @@ genDerivStuff loc clas dfun_name tycon inst_tys tyvars
   = let gk = if ck == genClassKey then Gen0 else Gen1
         -- TODO NSF: correctly identify when we're building Both instead of One
     in do
-      (binds, faminst) <- gen_Generic_binds gk tycon (nameModule dfun_name)
+      let inst_ty = ASSERT(not $ null inst_tys)
+                          head inst_tys
+      (binds, faminst) <- gen_Generic_binds gk tycon inst_ty
+                                            (nameModule dfun_name)
       return (binds, unitBag (DerivFamInst faminst))
 
   -- Not deriving Generic(1), so we first check if the compiler has built-in
diff --git a/compiler/typecheck/TcGenGenerics.hs b/compiler/typecheck/TcGenGenerics.hs
index 0477767bd2..03b4d65c6f 100644
--- a/compiler/typecheck/TcGenGenerics.hs
+++ b/compiler/typecheck/TcGenGenerics.hs
@@ -18,7 +18,6 @@ import Type
 import TcType
 import TcGenDeriv
 import DataCon
-import DynFlags    ( DynFlags, GeneralFlag(Opt_PrintExplicitKinds), gopt )
 import TyCon
 import FamInstEnv       ( FamInst, FamFlavor(..), mkSingleCoAxiom )
 import FamInst
@@ -37,7 +36,8 @@ import HscTypes
 import ErrUtils( Validity(..), andValid )
 import SrcLoc
 import Bag
-import VarSet (elemVarSet)
+import VarEnv
+import VarSet (elemVarSet, partitionVarSet)
 import Outputable
 import FastString
 import Util
@@ -63,10 +63,10 @@ For the generic representation we need to generate:
 \end{itemize}
 -}
 
-gen_Generic_binds :: GenericKind -> TyCon -> Module
+gen_Generic_binds :: GenericKind -> TyCon -> Type -> Module
                  -> TcM (LHsBinds RdrName, FamInst)
-gen_Generic_binds gk tc mod = do
-  repTyInsts <- tc_mkRepFamInsts gk tc mod
+gen_Generic_binds gk tc inst_ty mod = do
+  repTyInsts <- tc_mkRepFamInsts gk tc inst_ty mod
   return (mkBindsRep gk tc, repTyInsts)
 
 {-
@@ -96,31 +96,31 @@ expressions.
 (Generic T) and (Rep T) are derivable for some type expression T if the
 following constraints are satisfied.
 
-  (a) T = (D v1 ... vn) with free variables v1, v2, ..., vn where n >= 0 v1
-      ... vn are distinct type variables. Cf #5939.
-
-  (b) D is a type constructor *value*. In other words, D is either a type
+  (a) D is a type constructor *value*. In other words, D is either a type
       constructor or it is equivalent to the head of a data family instance (up to
       alpha-renaming).
 
-  (c) D cannot have a "stupid context".
+  (b) D cannot have a "stupid context".
 
-  (d) The right-hand side of D cannot include unboxed types, existential types,
-      or universally quantified types.
+  (c) The right-hand side of D cannot include existential types, universally
+      quantified types, or "exotic" unlifted types. An exotic unlifted type
+      is one which is not listed in the definition of allowedUnliftedTy
+      (i.e., one for which we have no representation type).
+      See Note [Generics and unlifted types]
 
-  (e) T :: *.
+  (d) T :: *.
 
 (Generic1 T) and (Rep1 T) are derivable for some type expression T if the
 following constraints are satisfied.
 
-  (a),(b),(c),(d) As above.
+  (a),(b),(c) As above.
 
-  (f) T must expect arguments, and its last parameter must have kind *.
+  (d) T must expect arguments, and its last parameter must have kind *.
 
       We use `a' to denote the parameter of D that corresponds to the last
       parameter of T.
 
-  (g) For any type-level application (Tfun Targ) in the right-hand side of D
+  (e) For any type-level application (Tfun Targ) in the right-hand side of D
       where the head of Tfun is not a tuple constructor:
 
       (b1) `a' must not occur in Tfun.
@@ -129,51 +129,31 @@ following constraints are satisfied.
 
 -}
 
-canDoGenerics :: DynFlags -> TyCon -> [Type] -> Validity
--- canDoGenerics rep_tc tc_args determines if Generic/Rep can be derived for a
--- type expression (rep_tc tc_arg0 tc_arg1 ... tc_argn).
+canDoGenerics :: TyCon -> Validity
+-- canDoGenerics determines if Generic/Rep can be derived.
 --
--- Check (b) from Note [Requirements for deriving Generic and Rep] is taken
+-- Check (a) from Note [Requirements for deriving Generic and Rep] is taken
 -- care of because canDoGenerics is applied to rep tycons.
 --
 -- It returns Nothing if deriving is possible. It returns (Just reason) if not.
-canDoGenerics dflags tc tc_args
+canDoGenerics tc
   = mergeErrors (
-          -- Check (c) from Note [Requirements for deriving Generic and Rep].
+          -- Check (b) from Note [Requirements for deriving Generic and Rep].
               (if (not (null (tyConStupidTheta tc)))
                 then (NotValid (tc_name <+> text "must not have a datatype context"))
-                else IsValid) :
-          -- Check (a) from Note [Requirements for deriving Generic and Rep].
-          --
-          -- Data family indices can be instantiated; the `tc_args` here are
-          -- the representation tycon args
-          --
-          -- NB: Use user_tc here. In the case of a data *instance*, the
-          -- user_tc is the family tc, which has the right visibility settings.
-          -- (For a normal datatype, user_tc == tc.) Getting this wrong
-          -- led to #11357.
-              (if (all isTyVarTy (filterOutInvisibleTypes user_tc tc_args))
-                then IsValid
-                else NotValid (tc_name <+> text "must not be instantiated;" <+>
-                               text "try deriving `" <> tc_name <+> tc_tys <>
-                               text "' instead"))
+                else IsValid)
           -- See comment below
             : (map bad_con (tyConDataCons tc)))
   where
     -- The tc can be a representation tycon. When we want to display it to the
     -- user (in an error message) we should print its parent
-    (user_tc, tc_name, tc_tys) = case tyConFamInst_maybe tc of
-        Just (ptc, tys) -> (ptc, ppr ptc, hsep (map ppr (filter_kinds $ tys ++ drop (length tys) tc_args)))
-        _               -> (tc, ppr tc, hsep (map ppr (filter_kinds $ mkTyVarTys $ tyConTyVars tc)))
-
-    filter_kinds | gopt Opt_PrintExplicitKinds dflags
-                 = id
-                 | otherwise
-                 = filterOutInvisibleTypes user_tc
+    tc_name = ppr $ case tyConFamInst_maybe tc of
+        Just (ptc, _) -> ptc
+        _             -> tc
 
-        -- Check (d) from Note [Requirements for deriving Generic and Rep].
+        -- Check (c) from Note [Requirements for deriving Generic and Rep].
         --
-        -- If any of the constructors has an unboxed type as argument,
+        -- If any of the constructors has an exotic unlifted type as argument,
         -- then we can't build the embedding-projection pair, because
         -- it relies on instantiating *polymorphic* sum and product types
         -- at the argument types of the constructors
@@ -189,6 +169,10 @@ canDoGenerics dflags tc tc_args
     bad_arg_type ty = (isUnliftedType ty && not (allowedUnliftedTy ty))
                       || not (isTauTy ty)
 
+-- Returns True the Type argument is an unlifted type which has a
+-- corresponding generic representation type. For example,
+-- (allowedUnliftedTy Int#) would return True since there is the UInt
+-- representation type.
 allowedUnliftedTy :: Type -> Bool
 allowedUnliftedTy = isJust . unboxedRepRDRs
 
@@ -232,19 +216,18 @@ explicitly, even though foldDataConArgs is also doing this internally.
 
 -}
 
--- canDoGenerics1 rep_tc tc_args determines if a Generic1/Rep1 can be derived
--- for a type expression (rep_tc tc_arg0 tc_arg1 ... tc_argn).
+-- canDoGenerics1 determines if a Generic1/Rep1 can be derived.
 --
--- Checks (a) through (d) from Note [Requirements for deriving Generic and Rep]
+-- Checks (a) through (c) from Note [Requirements for deriving Generic and Rep]
 -- are taken care of by the call to canDoGenerics.
 --
 -- It returns Nothing if deriving is possible. It returns (Just reason) if not.
-canDoGenerics1 :: DynFlags -> TyCon -> [Type] -> Validity
-canDoGenerics1 dflags rep_tc tc_args =
-  canDoGenerics dflags rep_tc tc_args `andValid` additionalChecks
+canDoGenerics1 :: TyCon -> Validity
+canDoGenerics1 rep_tc =
+  canDoGenerics rep_tc `andValid` additionalChecks
   where
     additionalChecks
-        -- check (f) from Note [Requirements for deriving Generic and Rep]
+        -- check (d) from Note [Requirements for deriving Generic and Rep]
       | null (tyConTyVars rep_tc) = NotValid $
           text "Data type" <+> quotes (ppr rep_tc)
       <+> text "must have some type parameters"
@@ -267,7 +250,8 @@ canDoGenerics1 dflags rep_tc tc_args =
     bmbad con s = CCDG1 True $ NotValid $ bad con s
     bmplus (CCDG1 b1 m1) (CCDG1 b2 m2) = CCDG1 (b1 || b2) (m1 `andValid` m2)
 
-    -- check (g) from Note [degenerate use of FFoldType]
+    -- check (e) from Note [Requirements for deriving Generic and Rep]
+    -- See also Note [degenerate use of FFoldType]
     ft_check :: DataCon -> FFoldType Check_for_CanDoGenerics1
     ft_check con = FT
       { ft_triv = bmzero
@@ -365,9 +349,11 @@ mkBindsRep gk tycon =
 
 tc_mkRepFamInsts :: GenericKind     -- Gen0 or Gen1
                -> TyCon           -- The type to generate representation for
+               -> Type            -- The above TyCon applied to its type
+                                  -- arguments in the generated instance
                -> Module          -- Used as the location of the new RepTy
                -> TcM (FamInst)   -- Generated representation0 coercion
-tc_mkRepFamInsts gk tycon mod =
+tc_mkRepFamInsts gk tycon inst_ty mod =
        -- Consider the example input tycon `D`, where data D a b = D_ a
        -- Also consider `R:DInt`, where { data family D x y :: * -> *
        --                               ; data instance D Int a b = D_ a }
@@ -376,6 +362,16 @@ tc_mkRepFamInsts gk tycon mod =
          Gen0 -> tcLookupTyCon repTyConName
          Gen1 -> tcLookupTyCon rep1TyConName
 
+     ; fam_envs <- tcGetFamInstEnvs
+
+     ; let mbFamInst         = tyConFamInst_maybe tycon
+           -- If we're examining a data family instance, we grab the parent
+           -- TyCon (ptc) and use it to determine the type arguments
+           -- (inst_args) for the data family *instance*'s type variables.
+           ptc               = maybe tycon fst mbFamInst
+           (_, inst_args, _) = tcLookupDataFamInst fam_envs ptc $ snd
+                                 $ tcSplitTyConApp inst_ty
+
      ; let -- `tyvars` = [a,b]
            (tyvars, gk_) = case gk of
              Gen0 -> (all_tyvars, Gen0_)
@@ -383,22 +379,6 @@ tc_mkRepFamInsts gk tycon mod =
                      (init all_tyvars, Gen1_ $ last all_tyvars)
              where all_tyvars = tyConTyVars tycon
 
-           tyvar_args = mkTyVarTys tyvars
-
-           appT :: [Type]
-           appT = case tyConFamInst_maybe tycon of
-                     -- `appT` = D Int a b (data families case)
-                     Just (famtycon, apps) ->
-                       -- `fam` = D
-                       -- `apps` = [Int, a, b]
-                       let allApps = case gk of
-                                       Gen0 -> apps
-                                       Gen1 -> ASSERT(not $ null apps)
-                                               init apps
-                       in [mkTyConApp famtycon allApps]
-                     -- `appT` = D a b (normal case)
-                     Nothing -> [mkTyConApp tycon tyvar_args]
-
        -- `repTy` = D1 ... (C1 ... (S1 ... (Rec0 a))) :: * -> *
      ; repTy <- tc_mkRepTy gk_ tycon
 
@@ -407,7 +387,21 @@ tc_mkRepFamInsts gk tycon mod =
                    in newGlobalBinder mod (mkGen (nameOccName (tyConName tycon)))
                         (nameSrcSpan (tyConName tycon))
 
-     ; let axiom = mkSingleCoAxiom Nominal rep_name tyvars [] fam_tc appT repTy
+       -- We make sure to substitute the tyvars with their user-supplied
+       -- type arguments before generating the Rep/Rep1 instance, since some
+       -- of the tyvars might have been instantiated when deriving.
+       -- See Note [Generating a correctly typed Rep instance].
+     ; let env      = zipTyEnv tyvars inst_args
+           in_scope = mkInScopeSet (tyCoVarsOfType inst_ty)
+           subst    = mkTvSubst in_scope env
+           repTy'   = substTy  subst repTy
+           tcv_set' = tyCoVarsOfType inst_ty
+           (tv_set', cv_set') = partitionVarSet isTyVar tcv_set'
+           tvs'     = varSetElemsWellScoped tv_set'
+           cvs'     = varSetElemsWellScoped cv_set'
+           axiom    = mkSingleCoAxiom Nominal rep_name tvs' cvs'
+                                      fam_tc [inst_ty] repTy'
+
      ; newFamInst SynFamilyInst axiom  }
 
 --------------------------------------------------------------------------------
@@ -835,4 +829,42 @@ data family instance; if so, we generate that instead.
 
 See wiki:Commentary/Compiler/GenericDeriving#Handlingunliftedtypes for more
 details on why URec is implemented the way it is.
+
+Note [Generating a correctly typed Rep instance]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+tc_mkRepTy derives the RHS of the Rep(1) type family instance when deriving
+Generic(1). That is, it derives the ellipsis in the following:
+
+    instance Generic Foo where
+      type Rep Foo = ...
+
+However, tc_mkRepTy only has knowledge of the *TyCon* of the type for which
+a Generic(1) instance is being derived, not the fully instantiated type. As a
+result, tc_mkRepTy builds the most generalized Rep(1) instance possible using
+the type variables it learns from the TyCon (i.e., it uses tyConTyVars). This
+can cause problems when the instance has instantiated type variables
+(see Trac #11732). As an example:
+
+    data T a = MkT a
+    deriving instance Generic (T Int)
+    ==>
+    instance Generic (T Int) where
+      type Rep (T Int) = (... (Rec0 a)) -- wrong!
+
+-XStandaloneDeriving is one way for the type variables to become instantiated.
+Another way is when Generic1 is being derived for a datatype with a visible
+kind binder, e.g.,
+
+   data P k (a :: k) = MkP k deriving Generic1
+   ==>
+   instance Generic1 (P *) where
+     type Rep1 (P *) = (... (Rec0 k)) -- wrong!
+
+See Note [Unify kinds in deriving] in TcDeriv.
+
+In any such scenario, we must prevent a discrepancy between the LHS and RHS of
+a Rep(1) instance. To do so, we create a type variable substitution that maps
+the tyConTyVars of the TyCon to their counterparts in the fully instantiated
+type. (For example, using T above as example, you'd map a :-> Int.) We then
+apply the substitution to the RHS before generating the instance.
 -}
diff --git a/docs/users_guide/8.0.1-notes.rst b/docs/users_guide/8.0.1-notes.rst
index fe77bf42c0..2e22f44e08 100644
--- a/docs/users_guide/8.0.1-notes.rst
+++ b/docs/users_guide/8.0.1-notes.rst
@@ -85,7 +85,7 @@ Language
    kinds, along with kind families and type-level GADTs. Support is still
    experimental, and it is expected to improve over the next several
    releases. See :ref:`type-in-type` for the details.
-   
+
 -  The parser now supports Haddock comments on GADT data constructors.
    For example ::
 
@@ -336,6 +336,13 @@ Compiler
 -  :ghc-flag:`-ddump-strsigs` has been renamed to
    :ghc-flag:`-ddump-str-signatures`.
 
+-  :ghc-flag:`-XDeriveGeneric` is now less picky about instantiating type
+   arguments when deriving (:ghc-ticket:`11732`). As a consequence, the
+   following code is now legal (whereas before it would have been rejected). ::
+
+     data T a b = T a b
+     deriving instance Generic (T Int b)
+
 GHCi
 ~~~~
 
diff --git a/testsuite/tests/deriving/should_compile/T11732a.hs b/testsuite/tests/deriving/should_compile/T11732a.hs
new file mode 100644
index 0000000000..54e1582642
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T11732a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T11732a where
+
+import GHC.Generics
+
+data Proxy k (a :: k) deriving Generic1
+
+data family ProxyFam (a :: y) (b :: z)
+data instance ProxyFam k (a :: k) deriving Generic1
diff --git a/testsuite/tests/deriving/should_compile/T11732b.hs b/testsuite/tests/deriving/should_compile/T11732b.hs
new file mode 100644
index 0000000000..ba71ba5b30
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T11732b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T11732b where
+
+data P1   (a :: k) = MkP1 deriving Functor
+data P2 k (a :: k) = MkP2 deriving Functor
+
+data family P1Fam (x :: y)
+data family P2Fam (x :: y) (z :: w)
+data instance P1Fam   (a :: k) deriving Functor
+data instance P2Fam k (a :: k) deriving Functor
diff --git a/testsuite/tests/deriving/should_compile/T11732c.hs b/testsuite/tests/deriving/should_compile/T11732c.hs
new file mode 100644
index 0000000000..e013383f22
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T11732c.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeInType #-}
+module T11732c where
+
+import Data.Kind
+
+class Cat k (cat :: k -> k -> *) where
+  catId   :: cat a a
+  catComp :: cat b c -> cat a b -> cat a c
+
+instance Cat * (->) where
+  catId   = id
+  catComp = (.)
+
+newtype Fun1 a b = Fun1 (a -> b) deriving (Cat k)
+newtype Fun2 a b = Fun2 (a -> b) deriving (Cat *)
diff --git a/testsuite/tests/deriving/should_compile/T5939.hs b/testsuite/tests/deriving/should_compile/T5939.hs
new file mode 100644
index 0000000000..30eda2c562
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T5939.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+module T5939 where
+
+import GHC.Generics
+
+data T a = T a
+deriving instance Generic (T Bool)
+
+data family TFam a b c
+data instance TFam Int b c
+deriving instance Generic (TFam Int Bool c)
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index e62c50c218..d5401e6e5f 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -27,6 +27,7 @@ test('T4302', normal, compile, [''])
 test('T4325', normal, compile, [''])
 test('T4816', normal, compile, [''])
 test('T4966', normal, compile, [''])
+test('T5939', normal, compile, [''])
 
 test('drv-functor1', normal, compile, [''])
 test('drv-functor2', normal, compile, [''])
@@ -65,3 +66,6 @@ test('T11174', normal, compile, [''])
 test('T11416', normal, compile, [''])
 test('T11396', normal, compile, [''])
 test('T11357', normal, compile, [''])
+test('T11732a', normal, compile, [''])
+test('T11732b', normal, compile, [''])
+test('T11732c', normal, compile, [''])
diff --git a/testsuite/tests/generics/GenCannotDoRep0_0.stderr b/testsuite/tests/generics/GenCannotDoRep0_0.stderr
index e1292b8e7e..be649e0d46 100644
--- a/testsuite/tests/generics/GenCannotDoRep0_0.stderr
+++ b/testsuite/tests/generics/GenCannotDoRep0_0.stderr
@@ -1,24 +1,14 @@
 
-GenCannotDoRep0_0.hs:6:14: Warning:
+GenCannotDoRep0_0.hs:6:14: warning:
     -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
 
-GenCannotDoRep0_0.hs:13:45:
-    Can't make a derived instance of ‘Generic Dynamic’:
-      Constructor ‘Dynamic’ has existentials or constraints in its type
-      Possible fix: use a standalone deriving declaration instead
-    In the data declaration for ‘Dynamic’
+GenCannotDoRep0_0.hs:13:45: error:
+    • Can't make a derived instance of ‘Generic Dynamic’:
+        Constructor ‘Dynamic’ has existentials or constraints in its type
+        Possible fix: use a standalone deriving declaration instead
+    • In the data declaration for ‘Dynamic’
 
-GenCannotDoRep0_0.hs:17:1:
-    Can't make a derived instance of ‘Generic (P Int)’:
-      P must not be instantiated; try deriving `P a' instead
-    In the stand-alone deriving instance for ‘Generic (P Int)’
-
-GenCannotDoRep0_0.hs:26:1:
-    Can't make a derived instance of ‘Generic (D Char Char)’:
-      D must not be instantiated; try deriving `D Char b' instead
-    In the stand-alone deriving instance for ‘Generic (D Char Char)’
-
-GenCannotDoRep0_0.hs:28:1:
-    Can't make a derived instance of ‘Generic (D Int a)’:
-      D must not have a datatype context
-    In the stand-alone deriving instance for ‘Generic (D Int a)’
+GenCannotDoRep0_0.hs:28:1: error:
+    • Can't make a derived instance of ‘Generic (D Int a)’:
+        D must not have a datatype context
+    • In the stand-alone deriving instance for ‘Generic (D Int a)’