never executed always true always false
    1 {-
    2 (c) The University of Glasgow 2006
    3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
    4 
    5 -}
    6 
    7 
    8 {-# LANGUAGE MultiWayIf #-}
    9 
   10 -- | Functions for inferring (and simplifying) the context for derived instances.
   11 module GHC.Tc.Deriv.Infer
   12    ( inferConstraints
   13    , simplifyInstanceContexts
   14    )
   15 where
   16 
   17 import GHC.Prelude
   18 
   19 import GHC.Data.Bag
   20 import GHC.Types.Basic
   21 import GHC.Core.Class
   22 import GHC.Core.DataCon
   23 import GHC.Utils.Error
   24 import GHC.Tc.Utils.Instantiate
   25 import GHC.Utils.Outputable
   26 import GHC.Utils.Panic
   27 import GHC.Utils.Panic.Plain
   28 import GHC.Data.Pair
   29 import GHC.Builtin.Names
   30 import GHC.Tc.Deriv.Utils
   31 import GHC.Tc.Utils.Env
   32 import GHC.Tc.Deriv.Generate
   33 import GHC.Tc.Deriv.Functor
   34 import GHC.Tc.Deriv.Generics
   35 import GHC.Tc.Utils.TcMType
   36 import GHC.Tc.Utils.Monad
   37 import GHC.Tc.Types.Origin
   38 import GHC.Tc.Types.Constraint
   39 import GHC.Core.Predicate
   40 import GHC.Tc.Utils.TcType
   41 import GHC.Core.TyCon
   42 import GHC.Core.TyCo.Ppr (pprTyVars)
   43 import GHC.Core.Type
   44 import GHC.Tc.Solver
   45 import GHC.Tc.Validity (validDerivPred)
   46 import GHC.Tc.Utils.Unify (buildImplicationFor, checkConstraints)
   47 import GHC.Builtin.Types (typeToTypeKind)
   48 import GHC.Core.Unify (tcUnifyTy)
   49 import GHC.Utils.Misc
   50 import GHC.Types.Var
   51 import GHC.Types.Var.Set
   52 
   53 import Control.Monad
   54 import Control.Monad.Trans.Class  (lift)
   55 import Control.Monad.Trans.Reader (ask)
   56 import Data.List                  (sortBy)
   57 import Data.Maybe
   58 
   59 ----------------------
   60 
   61 inferConstraints :: DerivSpecMechanism
   62                  -> DerivM ([ThetaOrigin], [TyVar], [TcType])
   63 -- inferConstraints figures out the constraints needed for the
   64 -- instance declaration generated by a 'deriving' clause on a
   65 -- data type declaration. It also returns the new in-scope type
   66 -- variables and instance types, in case they were changed due to
   67 -- the presence of functor-like constraints.
   68 -- See Note [Inferring the instance context]
   69 
   70 -- e.g. inferConstraints
   71 --        C Int (T [a])    -- Class and inst_tys
   72 --        :RTList a        -- Rep tycon and its arg tys
   73 -- where T [a] ~R :RTList a
   74 --
   75 -- Generate a sufficiently large set of constraints that typechecking the
   76 -- generated method definitions should succeed.   This set will be simplified
   77 -- before being used in the instance declaration
   78 inferConstraints mechanism
   79   = do { DerivEnv { denv_tvs      = tvs
   80                   , denv_cls      = main_cls
   81                   , denv_inst_tys = inst_tys } <- ask
   82        ; wildcard <- isStandaloneWildcardDeriv
   83        ; let infer_constraints :: DerivM ([ThetaOrigin], [TyVar], [TcType])
   84              infer_constraints =
   85                case mechanism of
   86                  DerivSpecStock{dsm_stock_dit = dit}
   87                    -> inferConstraintsStock dit
   88                  DerivSpecAnyClass
   89                    -> infer_constraints_simple inferConstraintsAnyclass
   90                  DerivSpecNewtype { dsm_newtype_dit =
   91                                       DerivInstTys{dit_cls_tys = cls_tys}
   92                                   , dsm_newtype_rep_ty = rep_ty }
   93                    -> infer_constraints_simple $
   94                       inferConstraintsCoerceBased cls_tys rep_ty
   95                  DerivSpecVia { dsm_via_cls_tys = cls_tys
   96                               , dsm_via_ty = via_ty }
   97                    -> infer_constraints_simple $
   98                       inferConstraintsCoerceBased cls_tys via_ty
   99 
  100              -- Most deriving strategies do not need to do anything special to
  101              -- the type variables and arguments to the class in the derived
  102              -- instance, so they can pass through unchanged. The exception to
  103              -- this rule is stock deriving. See
  104              -- Note [Inferring the instance context].
  105              infer_constraints_simple
  106                :: DerivM [ThetaOrigin]
  107                -> DerivM ([ThetaOrigin], [TyVar], [TcType])
  108              infer_constraints_simple infer_thetas = do
  109                thetas <- infer_thetas
  110                pure (thetas, tvs, inst_tys)
  111 
  112              -- Constraints arising from superclasses
  113              -- See Note [Superclasses of derived instance]
  114              cls_tvs  = classTyVars main_cls
  115              sc_constraints = assertPpr (equalLength cls_tvs inst_tys)
  116                                         (ppr main_cls <+> ppr inst_tys)
  117                               [ mkThetaOrigin (mkDerivOrigin wildcard)
  118                                               TypeLevel [] [] [] $
  119                                 substTheta cls_subst (classSCTheta main_cls) ]
  120              cls_subst = assert (equalLength cls_tvs inst_tys) $
  121                          zipTvSubst cls_tvs inst_tys
  122 
  123        ; (inferred_constraints, tvs', inst_tys') <- infer_constraints
  124        ; lift $ traceTc "inferConstraints" $ vcat
  125               [ ppr main_cls <+> ppr inst_tys'
  126               , ppr inferred_constraints
  127               ]
  128        ; return ( sc_constraints ++ inferred_constraints
  129                 , tvs', inst_tys' ) }
  130 
  131 -- | Like 'inferConstraints', but used only in the case of the @stock@ deriving
  132 -- strategy. The constraints are inferred by inspecting the fields of each data
  133 -- constructor. In this example:
  134 --
  135 -- > data Foo = MkFoo Int Char deriving Show
  136 --
  137 -- We would infer the following constraints ('ThetaOrigin's):
  138 --
  139 -- > (Show Int, Show Char)
  140 --
  141 -- Note that this function also returns the type variables ('TyVar's) and
  142 -- class arguments ('TcType's) for the resulting instance. This is because
  143 -- when deriving 'Functor'-like classes, we must sometimes perform kind
  144 -- substitutions to ensure the resulting instance is well kinded, which may
  145 -- affect the type variables and class arguments. In this example:
  146 --
  147 -- > newtype Compose (f :: k -> Type) (g :: Type -> k) (a :: Type) =
  148 -- >   Compose (f (g a)) deriving stock Functor
  149 --
  150 -- We must unify @k@ with @Type@ in order for the resulting 'Functor' instance
  151 -- to be well kinded, so we return @[]@/@[Type, f, g]@ for the
  152 -- 'TyVar's/'TcType's, /not/ @[k]@/@[k, f, g]@.
  153 -- See Note [Inferring the instance context].
  154 inferConstraintsStock :: DerivInstTys
  155                       -> DerivM ([ThetaOrigin], [TyVar], [TcType])
  156 inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
  157                                     , dit_tc          = tc
  158                                     , dit_tc_args     = tc_args
  159                                     , dit_rep_tc      = rep_tc
  160                                     , dit_rep_tc_args = rep_tc_args })
  161   = do DerivEnv { denv_tvs      = tvs
  162                 , denv_cls      = main_cls
  163                 , denv_inst_tys = inst_tys } <- ask
  164        wildcard <- isStandaloneWildcardDeriv
  165 
  166        let inst_ty    = mkTyConApp tc tc_args
  167            tc_binders = tyConBinders rep_tc
  168            choose_level bndr
  169              | isNamedTyConBinder bndr = KindLevel
  170              | otherwise               = TypeLevel
  171            t_or_ks = map choose_level tc_binders ++ repeat TypeLevel
  172               -- want to report *kind* errors when possible
  173 
  174               -- Constraints arising from the arguments of each constructor
  175            con_arg_constraints
  176              :: (CtOrigin -> TypeOrKind
  177                           -> Type
  178                           -> [([PredOrigin], Maybe TCvSubst)])
  179              -> ([ThetaOrigin], [TyVar], [TcType])
  180            con_arg_constraints get_arg_constraints
  181              = let (predss, mbSubsts) = unzip
  182                      [ preds_and_mbSubst
  183                      | data_con <- tyConDataCons rep_tc
  184                      , (arg_n, arg_t_or_k, arg_ty)
  185                          <- zip3 [1..] t_or_ks $
  186                             dataConInstOrigArgTys data_con all_rep_tc_args
  187                        -- No constraints for unlifted types
  188                        -- See Note [Deriving and unboxed types]
  189                      , not (isUnliftedType (irrelevantMult arg_ty))
  190                      , let orig = DerivOriginDC data_con arg_n wildcard
  191                      , preds_and_mbSubst
  192                          <- get_arg_constraints orig arg_t_or_k (irrelevantMult arg_ty)
  193                      ]
  194                    preds = concat predss
  195                    -- If the constraints require a subtype to be of kind
  196                    -- (* -> *) (which is the case for functor-like
  197                    -- constraints), then we explicitly unify the subtype's
  198                    -- kinds with (* -> *).
  199                    -- See Note [Inferring the instance context]
  200                    subst        = foldl' composeTCvSubst
  201                                          emptyTCvSubst (catMaybes mbSubsts)
  202                    unmapped_tvs = filter (\v -> v `notElemTCvSubst` subst
  203                                              && not (v `isInScope` subst)) tvs
  204                    (subst', _)  = substTyVarBndrs subst unmapped_tvs
  205                    preds'       = map (substPredOrigin subst') preds
  206                    inst_tys'    = substTys subst' inst_tys
  207                    tvs'         = tyCoVarsOfTypesWellScoped inst_tys'
  208                in ([mkThetaOriginFromPreds preds'], tvs', inst_tys')
  209 
  210            is_generic  = main_cls `hasKey` genClassKey
  211            is_generic1 = main_cls `hasKey` gen1ClassKey
  212            -- is_functor_like: see Note [Inferring the instance context]
  213            is_functor_like = tcTypeKind inst_ty `tcEqKind` typeToTypeKind
  214                           || is_generic1
  215 
  216            get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
  217                                 -> [([PredOrigin], Maybe TCvSubst)]
  218            get_gen1_constraints functor_cls orig t_or_k ty
  219               = mk_functor_like_constraints orig t_or_k functor_cls $
  220                 get_gen1_constrained_tys last_tv ty
  221 
  222            get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
  223                                    -> [([PredOrigin], Maybe TCvSubst)]
  224            get_std_constrained_tys orig t_or_k ty
  225                | is_functor_like
  226                = mk_functor_like_constraints orig t_or_k main_cls $
  227                  deepSubtypesContaining last_tv ty
  228                | otherwise
  229                = [( [mk_cls_pred orig t_or_k main_cls ty]
  230                   , Nothing )]
  231 
  232            mk_functor_like_constraints :: CtOrigin -> TypeOrKind
  233                                        -> Class -> [Type]
  234                                        -> [([PredOrigin], Maybe TCvSubst)]
  235            -- 'cls' is usually main_cls (Functor or Traversable etc), but if
  236            -- main_cls = Generic1, then 'cls' can be Functor; see
  237            -- get_gen1_constraints
  238            --
  239            -- For each type, generate two constraints,
  240            -- [cls ty, kind(ty) ~ (*->*)], and a kind substitution that results
  241            -- from unifying  kind(ty) with * -> *. If the unification is
  242            -- successful, it will ensure that the resulting instance is well
  243            -- kinded. If not, the second constraint will result in an error
  244            -- message which points out the kind mismatch.
  245            -- See Note [Inferring the instance context]
  246            mk_functor_like_constraints orig t_or_k cls
  247               = map $ \ty -> let ki = tcTypeKind ty in
  248                              ( [ mk_cls_pred orig t_or_k cls ty
  249                                , mkPredOrigin orig KindLevel
  250                                    (mkPrimEqPred ki typeToTypeKind) ]
  251                              , tcUnifyTy ki typeToTypeKind
  252                              )
  253 
  254            rep_tc_tvs      = tyConTyVars rep_tc
  255            last_tv         = last rep_tc_tvs
  256            -- When we first gather up the constraints to solve, most of them
  257            -- contain rep_tc_tvs, i.e., the type variables from the derived
  258            -- datatype's type constructor. We don't want these type variables
  259            -- to appear in the final instance declaration, so we must
  260            -- substitute each type variable with its counterpart in the derived
  261            -- instance. rep_tc_args lists each of these counterpart types in
  262            -- the same order as the type variables.
  263            all_rep_tc_args = tyConInstArgTys rep_tc rep_tc_args
  264 
  265                -- Stupid constraints
  266            stupid_constraints
  267              = [ mkThetaOrigin deriv_origin TypeLevel [] [] [] $
  268                  substTheta tc_subst (tyConStupidTheta rep_tc) ]
  269            tc_subst = -- See the comment with all_rep_tc_args for an
  270                       -- explanation of this assertion
  271                       assert (equalLength rep_tc_tvs all_rep_tc_args) $
  272                       zipTvSubst rep_tc_tvs all_rep_tc_args
  273 
  274            -- Extra Data constraints
  275            -- The Data class (only) requires that for
  276            --    instance (...) => Data (T t1 t2)
  277            -- IF   t1:*, t2:*
  278            -- THEN (Data t1, Data t2) are among the (...) constraints
  279            -- Reason: when the IF holds, we generate a method
  280            --             dataCast2 f = gcast2 f
  281            --         and we need the Data constraints to typecheck the method
  282            extra_constraints = [mkThetaOriginFromPreds constrs]
  283              where
  284                constrs
  285                  | main_cls `hasKey` dataClassKey
  286                  , all (isLiftedTypeKind . tcTypeKind) rep_tc_args
  287                  = [ mk_cls_pred deriv_origin t_or_k main_cls ty
  288                    | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
  289                  | otherwise
  290                  = []
  291 
  292            mk_cls_pred orig t_or_k cls ty
  293                 -- Don't forget to apply to cls_tys' too
  294               = mkPredOrigin orig t_or_k (mkClassPred cls (cls_tys' ++ [ty]))
  295            cls_tys' | is_generic1 = []
  296                       -- In the awkward Generic1 case, cls_tys' should be
  297                       -- empty, since we are applying the class Functor.
  298 
  299                     | otherwise   = cls_tys
  300 
  301            deriv_origin = mkDerivOrigin wildcard
  302 
  303        if    -- Generic constraints are easy
  304           |  is_generic
  305            -> return ([], tvs, inst_tys)
  306 
  307              -- Generic1 needs Functor
  308              -- See Note [Getting base classes]
  309           |  is_generic1
  310            -> assert (rep_tc_tvs `lengthExceeds` 0) $
  311               -- Generic1 has a single kind variable
  312               assert (cls_tys `lengthIs` 1) $
  313               do { functorClass <- lift $ tcLookupClass functorClassName
  314                  ; pure $ con_arg_constraints
  315                         $ get_gen1_constraints functorClass }
  316 
  317              -- The others are a bit more complicated
  318           |  otherwise
  319            -> -- See the comment with all_rep_tc_args for an explanation of
  320               -- this assertion
  321               assertPpr (equalLength rep_tc_tvs all_rep_tc_args)
  322                         ( ppr main_cls <+> ppr rep_tc
  323                           $$ ppr rep_tc_tvs $$ ppr all_rep_tc_args) $
  324                 do { let (arg_constraints, tvs', inst_tys')
  325                            = con_arg_constraints get_std_constrained_tys
  326                    ; lift $ traceTc "inferConstraintsStock" $ vcat
  327                           [ ppr main_cls <+> ppr inst_tys'
  328                           , ppr arg_constraints
  329                           ]
  330                    ; return ( stupid_constraints ++ extra_constraints
  331                                                  ++ arg_constraints
  332                             , tvs', inst_tys') }
  333 
  334 -- | Like 'inferConstraints', but used only in the case of @DeriveAnyClass@,
  335 -- which gathers its constraints based on the type signatures of the class's
  336 -- methods instead of the types of the data constructor's field.
  337 --
  338 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
  339 -- for an explanation of how these constraints are used to determine the
  340 -- derived instance context.
  341 inferConstraintsAnyclass :: DerivM [ThetaOrigin]
  342 inferConstraintsAnyclass
  343   = do { DerivEnv { denv_cls      = cls
  344                   , denv_inst_tys = inst_tys } <- ask
  345        ; wildcard <- isStandaloneWildcardDeriv
  346 
  347        ; let gen_dms = [ (sel_id, dm_ty)
  348                        | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ]
  349 
  350              cls_tvs = classTyVars cls
  351 
  352              do_one_meth :: (Id, Type) -> TcM ThetaOrigin
  353                -- (Id,Type) are the selector Id and the generic default method type
  354                -- NB: the latter is /not/ quantified over the class variables
  355                -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
  356              do_one_meth (sel_id, gen_dm_ty)
  357                = do { let (sel_tvs, _cls_pred, meth_ty)
  358                                    = tcSplitMethodTy (varType sel_id)
  359                           meth_ty' = substTyWith sel_tvs inst_tys meth_ty
  360                           (meth_tvs, meth_theta, meth_tau)
  361                                    = tcSplitNestedSigmaTys meth_ty'
  362 
  363                           gen_dm_ty' = substTyWith cls_tvs inst_tys gen_dm_ty
  364                           (dm_tvs, dm_theta, dm_tau)
  365                                      = tcSplitNestedSigmaTys gen_dm_ty'
  366                           tau_eq     = mkPrimEqPred meth_tau dm_tau
  367                     ; return (mkThetaOrigin (mkDerivOrigin wildcard) TypeLevel
  368                                 meth_tvs dm_tvs meth_theta (tau_eq:dm_theta)) }
  369 
  370        ; lift $ mapM do_one_meth gen_dms }
  371 
  372 -- Like 'inferConstraints', but used only for @GeneralizedNewtypeDeriving@ and
  373 -- @DerivingVia@. Since both strategies generate code involving 'coerce', the
  374 -- inferred constraints set up the scaffolding needed to typecheck those uses
  375 -- of 'coerce'. In this example:
  376 --
  377 -- > newtype Age = MkAge Int deriving newtype Num
  378 --
  379 -- We would infer the following constraints ('ThetaOrigin's):
  380 --
  381 -- > (Num Int, Coercible Age Int)
  382 inferConstraintsCoerceBased :: [Type] -> Type
  383                             -> DerivM [ThetaOrigin]
  384 inferConstraintsCoerceBased cls_tys rep_ty = do
  385   DerivEnv { denv_tvs      = tvs
  386            , denv_cls      = cls
  387            , denv_inst_tys = inst_tys } <- ask
  388   sa_wildcard <- isStandaloneWildcardDeriv
  389   let -- The following functions are polymorphic over the representation
  390       -- type, since we might either give it the underlying type of a
  391       -- newtype (for GeneralizedNewtypeDeriving) or a @via@ type
  392       -- (for DerivingVia).
  393       rep_tys ty  = cls_tys ++ [ty]
  394       rep_pred ty = mkClassPred cls (rep_tys ty)
  395       rep_pred_o ty = mkPredOrigin deriv_origin TypeLevel (rep_pred ty)
  396               -- rep_pred is the representation dictionary, from where
  397               -- we are going to get all the methods for the final
  398               -- dictionary
  399       deriv_origin = mkDerivOrigin sa_wildcard
  400 
  401       -- Next we collect constraints for the class methods
  402       -- If there are no methods, we don't need any constraints
  403       -- Otherwise we need (C rep_ty), for the representation methods,
  404       -- and constraints to coerce each individual method
  405       meth_preds :: Type -> [PredOrigin]
  406       meth_preds ty
  407         | null meths = [] -- No methods => no constraints
  408                           -- (#12814)
  409         | otherwise = rep_pred_o ty : coercible_constraints ty
  410       meths = classMethods cls
  411       coercible_constraints ty
  412         = [ mkPredOrigin (DerivOriginCoerce meth t1 t2 sa_wildcard)
  413                          TypeLevel (mkReprPrimEqPred t1 t2)
  414           | meth <- meths
  415           , let (Pair t1 t2) = mkCoerceClassMethEqn cls tvs
  416                                        inst_tys ty meth ]
  417 
  418       all_thetas :: Type -> [ThetaOrigin]
  419       all_thetas ty = [mkThetaOriginFromPreds $ meth_preds ty]
  420 
  421   pure (all_thetas rep_ty)
  422 
  423 {- Note [Inferring the instance context]
  424 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  425 There are two sorts of 'deriving', as represented by the two constructors
  426 for DerivContext:
  427 
  428   * InferContext mb_wildcard: This can either be:
  429     - The deriving clause for a data type.
  430         (e.g, data T a = T1 a deriving( Eq ))
  431       In this case, mb_wildcard = Nothing.
  432     - A standalone declaration with an extra-constraints wildcard
  433         (e.g., deriving instance _ => Eq (Foo a))
  434       In this case, mb_wildcard = Just loc, where loc is the location
  435       of the extra-constraints wildcard.
  436 
  437     Here we must infer an instance context,
  438     and generate instance declaration
  439       instance Eq a => Eq (T a) where ...
  440 
  441   * SupplyContext theta: standalone deriving
  442       deriving instance Eq a => Eq (T a)
  443     Here we only need to fill in the bindings;
  444     the instance context (theta) is user-supplied
  445 
  446 For the InferContext case, we must figure out the
  447 instance context (inferConstraintsStock). Suppose we are inferring
  448 the instance context for
  449     C t1 .. tn (T s1 .. sm)
  450 There are two cases
  451 
  452   * (T s1 .. sm) :: *         (the normal case)
  453     Then we behave like Eq and guess (C t1 .. tn t)
  454     for each data constructor arg of type t.  More
  455     details below.
  456 
  457   * (T s1 .. sm) :: * -> *    (the functor-like case)
  458     Then we behave like Functor.
  459 
  460 In both cases we produce a bunch of un-simplified constraints
  461 and them simplify them in simplifyInstanceContexts; see
  462 Note [Simplifying the instance context].
  463 
  464 In the functor-like case, we may need to unify some kind variables with * in
  465 order for the generated instance to be well-kinded. An example from #10524:
  466 
  467   newtype Compose (f :: k2 -> *) (g :: k1 -> k2) (a :: k1)
  468     = Compose (f (g a)) deriving Functor
  469 
  470 Earlier in the deriving pipeline, GHC unifies the kind of Compose f g
  471 (k1 -> *) with the kind of Functor's argument (* -> *), so k1 := *. But this
  472 alone isn't enough, since k2 wasn't unified with *:
  473 
  474   instance (Functor (f :: k2 -> *), Functor (g :: * -> k2)) =>
  475     Functor (Compose f g) where ...
  476 
  477 The two Functor constraints are ill-kinded. To ensure this doesn't happen, we:
  478 
  479   1. Collect all of a datatype's subtypes which require functor-like
  480      constraints.
  481   2. For each subtype, create a substitution by unifying the subtype's kind
  482      with (* -> *).
  483   3. Compose all the substitutions into one, then apply that substitution to
  484      all of the in-scope type variables and the instance types.
  485 
  486 Note [Getting base classes]
  487 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  488 Functor and Typeable are defined in package 'base', and that is not available
  489 when compiling 'ghc-prim'.  So we must be careful that 'deriving' for stuff in
  490 ghc-prim does not use Functor or Typeable implicitly via these lookups.
  491 
  492 Note [Deriving and unboxed types]
  493 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  494 We have some special hacks to support things like
  495    data T = MkT Int# deriving ( Show )
  496 
  497 Specifically, we use GHC.Tc.Deriv.Generate.box to box the Int# into an Int
  498 (which we know how to show), and append a '#'. Parentheses are not required
  499 for unboxed values (`MkT -3#` is a valid expression).
  500 
  501 Note [Superclasses of derived instance]
  502 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  503 In general, a derived instance decl needs the superclasses of the derived
  504 class too.  So if we have
  505         data T a = ...deriving( Ord )
  506 then the initial context for Ord (T a) should include Eq (T a).  Often this is
  507 redundant; we'll also generate an Ord constraint for each constructor argument,
  508 and that will probably generate enough constraints to make the Eq (T a) constraint
  509 be satisfied too.  But not always; consider:
  510 
  511  data S a = S
  512  instance Eq (S a)
  513  instance Ord (S a)
  514 
  515  data T a = MkT (S a) deriving( Ord )
  516  instance Num a => Eq (T a)
  517 
  518 The derived instance for (Ord (T a)) must have a (Num a) constraint!
  519 Similarly consider:
  520         data T a = MkT deriving( Data )
  521 Here there *is* no argument field, but we must nevertheless generate
  522 a context for the Data instances:
  523         instance Typeable a => Data (T a) where ...
  524 
  525 
  526 ************************************************************************
  527 *                                                                      *
  528          Finding the fixed point of deriving equations
  529 *                                                                      *
  530 ************************************************************************
  531 
  532 Note [Simplifying the instance context]
  533 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  534 Consider
  535 
  536         data T a b = C1 (Foo a) (Bar b)
  537                    | C2 Int (T b a)
  538                    | C3 (T a a)
  539                    deriving (Eq)
  540 
  541 We want to come up with an instance declaration of the form
  542 
  543         instance (Ping a, Pong b, ...) => Eq (T a b) where
  544                 x == y = ...
  545 
  546 It is pretty easy, albeit tedious, to fill in the code "...".  The
  547 trick is to figure out what the context for the instance decl is,
  548 namely Ping, Pong and friends.
  549 
  550 Let's call the context reqd for the T instance of class C at types
  551 (a,b, ...)  C (T a b).  Thus:
  552 
  553         Eq (T a b) = (Ping a, Pong b, ...)
  554 
  555 Now we can get a (recursive) equation from the data decl.  This part
  556 is done by inferConstraintsStock.
  557 
  558         Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
  559                    u Eq (T b a) u Eq Int        -- From C2
  560                    u Eq (T a a)                 -- From C3
  561 
  562 
  563 Foo and Bar may have explicit instances for Eq, in which case we can
  564 just substitute for them.  Alternatively, either or both may have
  565 their Eq instances given by deriving clauses, in which case they
  566 form part of the system of equations.
  567 
  568 Now all we need do is simplify and solve the equations, iterating to
  569 find the least fixpoint.  This is done by simplifyInstanceConstraints.
  570 Notice that the order of the arguments can
  571 switch around, as here in the recursive calls to T.
  572 
  573 Let's suppose Eq (Foo a) = Eq a, and Eq (Bar b) = Ping b.
  574 
  575 We start with:
  576 
  577         Eq (T a b) = {}         -- The empty set
  578 
  579 Next iteration:
  580         Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
  581                    u Eq (T b a) u Eq Int        -- From C2
  582                    u Eq (T a a)                 -- From C3
  583 
  584         After simplification:
  585                    = Eq a u Ping b u {} u {} u {}
  586                    = Eq a u Ping b
  587 
  588 Next iteration:
  589 
  590         Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
  591                    u Eq (T b a) u Eq Int        -- From C2
  592                    u Eq (T a a)                 -- From C3
  593 
  594         After simplification:
  595                    = Eq a u Ping b
  596                    u (Eq b u Ping a)
  597                    u (Eq a u Ping a)
  598 
  599                    = Eq a u Ping b u Eq b u Ping a
  600 
  601 The next iteration gives the same result, so this is the fixpoint.  We
  602 need to make a canonical form of the RHS to ensure convergence.  We do
  603 this by simplifying the RHS to a form in which
  604 
  605         - the classes constrain only tyvars
  606         - the list is sorted by tyvar (major key) and then class (minor key)
  607         - no duplicates, of course
  608 
  609 Note [Deterministic simplifyInstanceContexts]
  610 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  611 Canonicalisation uses nonDetCmpType which is nondeterministic. Sorting
  612 with nonDetCmpType puts the returned lists in a nondeterministic order.
  613 If we were to return them, we'd get class constraints in
  614 nondeterministic order.
  615 
  616 Consider:
  617 
  618   data ADT a b = Z a b deriving Eq
  619 
  620 The generated code could be either:
  621 
  622   instance (Eq a, Eq b) => Eq (Z a b) where
  623 
  624 Or:
  625 
  626   instance (Eq b, Eq a) => Eq (Z a b) where
  627 
  628 To prevent the order from being nondeterministic we only
  629 canonicalize when comparing and return them in the same order as
  630 simplifyDeriv returned them.
  631 See also Note [nonDetCmpType nondeterminism]
  632 -}
  633 
  634 
  635 simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]]
  636                          -> TcM [DerivSpec ThetaType]
  637 -- Used only for deriving clauses or standalone deriving with an
  638 -- extra-constraints wildcard (InferContext)
  639 -- See Note [Simplifying the instance context]
  640 
  641 simplifyInstanceContexts [] = return []
  642 
  643 simplifyInstanceContexts infer_specs
  644   = do  { traceTc "simplifyInstanceContexts" $ vcat (map pprDerivSpec infer_specs)
  645         ; iterate_deriv 1 initial_solutions }
  646   where
  647     ------------------------------------------------------------------
  648         -- The initial solutions for the equations claim that each
  649         -- instance has an empty context; this solution is certainly
  650         -- in canonical form.
  651     initial_solutions :: [ThetaType]
  652     initial_solutions = [ [] | _ <- infer_specs ]
  653 
  654     ------------------------------------------------------------------
  655         -- iterate_deriv calculates the next batch of solutions,
  656         -- compares it with the current one; finishes if they are the
  657         -- same, otherwise recurses with the new solutions.
  658         -- It fails if any iteration fails
  659     iterate_deriv :: Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
  660     iterate_deriv n current_solns
  661       | n > 20  -- Looks as if we are in an infinite loop
  662                 -- This can happen if we have -XUndecidableInstances
  663                 -- (See GHC.Tc.Solver.tcSimplifyDeriv.)
  664       = pprPanic "solveDerivEqns: probable loop"
  665                  (vcat (map pprDerivSpec infer_specs) $$ ppr current_solns)
  666       | otherwise
  667       = do {      -- Extend the inst info from the explicit instance decls
  668                   -- with the current set of solutions, and simplify each RHS
  669              inst_specs <- zipWithM newDerivClsInst current_solns infer_specs
  670            ; new_solns <- checkNoErrs $
  671                           extendLocalInstEnv inst_specs $
  672                           mapM gen_soln infer_specs
  673 
  674            ; if (current_solns `eqSolution` new_solns) then
  675                 return [ spec { ds_theta = soln }
  676                        | (spec, soln) <- zip infer_specs current_solns ]
  677              else
  678                 iterate_deriv (n+1) new_solns }
  679 
  680     eqSolution a b = eqListBy (eqListBy eqType) (canSolution a) (canSolution b)
  681        -- Canonicalise for comparison
  682        -- See Note [Deterministic simplifyInstanceContexts]
  683     canSolution = map (sortBy nonDetCmpType)
  684     ------------------------------------------------------------------
  685     gen_soln :: DerivSpec [ThetaOrigin] -> TcM ThetaType
  686     gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
  687                  , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
  688       = setSrcSpan loc  $
  689         addErrCtxt (derivInstCtxt the_pred) $
  690         do { theta <- simplifyDeriv the_pred tyvars deriv_rhs
  691                 -- checkValidInstance tyvars theta clas inst_tys
  692                 -- Not necessary; see Note [Exotic derived instance contexts]
  693 
  694            ; traceTc "GHC.Tc.Deriv" (ppr deriv_rhs $$ ppr theta)
  695                 -- Claim: the result instance declaration is guaranteed valid
  696                 -- Hence no need to call:
  697                 --   checkValidInstance tyvars theta clas inst_tys
  698            ; return theta }
  699       where
  700         the_pred = mkClassPred clas inst_tys
  701 
  702 derivInstCtxt :: PredType -> SDoc
  703 derivInstCtxt pred
  704   = text "When deriving the instance for" <+> parens (ppr pred)
  705 
  706 {-
  707 ***********************************************************************************
  708 *                                                                                 *
  709 *            Simplify derived constraints
  710 *                                                                                 *
  711 ***********************************************************************************
  712 -}
  713 
  714 -- | Given @instance (wanted) => C inst_ty@, simplify 'wanted' as much
  715 -- as possible. Fail if not possible.
  716 simplifyDeriv :: PredType -- ^ @C inst_ty@, head of the instance we are
  717                           -- deriving.  Only used for SkolemInfo.
  718               -> [TyVar]  -- ^ The tyvars bound by @inst_ty@.
  719               -> [ThetaOrigin] -- ^ Given and wanted constraints
  720               -> TcM ThetaType -- ^ Needed constraints (after simplification),
  721                                -- i.e. @['PredType']@.
  722 simplifyDeriv pred tvs thetas
  723   = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
  724                 -- The constraint solving machinery
  725                 -- expects *TcTyVars* not TyVars.
  726                 -- We use *non-overlappable* (vanilla) skolems
  727                 -- See Note [Overlap and deriving]
  728 
  729        ; let skol_set  = mkVarSet tvs_skols
  730              skol_info = DerivSkol pred
  731              doc = text "deriving" <+> parens (ppr pred)
  732 
  733              mk_given_ev :: PredType -> TcM EvVar
  734              mk_given_ev given =
  735                let given_pred = substTy skol_subst given
  736                in newEvVar given_pred
  737 
  738              emit_wanted_constraints :: [TyVar] -> [PredOrigin] -> TcM ()
  739              emit_wanted_constraints metas_to_be preds
  740                = do { -- We instantiate metas_to_be with fresh meta type
  741                       -- variables. Currently, these can only be type variables
  742                       -- quantified in generic default type signatures.
  743                       -- See Note [Gathering and simplifying constraints for
  744                       -- DeriveAnyClass]
  745                       (meta_subst, _meta_tvs) <- newMetaTyVars metas_to_be
  746 
  747                     -- Now make a constraint for each of the instantiated predicates
  748                     ; let wanted_subst = skol_subst `unionTCvSubst` meta_subst
  749                           mk_wanted_ct (PredOrigin wanted orig t_or_k)
  750                             = do { ev <- newWanted orig (Just t_or_k) $
  751                                          substTyUnchecked wanted_subst wanted
  752                                  ; return (mkNonCanonical ev) }
  753                     ; cts <- mapM mk_wanted_ct preds
  754 
  755                     -- And emit them into the monad
  756                     ; emitSimples (listToCts cts) }
  757 
  758              -- Create the implications we need to solve. For stock and newtype
  759              -- deriving, these implication constraints will be simple class
  760              -- constraints like (C a, Ord b).
  761              -- But with DeriveAnyClass, we make an implication constraint.
  762              -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
  763              mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
  764              mk_wanteds (ThetaOrigin { to_anyclass_skols  = ac_skols
  765                                      , to_anyclass_metas  = ac_metas
  766                                      , to_anyclass_givens = ac_givens
  767                                      , to_wanted_origins  = preds })
  768                = do { ac_given_evs <- mapM mk_given_ev ac_givens
  769                     ; (_, wanteds)
  770                         <- captureConstraints $
  771                            checkConstraints skol_info ac_skols ac_given_evs $
  772                               -- The checkConstraints bumps the TcLevel, and
  773                               -- wraps the wanted constraints in an implication,
  774                               -- when (but only when) necessary
  775                            emit_wanted_constraints ac_metas preds
  776                     ; pure wanteds }
  777 
  778        -- See [STEP DAC BUILD]
  779        -- Generate the implication constraints, one for each method, to solve
  780        -- with the skolemized variables.  Start "one level down" because
  781        -- we are going to wrap the result in an implication with tvs_skols,
  782        -- in step [DAC RESIDUAL]
  783        ; (tc_lvl, wanteds) <- pushTcLevelM $
  784                               mapM mk_wanteds thetas
  785 
  786        ; traceTc "simplifyDeriv inputs" $
  787          vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
  788 
  789        -- See [STEP DAC SOLVE]
  790        -- Simplify the constraints, starting at the same level at which
  791        -- they are generated (c.f. the call to runTcSWithEvBinds in
  792        -- simplifyInfer)
  793        ; solved_wanteds <- setTcLevel tc_lvl   $
  794                            runTcSDeriveds      $
  795                            solveWantedsAndDrop $
  796                            unionsWC wanteds
  797 
  798        -- It's not yet zonked!  Obviously zonk it before peering at it
  799        ; solved_wanteds <- zonkWC solved_wanteds
  800 
  801        -- See [STEP DAC HOIST]
  802        -- From the simplified constraints extract a subset 'good' that will
  803        -- become the context 'min_theta' for the derived instance.
  804        ; let residual_simple = approximateWC True solved_wanteds
  805              good = mapMaybeBag get_good residual_simple
  806 
  807              -- Returns @Just p@ (where @p@ is the type of the Ct) if a Ct is
  808              -- suitable to be inferred in the context of a derived instance.
  809              -- Returns @Nothing@ if the Ct is too exotic.
  810              -- See Note [Exotic derived instance contexts] for what
  811              -- constitutes an exotic constraint.
  812              get_good :: Ct -> Maybe PredType
  813              get_good ct | validDerivPred skol_set p
  814                          , isWantedCt ct
  815                          = Just p
  816                           -- TODO: This is wrong
  817                           -- NB re 'isWantedCt': residual_wanted may contain
  818                           -- unsolved CtDerived and we stick them into the
  819                           -- bad set so that reportUnsolved may decide what
  820                           -- to do with them
  821                          | otherwise
  822                          = Nothing
  823                            where p = ctPred ct
  824 
  825        ; traceTc "simplifyDeriv outputs" $
  826          vcat [ ppr tvs_skols, ppr residual_simple, ppr good ]
  827 
  828        -- Return the good unsolved constraints (unskolemizing on the way out.)
  829        ; let min_theta = mkMinimalBySCs id (bagToList good)
  830              -- An important property of mkMinimalBySCs (used above) is that in
  831              -- addition to removing constraints that are made redundant by
  832              -- superclass relationships, it also removes _duplicate_
  833              -- constraints.
  834              -- See Note [Gathering and simplifying constraints for
  835              --           DeriveAnyClass]
  836              subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs
  837                           -- The reverse substitution (sigh)
  838 
  839        -- See [STEP DAC RESIDUAL]
  840        -- Ensure that min_theta is enough to solve /all/ the constraints in
  841        -- solved_wanteds, by solving the implication constraint
  842        --
  843        --    forall tvs. min_theta => solved_wanteds
  844        ; min_theta_vars <- mapM newEvVar min_theta
  845        ; (leftover_implic, _)
  846            <- buildImplicationFor tc_lvl skol_info tvs_skols
  847                                   min_theta_vars solved_wanteds
  848        -- This call to simplifyTop is purely for error reporting
  849        -- See Note [Error reporting for deriving clauses]
  850        -- See also Note [Exotic derived instance contexts], which are caught
  851        -- in this line of code.
  852        ; simplifyTopImplic leftover_implic
  853 
  854        ; return (substTheta subst_skol min_theta) }
  855 
  856 {-
  857 Note [Overlap and deriving]
  858 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
  859 Consider some overlapping instances:
  860   instance Show a => Show [a] where ..
  861   instance Show [Char] where ...
  862 
  863 Now a data type with deriving:
  864   data T a = MkT [a] deriving( Show )
  865 
  866 We want to get the derived instance
  867   instance Show [a] => Show (T a) where...
  868 and NOT
  869   instance Show a => Show (T a) where...
  870 so that the (Show (T Char)) instance does the Right Thing
  871 
  872 It's very like the situation when we're inferring the type
  873 of a function
  874    f x = show [x]
  875 and we want to infer
  876    f :: Show [a] => a -> String
  877 
  878 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
  879              the context for the derived instance.
  880              Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
  881 
  882 Note [Gathering and simplifying constraints for DeriveAnyClass]
  883 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  884 DeriveAnyClass works quite differently from stock and newtype deriving in
  885 the way it gathers and simplifies constraints to be used in a derived
  886 instance's context. Stock and newtype deriving gather constraints by looking
  887 at the data constructors of the data type for which we are deriving an
  888 instance. But DeriveAnyClass doesn't need to know about a data type's
  889 definition at all!
  890 
  891 To see why, consider this example of DeriveAnyClass:
  892 
  893   class Foo a where
  894     bar :: forall b. Ix b => a -> b -> String
  895     default bar :: (Show a, Ix c) => a -> c -> String
  896     bar x y = show x ++ show (range (y,y))
  897 
  898     baz :: Eq a => a -> a -> Bool
  899     default baz :: (Ord a, Show a) => a -> a -> Bool
  900     baz x y = compare x y == EQ
  901 
  902 Because 'bar' and 'baz' have default signatures, this generates a top-level
  903 definition for these generic default methods
  904 
  905   $gdm_bar :: forall a. Foo a
  906            => forall c. (Show a, Ix c)
  907            => a -> c -> String
  908   $gdm_bar x y = show x ++ show (range (y,y))
  909 
  910 (and similarly for baz).  Now consider a 'deriving' clause
  911   data Maybe s = ... deriving Foo
  912 
  913 This derives an instance of the form:
  914   instance (CX) => Foo (Maybe s) where
  915     bar = $gdm_bar
  916     baz = $gdm_baz
  917 
  918 Now it is GHC's job to fill in a suitable instance context (CX).  If
  919 GHC were typechecking the binding
  920    bar = $gdm bar
  921 it would
  922    * skolemise the expected type of bar
  923    * instantiate the type of $gdm_bar with meta-type variables
  924    * build an implication constraint
  925 
  926 [STEP DAC BUILD]
  927 So that's what we do.  We build the constraint (call it C1)
  928 
  929    forall[2] b. Ix b => (Show (Maybe s), Ix cc,
  930                         Maybe s -> b -> String
  931                             ~ Maybe s -> cc -> String)
  932 
  933 Here:
  934 * The level of this forall constraint is forall[2], because we are later
  935   going to wrap it in a forall[1] in [STEP DAC RESIDUAL]
  936 
  937 * The 'b' comes from the quantified type variable in the expected type
  938   of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
  939   variable that comes from instantiating the quantified type variable 'c' in
  940   $gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
  941 
  942 * The (Ix b) constraint comes from the context of bar's type
  943   (i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
  944   constraints come from the context of $gdm_bar's type
  945   (i.e., 'to_anyclass_givens' in 'ThetaOrigin').
  946 
  947 * The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
  948   comes from marrying up the instantiated type of $gdm_bar with the specified
  949   type of bar. Notice that the type variables from the instance, 's' in this
  950   case, are global to this constraint.
  951 
  952 Note that it is vital that we instantiate the `c` in $gdm_bar's type with a new
  953 unification variable for each iteration of simplifyDeriv. If we re-use the same
  954 unification variable across multiple iterations, then bad things can happen,
  955 such as #14933.
  956 
  957 Similarly for 'baz', giving the constraint C2
  958 
  959    forall[2]. Eq (Maybe s) => (Ord a, Show a,
  960                               Maybe s -> Maybe s -> Bool
  961                                 ~ Maybe s -> Maybe s -> Bool)
  962 
  963 In this case baz has no local quantification, so the implication
  964 constraint has no local skolems and there are no unification
  965 variables.
  966 
  967 [STEP DAC SOLVE]
  968 We can combine these two implication constraints into a single
  969 constraint (C1, C2), and simplify, unifying cc:=b, to get:
  970 
  971    forall[2] b. Ix b => Show a
  972    /\
  973    forall[2]. Eq (Maybe s) => (Ord a, Show a)
  974 
  975 [STEP DAC HOIST]
  976 Let's call that (C1', C2').  Now we need to hoist the unsolved
  977 constraints out of the implications to become our candidate for
  978 (CX). That is done by approximateWC, which will return:
  979 
  980   (Show a, Ord a, Show a)
  981 
  982 Now we can use mkMinimalBySCs to remove superclasses and duplicates, giving
  983 
  984   (Show a, Ord a)
  985 
  986 And that's what GHC uses for CX.
  987 
  988 [STEP DAC RESIDUAL]
  989 In this case we have solved all the leftover constraints, but what if
  990 we don't?  Simple!  We just form the final residual constraint
  991 
  992    forall[1] s. CX => (C1',C2')
  993 
  994 and simplify that. In simple cases it'll succeed easily, because CX
  995 literally contains the constraints in C1', C2', but if there is anything
  996 more complicated it will be reported in a civilised way.
  997 
  998 Note [Error reporting for deriving clauses]
  999 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1000 A surprisingly tricky aspect of deriving to get right is reporting sensible
 1001 error messages. In particular, if simplifyDeriv reaches a constraint that it
 1002 cannot solve, which might include:
 1003 
 1004 1. Insoluble constraints
 1005 2. "Exotic" constraints (See Note [Exotic derived instance contexts])
 1006 
 1007 Then we report an error immediately in simplifyDeriv.
 1008 
 1009 Another possible choice is to punt and let another part of the typechecker
 1010 (e.g., simplifyInstanceContexts) catch the errors. But this tends to lead
 1011 to worse error messages, so we do it directly in simplifyDeriv.
 1012 
 1013 simplifyDeriv checks for errors in a clever way. If the deriving machinery
 1014 infers the context (Foo a)--that is, if this instance is to be generated:
 1015 
 1016   instance Foo a => ...
 1017 
 1018 Then we form an implication of the form:
 1019 
 1020   forall a. Foo a => <residual_wanted_constraints>
 1021 
 1022 And pass it to the simplifier. If the context (Foo a) is enough to discharge
 1023 all the constraints in <residual_wanted_constraints>, then everything is
 1024 hunky-dory. But if <residual_wanted_constraints> contains, say, an insoluble
 1025 constraint, then (Foo a) won't be able to solve it, causing GHC to error.
 1026 
 1027 Note [Exotic derived instance contexts]
 1028 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1029 In a 'derived' instance declaration, we *infer* the context.  It's a
 1030 bit unclear what rules we should apply for this; the Haskell report is
 1031 silent.  Obviously, constraints like (Eq a) are fine, but what about
 1032         data T f a = MkT (f a) deriving( Eq )
 1033 where we'd get an Eq (f a) constraint.  That's probably fine too.
 1034 
 1035 One could go further: consider
 1036         data T a b c = MkT (Foo a b c) deriving( Eq )
 1037         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
 1038 
 1039 Notice that this instance (just) satisfies the Paterson termination
 1040 conditions.  Then we *could* derive an instance decl like this:
 1041 
 1042         instance (C Int a, Eq b, Eq c) => Eq (T a b c)
 1043 even though there is no instance for (C Int a), because there just
 1044 *might* be an instance for, say, (C Int Bool) at a site where we
 1045 need the equality instance for T's.
 1046 
 1047 However, this seems pretty exotic, and it's quite tricky to allow
 1048 this, and yet give sensible error messages in the (much more common)
 1049 case where we really want that instance decl for C.
 1050 
 1051 So for now we simply require that the derived instance context
 1052 should have only type-variable constraints.
 1053 
 1054 Here is another example:
 1055         data Fix f = In (f (Fix f)) deriving( Eq )
 1056 Here, if we are prepared to allow -XUndecidableInstances we
 1057 could derive the instance
 1058         instance Eq (f (Fix f)) => Eq (Fix f)
 1059 but this is so delicate that I don't think it should happen inside
 1060 'deriving'. If you want this, write it yourself!
 1061 
 1062 NB: if you want to lift this condition, make sure you still meet the
 1063 termination conditions!  If not, the deriving mechanism generates
 1064 larger and larger constraints.  Example:
 1065   data Succ a = S a
 1066   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
 1067 
 1068 Note the lack of a Show instance for Succ.  First we'll generate
 1069   instance (Show (Succ a), Show a) => Show (Seq a)
 1070 and then
 1071   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
 1072 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
 1073 
 1074 The bottom line
 1075 ~~~~~~~~~~~~~~~
 1076 Allow constraints which consist only of type variables, with no repeats.
 1077 -}