[commit: ghc] master: Expand type/kind synonyms in TyVars before deriving-related typechecking (165ae44)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/165ae440b6bbf577eabf0b6d422ed6ea3bf949b4/ghc

>---------------------------------------------------------------

commit 165ae440b6bbf577eabf0b6d422ed6ea3bf949b4
Author: RyanGlScott <ryan.gl.scott at gmail.com>
Date:   Fri Jan 15 17:42:02 2016 +0100

    Expand type/kind synonyms in TyVars before deriving-related typechecking
    
    Before, it was possible to have a datatypes such as
    
    ```
    type ConstantT a b = a
    newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor
    
    data family TFam (f :: * -> *) (a :: *)
    newtype instance TFam f (ConstantT a f) = TFam (f a) deriving Functor
    ```
    
    fail to eta-reduce because either (1) a TyVar had a kind synonym that
    mentioned another TyVar, or (2) an instantiated type was itself a type
    synonym that mentioned another TyVar. A little bit of tweaking to
    `expandTypeSynonyms` and applying it before the eta-reduction check in
    the `deriving` machinery is sufficient to fix this.
    
    Fixes #11416.
    
    Test Plan: ./validate
    
    Reviewers: goldfire, simonpj, austin, bgamari
    
    Reviewed By: simonpj
    
    Subscribers: thomie
    
    Differential Revision: https://phabricator.haskell.org/D1772
    
    GHC Trac Issues: #11416


>---------------------------------------------------------------

165ae440b6bbf577eabf0b6d422ed6ea3bf949b4
 compiler/typecheck/TcDeriv.hs                     | 32 ++++++++++++++++++++++-
 compiler/types/Type.hs                            |  3 +++
 testsuite/tests/deriving/should_compile/T11416.hs | 19 ++++++++++++++
 testsuite/tests/deriving/should_compile/all.T     |  1 +
 4 files changed, 54 insertions(+), 1 deletion(-)

diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index d40aca1..e351f28 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -597,7 +597,11 @@ deriveTyData tvs tc tc_args deriv_pred
               (tc_args_to_keep, args_to_drop)
                               = splitAt n_args_to_keep tc_args
               inst_ty_kind    = typeKind (mkTyConApp tc tc_args_to_keep)
-              dropped_tvs     = tyCoVarsOfTypes args_to_drop
+              -- Use exactTyCoVarsOfTypes, not tyCoVarsOfTypes, so that we
+              -- don't mistakenly grab a type variable mentioned in a type
+              -- synonym that drops it.
+              -- See Note [Eta-reducing type synonyms].
+              dropped_tvs     = exactTyCoVarsOfTypes args_to_drop
 
               -- Match up the kinds, and apply the resulting kind substitution
               -- to the types.  See Note [Unify kinds in deriving]
@@ -701,6 +705,32 @@ When deriving Functor for P, we unify k to *, but we then want
 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.
+
+Note [Eta-reducing type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+One can instantiate a type in a data family instance with a type synonym that
+mentions other type variables:
+
+  type Const a b = a
+  data family Fam (f :: * -> *) (a :: *)
+  newtype instance Fam f (Const a f) = Fam (f a) deriving Functor
+
+With -XTypeInType, it is also possible to define kind synonyms, and they can
+mention other types in a datatype declaration. For example,
+
+  type Const a b = a
+  newtype T f (a :: Const * f) = T (f a) deriving Functor
+
+When deriving, we need to perform eta-reduction analysis to ensure that none of
+the eta-reduced type variables are mentioned elsewhere in the declaration. But
+we need to be careful, because if we don't expand through the Const type
+synonym, we will mistakenly believe that f is an eta-reduced type variable and
+fail to derive Functor, even though the code above is correct (see Trac #11416,
+where this was first noticed).
+
+For this reason, we call exactTyCoVarsOfTypes on the eta-reduced types so that
+we only consider the type variables that remain after expanding through type
+synonyms.
 -}
 
 mkEqnHelp :: Maybe OverlapMode
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index c727da6..3572434 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -314,6 +314,9 @@ expandTypeSynonyms :: Type -> Type
 -- ^ Expand out all type synonyms.  Actually, it'd suffice to expand out
 -- just the ones that discard type variables (e.g.  type Funny a = Int)
 -- But we don't know which those are currently, so we just expand all.
+--
+-- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
+-- not in the kinds of any TyCon or TyVar mentioned in the type.
 expandTypeSynonyms ty
   = go (mkEmptyTCvSubst (mkTyCoInScopeSet [ty] [])) ty
   where
diff --git a/testsuite/tests/deriving/should_compile/T11416.hs b/testsuite/tests/deriving/should_compile/T11416.hs
new file mode 100644
index 0000000..4696306
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T11416.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T11416 where
+
+import Data.Kind
+
+type ConstantT a b = a
+
+newtype T f (a :: ConstantT * f) = T (f a)
+  deriving Functor
+
+data family TFam1 (f :: k1) (a :: k2)
+newtype instance TFam1 f (ConstantT a f) = TFam1 (f a)
+  deriving Functor
+
+data family TFam2 (f :: k1) (a :: k2)
+newtype instance TFam2 f (a :: ConstantT * f) = TFam2 (f a)
+  deriving Functor
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index ff26d37..a18a257 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -61,3 +61,4 @@ test('T10524', normal, compile, [''])
 test('T11148', normal, run_command,
      ['$MAKE -s --no-print-directory T11148'])
 test('T9968', normal, compile, [''])
+test('T11416', normal, compile, [''])