From 9c48d8a02dd80bba3bd313bc52add841530e28dc Mon Sep 17 00:00:00 2001
From: RyanGlScott <ryan.gl.scott@gmail.com>
Date: Mon, 11 Apr 2016 02:53:23 +0200
Subject: [PATCH] Deriving Functor-like classes should unify kind variables
While the deriving machinery always unifies the kind of the typeclass
argument with the kind of the datatype, this proves not to be sufficient
to produce well kinded instances for some poly-kinded datatypes. For
example:
```
newtype Compose (f :: k2 -> *) (g :: k1 -> k2) (a :: k1)
= Compose (f (g a)) deriving Functor
```
would fail because only `k1` would get unified with `*`, causing the
following
ill kinded instance to be generated:
```
instance (Functor (f :: k2 -> *), Functor (g :: * -> k2)) =>
Functor (Compose f g) where ...
```
To prevent this, we need to take the subtypes and unify their kinds with
`* -> *`.
Fixes #10524 for good.
Test Plan: ./validate
Reviewers: simonpj, hvr, austin, bgamari
Subscribers: thomie
Differential Revision: https://phabricator.haskell.org/D2097
GHC Trac Issues: #10524, #10561
(cherry picked from commit aadde2b90817c577336da0d4a10ea47551d60c7e)
---
compiler/typecheck/TcDeriv.hs | 156 +++++++++++++-----
libraries/base/Data/Functor/Compose.hs | 7 +-
.../tests/deriving/should_compile/T10561.hs | 14 --
.../deriving/should_compile/T10561.stderr | 7 -
testsuite/tests/deriving/should_compile/all.T | 2 +-
5 files changed, 117 insertions(+), 69 deletions(-)
delete mode 100644 testsuite/tests/deriving/should_compile/T10561.stderr
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 447cffca4d72..9b9a22b283b8 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -7,6 +7,7 @@ Handles @deriving@ clauses on @data@ declarations.
-}
{-# LANGUAGE CPP #-}
+{-# LANGUAGE ImplicitParams #-}
module TcDeriv ( tcDeriving, DerivInfo(..), mkDerivInfos ) where
@@ -66,6 +67,9 @@ import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
import Data.List
+#if __GLASGOW_HASKELL__ > 710
+import GHC.Stack (CallStack)
+#endif
{-
************************************************************************
@@ -134,6 +138,23 @@ mkPredOrigin origin t_or_k pred = PredOrigin pred origin t_or_k
mkThetaOrigin :: CtOrigin -> TypeOrKind -> ThetaType -> ThetaOrigin
mkThetaOrigin origin t_or_k = map (mkPredOrigin origin t_or_k)
+substPredOrigin ::
+-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
+#if __GLASGOW_HASKELL__ > 710
+ (?callStack :: CallStack) =>
+#endif
+ TCvSubst -> PredOrigin -> PredOrigin
+substPredOrigin subst (PredOrigin pred origin t_or_k)
+ = PredOrigin (substTy subst pred) origin t_or_k
+
+substThetaOrigin ::
+-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
+#if __GLASGOW_HASKELL__ > 710
+ (?callStack :: CallStack) =>
+#endif
+ TCvSubst -> ThetaOrigin -> ThetaOrigin
+substThetaOrigin subst = map (substPredOrigin subst)
+
data EarlyDerivSpec = InferTheta (DerivSpec ThetaOrigin)
| GivenTheta (DerivSpec ThetaType)
-- InferTheta ds => the context for the instance should be inferred
@@ -212,6 +233,28 @@ In both cases we produce a bunch of un-simplified constraints
and them simplify them in simplifyInstanceContexts; see
Note [Simplifying the instance context].
+In the functor-like case, we may need to unify some kind variables with * in
+order for the generated instance to be well-kinded. An example from
+Trac #10524:
+
+ newtype Compose (f :: k2 -> *) (g :: k1 -> k2) (a :: k1)
+ = Compose (f (g a)) deriving Functor
+
+Earlier in the deriving pipeline, GHC unifies the kind of Compose f g
+(k1 -> *) with the kind of Functor's argument (* -> *), so k1 := *. But this
+alone isn't enough, since k2 wasn't unified with *:
+
+ instance (Functor (f :: k2 -> *), Functor (g :: * -> k2)) =>
+ Functor (Compose f g) where ...
+
+The two Functor constraints are ill-kinded. To ensure this doesn't happen, we:
+
+ 1. Collect all of a datatype's subtypes which require functor-like
+ constraints.
+ 2. For each subtype, create a substitution by unifying the subtype's kind
+ with (* -> *).
+ 3. Compose all the substitutions into one, then apply that substitution to
+ all of the in-scope type variables and the instance types.
Note [Data decl contexts]
~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -923,12 +966,14 @@ mk_data_eqn overlap_mode tvs cls cls_tys tycon tc_args rep_tc rep_tc_args mtheta
= do loc <- getSrcSpanM
dfun_name <- newDFunName' cls tycon
case mtheta of
- Nothing -> do --Infer context
- inferred_constraints <- inferConstraints cls cls_tys inst_ty rep_tc rep_tc_args
+ Nothing -> -- Infer context
+ inferConstraints tvs cls cls_tys
+ inst_ty rep_tc rep_tc_args
+ $ \inferred_constraints tvs' inst_tys' ->
return $ InferTheta $ DS
{ ds_loc = loc
- , ds_name = dfun_name, ds_tvs = tvs
- , ds_cls = cls, ds_tys = inst_tys
+ , ds_name = dfun_name, ds_tvs = tvs'
+ , ds_cls = cls, ds_tys = inst_tys'
, ds_tc = rep_tc
, ds_theta = inferred_constraints
, ds_overlap = overlap_mode
@@ -948,12 +993,15 @@ mk_data_eqn overlap_mode tvs cls cls_tys tycon tc_args rep_tc rep_tc_args mtheta
----------------------
-inferConstraints :: Class -> [TcType] -> TcType
+inferConstraints :: [TyVar] -> Class -> [TcType] -> TcType
-> TyCon -> [TcType]
- -> TcM ThetaOrigin
+ -> (ThetaOrigin -> [TyVar] -> [TcType] -> TcM a)
+ -> TcM a
-- inferConstraints figures out the constraints needed for the
-- instance declaration generated by a 'deriving' clause on a
--- data type declaration.
+-- data type declaration. It also returns the new in-scope type
+-- variables and instance types, in case they were changed due to
+-- the presence of functor-like constraints.
-- See Note [Inferring the instance context]
-- e.g. inferConstraints
@@ -964,24 +1012,29 @@ inferConstraints :: Class -> [TcType] -> TcType
-- Generate a sufficiently large set of constraints that typechecking the
-- generated method definitions should succeed. This set will be simplified
-- before being used in the instance declaration
-inferConstraints main_cls cls_tys inst_ty rep_tc rep_tc_args
+inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
| main_cls `hasKey` genClassKey -- Generic constraints are easy
- = return []
+ = mkTheta [] tvs inst_tys
| main_cls `hasKey` gen1ClassKey -- Gen1 needs Functor
= ASSERT( length rep_tc_tvs > 0 ) -- See Note [Getting base classes]
ASSERT( null cls_tys )
do { functorClass <- tcLookupClass functorClassName
- ; return (con_arg_constraints (get_gen1_constraints functorClass)) }
+ ; con_arg_constraints (get_gen1_constraints functorClass) mkTheta }
| otherwise -- The others are a bit more complicated
= ASSERT2( equalLength rep_tc_tvs all_rep_tc_args
, ppr main_cls <+> ppr rep_tc
$$ ppr rep_tc_tvs $$ ppr all_rep_tc_args )
- do { traceTc "inferConstraints" (vcat [ppr main_cls <+> ppr inst_tys, ppr arg_constraints])
- ; return (stupid_constraints ++ extra_constraints
- ++ sc_constraints
- ++ arg_constraints) }
+ con_arg_constraints get_std_constrained_tys
+ $ \arg_constraints tvs' inst_tys' ->
+ do { traceTc "inferConstraints" $ vcat
+ [ ppr main_cls <+> ppr inst_tys'
+ , ppr arg_constraints
+ ]
+ ; mkTheta (stupid_constraints ++ extra_constraints
+ ++ sc_constraints ++ arg_constraints)
+ tvs' inst_tys' }
where
tc_binders = tyConBinders rep_tc
choose_level bndr
@@ -990,52 +1043,73 @@ inferConstraints main_cls cls_tys inst_ty rep_tc rep_tc_args
t_or_ks = map choose_level tc_binders ++ repeat TypeLevel
-- want to report *kind* errors when possible
- arg_constraints = con_arg_constraints get_std_constrained_tys
-
-- Constraints arising from the arguments of each constructor
- con_arg_constraints :: (CtOrigin -> TypeOrKind -> Type -> [PredOrigin])
- -> [PredOrigin]
- con_arg_constraints get_arg_constraints
- = [ pred
- | data_con <- tyConDataCons rep_tc
- , (arg_n, arg_t_or_k, arg_ty)
- <- zip3 [1..] t_or_ks $
- dataConInstOrigArgTys data_con all_rep_tc_args
- , not (isUnliftedType arg_ty)
- , let orig = DerivOriginDC data_con arg_n
- , pred <- get_arg_constraints orig arg_t_or_k arg_ty ]
-
+ con_arg_constraints :: (CtOrigin -> TypeOrKind
+ -> Type
+ -> [(ThetaOrigin, Maybe TCvSubst)])
+ -> (ThetaOrigin -> [TyVar] -> [TcType] -> TcM a)
+ -> TcM a
+ con_arg_constraints get_arg_constraints mkTheta
+ = let (predss, mbSubsts) = unzip
+ [ preds_and_mbSubst
+ | data_con <- tyConDataCons rep_tc
+ , (arg_n, arg_t_or_k, arg_ty)
+ <- zip3 [1..] t_or_ks $
+ dataConInstOrigArgTys data_con all_rep_tc_args
-- No constraints for unlifted types
-- See Note [Deriving and unboxed types]
+ , not (isUnliftedType arg_ty)
+ , let orig = DerivOriginDC data_con arg_n
+ , preds_and_mbSubst <- get_arg_constraints orig arg_t_or_k arg_ty
+ ]
+ preds = concat predss
+ -- If the constraints require a subtype to be of kind (* -> *)
+ -- (which is the case for functor-like constraints), then we
+ -- explicitly unify the subtype's kinds with (* -> *).
+ -- See Note [Inferring the instance context]
+ subst = foldl' composeTCvSubst emptyTCvSubst (catMaybes mbSubsts)
+ unmapped_tvs = filter (`notElemTCvSubst` subst) tvs
+ (subst', tvs') = mapAccumL substTyVarBndr subst unmapped_tvs
+ preds' = substThetaOrigin subst' preds
+ inst_tys' = substTys subst' inst_tys
+ in mkTheta preds' tvs' inst_tys'
-- is_functor_like: see Note [Inferring the instance context]
is_functor_like = typeKind inst_ty `tcEqKind` typeToTypeKind
+ get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
+ -> [(ThetaOrigin, Maybe TCvSubst)]
get_gen1_constraints functor_cls orig t_or_k ty
= mk_functor_like_constraints orig t_or_k functor_cls $
get_gen1_constrained_tys last_tv ty
- get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type -> [PredOrigin]
+ get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
+ -> [(ThetaOrigin, Maybe TCvSubst)]
get_std_constrained_tys orig t_or_k ty
| is_functor_like = mk_functor_like_constraints orig t_or_k main_cls $
deepSubtypesContaining last_tv ty
- | otherwise = [mk_cls_pred orig t_or_k main_cls ty]
+ | otherwise = [( [mk_cls_pred orig t_or_k main_cls ty]
+ , Nothing )]
mk_functor_like_constraints :: CtOrigin -> TypeOrKind
- -> Class -> [Type] -> [PredOrigin]
+ -> Class -> [Type]
+ -> [(ThetaOrigin, Maybe TCvSubst)]
-- 'cls' is usually main_cls (Functor or Traversable etc), but if
-- main_cls = Generic1, then 'cls' can be Functor; see get_gen1_constraints
--
- -- For each type, generate two constraints: (cls ty, kind(ty) ~ (*->*))
- -- The second constraint checks that the first is well-kinded.
- -- Lacking that, as Trac #10561 showed, we can just generate an
- -- ill-kinded instance.
- mk_functor_like_constraints orig t_or_k cls tys
- = [ pred_o
- | ty <- tys
- , pred_o <- [ mk_cls_pred orig t_or_k cls ty
- , mkPredOrigin orig KindLevel
- (mkPrimEqPred (typeKind ty) typeToTypeKind) ] ]
+ -- For each type, generate two constraints, [cls ty, kind(ty) ~ (*->*)],
+ -- and a kind substitution that results from unifying kind(ty) with * -> *.
+ -- If the unification is successful, it will ensure that the resulting
+ -- instance is well kinded. If not, the second constraint will result
+ -- in an error message which points out the kind mismatch.
+ -- See Note [Inferring the instance context]
+ mk_functor_like_constraints orig t_or_k cls
+ = map $ \ty -> let ki = typeKind ty in
+ ( [ mk_cls_pred orig t_or_k cls ty
+ , mkPredOrigin orig KindLevel
+ (mkPrimEqPred ki typeToTypeKind) ]
+ , tcUnifyTy ki typeToTypeKind
+ )
rep_tc_tvs = tyConTyVars rep_tc
last_tv = last rep_tc_tvs
diff --git a/libraries/base/Data/Functor/Compose.hs b/libraries/base/Data/Functor/Compose.hs
index 230f4e77def3..d54883682033 100644
--- a/libraries/base/Data/Functor/Compose.hs
+++ b/libraries/base/Data/Functor/Compose.hs
@@ -2,7 +2,6 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Safe #-}
-{-# LANGUAGE StandaloneDeriving #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Functor.Compose
@@ -36,11 +35,7 @@ infixr 9 `Compose`
-- The composition of applicative functors is always applicative,
-- but the composition of monads is not always a monad.
newtype Compose f g a = Compose { getCompose :: f (g a) }
- deriving (Data, Generic)
-
--- We must use standalone deriving here due to a bad interaction between
--- PolyKinds and GHC generics
-deriving instance Functor f => Generic1 (Compose f g)
+ deriving (Data, Generic, Generic1)
-- Instances of lifted Prelude classes
diff --git a/testsuite/tests/deriving/should_compile/T10561.hs b/testsuite/tests/deriving/should_compile/T10561.hs
index 85acc516d9f7..632863270c79 100644
--- a/testsuite/tests/deriving/should_compile/T10561.hs
+++ b/testsuite/tests/deriving/should_compile/T10561.hs
@@ -2,18 +2,4 @@
module T10561 where
--- Ultimately this should "Just Work",
--- but in GHC 7.10 it gave a Lint failure
--- For now (HEAD, Jun 2015) it gives a kind error message,
--- which is better than a crash
-
newtype Compose f g a = Compose (f (g a)) deriving Functor
-
-{-
-instance forall (f_ant :: k_ans -> *)
- (g_anu :: * -> k_ans).
- (Functor f_ant, Functor g_anu) =>
- Functor (Compose f_ant g_anu) where
- fmap f_anv (T10561.Compose a1_anw)
- = Compose (fmap (fmap f_anv) a1_anw)
--}
diff --git a/testsuite/tests/deriving/should_compile/T10561.stderr b/testsuite/tests/deriving/should_compile/T10561.stderr
deleted file mode 100644
index c74967ff43a0..000000000000
--- a/testsuite/tests/deriving/should_compile/T10561.stderr
+++ /dev/null
@@ -1,7 +0,0 @@
-
-T10561.hs:10:52: error:
- • Couldn't match kind ‘k’ with ‘*’
- arising from the first field of ‘Compose’ (type ‘f (g a)’)
- ‘k’ is a rigid type variable bound by
- the deriving clause for ‘Functor (Compose f g)’ at T10561.hs:10:52
- • When deriving the instance for (Functor (Compose f g))
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index d5401e6e5fac..cfbb977abe26 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -56,7 +56,7 @@ test('T9069', normal, compile, [''])
test('T9359', normal, compile, [''])
test('T4896', normal, compile, [''])
test('T7947', extra_clean(['T7947a.o', 'T7947a.hi', 'T7947b.o', 'T7947b.hi']), multimod_compile, ['T7947', '-v0'])
-test('T10561', normal, compile_fail, [''])
+test('T10561', normal, compile, [''])
test('T10487', extra_clean(['T10487_M.o', 'T10487_M.hi']), multimod_compile, ['T10487', '-v0'])
test('T10524', normal, compile, [''])
test('T11148', normal, run_command,
--
GitLab