diff options
Diffstat (limited to 'compiler/GHC/Tc/Deriv/Infer.hs')
| -rw-r--r-- | compiler/GHC/Tc/Deriv/Infer.hs | 1074 |
1 files changed, 1074 insertions, 0 deletions
diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs new file mode 100644 index 0000000000..47257d6b23 --- /dev/null +++ b/compiler/GHC/Tc/Deriv/Infer.hs @@ -0,0 +1,1074 @@ +{- +(c) The University of Glasgow 2006 +(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 + +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE MultiWayIf #-} + +-- | Functions for inferring (and simplifying) the context for derived instances. +module GHC.Tc.Deriv.Infer + ( inferConstraints + , simplifyInstanceContexts + ) +where + +#include "HsVersions.h" + +import GhcPrelude + +import Bag +import GHC.Types.Basic +import GHC.Core.Class +import GHC.Core.DataCon +import ErrUtils +import GHC.Tc.Utils.Instantiate +import Outputable +import Pair +import PrelNames +import GHC.Tc.Deriv.Utils +import GHC.Tc.Utils.Env +import GHC.Tc.Deriv.Generate +import GHC.Tc.Deriv.Functor +import GHC.Tc.Deriv.Generics +import GHC.Tc.Utils.TcMType +import GHC.Tc.Utils.Monad +import GHC.Tc.Types.Origin +import GHC.Tc.Types.Constraint +import GHC.Core.Predicate +import GHC.Tc.Utils.TcType +import GHC.Core.TyCon +import GHC.Core.TyCo.Ppr (pprTyVars) +import GHC.Core.Type +import GHC.Tc.Solver +import GHC.Tc.Validity (validDerivPred) +import GHC.Tc.Utils.Unify (buildImplicationFor, checkConstraints) +import TysWiredIn (typeToTypeKind) +import GHC.Core.Unify (tcUnifyTy) +import Util +import GHC.Types.Var +import GHC.Types.Var.Set + +import Control.Monad +import Control.Monad.Trans.Class (lift) +import Control.Monad.Trans.Reader (ask) +import Data.List (sortBy) +import Data.Maybe + +---------------------- + +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 +-- variables and instance types, in case they were changed due to +-- the presence of functor-like constraints. +-- See Note [Inferring the instance context] + +-- e.g. inferConstraints +-- C Int (T [a]) -- Class and inst_tys +-- :RTList a -- Rep tycon and its arg tys +-- where T [a] ~R :RTList a +-- +-- 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 mechanism + = do { DerivEnv { denv_tvs = tvs + , denv_cls = main_cls + , denv_inst_tys = inst_tys } <- ask + ; wildcard <- isStandaloneWildcardDeriv + ; let infer_constraints :: DerivM ([ThetaOrigin], [TyVar], [TcType]) + infer_constraints = + case mechanism of + DerivSpecStock{dsm_stock_dit = dit} + -> inferConstraintsStock dit + DerivSpecAnyClass + -> infer_constraints_simple inferConstraintsAnyclass + DerivSpecNewtype { dsm_newtype_dit = + DerivInstTys{dit_cls_tys = cls_tys} + , dsm_newtype_rep_ty = rep_ty } + -> infer_constraints_simple $ + inferConstraintsCoerceBased cls_tys rep_ty + DerivSpecVia { dsm_via_cls_tys = cls_tys + , dsm_via_ty = via_ty } + -> infer_constraints_simple $ + inferConstraintsCoerceBased cls_tys via_ty + + -- Most deriving strategies do not need to do anything special to + -- the type variables and arguments to the class in the derived + -- instance, so they can pass through unchanged. The exception to + -- this rule is stock deriving. See + -- Note [Inferring the instance context]. + infer_constraints_simple + :: DerivM [ThetaOrigin] + -> DerivM ([ThetaOrigin], [TyVar], [TcType]) + infer_constraints_simple infer_thetas = do + thetas <- infer_thetas + pure (thetas, tvs, inst_tys) + + -- 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 (mkDerivOrigin wildcard) + 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 + ] + ; return ( sc_constraints ++ inferred_constraints + , tvs', inst_tys' ) } + +-- | Like 'inferConstraints', but used only in the case of the @stock@ deriving +-- strategy. The constraints are inferred by inspecting the fields of each data +-- constructor. In this example: +-- +-- > data Foo = MkFoo Int Char deriving Show +-- +-- We would infer the following constraints ('ThetaOrigin's): +-- +-- > (Show Int, Show Char) +-- +-- Note that this function also returns the type variables ('TyVar's) and +-- class arguments ('TcType's) for the resulting instance. This is because +-- when deriving 'Functor'-like classes, we must sometimes perform kind +-- substitutions to ensure the resulting instance is well kinded, which may +-- affect the type variables and class arguments. In this example: +-- +-- > newtype Compose (f :: k -> Type) (g :: Type -> k) (a :: Type) = +-- > Compose (f (g a)) deriving stock Functor +-- +-- We must unify @k@ with @Type@ in order for the resulting 'Functor' instance +-- to be well kinded, so we return @[]@/@[Type, f, g]@ for the +-- 'TyVar's/'TcType's, /not/ @[k]@/@[k, f, g]@. +-- See Note [Inferring the instance context]. +inferConstraintsStock :: DerivInstTys + -> DerivM ([ThetaOrigin], [TyVar], [TcType]) +inferConstraintsStock (DerivInstTys { dit_cls_tys = cls_tys + , dit_tc = tc + , dit_tc_args = tc_args + , dit_rep_tc = rep_tc + , dit_rep_tc_args = rep_tc_args }) + = do DerivEnv { denv_tvs = tvs + , denv_cls = main_cls + , denv_inst_tys = inst_tys } <- ask + wildcard <- isStandaloneWildcardDeriv + + let inst_ty = mkTyConApp tc tc_args + 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 wildcard + , 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', _) = substTyVarBndrs 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 = tcTypeKind 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 = tcTypeKind 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 deriv_origin 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 . tcTypeKind) rep_tc_args + = [ mk_cls_pred deriv_origin 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 + + deriv_origin = mkDerivOrigin wildcard + + 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 "inferConstraintsStock" $ vcat + [ ppr main_cls <+> ppr inst_tys' + , ppr arg_constraints + ] + ; return ( stupid_constraints ++ extra_constraints + ++ arg_constraints + , tvs', inst_tys') } + +-- | 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. +inferConstraintsAnyclass :: DerivM [ThetaOrigin] +inferConstraintsAnyclass + = do { DerivEnv { denv_cls = cls + , denv_inst_tys = inst_tys } <- ask + ; wildcard <- isStandaloneWildcardDeriv + + ; let gen_dms = [ (sel_id, dm_ty) + | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ] + + cls_tvs = classTyVars cls + + 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' + tau_eq = mkPrimEqPred meth_tau dm_tau + ; return (mkThetaOrigin (mkDerivOrigin wildcard) TypeLevel + meth_tvs dm_tvs meth_theta (tau_eq:dm_theta)) } + + ; theta_origins <- lift $ mapM do_one_meth gen_dms + ; return theta_origins } + +-- Like 'inferConstraints', but used only for @GeneralizedNewtypeDeriving@ and +-- @DerivingVia@. Since both strategies generate code involving 'coerce', the +-- inferred constraints set up the scaffolding needed to typecheck those uses +-- of 'coerce'. In this example: +-- +-- > newtype Age = MkAge Int deriving newtype Num +-- +-- We would infer the following constraints ('ThetaOrigin's): +-- +-- > (Num Int, Coercible Age Int) +inferConstraintsCoerceBased :: [Type] -> Type + -> DerivM [ThetaOrigin] +inferConstraintsCoerceBased cls_tys rep_ty = do + DerivEnv { denv_tvs = tvs + , denv_cls = cls + , denv_inst_tys = inst_tys } <- ask + sa_wildcard <- isStandaloneWildcardDeriv + let -- The following functions are polymorphic over the representation + -- type, since we might either give it the underlying type of a + -- newtype (for GeneralizedNewtypeDeriving) or a @via@ type + -- (for DerivingVia). + rep_tys ty = cls_tys ++ [ty] + rep_pred ty = mkClassPred cls (rep_tys ty) + rep_pred_o ty = mkPredOrigin deriv_origin TypeLevel (rep_pred ty) + -- rep_pred is the representation dictionary, from where + -- we are going to get all the methods for the final + -- dictionary + deriv_origin = mkDerivOrigin sa_wildcard + + -- Next we collect constraints for the class methods + -- If there are no methods, we don't need any constraints + -- Otherwise we need (C rep_ty), for the representation methods, + -- and constraints to coerce each individual method + meth_preds :: Type -> [PredOrigin] + meth_preds ty + | null meths = [] -- No methods => no constraints + -- (#12814) + | otherwise = rep_pred_o ty : coercible_constraints ty + meths = classMethods cls + coercible_constraints ty + = [ mkPredOrigin (DerivOriginCoerce meth t1 t2 sa_wildcard) + TypeLevel (mkReprPrimEqPred t1 t2) + | meth <- meths + , let (Pair t1 t2) = mkCoerceClassMethEqn cls tvs + inst_tys ty meth ] + + all_thetas :: Type -> [ThetaOrigin] + all_thetas ty = [mkThetaOriginFromPreds $ meth_preds ty] + + pure (all_thetas rep_ty) + +{- Note [Inferring the instance context] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +There are two sorts of 'deriving', as represented by the two constructors +for DerivContext: + + * InferContext mb_wildcard: This can either be: + - The deriving clause for a data type. + (e.g, data T a = T1 a deriving( Eq )) + In this case, mb_wildcard = Nothing. + - A standalone declaration with an extra-constraints wildcard + (e.g., deriving instance _ => Eq (Foo a)) + In this case, mb_wildcard = Just loc, where loc is the location + of the extra-constraints wildcard. + + Here we must infer an instance context, + and generate instance declaration + instance Eq a => Eq (T a) where ... + + * SupplyContext theta: standalone deriving + deriving instance Eq a => Eq (T a) + Here we only need to fill in the bindings; + the instance context (theta) is user-supplied + +For the InferContext case, we must figure out the +instance context (inferConstraintsStock). Suppose we are inferring +the instance context for + C t1 .. tn (T s1 .. sm) +There are two cases + + * (T s1 .. sm) :: * (the normal case) + Then we behave like Eq and guess (C t1 .. tn t) + for each data constructor arg of type t. More + details below. + + * (T s1 .. sm) :: * -> * (the functor-like case) + Then we behave like Functor. + +In both cases we produce a bunch of un-simplified constraints +and them simplify them in simplifyInstanceContexts; see +Note [Simplifying the instance context]. + +In the functor-like case, we may need to unify some kind variables with * in +order for the generated instance to be well-kinded. An example from +#10524: + + newtype Compose (f :: k2 -> *) (g :: k1 -> k2) (a :: k1) + = Compose (f (g a)) deriving Functor + +Earlier in the deriving pipeline, GHC unifies the kind of Compose f g +(k1 -> *) with the kind of Functor's argument (* -> *), so k1 := *. But this +alone isn't enough, since k2 wasn't unified with *: + + instance (Functor (f :: k2 -> *), Functor (g :: * -> k2)) => + Functor (Compose f g) where ... + +The two Functor constraints are ill-kinded. To ensure this doesn't happen, we: + + 1. Collect all of a datatype's subtypes which require functor-like + constraints. + 2. For each subtype, create a substitution by unifying the subtype's kind + with (* -> *). + 3. Compose all the substitutions into one, then apply that substitution to + all of the in-scope type variables and the instance types. + +Note [Getting base classes] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Functor and Typeable are defined in package 'base', and that is not available +when compiling 'ghc-prim'. So we must be careful that 'deriving' for stuff in +ghc-prim does not use Functor or Typeable implicitly via these lookups. + +Note [Deriving and unboxed types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We have some special hacks to support things like + data T = MkT Int# deriving ( Show ) + +Specifically, we use GHC.Tc.Deriv.Generate.box to box the Int# into an Int +(which we know how to show), and append a '#'. Parentheses are not required +for unboxed values (`MkT -3#` is a valid expression). + +Note [Superclasses of derived instance] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In general, a derived instance decl needs the superclasses of the derived +class too. So if we have + data T a = ...deriving( Ord ) +then the initial context for Ord (T a) should include Eq (T a). Often this is +redundant; we'll also generate an Ord constraint for each constructor argument, +and that will probably generate enough constraints to make the Eq (T a) constraint +be satisfied too. But not always; consider: + + data S a = S + instance Eq (S a) + instance Ord (S a) + + data T a = MkT (S a) deriving( Ord ) + instance Num a => Eq (T a) + +The derived instance for (Ord (T a)) must have a (Num a) constraint! +Similarly consider: + data T a = MkT deriving( Data ) +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 +* * +************************************************************************ + +Note [Simplifying the instance context] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + + data T a b = C1 (Foo a) (Bar b) + | C2 Int (T b a) + | C3 (T a a) + deriving (Eq) + +We want to come up with an instance declaration of the form + + instance (Ping a, Pong b, ...) => Eq (T a b) where + x == y = ... + +It is pretty easy, albeit tedious, to fill in the code "...". The +trick is to figure out what the context for the instance decl is, +namely Ping, Pong and friends. + +Let's call the context reqd for the T instance of class C at types +(a,b, ...) C (T a b). Thus: + + Eq (T a b) = (Ping a, Pong b, ...) + +Now we can get a (recursive) equation from the data decl. This part +is done by inferConstraintsStock. + + Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1 + u Eq (T b a) u Eq Int -- From C2 + u Eq (T a a) -- From C3 + + +Foo and Bar may have explicit instances for Eq, in which case we can +just substitute for them. Alternatively, either or both may have +their Eq instances given by deriving clauses, in which case they +form part of the system of equations. + +Now all we need do is simplify and solve the equations, iterating to +find the least fixpoint. This is done by simplifyInstanceConstraints. +Notice that the order of the arguments can +switch around, as here in the recursive calls to T. + +Let's suppose Eq (Foo a) = Eq a, and Eq (Bar b) = Ping b. + +We start with: + + Eq (T a b) = {} -- The empty set + +Next iteration: + Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1 + u Eq (T b a) u Eq Int -- From C2 + u Eq (T a a) -- From C3 + + After simplification: + = Eq a u Ping b u {} u {} u {} + = Eq a u Ping b + +Next iteration: + + Eq (T a b) = Eq (Foo a) u Eq (Bar b) -- From C1 + u Eq (T b a) u Eq Int -- From C2 + u Eq (T a a) -- From C3 + + After simplification: + = Eq a u Ping b + u (Eq b u Ping a) + u (Eq a u Ping a) + + = Eq a u Ping b u Eq b u Ping a + +The next iteration gives the same result, so this is the fixpoint. We +need to make a canonical form of the RHS to ensure convergence. We do +this by simplifying the RHS to a form in which + + - the classes constrain only tyvars + - the list is sorted by tyvar (major key) and then class (minor key) + - no duplicates, of course + +Note [Deterministic simplifyInstanceContexts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Canonicalisation uses nonDetCmpType which is nondeterministic. Sorting +with nonDetCmpType puts the returned lists in a nondeterministic order. +If we were to return them, we'd get class constraints in +nondeterministic order. + +Consider: + + data ADT a b = Z a b deriving Eq + +The generated code could be either: + + instance (Eq a, Eq b) => Eq (Z a b) where + +Or: + + instance (Eq b, Eq a) => Eq (Z a b) where + +To prevent the order from being nondeterministic we only +canonicalize when comparing and return them in the same order as +simplifyDeriv returned them. +See also Note [nonDetCmpType nondeterminism] +-} + + +simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]] + -> TcM [DerivSpec ThetaType] +-- Used only for deriving clauses or standalone deriving with an +-- extra-constraints wildcard (InferContext) +-- See Note [Simplifying the instance context] + +simplifyInstanceContexts [] = return [] + +simplifyInstanceContexts infer_specs + = do { traceTc "simplifyInstanceContexts" $ vcat (map pprDerivSpec infer_specs) + ; iterate_deriv 1 initial_solutions } + where + ------------------------------------------------------------------ + -- The initial solutions for the equations claim that each + -- instance has an empty context; this solution is certainly + -- in canonical form. + initial_solutions :: [ThetaType] + initial_solutions = [ [] | _ <- infer_specs ] + + ------------------------------------------------------------------ + -- iterate_deriv calculates the next batch of solutions, + -- compares it with the current one; finishes if they are the + -- same, otherwise recurses with the new solutions. + -- It fails if any iteration fails + iterate_deriv :: Int -> [ThetaType] -> TcM [DerivSpec ThetaType] + iterate_deriv n current_solns + | n > 20 -- Looks as if we are in an infinite loop + -- This can happen if we have -XUndecidableInstances + -- (See GHC.Tc.Solver.tcSimplifyDeriv.) + = pprPanic "solveDerivEqns: probable loop" + (vcat (map pprDerivSpec infer_specs) $$ ppr current_solns) + | otherwise + = do { -- Extend the inst info from the explicit instance decls + -- with the current set of solutions, and simplify each RHS + inst_specs <- zipWithM newDerivClsInst current_solns infer_specs + ; new_solns <- checkNoErrs $ + extendLocalInstEnv inst_specs $ + mapM gen_soln infer_specs + + ; if (current_solns `eqSolution` new_solns) then + return [ spec { ds_theta = soln } + | (spec, soln) <- zip infer_specs current_solns ] + else + iterate_deriv (n+1) new_solns } + + eqSolution a b = eqListBy (eqListBy eqType) (canSolution a) (canSolution b) + -- Canonicalise for comparison + -- See Note [Deterministic simplifyInstanceContexts] + canSolution = map (sortBy nonDetCmpType) + ------------------------------------------------------------------ + 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 $ + addErrCtxt (derivInstCtxt the_pred) $ + do { theta <- simplifyDeriv the_pred tyvars deriv_rhs + -- checkValidInstance tyvars theta clas inst_tys + -- Not necessary; see Note [Exotic derived instance contexts] + + ; traceTc "GHC.Tc.Deriv" (ppr deriv_rhs $$ ppr theta) + -- Claim: the result instance declaration is guaranteed valid + -- Hence no need to call: + -- checkValidInstance tyvars theta clas inst_tys + ; return theta } + where + the_pred = mkClassPred clas inst_tys + +derivInstCtxt :: PredType -> MsgDoc +derivInstCtxt pred + = text "When deriving the instance for" <+> parens (ppr pred) + +{- +*********************************************************************************** +* * +* Simplify derived constraints +* * +*********************************************************************************** +-} + +-- | Given @instance (wanted) => C inst_ty@, simplify 'wanted' as much +-- as possible. Fail if not possible. +simplifyDeriv :: PredType -- ^ @C inst_ty@, head of the instance we are + -- deriving. Only used for SkolemInfo. + -> [TyVar] -- ^ The tyvars bound by @inst_ty@. + -> [ThetaOrigin] -- ^ Given and wanted constraints + -> TcM ThetaType -- ^ Needed constraints (after simplification), + -- i.e. @['PredType']@. +simplifyDeriv pred tvs thetas + = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize + -- The constraint solving machinery + -- expects *TcTyVars* not TyVars. + -- We use *non-overlappable* (vanilla) skolems + -- See Note [Overlap and deriving] + + ; let skol_set = mkVarSet tvs_skols + skol_info = DerivSkol pred + doc = text "deriving" <+> parens (ppr pred) + + mk_given_ev :: PredType -> TcM EvVar + mk_given_ev given = + let given_pred = substTy skol_subst given + in newEvVar given_pred + + emit_wanted_constraints :: [TyVar] -> [PredOrigin] -> TcM () + emit_wanted_constraints metas_to_be preds + = do { -- We instantiate metas_to_be with fresh meta type + -- variables. Currently, these can only be type variables + -- quantified in generic default type signatures. + -- See Note [Gathering and simplifying constraints for + -- DeriveAnyClass] + (meta_subst, _meta_tvs) <- newMetaTyVars metas_to_be + + -- Now make a constraint for each of the instantiated predicates + ; let wanted_subst = skol_subst `unionTCvSubst` meta_subst + mk_wanted_ct (PredOrigin wanted orig t_or_k) + = do { ev <- newWanted orig (Just t_or_k) $ + substTyUnchecked wanted_subst wanted + ; return (mkNonCanonical ev) } + ; cts <- mapM mk_wanted_ct preds + + -- And emit them into the monad + ; emitSimples (listToCts cts) } + + -- 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_anyclass_skols = ac_skols + , to_anyclass_metas = ac_metas + , to_anyclass_givens = ac_givens + , to_wanted_origins = preds }) + = do { ac_given_evs <- mapM mk_given_ev ac_givens + ; (_, wanteds) + <- captureConstraints $ + checkConstraints skol_info ac_skols ac_given_evs $ + -- The checkConstraints bumps the TcLevel, and + -- wraps the wanted constraints in an implication, + -- when (but only when) necessary + emit_wanted_constraints ac_metas preds + ; pure wanteds } + + -- See [STEP DAC BUILD] + -- Generate the implication constraints, one for each method, to solve + -- with the skolemized variables. Start "one level down" because + -- we are going to wrap the result in an implication with tvs_skols, + -- in step [DAC RESIDUAL] + ; (tc_lvl, wanteds) <- pushTcLevelM $ + mapM mk_wanteds thetas + + ; traceTc "simplifyDeriv inputs" $ + vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ] + + -- See [STEP DAC SOLVE] + -- Simplify the constraints, starting at the same level at which + -- they are generated (c.f. the call to runTcSWithEvBinds in + -- simplifyInfer) + ; solved_wanteds <- setTcLevel tc_lvl $ + runTcSDeriveds $ + solveWantedsAndDrop $ + unionsWC wanteds + + -- It's not yet zonked! Obviously zonk it before peering at it + ; solved_wanteds <- zonkWC solved_wanteds + + -- 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 = approximateWC True solved_wanteds + (bad, good) = partitionBagWith get_good residual_simple + + 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 + -- to do with them + | otherwise + = Left ct + where p = ctPred ct + + ; traceTc "simplifyDeriv outputs" $ + 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 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 tc_lvl skol_info tvs_skols + min_theta_vars solved_wanteds + -- 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) } + +{- +Note [Overlap and deriving] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider some overlapping instances: + instance Show a => Show [a] where .. + instance Show [Char] where ... + +Now a data type with deriving: + data T a = MkT [a] deriving( Show ) + +We want to get the derived instance + instance Show [a] => Show (T a) where... +and NOT + instance Show a => Show (T a) where... +so that the (Show (T Char)) instance does the Right Thing + +It's very like the situation when we're inferring the type +of a function + f x = show [x] +and we want to infer + f :: Show [a] => a -> String + +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 $gdm_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[2] b. Ix b => (Show (Maybe s), Ix cc, + Maybe s -> b -> String + ~ Maybe s -> cc -> String) + +Here: +* The level of this forall constraint is forall[2], because we are later + going to wrap it in a forall[1] in [STEP DAC RESIDUAL] + +* The 'b' comes from the quantified type variable in the expected type + of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification + variable that comes from instantiating the quantified type variable 'c' in + $gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin). + +* The (Ix b) constraint comes from the context of bar's type + (i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc) + constraints come from the context of $gdm_bar's type + (i.e., 'to_anyclass_givens' in 'ThetaOrigin'). + +* The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String) + comes from marrying up the instantiated type of $gdm_bar with the specified + type of bar. Notice that the type variables from the instance, 's' in this + case, are global to this constraint. + +Note that it is vital that we instantiate the `c` in $gdm_bar's type with a new +unification variable for each iteration of simplifyDeriv. If we re-use the same +unification variable across multiple iterations, then bad things can happen, +such as #14933. + +Similarly for 'baz', giving the constraint C2 + + forall[2]. 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[2] b. Ix b => Show a + /\ + forall[2]. 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[1] 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 surprisingly 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 +bit unclear what rules we should apply for this; the Haskell report is +silent. Obviously, constraints like (Eq a) are fine, but what about + data T f a = MkT (f a) deriving( Eq ) +where we'd get an Eq (f a) constraint. That's probably fine too. + +One could go further: consider + data T a b c = MkT (Foo a b c) deriving( Eq ) + instance (C Int a, Eq b, Eq c) => Eq (Foo a b c) + +Notice that this instance (just) satisfies the Paterson termination +conditions. Then we *could* derive an instance decl like this: + + instance (C Int a, Eq b, Eq c) => Eq (T a b c) +even though there is no instance for (C Int a), because there just +*might* be an instance for, say, (C Int Bool) at a site where we +need the equality instance for T's. + +However, this seems pretty exotic, and it's quite tricky to allow +this, and yet give sensible error messages in the (much more common) +case where we really want that instance decl for C. + +So for now we simply require that the derived instance context +should have only type-variable constraints. + +Here is another example: + data Fix f = In (f (Fix f)) deriving( Eq ) +Here, if we are prepared to allow -XUndecidableInstances we +could derive the instance + instance Eq (f (Fix f)) => Eq (Fix f) +but this is so delicate that I don't think it should happen inside +'deriving'. If you want this, write it yourself! + +NB: if you want to lift this condition, make sure you still meet the +termination conditions! If not, the deriving mechanism generates +larger and larger constraints. Example: + data Succ a = S a + data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show + +Note the lack of a Show instance for Succ. First we'll generate + instance (Show (Succ a), Show a) => Show (Seq a) +and then + instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a) +and so on. Instead we want to complain of no instance for (Show (Succ a)). + +The bottom line +~~~~~~~~~~~~~~~ +Allow constraints which consist only of type variables, with no repeats. +-} |