Add network submodule.
[ghc.git] / compiler / typecheck / TcDerivInfer.hs
index 109e634..efad80f 100644 (file)
@@ -7,22 +7,26 @@ Functions for inferring (and simplifying) the context for derived instances.
 -}
 
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE MultiWayIf #-}
 
 module TcDerivInfer (inferConstraints, simplifyInstanceContexts) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import Bag
+import BasicTypes
 import Class
 import DataCon
-import DynFlags
+-- import DynFlags
 import ErrUtils
 import Inst
 import Outputable
 import PrelNames
 import TcDerivUtils
 import TcEnv
-import TcErrors (reportAllUnsolved)
+-- import TcErrors (reportAllUnsolved)
 import TcGenFunctor
 import TcGenGenerics
 import TcMType
@@ -35,18 +39,20 @@ import TcValidity (validDerivPred)
 import TcUnify (buildImplicationFor)
 import Unify (tcUnifyTy)
 import Util
+import Var
+import VarEnv
 import VarSet
 
 import Control.Monad
+import Control.Monad.Trans.Class  (lift)
+import Control.Monad.Trans.Reader (ask)
 import Data.List
 import Data.Maybe
 
 ----------------------
 
-inferConstraints :: [TyVar] -> Class -> [TcType] -> TcType
-                 -> TyCon -> [TcType]
-                 -> (ThetaOrigin -> [TyVar] -> [TcType] -> TcM a)
-                 -> TcM a
+inferConstraints :: DerivSpecMechanism
+                 -> DerivM ([ThetaOrigin], [TyVar], [TcType])
 -- inferConstraints figures out the constraints needed for the
 -- instance declaration generated by a 'deriving' clause on a
 -- data type declaration. It also returns the new in-scope type
@@ -62,164 +68,271 @@ inferConstraints :: [TyVar] -> 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 tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
-  | is_generic                        -- Generic constraints are easy
-  = mkTheta [] tvs inst_tys
-
-  | is_generic1                       -- Generic1 needs Functor
-  = ASSERT( length rep_tc_tvs > 0 )   -- See Note [Getting base classes]
-    ASSERT( length cls_tys   == 1 )   -- Generic1 has a single kind variable
-    do { functorClass <- tcLookupClass functorClassName
-       ; 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 )
-    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
-      | isNamedTyConBinder bndr = KindLevel
-      | otherwise               = TypeLevel
-    t_or_ks = map choose_level tc_binders ++ repeat TypeLevel
-       -- want to report *kind* errors when possible
-
-       -- Constraints arising from the arguments of each constructor
-    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
+inferConstraints mechanism
+  = do { DerivEnv { denv_tc          = tc
+                  , denv_tc_args     = tc_args
+                  , denv_cls         = main_cls
+                  , denv_cls_tys     = cls_tys } <- ask
+       ; let is_anyclass = isDerivSpecAnyClass mechanism
+             infer_constraints
+               | is_anyclass = inferConstraintsDAC inst_tys
+               | otherwise   = inferConstraintsDataConArgs inst_ty inst_tys
+
+             inst_ty  = mkTyConApp tc tc_args
+             inst_tys = cls_tys ++ [inst_ty]
+
+             -- Constraints arising from superclasses
+             -- See Note [Superclasses of derived instance]
+             cls_tvs  = classTyVars main_cls
+             sc_constraints = ASSERT2( equalLength cls_tvs inst_tys
+                                     , ppr main_cls <+> ppr inst_tys )
+                              [ mkThetaOrigin DerivOrigin TypeLevel [] [] $
+                                substTheta cls_subst (classSCTheta main_cls) ]
+             cls_subst = ASSERT( equalLength cls_tvs inst_tys )
+                         zipTvSubst cls_tvs inst_tys
+
+       ; (inferred_constraints, tvs', inst_tys') <- infer_constraints
+       ; lift $ traceTc "inferConstraints" $ vcat
+              [ ppr main_cls <+> ppr inst_tys'
+              , ppr inferred_constraints
               ]
-            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 (\v -> v `notElemTCvSubst` subst
-                                      && not (v `isInScope` subst)) tvs
-            (subst', _)  = mapAccumL substTyVarBndr subst unmapped_tvs
-            preds'       = substThetaOrigin subst' preds
-            inst_tys'    = substTys subst' inst_tys
-            tvs'         = tyCoVarsOfTypesWellScoped inst_tys'
-        in mkTheta preds' tvs' inst_tys'
-
-    is_generic  = main_cls `hasKey` genClassKey
-    is_generic1 = main_cls `hasKey` gen1ClassKey
-    -- is_functor_like: see Note [Inferring the instance context]
-    is_functor_like = typeKind inst_ty `tcEqKind` typeToTypeKind
-                   || is_generic1 -- Technically, Generic1 requires a type of
-                                  -- kind (k -> *), not (* -> *), but we still
-                                  -- label it "functor-like" to make sure
-                                  -- all_rep_tc_args has all the necessary type
-                                  -- variables it needs to function.
-
-    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
-                            -> [(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]
-                             , Nothing )]
-
-    mk_functor_like_constraints :: CtOrigin -> TypeOrKind
-                                -> 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) ~ (*->*)],
-    -- 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
-    all_rep_tc_args | is_functor_like = rep_tc_args ++ [mkTyVarTy last_tv]
-                    | otherwise       = rep_tc_args
-
-        -- Constraints arising from superclasses
-        -- See Note [Superclasses of derived instance]
-    cls_tvs  = classTyVars main_cls
-    inst_tys = cls_tys ++ [inst_ty]
-    sc_constraints = ASSERT2( equalLength cls_tvs inst_tys, ppr main_cls <+> ppr rep_tc)
-                     mkThetaOrigin DerivOrigin TypeLevel $
-                     substTheta cls_subst (classSCTheta main_cls)
-    cls_subst = ASSERT( equalLength cls_tvs inst_tys )
-                zipTvSubst cls_tvs inst_tys
-
-        -- Stupid constraints
-    stupid_constraints = mkThetaOrigin DerivOrigin TypeLevel $
-                         substTheta tc_subst (tyConStupidTheta rep_tc)
-    tc_subst = ASSERT( equalLength rep_tc_tvs all_rep_tc_args )
-               zipTvSubst rep_tc_tvs all_rep_tc_args
-
-        -- Extra Data constraints
-        -- The Data class (only) requires that for
-        --    instance (...) => Data (T t1 t2)
-        -- IF   t1:*, t2:*
-        -- THEN (Data t1, Data t2) are among the (...) constraints
-        -- Reason: when the IF holds, we generate a method
-        --             dataCast2 f = gcast2 f
-        --         and we need the Data constraints to typecheck the method
-    extra_constraints
-      | main_cls `hasKey` dataClassKey
-      , all (isLiftedTypeKind . typeKind) rep_tc_args
-      = [ mk_cls_pred DerivOrigin t_or_k main_cls ty
-        | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
-      | otherwise
-      = []
-
-    mk_cls_pred orig t_or_k cls ty   -- Don't forget to apply to cls_tys' too
-       = mkPredOrigin orig t_or_k (mkClassPred cls (cls_tys' ++ [ty]))
-    cls_tys' | is_generic1 = [] -- In the awkward Generic1 case, cls_tys'
-                                -- should be empty, since we are applying the
-                                -- class Functor.
-             | otherwise   = cls_tys
+       ; return ( sc_constraints ++ inferred_constraints
+                , tvs', inst_tys' ) }
+
+-- | Like 'inferConstraints', but used only in the case of deriving strategies
+-- where the constraints are inferred by inspecting the fields of each data
+-- constructor (i.e., stock- and newtype-deriving).
+inferConstraintsDataConArgs :: TcType -> [TcType]
+                            -> DerivM ([ThetaOrigin], [TyVar], [TcType])
+inferConstraintsDataConArgs inst_ty inst_tys
+  = do DerivEnv { denv_tvs         = tvs
+                , denv_rep_tc      = rep_tc
+                , denv_rep_tc_args = rep_tc_args
+                , denv_cls         = main_cls
+                , denv_cls_tys     = cls_tys } <- ask
+
+       let tc_binders = tyConBinders rep_tc
+           choose_level bndr
+             | isNamedTyConBinder bndr = KindLevel
+             | otherwise               = TypeLevel
+           t_or_ks = map choose_level tc_binders ++ repeat TypeLevel
+              -- want to report *kind* errors when possible
+
+              -- Constraints arising from the arguments of each constructor
+           con_arg_constraints
+             :: (CtOrigin -> TypeOrKind
+                          -> Type
+                          -> [([PredOrigin], Maybe TCvSubst)])
+             -> ([ThetaOrigin], [TyVar], [TcType])
+           con_arg_constraints get_arg_constraints
+             = 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 (\v -> v `notElemTCvSubst` subst
+                                             && not (v `isInScope` subst)) tvs
+                   (subst', _)  = mapAccumL substTyVarBndr subst unmapped_tvs
+                   preds'       = map (substPredOrigin subst') preds
+                   inst_tys'    = substTys subst' inst_tys
+                   tvs'         = tyCoVarsOfTypesWellScoped inst_tys'
+               in ([mkThetaOriginFromPreds preds'], tvs', inst_tys')
+
+           is_generic  = main_cls `hasKey` genClassKey
+           is_generic1 = main_cls `hasKey` gen1ClassKey
+           -- is_functor_like: see Note [Inferring the instance context]
+           is_functor_like = typeKind inst_ty `tcEqKind` typeToTypeKind
+                          || is_generic1
+
+           get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
+                                -> [([PredOrigin], 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], 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]
+                  , Nothing )]
+
+           mk_functor_like_constraints :: CtOrigin -> TypeOrKind
+                                       -> Class -> [Type]
+                                       -> [([PredOrigin], 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) ~ (*->*)], 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
+           -- When we first gather up the constraints to solve, most of them
+           -- contain rep_tc_tvs, i.e., the type variables from the derived
+           -- datatype's type constructor. We don't want these type variables
+           -- to appear in the final instance declaration, so we must
+           -- substitute each type variable with its counterpart in the derived
+           -- instance. rep_tc_args lists each of these counterpart types in
+           -- the same order as the type variables.
+           all_rep_tc_args
+             = rep_tc_args ++ map mkTyVarTy
+                                  (drop (length rep_tc_args) rep_tc_tvs)
+
+               -- Stupid constraints
+           stupid_constraints
+             = [ mkThetaOrigin DerivOrigin TypeLevel [] [] $
+                 substTheta tc_subst (tyConStupidTheta rep_tc) ]
+           tc_subst = -- See the comment with all_rep_tc_args for an
+                      -- explanation of this assertion
+                      ASSERT( equalLength rep_tc_tvs all_rep_tc_args )
+                      zipTvSubst rep_tc_tvs all_rep_tc_args
+
+           -- Extra Data constraints
+           -- The Data class (only) requires that for
+           --    instance (...) => Data (T t1 t2)
+           -- IF   t1:*, t2:*
+           -- THEN (Data t1, Data t2) are among the (...) constraints
+           -- Reason: when the IF holds, we generate a method
+           --             dataCast2 f = gcast2 f
+           --         and we need the Data constraints to typecheck the method
+           extra_constraints = [mkThetaOriginFromPreds constrs]
+             where
+               constrs
+                 | main_cls `hasKey` dataClassKey
+                 , all (isLiftedTypeKind . typeKind) rep_tc_args
+                 = [ mk_cls_pred DerivOrigin t_or_k main_cls ty
+                   | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
+                 | otherwise
+                 = []
+
+           mk_cls_pred orig t_or_k cls ty
+                -- Don't forget to apply to cls_tys' too
+              = mkPredOrigin orig t_or_k (mkClassPred cls (cls_tys' ++ [ty]))
+           cls_tys' | is_generic1 = []
+                      -- In the awkward Generic1 case, cls_tys' should be
+                      -- empty, since we are applying the class Functor.
+
+                    | otherwise   = cls_tys
+
+       if    -- Generic constraints are easy
+          |  is_generic
+           -> return ([], tvs, inst_tys)
+
+             -- Generic1 needs Functor
+             -- See Note [Getting base classes]
+          |  is_generic1
+           -> ASSERT( rep_tc_tvs `lengthExceeds` 0 )
+              -- Generic1 has a single kind variable
+              ASSERT( cls_tys `lengthIs` 1 )
+              do { functorClass <- lift $ tcLookupClass functorClassName
+                 ; pure $ con_arg_constraints
+                        $ get_gen1_constraints functorClass }
+
+             -- The others are a bit more complicated
+          |  otherwise
+           -> -- See the comment with all_rep_tc_args for an explanation of
+              -- this assertion
+              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 { let (arg_constraints, tvs', inst_tys')
+                           = con_arg_constraints get_std_constrained_tys
+                   ; lift $ traceTc "inferConstraintsDataConArgs" $ vcat
+                          [ ppr main_cls <+> ppr inst_tys'
+                          , ppr arg_constraints
+                          ]
+                   ; return ( stupid_constraints ++ extra_constraints
+                                                 ++ arg_constraints
+                            , tvs', inst_tys') }
 
 typeToTypeKind :: Kind
 typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
 
-{-
-Note [Inferring the instance context]
+-- | Like 'inferConstraints', but used only in the case of @DeriveAnyClass@,
+-- which gathers its constraints based on the type signatures of the class's
+-- methods instead of the types of the data constructor's field.
+--
+-- See Note [Gathering and simplifying constraints for DeriveAnyClass]
+-- for an explanation of how these constraints are used to determine the
+-- derived instance context.
+inferConstraintsDAC :: [TcType] -> DerivM ([ThetaOrigin], [TyVar], [TcType])
+inferConstraintsDAC inst_tys
+  = do { DerivEnv { denv_tvs = tvs
+                  , denv_cls = cls } <- ask
+
+       ; let gen_dms = [ (sel_id, dm_ty)
+                       | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ]
+
+             cls_tvs = classTyVars cls
+             empty_subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet tvs))
+
+             do_one_meth :: (Id, Type) -> TcM ThetaOrigin
+               -- (Id,Type) are the selector Id and the generic default method type
+               -- NB: the latter is /not/ quantified over the class variables
+               -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
+             do_one_meth (sel_id, gen_dm_ty)
+               = do { let (sel_tvs, _cls_pred, meth_ty)
+                                   = tcSplitMethodTy (varType sel_id)
+                          meth_ty' = substTyWith sel_tvs inst_tys meth_ty
+                          (meth_tvs, meth_theta, meth_tau)
+                                   = tcSplitNestedSigmaTys meth_ty'
+
+                          gen_dm_ty' = substTyWith cls_tvs inst_tys gen_dm_ty
+                          (dm_tvs, dm_theta, dm_tau)
+                                     = tcSplitNestedSigmaTys gen_dm_ty'
+
+                    ; (subst, _meta_tvs) <- pushTcLevelM_ $
+                                            newMetaTyVarsX empty_subst dm_tvs
+                      -- Yuk: the pushTcLevel is to match the one in mk_wanteds
+                      --      simplifyDeriv.  If we don't, the unification
+                      --      variables will bogusly be untouchable.
+
+                    ; let dm_theta' = substTheta subst dm_theta
+                          tau_eq = mkPrimEqPred meth_tau (substTy subst dm_tau)
+                    ; return (mkThetaOrigin DerivOrigin TypeLevel
+                                meth_tvs meth_theta (tau_eq:dm_theta')) }
+
+       ; theta_origins <- lift $ pushTcLevelM_ (mapM do_one_meth gen_dms)
+            -- Yuk: the pushTcLevel is to match the one wrapping the call
+            --      to mk_wanteds in simplifyDeriv.  If we omit this, the
+            --      unification variables will wrongly be untouchable.
+
+       ; return (theta_origins, tvs, inst_tys) }
+
+{- Note [Inferring the instance context]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 There are two sorts of 'deriving':
 
@@ -235,7 +348,7 @@ There are two sorts of 'deriving':
     the instance context is user-supplied
 
 For a deriving clause (InferTheta) we must figure out the
-instance context (inferConstraints). Suppose we are inferring
+instance context (inferConstraintsDataConArgs). Suppose we are inferring
 the instance context for
     C t1 .. tn (T s1 .. sm)
 There are two cases
@@ -314,6 +427,7 @@ Here there *is* no argument field, but we must nevertheless generate
 a context for the Data instances:
         instance Typeable a => Data (T a) where ...
 
+
 ************************************************************************
 *                                                                      *
          Finding the fixed point of deriving equations
@@ -344,7 +458,7 @@ Let's call the context reqd for the T instance of class C at types
         Eq (T a b) = (Ping a, Pong b, ...)
 
 Now we can get a (recursive) equation from the data decl.  This part
-is done by inferConstraints.
+is done by inferConstraintsDataConArgs.
 
         Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
                    u Eq (T b a) u Eq Int        -- From C2
@@ -423,7 +537,8 @@ See also Note [nonDetCmpType nondeterminism]
 -}
 
 
-simplifyInstanceContexts :: [DerivSpec ThetaOrigin] -> TcM [DerivSpec ThetaType]
+simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]]
+                         -> TcM [DerivSpec ThetaType]
 -- Used only for deriving clauses (InferTheta)
 -- not for standalone deriving
 -- See Note [Simplifying the instance context]
@@ -472,7 +587,7 @@ simplifyInstanceContexts infer_specs
        -- See Note [Deterministic simplifyInstanceContexts]
     canSolution = map (sortBy nonDetCmpType)
     ------------------------------------------------------------------
-    gen_soln :: DerivSpec ThetaOrigin -> TcM ThetaType
+    gen_soln :: DerivSpec [ThetaOrigin] -> TcM ThetaType
     gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
                  , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
       = setSrcSpan loc  $
@@ -506,10 +621,10 @@ derivInstCtxt pred
 simplifyDeriv :: PredType -- ^ @C inst_ty@, head of the instance we are
                           -- deriving.  Only used for SkolemInfo.
               -> [TyVar]  -- ^ The tyvars bound by @inst_ty@.
-              -> ThetaOrigin   -- ^ @wanted@ constraints, i.e. @['PredOrigin']@.
+              -> [ThetaOrigin] -- ^ Given and wanted constraints
               -> TcM ThetaType -- ^ Needed constraints (after simplification),
                                -- i.e. @['PredType']@.
-simplifyDeriv pred tvs theta
+simplifyDeriv pred tvs thetas
   = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
                 -- The constraint solving machinery
                 -- expects *TcTyVars* not TyVars.
@@ -519,32 +634,64 @@ simplifyDeriv pred tvs theta
        ; let skol_set  = mkVarSet tvs_skols
              skol_info = DerivSkol pred
              doc = text "deriving" <+> parens (ppr pred)
-             mk_ct (PredOrigin t o t_or_k)
-                 = newWanted o (Just t_or_k) (substTy skol_subst t)
 
-       -- Generate the wanted constraints with the skolemized variables
-       ; (wanted, tclvl) <- pushTcLevelM (mapM mk_ct theta)
+             mk_given_ev :: PredType -> TcM EvVar
+             mk_given_ev given =
+               let given_pred = substTy skol_subst given
+               in newEvVar given_pred
+
+             mk_wanted_ct :: PredOrigin -> TcM CtEvidence
+             mk_wanted_ct (PredOrigin wanted o t_or_k)
+               = newWanted o (Just t_or_k) (substTyUnchecked skol_subst wanted)
+
+             -- Create the implications we need to solve. For stock and newtype
+             -- deriving, these implication constraints will be simple class
+             -- constraints like (C a, Ord b).
+             -- But with DeriveAnyClass, we make an implication constraint.
+             -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
+             mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
+             mk_wanteds (ThetaOrigin { to_tvs            = local_skols
+                                     , to_givens         = givens
+                                     , to_wanted_origins = wanteds })
+               | null local_skols, null givens
+               = do { wanted_cts <- mapM mk_wanted_ct wanteds
+                    ; return (mkSimpleWC wanted_cts) }
+               | otherwise
+               = do { given_evs <- mapM mk_given_ev givens
+                    ; (wanted_cts, tclvl) <- pushTcLevelM $
+                                             mapM mk_wanted_ct wanteds
+                    ; (implic, _) <- buildImplicationFor tclvl skol_info local_skols
+                                                   given_evs (mkSimpleWC wanted_cts)
+                    ; pure (mkImplicWC implic) }
+
+       -- See [STEP DAC BUILD]
+       -- Generate the implication constraints constraints to solve with the
+       -- skolemized variables
+       ; (wanteds, tclvl) <- pushTcLevelM $ mapM mk_wanteds thetas
 
        ; traceTc "simplifyDeriv inputs" $
-         vcat [ pprTyVars tvs $$ ppr theta $$ ppr wanted, doc ]
+         vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
+
+       -- See [STEP DAC SOLVE]
        -- Simplify the constraints
-       ; residual_wanted <- simplifyWantedsTcM wanted
-            -- Result is zonked
+       ; solved_implics <- runTcSDeriveds $ solveWantedsAndDrop
+                                          $ unionsWC wanteds
+       -- It's not yet zonked!  Obviously zonk it before peering at it
+       ; solved_implics <- zonkWC solved_implics
 
+       -- See [STEP DAC HOIST]
        -- Split the resulting constraints into bad and good constraints,
        -- building an @unsolved :: WantedConstraints@ representing all
        -- the constraints we can't just shunt to the predicates.
        -- See Note [Exotic derived instance contexts]
-       ; let residual_simple = wc_simple residual_wanted
+       ; let residual_simple = approximateWC True solved_implics
              (bad, good) = partitionBagWith get_good residual_simple
-             unsolved    = residual_wanted { wc_simple = bad }
-
-                         -- See Note [Exotic derived instance contexts]
 
              get_good :: Ct -> Either Ct PredType
              get_good ct | validDerivPred skol_set p
                          , isWantedCt ct
                          = Right p
+                          -- TODO: This is wrong
                           -- NB re 'isWantedCt': residual_wanted may contain
                           -- unsolved CtDerived and we stick them into the
                           -- bad set so that reportUnsolved may decide what
@@ -556,22 +703,27 @@ simplifyDeriv pred tvs theta
        ; traceTc "simplifyDeriv outputs" $
          vcat [ ppr tvs_skols, ppr residual_simple, ppr good, ppr bad ]
 
-       -- If we are deferring type errors, simply ignore any insoluble
-       -- constraints.  They'll come up again when we typecheck the
-       -- generated instance declaration
-       ; defer <- goptM Opt_DeferTypeErrors
-       ; (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols [] unsolved
-                   -- The buildImplicationFor is just to bind the skolems,
-                   -- in case they are mentioned in error messages
-                   -- See Trac #11347
-       -- Report the (bad) unsolved constraints
-       ; unless defer (reportAllUnsolved (mkImplicWC implic))
-
-
        -- Return the good unsolved constraints (unskolemizing on the way out.)
-       ; let min_theta  = mkMinimalBySCs (bagToList good)
+       ; let min_theta = mkMinimalBySCs id (bagToList good)
+             -- An important property of mkMinimalBySCs (used above) is that in
+             -- addition to removing constraints that are made redundant by
+             -- superclass relationships, it also removes _duplicate_
+             -- constraints.
+             -- See Note [Gathering and simplifying constraints for
+             --           DeriveAnyClass]
              subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs
                           -- The reverse substitution (sigh)
+
+       -- See [STEP DAC RESIDUAL]
+       ; min_theta_vars <- mapM newEvVar min_theta
+       ; (leftover_implic, _) <- buildImplicationFor tclvl skol_info tvs_skols
+                                   min_theta_vars solved_implics
+       -- This call to simplifyTop is purely for error reporting
+       -- See Note [Error reporting for deriving clauses]
+       -- See also Note [Exotic derived instance contexts], which are caught
+       -- in this line of code.
+       ; simplifyTopImplic leftover_implic
+
        ; return (substTheta subst_skol min_theta) }
 
 {-
@@ -600,6 +752,133 @@ BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
              the context for the derived instance.
              Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
 
+Note [Gathering and simplifying constraints for DeriveAnyClass]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+DeriveAnyClass works quite differently from stock and newtype deriving in
+the way it gathers and simplifies constraints to be used in a derived
+instance's context. Stock and newtype deriving gather constraints by looking
+at the data constructors of the data type for which we are deriving an
+instance. But DeriveAnyClass doesn't need to know about a data type's
+definition at all!
+
+To see why, consider this example of DeriveAnyClass:
+
+  class Foo a where
+    bar :: forall b. Ix b => a -> b -> String
+    default bar :: (Show a, Ix c) => a -> c -> String
+    bar x y = show x ++ show (range (y,y))
+
+    baz :: Eq a => a -> a -> Bool
+    default baz :: (Ord a, Show a) => a -> a -> Bool
+    baz x y = compare x y == EQ
+
+Because 'bar' and 'baz' have default signatures, this generates a top-level
+definition for these generic default methods
+
+  $gdm_bar :: forall a. Foo a
+           => forall c. (Show a, Ix c)
+           => a -> c -> String
+  $gdm_bar x y = show x ++ show (range (y,y))
+
+(and similarly for baz).  Now consider a 'deriving' clause
+  data Maybe s = ... deriving Foo
+
+This derives an instance of the form:
+  instance (CX) => Foo (Maybe s) where
+    bar = $gdm_bar
+    baz = $gdm_baz
+
+Now it is GHC's job to fill in a suitable instance context (CX).  If
+GHC were typechecking the binding
+   bar = $gdm bar
+it would
+   * skolemise the expected type of bar
+   * instantiate the type of $dm_bar with meta-type variables
+   * build an implication constraint
+
+[STEP DAC BUILD]
+So that's what we do.  We build the constraint (call it C1)
+
+   forall b. Ix b => (Show (Maybe s), Ix cc,
+                      Maybe s -> b -> String
+                          ~ Maybe s -> cc -> String)
+
+The 'cc' is a unification variable that comes from instantiating
+$dm_bar's type.  The equality constraint comes from marrying up
+the instantiated type of $dm_bar with the specified type of bar.
+Notice that the type variables from the instance, 's' in this case,
+are global to this constraint.
+
+Similarly for 'baz', givng the constraint C2
+
+   forall. Eq (Maybe s) => (Ord a, Show a,
+                            Maybe s -> Maybe s -> Bool
+                                ~ Maybe s -> Maybe s -> Bool)
+
+In this case baz has no local quantification, so the implication
+constraint has no local skolems and there are no unification
+variables.
+
+[STEP DAC SOLVE]
+We can combine these two implication constraints into a single
+constraint (C1, C2), and simplify, unifying cc:=b, to get:
+
+   forall b. Ix b => Show a
+   /\
+   forall. Eq (Maybe s) => (Ord a, Show a)
+
+[STEP DAC HOIST]
+Let's call that (C1', C2').  Now we need to hoist the unsolved
+constraints out of the implications to become our candidate for
+(CX). That is done by approximateWC, which will return:
+
+  (Show a, Ord a, Show a)
+
+Now we can use mkMinimalBySCs to remove superclasses and duplicates, giving
+
+  (Show a, Ord a)
+
+And that's what GHC uses for CX.
+
+[STEP DAC RESIDUAL]
+In this case we have solved all the leftover constraints, but what if
+we don't?  Simple!  We just form the final residual constraint
+
+   forall s. CX => (C1',C2')
+
+and simplify that. In simple cases it'll succeed easily, because CX
+literally contains the constraints in C1', C2', but if there is anything
+more complicated it will be reported in a civilised way.
+
+Note [Error reporting for deriving clauses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A suprisingly tricky aspect of deriving to get right is reporting sensible
+error messages. In particular, if simplifyDeriv reaches a constraint that it
+cannot solve, which might include:
+
+1. Insoluble constraints
+2. "Exotic" constraints (See Note [Exotic derived instance contexts])
+
+Then we report an error immediately in simplifyDeriv.
+
+Another possible choice is to punt and let another part of the typechecker
+(e.g., simplifyInstanceContexts) catch the errors. But this tends to lead
+to worse error messages, so we do it directly in simplifyDeriv.
+
+simplifyDeriv checks for errors in a clever way. If the deriving machinery
+infers the context (Foo a)--that is, if this instance is to be generated:
+
+  instance Foo a => ...
+
+Then we form an implication of the form:
+
+  forall a. Foo a => <residual_wanted_constraints>
+
+And pass it to the simplifier. If the context (Foo a) is enough to discharge
+all the constraints in <residual_wanted_constraints>, then everything is
+hunky-dory. But if <residual_wanted_constraints> contains, say, an insoluble
+constraint, then (Foo a) won't be able to solve it, causing GHC to error.
+
 Note [Exotic derived instance contexts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In a 'derived' instance declaration, we *infer* the context.  It's a