Add network submodule.
[ghc.git] / compiler / typecheck / TcDerivInfer.hs
index 02e9f1f..efad80f 100644 (file)
@@ -7,11 +7,14 @@ 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
@@ -34,22 +37,22 @@ import Type
 import TcSimplify
 import TcValidity (validDerivPred)
 import TcUnify (buildImplicationFor)
-import Unify ( {- tcMatchTy, -} tcUnifyTy)
+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] -> DerivSpecMechanism
-                 -> ([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
@@ -65,172 +68,215 @@ 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
-                 mechanism thing
-  | is_generic && not is_anyclass     -- Generic constraints are easy
-  = thing [mkThetaOriginFromPreds []] tvs inst_tys
-
-  | is_generic1 && not is_anyclass    -- 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) thing }
-
-  | otherwise  -- The others are a bit more complicated
-  = -- 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 )
-    infer_constraints $ \arg_constraints tvs' inst_tys' ->
-      do { traceTc "inferConstraints" $ vcat
-                [ ppr main_cls <+> ppr inst_tys'
-                , ppr arg_constraints
-                ]
-         ; thing (stupid_constraints ++ extra_constraints
-                     ++ sc_constraints ++ arg_constraints)
-                 tvs' inst_tys' }
-  where
-    is_anyclass = isDerivSpecAnyClass mechanism
-    infer_constraints
-      | is_anyclass = inferConstraintsDAC main_cls tvs inst_tys
-      | otherwise   = con_arg_constraints get_std_constrained_tys
-
-    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] -> TcM a)
-                        -> TcM a
-    con_arg_constraints get_arg_constraints thing
-      = 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'       = map (substPredOrigin subst') preds
-            inst_tys'    = substTys subst' inst_tys
-            tvs'         = tyCoVarsOfTypesWellScoped inst_tys'
-        in thing [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]
+       ; 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)]
-    -- '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)
-
-        -- 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 = -- 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
+           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
@@ -242,44 +288,49 @@ typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
 -- for an explanation of how these constraints are used to determine the
 -- derived instance context.
-inferConstraintsDAC :: Class -> [TyVar] -> [TcType]
-                    -> ([ThetaOrigin] -> [TyVar] -> [TcType] -> TcM a)
-                    -> TcM a
-inferConstraintsDAC cls tvs inst_tys thing
-  = do { let gen_dms = [ (sel_id, dm_ty)
+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 ]
 
-       ; (theta_origins, _lvl) <- pushTcLevelM (mapM do_one_meth gen_dms)
+             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.
 
-       ; thing theta_origins tvs inst_tys }
-  where
-    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), _lvl) <- 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')) }
+       ; return (theta_origins, tvs, inst_tys) }
 
 {- Note [Inferring the instance context]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -297,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
@@ -407,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
@@ -595,7 +646,7 @@ simplifyDeriv pred tvs thetas
 
              -- Create the implications we need to solve. For stock and newtype
              -- deriving, these implication constraints will be simple class
-             -- constriants like (C a, Ord b).
+             -- 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
@@ -625,6 +676,8 @@ simplifyDeriv pred tvs thetas
        -- Simplify the constraints
        ; 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,
@@ -651,7 +704,7 @@ simplifyDeriv pred tvs thetas
          vcat [ ppr tvs_skols, ppr residual_simple, ppr good, ppr bad ]
 
        -- 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_
@@ -669,7 +722,7 @@ simplifyDeriv pred tvs thetas
        -- See Note [Error reporting for deriving clauses]
        -- See also Note [Exotic derived instance contexts], which are caught
        -- in this line of code.
-       ; _ <- simplifyTop $ mkImplicWC leftover_implic
+       ; simplifyTopImplic leftover_implic
 
        ; return (substTheta subst_skol min_theta) }
 
@@ -719,8 +772,8 @@ To see why, consider this example of DeriveAnyClass:
     default baz :: (Ord a, Show a) => a -> a -> Bool
     baz x y = compare x y == EQ
 
-Because 'bar' and 'baz' have default signatures, generates a top-level
-definition for thse generic default methods
+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)
@@ -740,14 +793,15 @@ GHC were typechecking the binding
    bar = $gdm bar
 it would
    * skolemise the expected type of bar
-   * instaniate the type of $dm_bar with meta-type varibles
+   * 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)
+                      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
@@ -762,7 +816,7 @@ Similarly for 'baz', givng the constraint C2
                                 ~ 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 unificaiton
+constraint has no local skolems and there are no unification
 variables.
 
 [STEP DAC SOLVE]