diff --git a/compiler/GHC/Core/Class.hs b/compiler/GHC/Core/Class.hs
index 3c3f0a1db62f85b48dad852a46c50381e82ded6b..ffadf0e4b9f94948216c130109042f83dfc5ec45 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 c06af227ab7928376efafc8c07239b6a1b0b2a5e..bc2abf11b0ad29de23a456c746eb9508b2877492 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 a678d5995023a4acbaf74dfeed12714dc625fd65..c51849029ca0fd498433b9b62586752da6c399ce 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 5e6ab56609d61d2023a4205b86533035e602ab16..8b6d08cf2f795f51681f75699cd841df1420ebbb 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 54bda892820886ed01e1d21155b4f16f0849e123..554d0acde4ec4c8d6d6351aefa76b6985d79a461 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 e1077b490f42cee4c6cd7084692d63afd9ec1caa..0de5dc3e7a6e2694af33cf97c01061a8b62e4e71 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 bb98c083754ede3a684167ce3bd10e689e46d71d..505899d474508836c5cf23fe87117f5cf420aedc 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 ece2c26c5192ed2140ac4f376e1887a9f4530cbf..b2f7830a52ff062bfd9140da42d26bc6be4ae333 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 788f6c582b55cec723d9ec1c9975f68f893f9634..0df9ddc8cbb1c655a23c3f1aa4f7c6de228eeac6 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 508938616a51f8dde9ad1aa3b022b583b7ae3d30..80bc9138403ad04a8304858da289181d455fe6d9 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 b118434a03b29f31dfb430c388e03fa8a026686e..600857e641f2a3572c48956b37ae02ec9c93ec23 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 f00c16a673e391933785e692a446962e40ca1cfa..69d7c77427ba0458ab68b26018884383c105fc1a 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 0000000000000000000000000000000000000000..b5ffbca9fd02172ec8f60a3bb79db6e69ce69cfd
--- /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 0eff733f82fa384bb33689018e4769306d0618e9..92bdeb40cb071629954020bd92568bc6d5d03bbc 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, [''])