From 28dd52eec98e50c711cd00df22f6ab9e054c8b75 Mon Sep 17 00:00:00 2001 From: sheaf <sam.derbyshire@gmail.com> Date: Thu, 3 Aug 2023 14:54:11 +0200 Subject: [PATCH] Unused tyvars in FamInst: only report user tyvars This commit changes how we perform some validity checking for coercion axioms to mirror how we handle default declarations for associated type families. This allows us to keep track of whether type variables in type and data family instances were user-written or not, in order to only report the user-written ones in "unused type variable" error messages. Consider for example: {-# LANGUAGE PolyKinds #-} type family F type instance forall a. F = () In this case, we get two quantified type variables, (k :: Type) and (a :: k); the second being user-written, but the first is introduced by the typechecker. We should only report 'a' as being unused, as the user has no idea what 'k' is. Fixes #23734 --- compiler/GHC/Core/Class.hs | 67 +++++---- compiler/GHC/Core/Coercion/Axiom.hs | 44 +++--- compiler/GHC/IfaceToCore.hs | 2 +- compiler/GHC/Tc/Deriv/Generate.hs | 4 +- compiler/GHC/Tc/TyCl.hs | 135 +++++++++++------- compiler/GHC/Tc/TyCl/Build.hs | 1 - compiler/GHC/Tc/TyCl/Instance.hs | 39 ++--- compiler/GHC/Tc/Validity.hs | 58 +++++--- compiler/GHC/Tc/Zonk/Type.hs | 2 +- .../should_fail/ExplicitForAllFams4b.stderr | 24 ++-- .../indexed-types/should_fail/T17008a.stderr | 4 +- .../tests/typecheck/should_fail/T23734.hs | 2 +- .../tests/typecheck/should_fail/T23734.stderr | 22 +++ testsuite/tests/typecheck/should_fail/all.T | 1 + 14 files changed, 261 insertions(+), 144 deletions(-) create mode 100644 testsuite/tests/typecheck/should_fail/T23734.stderr diff --git a/compiler/GHC/Core/Class.hs b/compiler/GHC/Core/Class.hs index 3c3f0a1db62f..ffadf0e4b9f9 100644 --- a/compiler/GHC/Core/Class.hs +++ b/compiler/GHC/Core/Class.hs @@ -8,7 +8,7 @@ module GHC.Core.Class ( Class, ClassOpItem, - ClassATItem(..), ATValidityInfo(..), + ClassATItem(..), TyFamEqnValidityInfo(..), ClassMinimalDef, DefMethInfo, pprDefMethInfo, @@ -33,6 +33,7 @@ import GHC.Types.Unique import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Types.SrcLoc +import GHC.Types.Var.Set import GHC.Utils.Outputable import GHC.Data.BooleanFormula (BooleanFormula, mkTrue) @@ -95,29 +96,42 @@ type DefMethInfo = Maybe (Name, DefMethSpec Type) data ClassATItem = ATI TyCon -- See Note [Associated type tyvar names] - (Maybe (Type, ATValidityInfo)) - -- Default associated type (if any) from this template - -- Note [Associated type defaults] - --- | Information about an associated type family default implementation. This --- is used solely for validity checking. + (Maybe (Type, TyFamEqnValidityInfo)) + -- ^ Default associated type (if any) from this template. + -- + -- As per Note [Associated type defaults], the Type has been renamed + -- to use the class tyvars, while the 'TyFamEqnValidityInfo' uses + -- the original user-written type variables. + +-- | Information about a type family equation, used for validity checking +-- of closed type family equations and associated type family default equations. +-- +-- This type exists to delay validity-checking after typechecking type declaration +-- groups, to avoid cyclic evaluation inside the typechecking knot. +-- -- See @Note [Type-checking default assoc decls]@ in "GHC.Tc.TyCl". -data ATValidityInfo - -- | Used for associated type families that are imported - -- from another module, for which we don't need to - -- perform any validity checking. - = NoATVI - - -- | Used for locally-defined associated type families. - | ATVI - { atvi_loc :: SrcSpan - , atvi_qtvs :: [TyVar] +data TyFamEqnValidityInfo + -- | Used for equations which don't need any validity checking, + -- for example equations imported from another module. + = NoVI + + -- | Information necessary for validity checking of a type family equation. + | VI + { vi_loc :: SrcSpan + , vi_qtvs :: [TcTyVar] -- ^ LHS quantified type variables - , atvi_pats :: [Type] + , vi_non_user_tvs :: TyVarSet + -- ^ non-user-written type variables (for error message reporting) + -- + -- Example: with -XPolyKinds, typechecking @type instance forall a. F = ()@ + -- introduces the kind variable @k@ for the kind of @a@. See #23734. + , vi_pats :: [Type] -- ^ LHS patterns - , atvi_rhs :: Type - -- ^ original RHS of the type family default declaration, - -- before applying the substitution from + , vi_rhs :: Type + -- ^ RHS of the equation + -- + -- NB: for associated type family default declarations, this is the RHS + -- *before* applying the substitution from -- Note [Type-checking default assoc decls] in GHC.Tc.TyCl. } @@ -176,9 +190,14 @@ Note that * HOWEVER, in the internal ClassATItem we rename the RHS to match the tyConTyVars of the family TyCon. So in the example above we'd get a ClassATItem of - ATI F ((x,a) -> b) - So the tyConTyVars of the family TyCon bind the free vars of - the default Type rhs + + ATI F (Just ((x,a) -> b, validity_info) + + That is, the type stored in the first component of the pair has been + renamed to use the class type variables. On the other hand, the + TyFamEqnValidityInfo, used for validity checking of the type family equation + (considered as a free-standing equation) uses the original types, e.g. + involving the type variables 'p', 'q', 'r'. The @mkClass@ function fills in the indirect superclasses. diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs index c06af227ab79..bc2abf11b0ad 100644 --- a/compiler/GHC/Core/Coercion/Axiom.hs +++ b/compiler/GHC/Core/Coercion/Axiom.hs @@ -235,25 +235,35 @@ data CoAxiom br -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1. } +-- | A branch of a coercion axiom, which provides the evidence for +-- unwrapping a newtype or a type-family reduction step using a single equation. data CoAxBranch = CoAxBranch - { cab_loc :: SrcSpan -- Location of the defining equation - -- See Note [CoAxiom locations] - , cab_tvs :: [TyVar] -- Bound type variables; not necessarily fresh - -- See Note [CoAxBranch type variables] - , cab_eta_tvs :: [TyVar] -- Eta-reduced tyvars - -- cab_tvs and cab_lhs may be eta-reduced; see - -- Note [Eta reduction for data families] - , cab_cvs :: [CoVar] -- Bound coercion variables - -- Always empty, for now. - -- See Note [Constraints in patterns] - -- in GHC.Tc.TyCl - , cab_roles :: [Role] -- See Note [CoAxBranch roles] - , cab_lhs :: [Type] -- Type patterns to match against - , cab_rhs :: Type -- Right-hand side of the equality - -- See Note [CoAxioms are homogeneous] - , cab_incomps :: [CoAxBranch] -- The previous incompatible branches - -- See Note [Storing compatibility] + { cab_loc :: SrcSpan + -- ^ Location of the defining equation + -- See Note [CoAxiom locations] + , cab_tvs :: [TyVar] + -- ^ Bound type variables; not necessarily fresh + -- See Note [CoAxBranch type variables] + , cab_eta_tvs :: [TyVar] + -- ^ Eta-reduced tyvars + -- cab_tvs and cab_lhs may be eta-reduced; see + -- Note [Eta reduction for data families] + , cab_cvs :: [CoVar] + -- ^ Bound coercion variables + -- Always empty, for now. + -- See Note [Constraints in patterns] + -- in GHC.Tc.TyCl + , cab_roles :: [Role] + -- ^ See Note [CoAxBranch roles] + , cab_lhs :: [Type] + -- ^ Type patterns to match against + , cab_rhs :: Type + -- ^ Right-hand side of the equality + -- See Note [CoAxioms are homogeneous] + , cab_incomps :: [CoAxBranch] + -- ^ The previous incompatible branches + -- See Note [Storing compatibility] } deriving Data.Data diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs index a678d5995023..c51849029ca0 100644 --- a/compiler/GHC/IfaceToCore.hs +++ b/compiler/GHC/IfaceToCore.hs @@ -825,7 +825,7 @@ tc_iface_decl _parent ignore_prags Just def -> forkM (mk_at_doc tc) $ extendIfaceTyVarEnv (tyConTyVars tc) $ do { tc_def <- tcIfaceType def - ; return (Just (tc_def, NoATVI)) } + ; return (Just (tc_def, NoVI)) } -- Must be done lazily in case the RHS of the defaults mention -- the type constructor being defined here -- e.g. type AT a; type AT b = AT [b] #8002 diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs index 5e6ab56609d6..8b6d08cf2f79 100644 --- a/compiler/GHC/Tc/Deriv/Generate.hs +++ b/compiler/GHC/Tc/Deriv/Generate.hs @@ -52,7 +52,7 @@ import GHC.Tc.Utils.Instantiate( newFamInst ) import GHC.Tc.Utils.Env import GHC.Tc.Utils.TcType import GHC.Tc.Zonk.Type -import GHC.Tc.Validity ( checkValidCoAxBranch ) +import GHC.Tc.Validity import GHC.Core.DataCon import GHC.Core.FamInstEnv @@ -71,6 +71,7 @@ import GHC.Types.SrcLoc import GHC.Types.Unique.FM ( lookupUFM, listToUFM ) import GHC.Types.Var.Env import GHC.Types.Var +import GHC.Types.Var.Set import GHC.Builtin.Names import GHC.Builtin.Names.TH @@ -2084,6 +2085,7 @@ gen_Newtype_fam_insts loc' cls inst_tvs inst_tys rhs_ty rep_lhs_tys let axiom = mkSingleCoAxiom Nominal rep_tc_name rep_tvs' [] rep_cvs' fam_tc rep_lhs_tys rep_rhs_ty + checkFamPatBinders fam_tc (rep_tvs' ++ rep_cvs') emptyVarSet rep_lhs_tys rep_rhs_ty -- Check (c) from Note [GND and associated type families] in GHC.Tc.Deriv checkValidCoAxBranch fam_tc (coAxiomSingleBranch axiom) newFamInst SynFamilyInst axiom diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 54bda8928208..554d0acde4ec 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -110,6 +110,7 @@ import Data.Functor.Identity import Data.List ( partition) import Data.List.NonEmpty ( NonEmpty(..) ) import qualified Data.List.NonEmpty as NE +import Data.Traversable ( for ) import Data.Tuple( swap ) {- @@ -195,12 +196,13 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds -- Step 1: Typecheck the standalone kind signatures and type/class declarations ; traceTc "---- tcTyClGroup ---- {" empty ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds)) - ; (tyclss, data_deriv_info, kindless) <- + ; (tyclss_with_validity_infos, data_deriv_info, kindless) <- tcExtendKindEnv (mkPromotionErrorEnv tyclds) $ -- See Note [Type environment evolution] do { kisig_env <- mkNameEnv <$> traverse tcStandaloneKindSig kisigs ; tcTyClDecls tyclds kisig_env role_annots } - + ; let tyclss = map fst tyclss_with_validity_infos -- Step 1.5: Make sure we don't have any type synonym cycles + ; traceTc "Starting synonym cycle check" (ppr tyclss) ; home_unit <- hsc_home_unit <$> getTopEnv ; checkSynCycles (homeUnitAsUnit home_unit) tyclss tyclds @@ -215,7 +217,11 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds -- NB: put the TyCons in the environment for validity checking, -- as we might look them up in checkTyConConsistentWithBoot. -- See Note [TyCon boot consistency checking]. - concatMapM checkValidTyCl tyclss + fmap concat . for tyclss_with_validity_infos $ \ (tycls, ax_validity_infos) -> + do { tcAddFamInstCtxt (text "type family") (tyConName tycls) $ + tcAddClosedTypeFamilyDeclCtxt tycls $ + mapM_ (checkTyFamEqnValidityInfo tycls) ax_validity_infos + ; checkValidTyCl tycls } ; traceTc "Done validity check" (ppr tyclss) ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss @@ -246,7 +252,7 @@ tcTyClDecls :: [LTyClDecl GhcRn] -> KindSigEnv -> RoleAnnotEnv - -> TcM ([TyCon], [DerivInfo], NameSet) + -> TcM ([(TyCon, [TyFamEqnValidityInfo])], [DerivInfo], NameSet) tcTyClDecls tyclds kisig_env role_annots = do { -- Step 1: kind-check this group and returns the final -- (possibly-polymorphic) kind of each TyCon and Class @@ -266,10 +272,11 @@ tcTyClDecls tyclds kisig_env role_annots -- NB: We have to be careful here to NOT eagerly unfold -- type synonyms, as we have not tested for type synonym -- loops yet and could fall into a black hole. - ; fixM $ \ ~(rec_tyclss, _, _) -> do + ; fixM $ \ ~(rec_tyclss_with_validity_infos, _, _) -> do { tcg_env <- getGblEnv -- Forced so we don't retain a reference to the TcGblEnv ; let !src = tcg_src tcg_env + rec_tyclss = map fst rec_tyclss_with_validity_infos roles = inferRoles src role_annots rec_tyclss -- Populate environment with knot-tied ATyCon for TyCons @@ -2522,23 +2529,26 @@ The IRs are already well-equipped to handle unlifted types, and unlifted datatypes are just a new sub-class thereof. -} -tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM (TyCon, [DerivInfo]) +tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM ((TyCon, [TyFamEqnValidityInfo]), [DerivInfo]) tcTyClDecl roles_info (L loc decl) | Just thing <- wiredInNameTyThing_maybe (tcdName decl) = case thing of -- See Note [Declarations for wired-in things] - ATyCon tc -> return (tc, wiredInDerivInfo tc decl) + ATyCon tc -> return ((tc, []), wiredInDerivInfo tc decl) _ -> pprPanic "tcTyClDecl" (ppr thing) | otherwise = setSrcSpanA loc $ tcAddDeclCtxt decl $ do { traceTc "---- tcTyClDecl ---- {" (ppr decl) - ; (tc, deriv_infos) <- tcTyClDecl1 Nothing roles_info decl + ; (tc_vi@(tc, _), deriv_infos) <- tcTyClDecl1 Nothing roles_info decl ; traceTc "---- tcTyClDecl end ---- }" (ppr tc) - ; return (tc, deriv_infos) } + ; return (tc_vi, deriv_infos) } noDerivInfos :: a -> (a, [DerivInfo]) noDerivInfos a = (a, []) +noEqnValidityInfos :: a -> (a, [TyFamEqnValidityInfo]) +noEqnValidityInfos a = (a, []) + wiredInDerivInfo :: TyCon -> TyClDecl GhcRn -> [DerivInfo] wiredInDerivInfo tycon decl | DataDecl { tcdDataDefn = dataDefn } <- decl @@ -2553,7 +2563,7 @@ wiredInDerivInfo tycon decl wiredInDerivInfo _ _ = [] -- "type family" declarations -tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM (TyCon, [DerivInfo]) +tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM ((TyCon, [TyFamEqnValidityInfo]), [DerivInfo]) tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd }) = fmap noDerivInfos $ tcFamDecl1 parent fd @@ -2563,7 +2573,7 @@ tcTyClDecl1 _parent roles_info (SynDecl { tcdLName = L _ tc_name , tcdRhs = rhs }) = assert (isNothing _parent ) - fmap noDerivInfos $ + fmap ( noDerivInfos . noEqnValidityInfos ) $ tcTySynRhs roles_info tc_name rhs -- "data/newtype" declaration @@ -2571,6 +2581,7 @@ tcTyClDecl1 _parent roles_info decl@(DataDecl { tcdLName = L _ tc_name , tcdDataDefn = defn }) = assert (isNothing _parent) $ + fmap (\(tc, deriv_info) -> ((tc, []), deriv_info)) $ tcDataDefn (tcMkDeclCtxt decl) roles_info tc_name defn tcTyClDecl1 _parent roles_info @@ -2584,7 +2595,7 @@ tcTyClDecl1 _parent roles_info = assert (isNothing _parent) $ do { clas <- tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs - ; return (noDerivInfos (classTyCon clas)) } + ; return (noDerivInfos $ noEqnValidityInfos (classTyCon clas)) } {- ********************************************************************* @@ -2672,13 +2683,13 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs {- Note [Associated type defaults] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - The following is an example of associated type defaults: - class C a where - data D a - type F a b :: * - type F a b = [a] -- Default + class C a where + data D a + + type F a b :: * + type F a b = [a] -- Default Note that we can get default definitions only for type families, not data families. @@ -2713,7 +2724,8 @@ tcClassATs class_name cls ats at_defs (at_def_tycon at_def) [at_def]) emptyNameEnv at_defs - tc_at at = do { fam_tc <- addLocMA (tcFamDecl1 (Just cls)) at + tc_at at = do { (fam_tc, val_infos) <- addLocMA (tcFamDecl1 (Just cls)) at + ; mapM_ (checkTyFamEqnValidityInfo fam_tc) val_infos ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at) `orElse` [] ; atd <- tcDefaultAssocDecl fam_tc at_defs @@ -2721,9 +2733,9 @@ tcClassATs class_name cls ats at_defs ------------------------- tcDefaultAssocDecl :: - TyCon -- ^ Family TyCon (not knot-tied) - -> [LTyFamDefltDecl GhcRn] -- ^ Defaults - -> TcM (Maybe (KnotTied Type, ATValidityInfo)) -- ^ Type checked RHS + TyCon -- ^ Family TyCon (not knot-tied) + -> [LTyFamDefltDecl GhcRn] -- ^ Defaults + -> TcM (Maybe (KnotTied Type, TyFamEqnValidityInfo)) -- ^ Type checked RHS tcDefaultAssocDecl _ [] = return Nothing -- No default declaration @@ -2763,8 +2775,9 @@ tcDefaultAssocDecl fam_tc -- at an associated type. But this would be wrong, because an associated -- type default LHS can mention *different* type variables than the -- enclosing class. So it's treated more as a freestanding beast. - ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc NotAssociated - outer_bndrs hs_pats hs_rhs_ty + ; (qtvs, non_user_tvs, pats, rhs_ty) + <- tcTyFamInstEqnGuts fam_tc NotAssociated + outer_bndrs hs_pats hs_rhs_ty ; let fam_tvs = tyConTyVars fam_tc ; traceTc "tcDefaultAssocDecl 2" (vcat @@ -2784,7 +2797,12 @@ tcDefaultAssocDecl fam_tc -- over later, in GHC.Tc.Validity.checkValidAssocTyFamDeflt. -- See Note [Type-checking default assoc decls]. - ; pure $ Just (substTyUnchecked subst rhs_ty, ATVI (locA loc) qtvs pats rhs_ty) + ; pure $ Just ( substTyUnchecked subst rhs_ty + , VI { vi_loc = locA loc + , vi_qtvs = qtvs + , vi_non_user_tvs = non_user_tvs + , vi_pats = pats + , vi_rhs = rhs_ty } ) -- We perform checks for well-formedness and validity later, in -- GHC.Tc.Validity.checkValidAssocTyFamDeflt. } @@ -2887,7 +2905,7 @@ any damage is done. * * ********************************************************************* -} -tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon +tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM (TyCon, [TyFamEqnValidityInfo]) tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info , fdLName = tc_lname@(L _ tc_name) , fdResultSig = L _ sig @@ -2916,7 +2934,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info (resultVariableName sig) (DataFamilyTyCon tc_rep_name) parent inj - ; return tycon } + ; return (tycon, []) } | OpenTypeFamily <- fam_info = bindTyClTyVarsAndZonk tc_name $ \ tc_bndrs res_kind -> do @@ -2927,7 +2945,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info ; let tycon = mkFamilyTyCon tc_name tc_bndrs res_kind (resultVariableName sig) OpenSynFamilyTyCon parent inj' - ; return tycon } + ; return (tycon, []) } | ClosedTypeFamily mb_eqns <- fam_info = -- Closed type families are a little tricky, because they contain the definition @@ -2947,10 +2965,11 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info -- but eqns might be empty in the Just case as well ; case mb_eqns of Nothing -> - return $ mkFamilyTyCon tc_name tc_bndrs res_kind - (resultVariableName sig) - AbstractClosedSynFamilyTyCon parent - inj' + let tc = mkFamilyTyCon tc_name tc_bndrs res_kind + (resultVariableName sig) + AbstractClosedSynFamilyTyCon parent + inj' + in return (tc, []) Just eqns -> do { -- Process the equations, creating CoAxBranches @@ -2959,7 +2978,8 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info False {- this doesn't matter here -} ClosedTypeFamilyFlavour - ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc NotAssociated) eqns + ; (branches, axiom_validity_infos) <- + unzip <$> mapAndReportM (tcTyFamInstEqn tc_fam_tc NotAssociated) eqns -- Do not attempt to drop equations dominated by earlier -- ones here; in the case of mutual recursion with a data -- type, we get a knot-tying failure. Instead we check @@ -2979,7 +2999,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info -- We check for instance validity later, when doing validity -- checking for the tycon. Exception: checking equations -- overlap done by dropDominatedAxioms - ; return fam_tc } } + ; return (fam_tc, axiom_validity_infos) } } -- | Maybe return a list of Bools that say whether a type family was declared -- injective in the corresponding type arguments. Length of the list is equal to @@ -3187,7 +3207,7 @@ kcTyFamInstEqn tc_fam_tc -------------------------- tcTyFamInstEqn :: TcTyCon -> AssocInstInfo -> LTyFamInstEqn GhcRn - -> TcM (KnotTied CoAxBranch) + -> TcM (KnotTied CoAxBranch, TyFamEqnValidityInfo) -- Needs to be here, not in GHC.Tc.TyCl.Instance, because closed families -- (typechecked here) have TyFamInstEqns @@ -3206,13 +3226,22 @@ tcTyFamInstEqn fam_tc mb_clsinfo ; checkTyFamInstEqn fam_tc eqn_tc_name hs_pats - ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc mb_clsinfo - outer_bndrs hs_pats hs_rhs_ty + ; (qtvs, non_user_tvs, pats, rhs_ty) + <- tcTyFamInstEqnGuts fam_tc mb_clsinfo + outer_bndrs hs_pats hs_rhs_ty -- Don't print results they may be knot-tied -- (tcFamInstEqnGuts zonks to Type) - ; return (mkCoAxBranch qtvs [] [] pats rhs_ty - (map (const Nominal) qtvs) - (locA loc)) } + + ; let ax = mkCoAxBranch qtvs [] [] pats rhs_ty + (map (const Nominal) qtvs) + (locA loc) + vi = VI { vi_loc = locA loc + , vi_qtvs = qtvs + , vi_non_user_tvs = non_user_tvs + , vi_pats = pats + , vi_rhs = rhs_ty } + + ; return (ax, vi) } checkTyFamInstEqn :: TcTyCon -> Name -> [HsArg p tm ty] -> TcM () checkTyFamInstEqn tc_fam_tc eqn_tc_name hs_pats = @@ -3296,11 +3325,13 @@ generalising over the type of a rewrite rule. -} -------------------------- + tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo -> HsOuterFamEqnTyVarBndrs GhcRn -- Implicit and explicit binders - -> HsFamEqnPats GhcRn -- Patterns + -> HsFamEqnPats GhcRn -- Patterns -> LHsType GhcRn -- RHS - -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs) + -> TcM ([TyVar], TyVarSet, [TcType], TcType) + -- (tyvars, non_user_tvs, pats, rhs) -- Used only for type families, not data families tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty = do { traceTc "tcTyFamInstEqnGuts {" (ppr fam_tc $$ ppr outer_hs_bndrs $$ ppr hs_pats) @@ -3354,11 +3385,12 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty ; return (tidy_env2, UninfTyCtx_TyFamRhs rhs_ty) } ; doNotQuantifyTyVars dvs_rhs err_ctx - ; (final_tvs, lhs_ty, rhs_ty) <- initZonkEnv NoFlexi $ + ; (final_tvs, non_user_tvs, lhs_ty, rhs_ty) <- initZonkEnv NoFlexi $ runZonkBndrT (zonkTyBndrsX final_tvs) $ \ final_tvs -> - do { lhs_ty <- zonkTcTypeToTypeX lhs_ty - ; rhs_ty <- zonkTcTypeToTypeX rhs_ty - ; return (final_tvs, lhs_ty, rhs_ty) } + do { lhs_ty <- zonkTcTypeToTypeX lhs_ty + ; rhs_ty <- zonkTcTypeToTypeX rhs_ty + ; non_user_tvs <- traverse lookupTyVarX qtvs + ; return (final_tvs, non_user_tvs, lhs_ty, rhs_ty) } ; let pats = unravelFamInstPats lhs_ty -- Note that we do this after solveEqualities @@ -3369,7 +3401,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty -- Don't try to print 'pats' here, because lhs_ty involves -- a knot-tied type constructor, so we get a black hole - ; return (final_tvs, pats, rhs_ty) } + ; return (final_tvs, mkVarSet non_user_tvs, pats, rhs_ty) } checkFamTelescope :: TcLevel -> HsOuterFamEqnTyVarBndrs GhcRn @@ -4887,12 +4919,17 @@ checkValidClass cls -- Check that any default declarations for associated types are valid ; whenIsJust m_dflt_rhs $ \ (_, at_validity_info) -> case at_validity_info of - NoATVI -> pure () - ATVI loc qtvs pats orig_rhs -> + NoVI -> pure () + VI { vi_loc = loc + , vi_qtvs = qtvs + , vi_non_user_tvs = non_user_tvs + , vi_pats = pats + , vi_rhs = orig_rhs } -> setSrcSpan loc $ tcAddFamInstCtxt (text "default type instance") (getName fam_tc) $ do { checkValidAssocTyFamDeflt fam_tc pats - ; checkValidTyFamEqn fam_tc qtvs pats orig_rhs }} + ; checkFamPatBinders fam_tc qtvs non_user_tvs pats orig_rhs + ; checkValidTyFamEqn fam_tc pats orig_rhs }} where fam_tvs = tyConTyVars fam_tc diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs index e1077b490f42..0de5dc3e7a6e 100644 --- a/compiler/GHC/Tc/TyCl/Build.hs +++ b/compiler/GHC/Tc/TyCl/Build.hs @@ -4,7 +4,6 @@ -} - {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module GHC.Tc.TyCl.Build ( diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index bb98c083754e..505899d47450 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -608,11 +608,13 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn })) -- (1) do the work of verifying the synonym group -- For some reason we don't have a location for the equation -- itself, so we make do with the location of family name - ; co_ax_branch <- tcTyFamInstEqn fam_tc mb_clsinfo - (L (na2la $ getLoc fam_lname) eqn) + ; (co_ax_branch, co_ax_validity_info) + <- tcTyFamInstEqn fam_tc mb_clsinfo + (L (na2la $ getLoc fam_lname) eqn) -- (2) check for validity ; checkConsistentFamInst mb_clsinfo fam_tc co_ax_branch + ; checkTyFamEqnValidityInfo fam_tc co_ax_validity_info ; checkValidCoAxBranch fam_tc co_ax_branch -- (3) construct coercion axiom @@ -713,7 +715,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env -- See [Arity of data families] in GHC.Core.FamInstEnv ; skol_info <- mkSkolemInfo FamInstSkol ; let new_or_data = dataDefnConsNewOrData hs_cons - ; (qtvs, pats, tc_res_kind, stupid_theta) + ; (qtvs, non_user_tvs, pats, tc_res_kind, stupid_theta) <- tcDataFamInstHeader mb_clsinfo skol_info fam_tc outer_bndrs fixity hs_ctxt hs_pats m_ksig new_or_data @@ -788,7 +790,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env , text "res_kind:" <+> ppr res_kind , text "eta_pats" <+> ppr eta_pats , text "eta_tcbs" <+> ppr eta_tcbs ] - ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) -> + ; (rep_tc, (axiom, ax_rhs)) <- fixM $ \ ~(rec_rep_tc, _) -> do { data_cons <- tcExtendTyVarEnv (binderVars tc_ty_binders) $ -- For H98 decls, the tyvars scope -- over the data constructors @@ -824,13 +826,15 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env -- further instance might not introduce a new recursive -- dependency. (2) They are always valid loop breakers as -- they involve a coercion. - ; return (rep_tc, axiom) } + + ; return (rep_tc, (axiom, ax_rhs)) } -- Remember to check validity; no recursion to worry about here -- Check that left-hand sides are ok (mono-types, no type families, -- consistent instantiations, etc) ; let ax_branch = coAxiomSingleBranch axiom ; checkConsistentFamInst mb_clsinfo fam_tc ax_branch + ; checkFamPatBinders fam_tc zonked_post_eta_qtvs non_user_tvs eta_pats ax_rhs ; checkValidCoAxBranch fam_tc ax_branch ; checkValidTyCon rep_tc @@ -838,10 +842,10 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env m_deriv_info = case derivs of [] -> Nothing preds -> - Just $ DerivInfo { di_rep_tc = rep_tc + Just $ DerivInfo { di_rep_tc = rep_tc , di_scoped_tvs = scoped_tvs - , di_clauses = preds - , di_ctxt = tcMkDataFamInstCtxt decl } + , di_clauses = preds + , di_ctxt = tcMkDataFamInstCtxt decl } ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom ; return (fam_inst, m_deriv_info) } @@ -915,7 +919,7 @@ tcDataFamInstHeader -> LexicalFixity -> Maybe (LHsContext GhcRn) -> HsFamEqnPats GhcRn -> Maybe (LHsKind GhcRn) -> NewOrData - -> TcM ([TcTyVar], [TcType], TcKind, TcThetaType) + -> TcM ([TcTyVar], TyVarSet, [TcType], TcKind, TcThetaType) -- All skolem TcTyVars, all zonked so it's clear what the free vars are -- The "header" of a data family instance is the part other than -- the data constructors themselves @@ -975,14 +979,15 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity -- the outer_tvs. See Note [Generalising in tcTyFamInstEqnGuts] ; reportUnsolvedEqualities skol_info final_tvs tclvl wanted - ; (final_tvs,lhs_ty,master_res_kind,instance_res_kind,stupid_theta) <- + ; (final_tvs, non_user_tvs, lhs_ty, master_res_kind, instance_res_kind, stupid_theta) <- liftZonkM $ do - { final_tvs <- zonkTcTyVarsToTcTyVars final_tvs - ; lhs_ty <- zonkTcType lhs_ty - ; master_res_kind <- zonkTcType master_res_kind - ; instance_res_kind <- zonkTcType instance_res_kind - ; stupid_theta <- zonkTcTypes stupid_theta - ; return (final_tvs,lhs_ty,master_res_kind,instance_res_kind,stupid_theta) } + { final_tvs <- mapM zonkTcTyVarToTcTyVar final_tvs + ; non_user_tvs <- mapM zonkTcTyVarToTcTyVar qtvs + ; lhs_ty <- zonkTcType lhs_ty + ; master_res_kind <- zonkTcType master_res_kind + ; instance_res_kind <- zonkTcType instance_res_kind + ; stupid_theta <- zonkTcTypes stupid_theta + ; return (final_tvs, non_user_tvs, lhs_ty, master_res_kind, instance_res_kind, stupid_theta) } -- Check that res_kind is OK with checkDataKindSig. We need to -- check that it's ok because res_kind can come from a user-written @@ -994,7 +999,7 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity -- For the scopedSort see Note [Generalising in tcTyFamInstEqnGuts] ; let pats = unravelFamInstPats lhs_ty - ; return (final_tvs, pats, master_res_kind, stupid_theta) } + ; return (final_tvs, mkVarSet non_user_tvs, pats, master_res_kind, stupid_theta) } where fam_name = tyConName fam_tc data_ctxt = DataKindCtxt fam_name diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index ece2c26c5192..b2f7830a52ff 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE LambdaCase #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -14,6 +15,7 @@ module GHC.Tc.Validity ( checkValidInstance, checkValidInstHead, validDerivPred, checkTySynRhs, checkEscapingKind, checkValidCoAxiom, checkValidCoAxBranch, + checkFamPatBinders, checkTyFamEqnValidityInfo, checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst, checkTyConTelescope, ) where @@ -2164,26 +2166,21 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches }) -- checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM () checkValidCoAxBranch fam_tc - (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs - , cab_lhs = typats + (CoAxBranch { cab_lhs = typats , cab_rhs = rhs, cab_loc = loc }) = setSrcSpan loc $ - checkValidTyFamEqn fam_tc (tvs++cvs) typats rhs + checkValidTyFamEqn fam_tc typats rhs -- | Do validity checks on a type family equation, including consistency -- with any enclosing class instance head, termination, and lack of -- polytypes. -checkValidTyFamEqn :: TyCon -- ^ of the type family - -> [Var] -- ^ Bound variables in the equation - -> [Type] -- ^ Type patterns - -> Type -- ^ Rhs +checkValidTyFamEqn :: TyCon -- ^ of the type family + -> [Type] -- ^ Type patterns + -> Type -- ^ Rhs -> TcM () -checkValidTyFamEqn fam_tc qvs typats rhs +checkValidTyFamEqn fam_tc typats rhs = do { checkValidTypePats fam_tc typats - -- Check for things used on the right but not bound on the left - ; checkFamPatBinders fam_tc qvs typats rhs - -- Check for oversaturated visible kind arguments in a type family -- equation. -- See Note [Oversaturated type family equations] @@ -2285,12 +2282,28 @@ checkFamInstRhs lhs_tc lhs_tys famInsts = Nothing ----------------- + +-- | Perform scoping check on a type family equation. +-- +-- See 'TyFamEqnValidityInfo'. +checkTyFamEqnValidityInfo :: TyCon -> TyFamEqnValidityInfo -> TcM () +checkTyFamEqnValidityInfo fam_tc = \ case + NoVI -> return () + VI { vi_loc = loc + , vi_qtvs = qtvs + , vi_non_user_tvs = non_user_tvs + , vi_pats = pats + , vi_rhs = rhs } -> + setSrcSpan loc $ + checkFamPatBinders fam_tc qtvs non_user_tvs pats rhs + checkFamPatBinders :: TyCon - -> [TcTyVar] -- Bound on LHS of family instance - -> [TcType] -- LHS patterns - -> Type -- RHS + -> [TcTyVar] -- ^ Bound on LHS of family instance + -> TyVarSet -- ^ non-user-written tyvars + -> [TcType] -- ^ LHS patterns + -> TcType -- ^ RHS -> TcM () -checkFamPatBinders fam_tc qtvs pats rhs +checkFamPatBinders fam_tc qtvs non_user_tvs pats rhs = do { traceTc "checkFamPatBinders" $ vcat [ debugPprType (mkTyConApp fam_tc pats) , ppr (mkTyConApp fam_tc pats) @@ -2351,10 +2364,19 @@ checkFamPatBinders fam_tc qtvs pats rhs -- message. used_tvs = cpt_tvs `unionVarSet` fvVarSet rhs_fvs - bad_qtvs = filterOut (`elemVarSet` used_tvs) qtvs - -- Bound but not used at all + + -- Bound but not used at all + bad_qtvs = filterOut ((`elemVarSet` used_tvs) <||> (`elemVarSet` non_user_tvs)) + qtvs + -- Filter out non-user-tvs in order to only report user-written type variables, + -- e.g. type instance forall a. F = () + -- -XPolyKinds introduces the binder 'k' for the kind of 'a', but + -- we don't want the error message to complain about 'k' being unused, + -- as the user has not written it. + + -- Used on RHS but not bound on LHS bad_rhs_tvs = filterOut (`elemVarSet` inj_cpt_tvs) (fvVarList rhs_fvs) - -- Used on RHS but not bound on LHS + dodgy_tvs = cpt_tvs `minusVarSet` inj_cpt_tvs check_tvs mk_err tvs diff --git a/compiler/GHC/Tc/Zonk/Type.hs b/compiler/GHC/Tc/Zonk/Type.hs index 788f6c582b55..0df9ddc8cbb1 100644 --- a/compiler/GHC/Tc/Zonk/Type.hs +++ b/compiler/GHC/Tc/Zonk/Type.hs @@ -16,7 +16,7 @@ module GHC.Tc.Zonk.Type ( zonkTopDecls, zonkTopExpr, zonkTopLExpr, zonkTopBndrs, zonkTyVarBindersX, zonkTyVarBinderX, - zonkTyBndrsX, + zonkTyBndrX, zonkTyBndrsX, zonkTcTypeToType, zonkTcTypeToTypeX, zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX, zonkTyVarOcc, diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr index 508938616a51..80bc9138403a 100644 --- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr +++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr @@ -14,9 +14,9 @@ ExplicitForAllFams4b.hs:9:22: error: [GHC-53634] All such variables must be bound on the LHS. • In the type instance declaration for ‘J’ -ExplicitForAllFams4b.hs:12:24: error: [GHC-53634] - • Out of scope type variable ‘b’ in the RHS of a family instance. - All such variables must be bound on the LHS. +ExplicitForAllFams4b.hs:12:24: error: [GHC-30337] + • Type variable ‘b’ is bound by a forall, + but not used in the family instance. • In the data instance declaration for ‘K’ ExplicitForAllFams4b.hs:12:27: error: [GHC-34447] @@ -29,9 +29,9 @@ ExplicitForAllFams4b.hs:13:22: error: [GHC-30337] but not used in the family instance. • In the data instance declaration for ‘K’ -ExplicitForAllFams4b.hs:16:27: error: [GHC-53634] - • Out of scope type variable ‘b’ in the RHS of a family instance. - All such variables must be bound on the LHS. +ExplicitForAllFams4b.hs:16:27: error: [GHC-30337] + • Type variable ‘b’ is bound by a forall, + but not used in the family instance. • In the newtype instance declaration for ‘L’ ExplicitForAllFams4b.hs:16:30: error: [GHC-34447] @@ -64,9 +64,9 @@ ExplicitForAllFams4b.hs:25:3: error: [GHC-95424] • In the data instance declaration for ‘CD’ In the instance declaration for ‘C Int’ -ExplicitForAllFams4b.hs:25:17: error: [GHC-53634] - • Out of scope type variable ‘b’ in the RHS of a family instance. - All such variables must be bound on the LHS. +ExplicitForAllFams4b.hs:25:17: error: [GHC-30337] + • Type variable ‘b’ is bound by a forall, + but not used in the family instance. • In the data instance declaration for ‘CD’ In the instance declaration for ‘C Int’ @@ -88,8 +88,8 @@ ExplicitForAllFams4b.hs:32:15: error: [GHC-30337] • In the type instance declaration for ‘CT’ In the instance declaration for ‘C Double’ -ExplicitForAllFams4b.hs:33:15: error: [GHC-53634] - • Out of scope type variable ‘b’ in the RHS of a family instance. - All such variables must be bound on the LHS. +ExplicitForAllFams4b.hs:33:15: error: [GHC-30337] + • Type variable ‘b’ is bound by a forall, + but not used in the family instance. • In the data instance declaration for ‘CD’ In the instance declaration for ‘C Double’ diff --git a/testsuite/tests/indexed-types/should_fail/T17008a.stderr b/testsuite/tests/indexed-types/should_fail/T17008a.stderr index b118434a03b2..600857e641f2 100644 --- a/testsuite/tests/indexed-types/should_fail/T17008a.stderr +++ b/testsuite/tests/indexed-types/should_fail/T17008a.stderr @@ -1,7 +1,7 @@ T17008a.hs:12:5: error: [GHC-53634] - • Out of scope type variable ‘a2’ in the RHS of a family instance. + • Out of scope type variable ‘a’ in the RHS of a family instance. All such variables must be bound on the LHS. - The real LHS (expanding synonyms) is: F @a1 x + The real LHS (expanding synonyms) is: F @a x • In the equations for closed type family ‘F’ In the type family declaration for ‘F’ diff --git a/testsuite/tests/typecheck/should_fail/T23734.hs b/testsuite/tests/typecheck/should_fail/T23734.hs index f00c16a673e3..69d7c77427ba 100644 --- a/testsuite/tests/typecheck/should_fail/T23734.hs +++ b/testsuite/tests/typecheck/should_fail/T23734.hs @@ -14,4 +14,4 @@ class C where type forall c. H = () data family D :: Type -data instance forall d. D = MkD +data instance forall (d :: Type). D = MkD diff --git a/testsuite/tests/typecheck/should_fail/T23734.stderr b/testsuite/tests/typecheck/should_fail/T23734.stderr new file mode 100644 index 000000000000..b5ffbca9fd02 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T23734.stderr @@ -0,0 +1,22 @@ + +T23734.hs:7:22: error: [GHC-30337] + • Type variable ‘a’ is bound by a forall, + but not used in the family instance. + • In the type instance declaration for ‘F’ + +T23734.hs:10:10: error: [GHC-30337] + • Type variable ‘b’ is bound by a forall, + but not used in the family instance. + • In the equations for closed type family ‘G’ + In the type family declaration for ‘G’ + +T23734.hs:14:15: error: [GHC-30337] + • Type variable ‘c’ is bound by a forall, + but not used in the family instance. + • In the default type instance declaration for ‘H’ + In the class declaration for ‘C’ + +T23734.hs:17:23: error: [GHC-30337] + • Type variable ‘d’ is bound by a forall, + but not used in the family instance. + • In the data instance declaration for ‘D’ diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 0eff733f82fa..92bdeb40cb07 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -685,6 +685,7 @@ test('CommonFieldTypeMismatch', normal, compile_fail, ['']) test('T17284', normal, compile_fail, ['']) test('T23427', normal, compile_fail, ['']) test('T23778', normal, compile_fail, ['']) +test('T23734', normal, compile_fail, ['']) test('T13981A', [extra_files(['T13981A.hs-boot', 'T13981B.hs', 'T13981C.hs', 'T13981F.hs'])], multimod_compile_fail, ['T13981A', '-v0']) test('T22560_fail_a', normal, compile_fail, ['']) test('T22560_fail_b', normal, compile_fail, ['']) -- GitLab