Commit 165ae440 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

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:

GHC Trac Issues: #11416
parent 443bf044
......@@ -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
mkEqnHelp :: Maybe OverlapMode
......@@ -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
{-# 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
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment