Deriving Functor-like classes should unify kind variables ghc-8.0.1-rc3
authorRyanGlScott <ryan.gl.scott@gmail.com>
Mon, 11 Apr 2016 00:53:23 +0000 (02:53 +0200)
committerBen Gamari <ben@smart-cactus.org>
Mon, 11 Apr 2016 01:18:11 +0000 (03:18 +0200)
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
libraries/base/Data/Functor/Compose.hs
testsuite/tests/deriving/should_compile/T10561.hs
testsuite/tests/deriving/should_compile/T10561.stderr [deleted file]
testsuite/tests/deriving/should_compile/all.T

index 447cffc..9b9a22b 100644 (file)
@@ -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
index 230f4e7..d548836 100644 (file)
@@ -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
 
index 85acc51..6328632 100644 (file)
@@ -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 (file)
index c74967f..0000000
+++ /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))
index d5401e6..cfbb977 100644 (file)
@@ -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,