Commit 9c48d8a0 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

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 aadde2b9)
parent 7b8beba7
......@@ -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
......
......@@ -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
......
......@@ -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)
-}
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))
......@@ -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,
......
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