diff options
Diffstat (limited to 'compiler/GHC/Tc')
-rw-r--r-- | compiler/GHC/Tc/Deriv.hs | 50 | ||||
-rw-r--r-- | compiler/GHC/Tc/Deriv/Generate.hs | 29 | ||||
-rw-r--r-- | compiler/GHC/Tc/Deriv/Infer.hs | 303 | ||||
-rw-r--r-- | compiler/GHC/Tc/Deriv/Utils.hs | 340 | ||||
-rw-r--r-- | compiler/GHC/Tc/Types/Constraint.hs | 5 |
5 files changed, 467 insertions, 260 deletions
diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs index 39900cb47e..29a58d9c01 100644 --- a/compiler/GHC/Tc/Deriv.hs +++ b/compiler/GHC/Tc/Deriv.hs @@ -88,7 +88,7 @@ Overall plan 3. Add the derived bindings, generating InstInfos -} -data EarlyDerivSpec = InferTheta (DerivSpec [ThetaOrigin]) +data EarlyDerivSpec = InferTheta (DerivSpec ThetaSpec) | GivenTheta (DerivSpec ThetaType) -- InferTheta ds => the context for the instance should be inferred -- In this case ds_theta is the list of all the sets of @@ -102,7 +102,7 @@ data EarlyDerivSpec = InferTheta (DerivSpec [ThetaOrigin]) -- See Note [Inferring the instance context] in GHC.Tc.Deriv.Infer splitEarlyDerivSpec :: [EarlyDerivSpec] - -> ([DerivSpec [ThetaOrigin]], [DerivSpec ThetaType]) + -> ([DerivSpec ThetaSpec], [DerivSpec ThetaType]) splitEarlyDerivSpec [] = ([],[]) splitEarlyDerivSpec (InferTheta spec : specs) = case splitEarlyDerivSpec specs of (is, gs) -> (spec : is, gs) @@ -1137,14 +1137,40 @@ mkEqnHelp :: Maybe OverlapMode mkEqnHelp overlap_mode tvs cls cls_args deriv_ctxt deriv_strat = do is_boot <- tcIsHsBootOrSig when is_boot $ bale_out DerivErrBootFileFound + + let pred = mkClassPred cls cls_args + skol_info <- mkSkolemInfo (DerivSkol pred) + (tvs', cls_args', deriv_strat') <- + skolemise_when_inferring_context skol_info deriv_ctxt + let deriv_env = DerivEnv + { denv_overlap_mode = overlap_mode + , denv_tvs = tvs' + , denv_cls = cls + , denv_inst_tys = cls_args' + , denv_ctxt = deriv_ctxt + , denv_skol_info = skol_info + , denv_strat = deriv_strat' } runReaderT mk_eqn deriv_env where - deriv_env = DerivEnv { denv_overlap_mode = overlap_mode - , denv_tvs = tvs - , denv_cls = cls - , denv_inst_tys = cls_args - , denv_ctxt = deriv_ctxt - , denv_strat = deriv_strat } + skolemise_when_inferring_context :: + SkolemInfo -> DerivContext + -> TcM ([TcTyVar], [TcType], Maybe (DerivStrategy GhcTc)) + skolemise_when_inferring_context skol_info deriv_ctxt = + case deriv_ctxt of + -- In order to infer an instance context, we must later make use of + -- the constraint solving machinery, which expects TcTyVars rather + -- than TyVars. We skolemise the type variables with non-overlappable + -- (vanilla) skolems. + -- See Note [Overlap and deriving] in GHC.Tc.Deriv.Infer. + InferContext{} -> do + (skol_subst, tvs') <- tcInstSkolTyVars skol_info tvs + let cls_args' = substTys skol_subst cls_args + deriv_strat' = fmap (mapDerivStrategy (substTy skol_subst)) + deriv_strat + pure (tvs', cls_args', deriv_strat') + -- If the instance context is supplied, we don't need to skolemise + -- at all. + SupplyContext{} -> pure (tvs, cls_args, deriv_strat) bale_out = failWithTc . TcRnCannotDeriveInstance cls cls_args deriv_strat NoGeneralizedNewtypeDeriving @@ -1308,7 +1334,9 @@ mk_eqn_from_mechanism mechanism , denv_tvs = tvs , denv_cls = cls , denv_inst_tys = inst_tys - , denv_ctxt = deriv_ctxt } <- ask + , denv_ctxt = deriv_ctxt + , denv_skol_info = skol_info } <- ask + user_ctxt <- askDerivUserTypeCtxt doDerivInstErrorChecks1 mechanism loc <- lift getSrcSpanM dfun_name <- lift $ newDFunName cls inst_tys loc @@ -1321,6 +1349,8 @@ mk_eqn_from_mechanism mechanism , ds_name = dfun_name, ds_tvs = tvs' , ds_cls = cls, ds_tys = inst_tys' , ds_theta = inferred_constraints + , ds_skol_info = skol_info + , ds_user_ctxt = user_ctxt , ds_overlap = overlap_mode , ds_standalone_wildcard = wildcard , ds_mechanism = mechanism' } } @@ -1331,6 +1361,8 @@ mk_eqn_from_mechanism mechanism , ds_name = dfun_name, ds_tvs = tvs , ds_cls = cls, ds_tys = inst_tys , ds_theta = theta + , ds_skol_info = skol_info + , ds_user_ctxt = user_ctxt , ds_overlap = overlap_mode , ds_standalone_wildcard = Nothing , ds_mechanism = mechanism } diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs index 3f8893460b..5bacc4fb30 100644 --- a/compiler/GHC/Tc/Deriv/Generate.hs +++ b/compiler/GHC/Tc/Deriv/Generate.hs @@ -39,7 +39,7 @@ module GHC.Tc.Deriv.Generate ( getPossibleDataCons, DerivInstTys(..), buildDataConInstArgEnv, - derivDataConInstArgTys, substDerivInstTys + derivDataConInstArgTys, substDerivInstTys, zonkDerivInstTys ) where import GHC.Prelude @@ -65,6 +65,7 @@ import GHC.Types.SrcLoc import GHC.Core.TyCon import GHC.Tc.Utils.Env import GHC.Tc.Utils.TcType +import GHC.Tc.Utils.Zonk import GHC.Tc.Validity ( checkValidCoAxBranch ) import GHC.Core.Coercion.Axiom ( coAxiomSingleBranch ) import GHC.Builtin.Types.Prim @@ -2694,6 +2695,12 @@ getPossibleDataCons tycon tycon_args = filter isPossible $ tyConDataCons tycon -- @dit_cls_tys ++ ['mkTyConApp' dit_tc dit_tc_args]@. Other parts of the -- instance declaration can be found in the 'DerivEnv'. For example, the @Cls@ -- in the example above corresponds to the 'denv_cls' field of 'DerivEnv'. +-- +-- Similarly, the type variables that appear in a 'DerivInstTys' value are the +-- same type variables as the 'denv_tvs' in the parent 'DerivEnv'. Accordingly, +-- if we are inferring an instance context, the type variables will be 'TcTyVar' +-- skolems. Otherwise, they will be ordinary 'TyVar's. +-- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer". data DerivInstTys = DerivInstTys { dit_cls_tys :: [Type] -- ^ Other arguments to the class except the last @@ -2771,6 +2778,26 @@ substDerivInstTys subst tc_args' = substTys subst tc_args rep_tc_args' = substTys subst rep_tc_args +-- | Zonk the 'TcTyVar's in a 'DerivInstTys' value to 'TyVar's. +-- See @Note [What is zonking?]@ in "GHC.Tc.Utils.TcMType". +-- +-- This is only used in the final zonking step when inferring +-- the context for a derived instance. +-- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer". +zonkDerivInstTys :: ZonkEnv -> DerivInstTys -> TcM DerivInstTys +zonkDerivInstTys ze dit@(DerivInstTys { dit_cls_tys = cls_tys + , dit_tc_args = tc_args + , dit_rep_tc = rep_tc + , dit_rep_tc_args = rep_tc_args }) = do + cls_tys' <- zonkTcTypesToTypesX ze cls_tys + tc_args' <- zonkTcTypesToTypesX ze tc_args + rep_tc_args' <- zonkTcTypesToTypesX ze rep_tc_args + pure dit{ dit_cls_tys = cls_tys' + , dit_tc_args = tc_args' + , dit_rep_tc_args = rep_tc_args' + , dit_dc_inst_arg_env = buildDataConInstArgEnv rep_tc rep_tc_args' + } + {- Note [Auxiliary binders] ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs index 3b2d3f80dd..94a00ce52b 100644 --- a/compiler/GHC/Tc/Deriv/Infer.hs +++ b/compiler/GHC/Tc/Deriv/Infer.hs @@ -21,7 +21,6 @@ import GHC.Types.Basic import GHC.Core.Class import GHC.Core.DataCon import GHC.Utils.Error -import GHC.Tc.Utils.Instantiate import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain @@ -44,7 +43,7 @@ import GHC.Core.Type import GHC.Tc.Solver import GHC.Tc.Solver.Monad ( runTcS ) import GHC.Tc.Validity (validDerivPred) -import GHC.Tc.Utils.Unify (buildImplicationFor, checkConstraints) +import GHC.Tc.Utils.Unify (buildImplicationFor) import GHC.Builtin.Types (typeToTypeKind) import GHC.Core.Unify (tcUnifyTy) import GHC.Utils.Misc @@ -60,7 +59,7 @@ import Data.Maybe ---------------------- inferConstraints :: DerivSpecMechanism - -> DerivM ([ThetaOrigin], [TyVar], [TcType], DerivSpecMechanism) + -> DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism) -- 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 @@ -81,7 +80,7 @@ inferConstraints mechanism , denv_cls = main_cls , denv_inst_tys = inst_tys } <- ask ; wildcard <- isStandaloneWildcardDeriv - ; let infer_constraints :: DerivM ([ThetaOrigin], [TyVar], [TcType], DerivSpecMechanism) + ; let infer_constraints :: DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism) infer_constraints = case mechanism of DerivSpecStock{dsm_stock_dit = dit} @@ -106,8 +105,8 @@ inferConstraints mechanism -- this rule is stock deriving. See -- Note [Inferring the instance context]. infer_constraints_simple - :: DerivM [ThetaOrigin] - -> DerivM ([ThetaOrigin], [TyVar], [TcType], DerivSpecMechanism) + :: DerivM ThetaSpec + -> DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism) infer_constraints_simple infer_thetas = do thetas <- infer_thetas pure (thetas, tvs, inst_tys, mechanism) @@ -116,10 +115,10 @@ inferConstraints mechanism -- See Note [Superclasses of derived instance] cls_tvs = classTyVars main_cls sc_constraints = assertPpr (equalLength cls_tvs inst_tys) - (ppr main_cls <+> ppr inst_tys) - [ mkThetaOrigin (mkDerivOrigin wildcard) - TypeLevel [] [] [] $ - substTheta cls_subst (classSCTheta main_cls) ] + (ppr main_cls <+> ppr inst_tys) $ + mkDirectThetaSpec + (mkDerivOrigin wildcard) TypeLevel + (substTheta cls_subst (classSCTheta main_cls)) cls_subst = assert (equalLength cls_tvs inst_tys) $ zipTvSubst cls_tvs inst_tys @@ -138,7 +137,7 @@ inferConstraints mechanism -- -- > data Foo = MkFoo Int Char deriving Show -- --- We would infer the following constraints ('ThetaOrigin's): +-- We would infer the following constraints ('ThetaSpec's): -- -- > (Show Int, Show Char) -- @@ -156,7 +155,7 @@ inferConstraints mechanism -- 'TyVar's/'TcType's, /not/ @[k]@/@[k, f, g]@. -- See Note [Inferring the instance context]. inferConstraintsStock :: DerivInstTys - -> DerivM ([ThetaOrigin], [TyVar], [TcType], DerivInstTys) + -> DerivM (ThetaSpec, [TyVar], [TcType], DerivInstTys) inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys , dit_tc = tc , dit_tc_args = tc_args @@ -179,8 +178,8 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys con_arg_constraints :: (CtOrigin -> TypeOrKind -> Type - -> [([PredOrigin], Maybe TCvSubst)]) - -> ([ThetaOrigin], [TyVar], [TcType], DerivInstTys) + -> [(ThetaSpec, Maybe TCvSubst)]) + -> (ThetaSpec, [TyVar], [TcType], DerivInstTys) con_arg_constraints get_arg_constraints = let -- Constraints from the fields of each data constructor. (predss, mbSubsts) = unzip @@ -220,13 +219,14 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys unmapped_tvs = filter (\v -> v `notElemTCvSubst` subst && not (v `isInScope` subst)) tvs (subst', _) = substTyVarBndrs subst unmapped_tvs - stupid_theta_origin = mkThetaOrigin deriv_origin TypeLevel [] [] [] $ - substTheta subst' stupid_theta - preds' = map (substPredOrigin subst') preds + stupid_theta_origin = mkDirectThetaSpec + deriv_origin TypeLevel + (substTheta subst' stupid_theta) + preds' = map (substPredSpec subst') preds inst_tys' = substTys subst' inst_tys dit' = substDerivInstTys subst' dit tvs' = tyCoVarsOfTypesWellScoped inst_tys' - in ( [stupid_theta_origin, mkThetaOriginFromPreds preds'] + in ( stupid_theta_origin ++ preds' , tvs', inst_tys', dit' ) is_generic = main_cls `hasKey` genClassKey @@ -236,13 +236,13 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys || is_generic1 get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type - -> [([PredOrigin], Maybe TCvSubst)] + -> [(ThetaSpec, 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)] + -> [(ThetaSpec, Maybe TCvSubst)] get_std_constrained_tys orig t_or_k ty | is_functor_like = mk_functor_like_constraints orig t_or_k main_cls $ @@ -253,7 +253,7 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys mk_functor_like_constraints :: CtOrigin -> TypeOrKind -> Class -> [Type] - -> [([PredOrigin], Maybe TCvSubst)] + -> [(ThetaSpec, 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 @@ -268,8 +268,12 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys 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) ] + , SimplePredSpec + { sps_pred = mkPrimEqPred ki typeToTypeKind + , sps_origin = orig + , sps_type_or_kind = KindLevel + } + ] , tcUnifyTy ki typeToTypeKind ) @@ -284,9 +288,7 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys -- 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 + extra_constraints | main_cls `hasKey` dataClassKey , all (isLiftedTypeKind . tcTypeKind) rep_tc_args = [ mk_cls_pred deriv_origin t_or_k main_cls ty @@ -296,7 +298,11 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys 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])) + = SimplePredSpec + { sps_pred = mkClassPred cls (cls_tys' ++ [ty]) + , sps_origin = orig + , sps_type_or_kind = t_or_k + } cls_tys' | is_generic1 = [] -- In the awkward Generic1 case, cls_tys' should be -- empty, since we are applying the class Functor. @@ -337,36 +343,32 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys = cls_tys -- 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 :: DerivM ThetaSpec inferConstraintsAnyclass - = do { DerivEnv { denv_cls = cls - , denv_inst_tys = inst_tys } <- ask - ; wildcard <- isStandaloneWildcardDeriv - + = do { DerivEnv { denv_cls = cls + , denv_inst_tys = inst_tys } <- ask ; let gen_dms = [ (sel_id, dm_ty) | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ] + ; wildcard <- isStandaloneWildcardDeriv - cls_tvs = classTyVars cls - - do_one_meth :: (Id, Type) -> TcM ThetaOrigin + ; let meth_pred :: (Id, Type) -> PredSpec -- (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)) } - - ; lift $ mapM do_one_meth gen_dms } + meth_pred (sel_id, gen_dm_ty) + = let (sel_tvs, _cls_pred, meth_ty) = tcSplitMethodTy (varType sel_id) + meth_ty' = substTyWith sel_tvs inst_tys meth_ty + gen_dm_ty' = substTyWith sel_tvs inst_tys gen_dm_ty in + -- This is the only place where a SubTypePredSpec is + -- constructed instead of a SimplePredSpec. See + -- Note [Gathering and simplifying constraints for DeriveAnyClass] + -- for a more in-depth explanation. + SubTypePredSpec { stps_ty_actual = gen_dm_ty' + , stps_ty_expected = meth_ty' + , stps_origin = mkDerivOrigin wildcard + } + + ; pure $ map meth_pred gen_dms } -- Like 'inferConstraints', but used only for @GeneralizedNewtypeDeriving@ and -- @DerivingVia@. Since both strategies generate code involving 'coerce', the @@ -375,11 +377,11 @@ inferConstraintsAnyclass -- -- > newtype Age = MkAge Int deriving newtype Num -- --- We would infer the following constraints ('ThetaOrigin's): +-- We would infer the following constraints ('ThetaSpec'): -- -- > (Num Int, Coercible Age Int) inferConstraintsCoerceBased :: [Type] -> Type - -> DerivM [ThetaOrigin] + -> DerivM ThetaSpec inferConstraintsCoerceBased cls_tys rep_ty = do DerivEnv { denv_tvs = tvs , denv_cls = cls @@ -391,7 +393,10 @@ inferConstraintsCoerceBased cls_tys rep_ty = do -- (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_o ty = SimplePredSpec { sps_pred = rep_pred ty + , sps_origin = deriv_origin + , sps_type_or_kind = TypeLevel + } -- rep_pred is the representation dictionary, from where -- we are going to get all the methods for the final -- dictionary @@ -401,23 +406,23 @@ inferConstraintsCoerceBased cls_tys rep_ty = do -- 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 :: Type -> ThetaSpec 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) + = [ SimplePredSpec + { sps_pred = mkReprPrimEqPred t1 t2 + , sps_origin = DerivOriginCoerce meth t1 t2 sa_wildcard + , sps_type_or_kind = TypeLevel + } | 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) + pure (meth_preds rep_ty) {- Note [Inferring the instance context] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -631,7 +636,7 @@ See also Note [nonDetCmpType nondeterminism] -} -simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]] +simplifyInstanceContexts :: [DerivSpec ThetaSpec] -> TcM [DerivSpec ThetaType] -- Used only for deriving clauses or standalone deriving with an -- extra-constraints wildcard (InferContext) @@ -641,7 +646,10 @@ simplifyInstanceContexts [] = return [] simplifyInstanceContexts infer_specs = do { traceTc "simplifyInstanceContexts" $ vcat (map pprDerivSpec infer_specs) - ; iterate_deriv 1 initial_solutions } + ; final_specs <- iterate_deriv 1 initial_solutions + -- After simplification finishes, zonk the TcTyVars as described + -- in Note [Overlap and deriving]. + ; traverse zonkDerivSpec final_specs } where ------------------------------------------------------------------ -- The initial solutions for the equations claim that each @@ -682,12 +690,13 @@ simplifyInstanceContexts infer_specs -- See Note [Deterministic simplifyInstanceContexts] canSolution = map (sortBy nonDetCmpType) ------------------------------------------------------------------ - gen_soln :: DerivSpec [ThetaOrigin] -> TcM ThetaType + gen_soln :: DerivSpec ThetaSpec -> TcM ThetaType gen_soln (DS { ds_loc = loc, ds_tvs = tyvars - , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs }) + , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs + , ds_skol_info = skol_info, ds_user_ctxt = user_ctxt }) = setSrcSpan loc $ addErrCtxt (derivInstCtxt the_pred) $ - do { theta <- simplifyDeriv the_pred tyvars deriv_rhs + do { theta <- simplifyDeriv skol_info user_ctxt tyvars deriv_rhs -- checkValidInstance tyvars theta clas inst_tys -- Not necessary; see Note [Exotic derived instance contexts] @@ -713,78 +722,27 @@ derivInstCtxt pred -- | 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 +simplifyDeriv :: SkolemInfo -- ^ The 'SkolemInfo' used to skolemise the + -- 'TcTyVar' arguments + -> UserTypeCtxt -- ^ Used to inform error messages as to whether + -- we are in a @deriving@ clause or a standalone + -- @deriving@ declaration + -> [TcTyVar] -- ^ The tyvars bound by @inst_ty@. + -> ThetaSpec -- ^ The constraints to solve and simplify -> TcM ThetaType -- ^ Needed constraints (after simplification), -- i.e. @['PredType']@. -simplifyDeriv pred tvs thetas - = do { skol_info <- mkSkolemInfo (DerivSkol pred) - ; (skol_subst, tvs_skols) <- tcInstSkolTyVars skol_info 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 - 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 (getSkolemInfo 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 } +simplifyDeriv skol_info user_ctxt tvs theta + = do { let skol_set = mkVarSet tvs -- 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, + -- we are going to wrap the result in an implication with tvs, -- in step [DAC RESIDUAL] - ; (tc_lvl, wanteds) <- pushTcLevelM $ - mapM mk_wanteds thetas + ; (tc_lvl, wanteds) <- captureThetaSpecConstraints user_ctxt theta ; traceTc "simplifyDeriv inputs" $ - vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ] + vcat [ pprTyVars tvs $$ ppr theta $$ ppr wanteds, ppr skol_info ] -- See [STEP DAC SOLVE] -- Simplify the constraints, starting at the same level at which @@ -792,8 +750,7 @@ simplifyDeriv pred tvs thetas -- simplifyInfer) ; (solved_wanteds, _) <- setTcLevel tc_lvl $ runTcS $ - solveWanteds $ - unionsWC wanteds + solveWanteds wanteds -- It's not yet zonked! Obviously zonk it before peering at it ; solved_wanteds <- zonkWC solved_wanteds @@ -817,7 +774,7 @@ simplifyDeriv pred tvs thetas where p = ctPred ct ; traceTc "simplifyDeriv outputs" $ - vcat [ ppr tvs_skols, ppr residual_simple, ppr good ] + vcat [ ppr tvs, ppr residual_simple, ppr good ] -- Return the good unsolved constraints (unskolemizing on the way out.) ; let min_theta = mkMinimalBySCs id (bagToList good) @@ -827,8 +784,6 @@ simplifyDeriv pred tvs thetas -- constraints. -- See Note [Gathering and simplifying constraints for -- DeriveAnyClass] - subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs - -- The reverse substitution (sigh) -- See [STEP DAC RESIDUAL] -- Ensure that min_theta is enough to solve /all/ the constraints in @@ -837,7 +792,7 @@ simplifyDeriv pred tvs thetas -- forall tvs. min_theta => solved_wanteds ; min_theta_vars <- mapM newEvVar min_theta ; (leftover_implic, _) - <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) tvs_skols + <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) tvs min_theta_vars solved_wanteds -- This call to simplifyTop is purely for error reporting -- See Note [Error reporting for deriving clauses] @@ -845,7 +800,7 @@ simplifyDeriv pred tvs thetas -- in this line of code. ; simplifyTopImplic leftover_implic - ; return (substTheta subst_skol min_theta) } + ; return min_theta } {- Note [Overlap and deriving] @@ -869,9 +824,20 @@ of a function 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 +As a result, we use vanilla, non-overlappable skolems when inferring the +context for the derived instances. Hence, we instantiate the type variables +using tcInstSkolTyVars, not tcInstSuperSkolTyVars. + +We do this skolemisation in GHC.Tc.Deriv.mkEqnHelp, a function which occurs +very early in the deriving pipeline, so that by the time GHC needs to infer the +instance context, all of the types in the computed DerivSpec have been +skolemised appropriately. After the instance context inference has completed, +GHC zonks the TcTyVars in the DerivSpec to ensure that types like +a[sk:1] do not appear in -ddump-deriv output. + +All of this is only needed when inferring an instance context, i.e., the +InferContext case. For the SupplyContext case, we don't bother skolemising +at all. Note [Gathering and simplifying constraints for DeriveAnyClass] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -902,7 +868,7 @@ definition for these generic default methods $gdm_bar x y = show x ++ show (range (y,y)) (and similarly for baz). Now consider a 'deriving' clause - data Maybe s = ... deriving Foo + data Maybe s = ... deriving anyclass Foo This derives an instance of the form: instance (CX) => Foo (Maybe s) where @@ -911,14 +877,34 @@ This derives an instance of the form: Now it is GHC's job to fill in a suitable instance context (CX). If GHC were typechecking the binding - bar = $gdm bar + 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) +So that's what we do. Fortunately, there is already functionality within GHC +to that does all of the above—namely, tcSubTypeSigma. In the example above, +we want to use tcSubTypeSigma to check the following subtyping relation: + + forall c. (Show a, Ix c) => Maybe s -> c -> String -- actual type + <= forall b. (Ix b) => Maybe s -> b -> String -- expected type + +That is, we check that the type of $gdm_bar (the actual type) is more +polymorphic than the type of bar (the expected type). We use SubTypePredSpec, +a special form of PredSpec that is only used by DeriveAnyClass, to store +the actual and expected types. + +(Aside: having a separate SubTypePredSpec is not strictly necessary, as we +could theoretically construct this implication constraint by hand and store it +in a SimplePredSpec. In fact, GHC used to do this. However, this is easier +said than done, and there were numerous subtle bugs that resulted from getting +this step wrong, such as #20719. Ultimately, we decided that special-casing a +PredSpec specifically for DeriveAnyClass was worth it.) + +tcSubTypeSigma will ultimately spit out an implication constraint, which will +look something like this (call it C1): forall[2] b. Ix b => (Show (Maybe s), Ix cc, Maybe s -> b -> String @@ -929,14 +915,31 @@ Here: 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'). + of bar. The 'cc' is a unification variable that comes from instantiating the + quantified type variable 'c' in $gdm_bar's type. The finer details of + skolemisation and metavariable instantiation are handled behind the scenes + by tcSubTypeSigma. + +* It is important that `b` be distinct from `cc`. In this example, this is + clearly the case, but it is not always so obvious when the type variables are + hidden behind type synonyms. Suppose the example were written like this, + for example: + + type Method a = forall b. Ix b => a -> b -> String + class Foo a where + bar :: Method a + default bar :: Show a => Method a + bar = ... + + Both method signatures quantify a `b` once the `Method` type synonym is + expanded. To ensure that GHC doesn't confuse the two `b`s during + typechecking, tcSubTypeSigma instantiates the `b` in the original signature + with a fresh skolem and the `b` in the default signature with a fresh + unification variable. Doing so prevents #20719 from happening. + +* The (Ix b) constraint comes from the context of bar's type. The + (Show (Maybe s)) and (Ix cc) constraints come from the context of $gdm_bar's + type. * The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String) comes from marrying up the instantiated type of $gdm_bar with the specified @@ -948,7 +951,7 @@ 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 +Similarly for 'baz', tcSubTypeSigma gives the constraint C2 forall[2]. Eq (Maybe s) => (Ord a, Show a, Maybe s -> Maybe s -> Bool diff --git a/compiler/GHC/Tc/Deriv/Utils.hs b/compiler/GHC/Tc/Deriv/Utils.hs index d25db38be0..aa89f94c4b 100644 --- a/compiler/GHC/Tc/Deriv/Utils.hs +++ b/compiler/GHC/Tc/Deriv/Utils.hs @@ -10,13 +10,15 @@ -- | Error-checking and other utilities for @deriving@ clauses or declarations. module GHC.Tc.Deriv.Utils ( DerivM, DerivEnv(..), - DerivSpec(..), pprDerivSpec, setDerivSpecTheta, + DerivSpec(..), pprDerivSpec, setDerivSpecTheta, zonkDerivSpec, DerivSpecMechanism(..), derivSpecMechanismToStrategy, isDerivSpecStock, - isDerivSpecNewtype, isDerivSpecAnyClass, isDerivSpecVia, + isDerivSpecNewtype, isDerivSpecAnyClass, + isDerivSpecVia, zonkDerivSpecMechanism, DerivContext(..), OriginativeDerivStatus(..), StockGenFns(..), - isStandaloneDeriv, isStandaloneWildcardDeriv, mkDerivOrigin, - PredOrigin(..), ThetaOrigin(..), mkPredOrigin, - mkThetaOrigin, mkThetaOriginFromPreds, substPredOrigin, + isStandaloneDeriv, isStandaloneWildcardDeriv, + askDerivUserTypeCtxt, mkDerivOrigin, + PredSpec(..), ThetaSpec, + mkDirectThetaSpec, substPredSpec, captureThetaSpecConstraints, checkOriginativeSideConditions, hasStockDeriving, std_class_via_coercible, non_coercible_class, newDerivClsInst, extendLocalInstEnv @@ -47,9 +49,12 @@ import GHC.Tc.Deriv.Generate import GHC.Tc.Deriv.Functor import GHC.Tc.Deriv.Generics import GHC.Tc.Errors.Types +import GHC.Tc.Types.Constraint (WantedConstraints, mkNonCanonical) import GHC.Tc.Types.Origin import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcType +import GHC.Tc.Utils.Unify (tcSubTypeSigma) +import GHC.Tc.Utils.Zonk import GHC.Builtin.Names.TH (liftClassKey) import GHC.Core.TyCon import GHC.Core.Type @@ -57,6 +62,7 @@ import GHC.Utils.Misc import GHC.Types.Var.Set import Control.Monad.Trans.Reader +import Data.Foldable (traverse_) import Data.Maybe import qualified GHC.LanguageExtensions as LangExt import GHC.Data.List.SetOps (assocMaybe) @@ -84,6 +90,16 @@ isStandaloneWildcardDeriv = asks (go . denv_ctxt) go (InferContext wildcard) = isJust wildcard go (SupplyContext {}) = False +-- | Return 'InstDeclCtxt' if processing with a standalone @deriving@ +-- declaration or 'DerivClauseCtxt' if processing a @deriving@ clause. +askDerivUserTypeCtxt :: DerivM UserTypeCtxt +askDerivUserTypeCtxt = asks (go . denv_ctxt) + where + go :: DerivContext -> UserTypeCtxt + go (SupplyContext {}) = InstDeclCtxt True + go (InferContext Just{}) = InstDeclCtxt True + go (InferContext Nothing) = DerivClauseCtxt + -- | @'mkDerivOrigin' wc@ returns 'StandAloneDerivOrigin' if @wc@ is 'True', -- and 'DerivClauseOrigin' if @wc@ is 'False'. Useful for error-reporting. mkDerivOrigin :: Bool -> CtOrigin @@ -98,7 +114,13 @@ data DerivEnv = DerivEnv { denv_overlap_mode :: Maybe OverlapMode -- ^ Is this an overlapping instance? , denv_tvs :: [TyVar] - -- ^ Universally quantified type variables in the instance + -- ^ Universally quantified type variables in the instance. If the + -- @denv_ctxt@ is 'InferContext', these will be 'TcTyVar' skolems. + -- If the @denv_ctxt@ is 'SupplyContext', these will be ordinary 'TyVar's. + -- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer". + -- + -- All type variables that appear in the 'denv_inst_tys', 'denv_ctxt', + -- 'denv_skol_info', and 'denv_strat' should come from 'denv_tvs'. , denv_cls :: Class -- ^ Class for which we need to derive an instance , denv_inst_tys :: [Type] @@ -109,6 +131,9 @@ data DerivEnv = DerivEnv -- 'InferContext' for @deriving@ clauses, or for standalone deriving that -- uses a wildcard constraint. -- See @Note [Inferring the instance context]@. + , denv_skol_info :: SkolemInfo + -- ^ The 'SkolemInfo' used to skolemise the @denv_tvs@ in the case where + -- the 'denv_ctxt' is 'InferContext'. , denv_strat :: Maybe (DerivStrategy GhcTc) -- ^ 'Just' if user requests a particular deriving strategy. -- Otherwise, 'Nothing'. @@ -120,6 +145,7 @@ instance Outputable DerivEnv where , denv_cls = cls , denv_inst_tys = inst_tys , denv_ctxt = ctxt + , denv_skol_info = skol_info , denv_strat = mb_strat }) = hang (text "DerivEnv") 2 (vcat [ text "denv_overlap_mode" <+> ppr overlap_mode @@ -127,6 +153,7 @@ instance Outputable DerivEnv where , text "denv_cls" <+> ppr cls , text "denv_inst_tys" <+> ppr inst_tys , text "denv_ctxt" <+> ppr ctxt + , text "denv_skol_info" <+> ppr skol_info , text "denv_strat" <+> ppr mb_strat ]) data DerivSpec theta = DS { ds_loc :: SrcSpan @@ -135,6 +162,8 @@ data DerivSpec theta = DS { ds_loc :: SrcSpan , ds_theta :: theta , ds_cls :: Class , ds_tys :: [Type] + , ds_skol_info :: SkolemInfo + , ds_user_ctxt :: UserTypeCtxt , ds_overlap :: Maybe OverlapMode , ds_standalone_wildcard :: Maybe SrcSpan -- See Note [Inferring the instance context] @@ -143,11 +172,20 @@ data DerivSpec theta = DS { ds_loc :: SrcSpan -- This spec implies a dfun declaration of the form -- df :: forall tvs. theta => C tys -- The Name is the name for the DFun we'll build - -- The tyvars bind all the variables in the theta + -- The tyvars bind all the variables in the rest of the DerivSpec. + -- If we are inferring an instance context, the tyvars will be TcTyVar + -- skolems. After the instance context inference is over, the tyvars + -- will be zonked to TyVars. See + -- Note [Overlap and deriving] in GHC.Tc.Deriv.Infer. -- the theta is either the given and final theta, in standalone deriving, -- or the not-yet-simplified list of constraints together with their origin + -- The ds_skol_info is the SkolemInfo that was used to skolemise the + -- TcTyVars (if we are inferring an instance context). The ds_user_ctxt + -- is the UserTypeCtxt that allows error messages to know if we are in + -- a deriving clause or a standalone deriving declaration. + -- ds_mechanism specifies the means by which GHC derives the instance. -- See Note [Deriving strategies] in GHC.Tc.Deriv @@ -165,7 +203,7 @@ Example: pprDerivSpec :: Outputable theta => DerivSpec theta -> SDoc pprDerivSpec (DS { ds_loc = l, ds_name = n, ds_tvs = tvs, ds_cls = c, - ds_tys = tys, ds_theta = rhs, + ds_tys = tys, ds_theta = rhs, ds_skol_info = skol_info, ds_standalone_wildcard = wildcard, ds_mechanism = mech }) = hang (text "DerivSpec") 2 (vcat [ text "ds_loc =" <+> ppr l @@ -174,6 +212,7 @@ pprDerivSpec (DS { ds_loc = l, ds_name = n, ds_tvs = tvs, ds_cls = c, , text "ds_cls =" <+> ppr c , text "ds_tys =" <+> ppr tys , text "ds_theta =" <+> ppr rhs + , text "ds_skol_info =" <+> ppr skol_info , text "ds_standalone_wildcard =" <+> ppr wildcard , text "ds_mechanism =" <+> ppr mech ]) @@ -184,6 +223,24 @@ instance Outputable theta => Outputable (DerivSpec theta) where setDerivSpecTheta :: theta' -> DerivSpec theta -> DerivSpec theta' setDerivSpecTheta theta ds = ds{ds_theta = theta} +-- | Zonk the 'TcTyVar's in a 'DerivSpec' to 'TyVar's. +-- See @Note [What is zonking?]@ in "GHC.Tc.Utils.TcMType". +-- +-- This is only used in the final zonking step when inferring +-- the context for a derived instance. +-- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer". +zonkDerivSpec :: DerivSpec ThetaType -> TcM (DerivSpec ThetaType) +zonkDerivSpec ds@(DS { ds_tvs = tvs, ds_theta = theta + , ds_tys = tys, ds_mechanism = mechanism + }) = do + (ze, tvs') <- zonkTyBndrs tvs + theta' <- zonkTcTypesToTypesX ze theta + tys' <- zonkTcTypesToTypesX ze tys + mechanism' <- zonkDerivSpecMechanism ze mechanism + pure ds{ ds_tvs = tvs', ds_theta = theta' + , ds_tys = tys', ds_mechanism = mechanism' + } + -- | What action to take in order to derive a class instance. -- See @Note [DerivEnv and DerivSpecMechanism]@, as well as -- @Note [Deriving strategies]@ in "GHC.Tc.Deriv". @@ -243,6 +300,44 @@ isDerivSpecAnyClass _ = False isDerivSpecVia (DerivSpecVia{}) = True isDerivSpecVia _ = False +-- | Zonk the 'TcTyVar's in a 'DerivSpecMechanism' to 'TyVar's. +-- See @Note [What is zonking?]@ in "GHC.Tc.Utils.TcMType". +-- +-- This is only used in the final zonking step when inferring +-- the context for a derived instance. +-- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer". +zonkDerivSpecMechanism :: ZonkEnv -> DerivSpecMechanism -> TcM DerivSpecMechanism +zonkDerivSpecMechanism ze mechanism = + case mechanism of + DerivSpecStock { dsm_stock_dit = dit + , dsm_stock_gen_fns = gen_fns + } -> do + dit' <- zonkDerivInstTys ze dit + pure $ DerivSpecStock { dsm_stock_dit = dit' + , dsm_stock_gen_fns = gen_fns + } + DerivSpecNewtype { dsm_newtype_dit = dit + , dsm_newtype_rep_ty = rep_ty + } -> do + dit' <- zonkDerivInstTys ze dit + rep_ty' <- zonkTcTypeToTypeX ze rep_ty + pure $ DerivSpecNewtype { dsm_newtype_dit = dit' + , dsm_newtype_rep_ty = rep_ty' + } + DerivSpecAnyClass -> + pure DerivSpecAnyClass + DerivSpecVia { dsm_via_cls_tys = cls_tys + , dsm_via_inst_ty = inst_ty + , dsm_via_ty = via_ty + } -> do + cls_tys' <- zonkTcTypesToTypesX ze cls_tys + inst_ty' <- zonkTcTypeToTypeX ze inst_ty + via_ty' <- zonkTcTypeToTypeX ze via_ty + pure $ DerivSpecVia { dsm_via_cls_tys = cls_tys' + , dsm_via_inst_ty = inst_ty' + , dsm_via_ty = via_ty' + } + instance Outputable DerivSpecMechanism where ppr (DerivSpecStock{dsm_stock_dit = dit}) = hang (text "DerivSpecStock") @@ -446,34 +541,43 @@ data StockGenFns = StockGenFns -- otherwise knows how to generate code for (possibly requiring the use of a -- language extension), such as Eq, Ord, Ix, Data, Generic, etc.) --- | A 'PredType' annotated with the origin of the constraint 'CtOrigin', --- and whether or the constraint deals in types or kinds. -data PredOrigin = PredOrigin PredType CtOrigin TypeOrKind +-- | A 'PredSpec' specifies a constraint to emitted when inferring the +-- instance context for a derived instance in 'GHC.Tc.Deriv.simplifyInfer'. +data PredSpec + = -- | An ordinary 'PredSpec' that directly stores a 'PredType', which + -- will be emitted as a wanted constraint in the constraint solving + -- machinery. This is the simple case, as there are no skolems, + -- metavariables, or given constraints involved. + SimplePredSpec + { sps_pred :: TcPredType + -- ^ The constraint to emit as a wanted + , sps_origin :: CtOrigin + -- ^ The origin of the constraint + , sps_type_or_kind :: TypeOrKind + -- ^ Whether the constraint is a type or kind + } + | -- | A special 'PredSpec' that is only used by @DeriveAnyClass@. This + -- will check if @stps_ty_actual@ is a subtype of (i.e., more polymorphic + -- than) @stps_ty_expected@ in the constraint solving machinery, emitting an + -- implication constraint as a side effect. For more details on how this + -- works, see @Note [Gathering and simplifying constraints for DeriveAnyClass]@ + -- in "GHC.Tc.Deriv.Infer". + SubTypePredSpec + { stps_ty_actual :: TcSigmaType + -- ^ The actual type. In the context of @DeriveAnyClass@, this is the + -- default method type signature. + , stps_ty_expected :: TcSigmaType + -- ^ The expected type. In the context of @DeriveAnyClass@, this is the + -- original method type signature. + , stps_origin :: CtOrigin + -- ^ The origin of the constraint + } --- | A list of wanted 'PredOrigin' constraints ('to_wanted_origins') to --- simplify when inferring a derived instance's context. These are used in all --- deriving strategies, but in the particular case of @DeriveAnyClass@, we --- need extra information. In particular, we need: --- --- * 'to_anyclass_skols', the list of type variables bound by a class method's --- regular type signature, which should be rigid. --- --- * 'to_anyclass_metas', the list of type variables bound by a class method's --- default type signature. These can be unified as necessary. --- --- * 'to_anyclass_givens', the list of constraints from a class method's --- regular type signature, which can be used to help solve constraints --- in the 'to_wanted_origins'. --- --- (Note that 'to_wanted_origins' will likely contain type variables from the --- derived type class or data type, neither of which will appear in --- 'to_anyclass_skols' or 'to_anyclass_metas'.) --- --- For all other deriving strategies, it is always the case that --- 'to_anyclass_skols', 'to_anyclass_metas', and 'to_anyclass_givens' are --- empty. --- --- Here is an example to illustrate this: +-- | A list of 'PredSpec' constraints to simplify when inferring a +-- derived instance's context. For the @stock@, @newtype@, and @via@ deriving +-- strategies, these will consist of 'SimplePredSpec's, and for +-- @DeriveAnyClass@, these will consist of 'SubTypePredSpec's. Here is an +-- example to illustrate the latter: -- -- @ -- class Foo a where @@ -488,75 +592,119 @@ data PredOrigin = PredOrigin PredType CtOrigin TypeOrKind -- data Quux q = Quux deriving anyclass Foo -- @ -- --- Then it would generate two 'ThetaOrigin's, one for each method: +-- Then it would generate two 'SubTypePredSpec's, one for each method: -- -- @ --- [ ThetaOrigin { to_anyclass_skols = [b] --- , to_anyclass_metas = [y] --- , to_anyclass_givens = [Ix b] --- , to_wanted_origins = [ Show (Quux q), Ix y --- , (Quux q -> b -> String) ~ --- (Quux q -> y -> String) --- ] } --- , ThetaOrigin { to_anyclass_skols = [] --- , to_anyclass_metas = [] --- , to_anyclass_givens = [Eq (Quux q)] --- , to_wanted_origins = [ Ord (Quux q) --- , (Quux q -> Quux q -> Bool) ~ --- (Quux q -> Quux q -> Bool) --- ] } +-- [ SubTypePredSpec +-- { stps_ty_actual = forall y. (Show (Quux q), Ix y) => Quux q -> y -> String +-- , stps_ty_expected = forall b. (Ix b) => Quux q -> b -> String +-- , stps_ty_origin = DerivClauseCtxt +-- } +-- , SubTypePredSpec +-- { stps_ty_actual = Ord (Quux q) => Quux q -> Quux q -> Bool +-- , stps_ty_expected = Eq (Quux q) => Quux q -> Quux q -> Bool +-- , stps_ty_origin = DerivClauseCtxt +-- } -- ] -- @ -- -- (Note that the type variable @q@ is bound by the data type @Quux@, and thus --- it appears in neither 'to_anyclass_skols' nor 'to_anyclass_metas'.) +-- appears free in the 'stps_ty_actual's and 'stps_ty_expected's.) -- -- See @Note [Gathering and simplifying constraints for DeriveAnyClass]@ --- in "GHC.Tc.Deriv.Infer" for an explanation of how 'to_wanted_origins' are --- determined in @DeriveAnyClass@, as well as how 'to_anyclass_skols', --- 'to_anyclass_metas', and 'to_anyclass_givens' are used. -data ThetaOrigin - = ThetaOrigin { to_anyclass_skols :: [TyVar] - , to_anyclass_metas :: [TyVar] - , to_anyclass_givens :: ThetaType - , to_wanted_origins :: [PredOrigin] } - -instance Outputable PredOrigin where - ppr (PredOrigin ty _ _) = ppr ty -- The origin is not so interesting when debugging - -instance Outputable ThetaOrigin where - ppr (ThetaOrigin { to_anyclass_skols = ac_skols - , to_anyclass_metas = ac_metas - , to_anyclass_givens = ac_givens - , to_wanted_origins = wanted_origins }) - = hang (text "ThetaOrigin") - 2 (vcat [ text "to_anyclass_skols =" <+> ppr ac_skols - , text "to_anyclass_metas =" <+> ppr ac_metas - , text "to_anyclass_givens =" <+> ppr ac_givens - , text "to_wanted_origins =" <+> ppr wanted_origins ]) - -mkPredOrigin :: CtOrigin -> TypeOrKind -> PredType -> PredOrigin -mkPredOrigin origin t_or_k pred = PredOrigin pred origin t_or_k - -mkThetaOrigin :: CtOrigin -> TypeOrKind - -> [TyVar] -> [TyVar] -> ThetaType -> ThetaType - -> ThetaOrigin -mkThetaOrigin origin t_or_k skols metas givens wanteds - = ThetaOrigin { to_anyclass_skols = skols - , to_anyclass_metas = metas - , to_anyclass_givens = givens - , to_wanted_origins = map (mkPredOrigin origin t_or_k) wanteds } - --- A common case where the ThetaOrigin only contains wanted constraints, with --- no givens or locally scoped type variables. -mkThetaOriginFromPreds :: [PredOrigin] -> ThetaOrigin -mkThetaOriginFromPreds origins - = ThetaOrigin { to_anyclass_skols = [], to_anyclass_metas = [] - , to_anyclass_givens = [], to_wanted_origins = origins } - -substPredOrigin :: HasCallStack => TCvSubst -> PredOrigin -> PredOrigin -substPredOrigin subst (PredOrigin pred origin t_or_k) - = PredOrigin (substTy subst pred) origin t_or_k +-- in "GHC.Tc.Deriv.Infer" for an explanation of how these 'SubTypePredSpec's +-- are used to compute implication constraints. +type ThetaSpec = [PredSpec] + +instance Outputable PredSpec where + ppr (SimplePredSpec{sps_pred = ty}) = + hang (text "SimplePredSpec") + 2 (vcat [ text "sps_pred" <+> ppr ty ]) + ppr (SubTypePredSpec { stps_ty_actual = ty_actual + , stps_ty_expected = ty_expected }) = + hang (text "SubTypePredSpec") + 2 (vcat [ text "stps_ty_actual" <+> ppr ty_actual + , text "stps_ty_expected" <+> ppr ty_expected + ]) + +-- | Build a list of 'SimplePredSpec's, using the supplied 'CtOrigin' and +-- 'TypeOrKind' values for each 'PredType'. +mkDirectThetaSpec :: CtOrigin -> TypeOrKind -> ThetaType -> ThetaSpec +mkDirectThetaSpec origin t_or_k = + map (\p -> SimplePredSpec + { sps_pred = p + , sps_origin = origin + , sps_type_or_kind = t_or_k + }) + +substPredSpec :: HasCallStack => TCvSubst -> PredSpec -> PredSpec +substPredSpec subst ps = + case ps of + SimplePredSpec { sps_pred = pred + , sps_origin = origin + , sps_type_or_kind = t_or_k + } + -> SimplePredSpec { sps_pred = substTy subst pred + , sps_origin = origin + , sps_type_or_kind = t_or_k + } + + SubTypePredSpec { stps_ty_actual = ty_actual + , stps_ty_expected = ty_expected + , stps_origin = origin + } + -> SubTypePredSpec { stps_ty_actual = substTy subst ty_actual + , stps_ty_expected = substTy subst ty_expected + , stps_origin = origin + } + +-- | Capture wanted constraints from a 'ThetaSpec'. +captureThetaSpecConstraints :: + UserTypeCtxt -- ^ Used to inform error messages as to whether + -- we are in a @deriving@ clause or a standalone + -- @deriving@ declaration + -> ThetaSpec -- ^ The specs from which constraints will be created + -> TcM (TcLevel, WantedConstraints) +captureThetaSpecConstraints user_ctxt theta = + pushTcLevelM $ mk_wanteds theta + where + -- Create the constraints we need to solve. For stock and newtype + -- deriving, these constraints will be simple wanted constraints + -- like (C a, Ord b). + -- But with DeriveAnyClass, we make an implication constraint. + -- See Note [Gathering and simplifying constraints for DeriveAnyClass] + -- in GHC.Tc.Deriv.Infer. + mk_wanteds :: ThetaSpec -> TcM WantedConstraints + mk_wanteds preds + = do { (_, wanteds) <- captureConstraints $ + traverse_ emit_constraints preds + ; pure wanteds } + + -- Emit the appropriate constraints depending on what sort of + -- PredSpec we are dealing with. + emit_constraints :: PredSpec -> TcM () + emit_constraints ps = + case ps of + -- For constraints like (C a, Ord b), emit the + -- constraints directly as simple wanted constraints. + SimplePredSpec { sps_pred = wanted + , sps_origin = orig + , sps_type_or_kind = t_or_k + } -> do + ev <- newWanted orig (Just t_or_k) wanted + emitSimple (mkNonCanonical ev) + + -- For DeriveAnyClass, check if ty_actual is a subtype of + -- ty_expected, which emits an implication constraint as a + -- side effect. See + -- Note [Gathering and simplifying constraints for DeriveAnyClass]. + -- in GHC.Tc.Deriv.Infer. + SubTypePredSpec { stps_ty_actual = ty_actual + , stps_ty_expected = ty_expected + , stps_origin = orig + } -> do + _ <- tcSubTypeSigma orig user_ctxt ty_actual ty_expected + return () {- ************************************************************************ diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 2db40c7f7c..f5a1c6ab17 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -121,7 +121,6 @@ import GHC.Data.Bag import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Utils.Constants (debugIsOn) -import GHC.Utils.Trace import Data.Coerce import Data.Monoid ( Endo(..) ) @@ -1539,9 +1538,7 @@ check_implic implic@(Implic { ic_tclvl = lvl check :: TcTyVar -> Maybe SDoc check tv | not (isTcTyVar tv) - = pprTrace "checkImplicationInvariants: not TcTyVar" (ppr tv) Nothing - -- Happens in 'deriving' code so I am punting for now - -- Just (ppr tv <+> text "is not a TcTyVar") + = Just (ppr tv <+> text "is not a TcTyVar") | otherwise = check_details tv (tcTyVarDetails tv) |