[Git][ghc/ghc][master] 5 commits: Pass quantified tyvars in tcDefaultAssocDecl
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Tue Sep 19 23:10:02 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
5f826c18 by sheaf at 2023-09-19T19:09:03-04:00
Pass quantified tyvars in tcDefaultAssocDecl
This commit passes the correct set of quantified type variables written
by the user in associated type default declarations for validity
checking. This ensures that validity checking of associated type defaults
mirrors that of standalone type family instances.
Fixes #23768 (see testcase T23734 in subsequent commit)
- - - - -
aba18424 by sheaf at 2023-09-19T19:09:03-04:00
Avoid panic in mkGADTVars
This commit avoids panicking in mkGADTVars when we encounter
a type variable as in #23784 that is bound by a user-written
forall but not actually used.
Fixes #23784
- - - - -
a525a92a by sheaf at 2023-09-19T19:09:03-04:00
Adjust reporting of unused tyvars in data FamInsts
This commit adjusts the validity checking of data family
instances to improve the reporting of unused type variables.
See Note [Out of scope tvs in data family instances] in GHC.Tc.Validity.
The problem was that, in a situation such as
data family D :: Type
data instance forall (d :: Type). D = MkD
the RHS passed to 'checkFamPatBinders' would be the TyCon app
R:D d
which mentions the type variable 'd' quantified in the user-written
forall. Thus, when computing the set of unused type variables in
the RHS of the data family instance, we would find that 'd' is used,
and report a strange error message that would say that 'd' is not
bound on the LHS.
To fix this, we special-case the data-family instance case,
manually extracting all the type variables that appear in the
arguments of all the data constructores of the data family instance.
Fixes #23778
- - - - -
28dd52ee by sheaf at 2023-09-19T19:09:03-04:00
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
- - - - -
1eed645c by sheaf at 2023-09-19T19:09:03-04:00
Validity: refactor treatment of data families
This commit refactors the reporting of unused type variables in type
and data family instances to be more principled. This avoids ad-hoc
logic in the treatment of data family instances.
- - - - -
23 changed files:
- compiler/GHC/Core/Class.hs
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/Deriv/Generate.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Build.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Validity.hs
- compiler/GHC/Tc/Zonk/Type.hs
- compiler/GHC/Utils/Outputable.hs
- testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
- testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
- testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
- testsuite/tests/indexed-types/should_fail/T17008a.stderr
- testsuite/tests/indexed-types/should_fail/T7536.stderr
- + testsuite/tests/typecheck/should_fail/T23734.hs
- + testsuite/tests/typecheck/should_fail/T23734.stderr
- + testsuite/tests/typecheck/should_fail/T23778.hs
- + testsuite/tests/typecheck/should_fail/T23778.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
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,20 +96,44 @@ 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
- = NoATVI -- Used for associated type families that are imported
- -- from another module, for which we don't need to
- -- perform any validity checking.
-
- | ATVI SrcSpan [Type] -- Used for locally defined associated type families.
- -- The [Type] are the LHS patterns.
+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
+ , 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 at . See #23734.
+ , vi_pats :: [Type]
+ -- ^ LHS patterns
+ , 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.
+ }
type ClassMinimalDef = BooleanFormula Name -- Required methods
@@ -165,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.
=====================================
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
=====================================
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
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -71,9 +71,9 @@ import GHC.Core.DataCon ( isSrcStrict )
import Control.Monad
import Control.Arrow ( first )
-import Data.Foldable ( toList )
+import Data.Foldable ( toList, for_ )
import Data.List ( mapAccumL )
-import Data.List.NonEmpty ( NonEmpty(..), head )
+import Data.List.NonEmpty ( NonEmpty(..), head, nonEmpty )
import Data.Maybe ( isNothing, fromMaybe, mapMaybe )
import qualified Data.Set as Set ( difference, fromList, toList, null )
import GHC.Types.GREInfo (ConInfo, mkConInfo, conInfoFields)
@@ -729,9 +729,10 @@ rnFamEqn doc atfi
&& not (cls_tkv `elemNameSet` pat_fvs)
-- ...but not bound on the LHS.
bad_tvs = filter improperly_scoped inst_head_tvs
- ; unless (null bad_tvs) $ addErr $
+ ; for_ (nonEmpty bad_tvs) $ \ ne_bad_tvs ->
+ addErr $
TcRnIllegalInstance $ IllegalFamilyInstance $
- FamInstRHSOutOfScopeTyVars Nothing bad_tvs
+ FamInstRHSOutOfScopeTyVars Nothing ne_bad_tvs
; let eqn_fvs = rhs_fvs `plusFV` pat_fvs
-- See Note [Type family equations and occurrences]
=====================================
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
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -6181,7 +6181,7 @@ pprIllegalFamilyInstance = \case
hang (text "Mismatched type name in type family instance.")
2 (vcat [ text "Expected:" <+> ppr fam_tc_name
, text " Actual:" <+> ppr eqn_tc_name ])
- FamInstRHSOutOfScopeTyVars mb_dodgy tvs ->
+ FamInstRHSOutOfScopeTyVars mb_dodgy (NE.toList -> tvs) ->
hang (text "Out of scope type variable" <> plural tvs
<+> pprWithCommas (quotes . ppr) tvs
<+> text "in the RHS of a family instance.")
@@ -6194,13 +6194,60 @@ pprIllegalFamilyInstance = \case
mk_extra = case mb_dodgy of
Nothing -> empty
Just (fam_tc, pats, dodgy_tvs) ->
- ppWhen (any (`elemVarSetByKey` dodgy_tvs) (map nameUnique tvs)) $
+ ppWhen (any (`elemVarSetByKey` dodgy_tvs) (fmap nameUnique tvs)) $
hang (text "The real LHS (expanding synonyms) is:")
2 (pprTypeApp fam_tc (map expandTypeSynonyms pats))
- FamInstLHSUnusedBoundTyVars tvs ->
- hang (text "Type variable" <> plural tvs <+> pprQuotedList tvs
- <+> isOrAre tvs <+> text "bound by a forall,")
- 2 (text "but not used in the family instance.")
+ FamInstLHSUnusedBoundTyVars (NE.toList -> bad_qtvs) ->
+ vcat [ not_bound_msg, not_used_msg, dodgy_msg ]
+ where
+
+ -- Filter to only keep user-written variables,
+ -- unless none were user-written in which case we report all of them
+ -- (as we need to report an error).
+ filter_user tvs
+ = map ifiqtv
+ $ case filter ifiqtv_user_written tvs of { [] -> tvs ; qvs -> qvs }
+
+ (not_bound, not_used, dodgy)
+ = case foldr acc_tv ([], [], []) bad_qtvs of
+ (nb, nu, d) -> (filter_user nb, filter_user nu, filter_user d)
+
+ acc_tv tv (nb, nu, d) = case ifiqtv_reason tv of
+ InvalidFamInstQTvNotUsedInRHS -> (nb, tv : nu, d)
+ InvalidFamInstQTvNotBoundInPats -> (tv : nb, nu, d)
+ InvalidFamInstQTvDodgy -> (nb, nu, tv : d)
+
+ -- Error message for type variables not bound in LHS patterns.
+ not_bound_msg
+ | null not_bound
+ = empty
+ | otherwise
+ = vcat [ text "The type variable" <> plural not_bound <+> pprQuotedList not_bound
+ <+> isOrAre not_bound <+> text "bound by a forall,"
+ , text "but" <+> doOrDoes not_bound <+> text "not appear in any of the LHS patterns of the family instance." ]
+
+ -- Error message for type variables bound by a forall but not used
+ -- in the RHS.
+ not_used_msg =
+ if null not_used
+ then empty
+ else text "The type variable" <> plural not_used <+> pprQuotedList not_used
+ <+> isOrAre not_used <+> text "bound by a forall," $$
+ text "but" <+> itOrThey not_used <+>
+ isOrAre not_used <> text "n't used in the family instance."
+
+ -- Error message for dodgy type variables.
+ -- See Note [Dodgy binding sites in type family instances] in GHC.Tc.Validity.
+ dodgy_msg
+ | null dodgy
+ = empty
+ | otherwise
+ = hang (text "Dodgy type variable" <> plural dodgy <+> pprQuotedList dodgy
+ <+> text "in the LHS of a family instance:")
+ 2 (text "the type variable" <> plural dodgy <+> pprQuotedList dodgy
+ <+> text "syntactically appear" <> singular dodgy <+> text "in LHS patterns,"
+ $$ text "but" <+> itOrThey dodgy <+> doOrDoes dodgy <> text "n't appear in an injective position.")
+
illegalFamilyInstanceHints :: IllegalFamilyInstanceReason -> [GhcHint]
illegalFamilyInstanceHints = \case
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -138,6 +138,7 @@ module GHC.Tc.Errors.Types (
, IllegalHasFieldInstance(..)
, CoverageProblem(..), FailedCoverageCondition(..)
, IllegalFamilyInstanceReason(..)
+ , InvalidFamInstQTv(..), InvalidFamInstQTvReason(..)
, InvalidAssoc(..), InvalidAssocInstance(..)
, InvalidAssocDefault(..), AssocDefaultBadArgs(..)
@@ -181,7 +182,7 @@ import GHC.Types.Avail
import GHC.Types.Hint (UntickedPromotedThing(..))
import GHC.Types.ForeignCall (CLabelString)
import GHC.Types.Id.Info ( RecSelParent(..) )
-import GHC.Types.Name (Name, OccName, getSrcLoc, getSrcSpan)
+import GHC.Types.Name (NamedThing(..), Name, OccName, getSrcLoc, getSrcSpan)
import qualified GHC.Types.Name.Occurrence as OccName
import GHC.Types.Name.Reader
import GHC.Types.SourceFile (HsBootOrSig(..))
@@ -4653,14 +4654,47 @@ data IllegalFamilyInstanceReason
-- ^ family 'TyCon', arguments, and set of "dodgy" type variables
-- See Note [Dodgy binding sites in type family instances]
-- in GHC.Tc.Validity
- ![Name] -- ^ the out-of-scope type variables
+ !(NE.NonEmpty Name) -- ^ the out-of-scope type variables
| FamInstLHSUnusedBoundTyVars
- ![Name] -- ^ the unused bound type variables
+ !(NE.NonEmpty InvalidFamInstQTv) -- ^ the unused bound type variables
| InvalidAssoc !InvalidAssoc
deriving Generic
+-- | A quantified type variable in a type or data family equation that
+-- is either not bound in any LHS patterns or not used in the RHS (or both).
+data InvalidFamInstQTv
+ = InvalidFamInstQTv
+ { ifiqtv :: TcTyVar
+ , ifiqtv_user_written :: Bool
+ -- ^ Did the user write this type variable, or was introduced by GHC?
+ -- For example: with @-XPolyKinds@, in @type instance forall a. F = ()@,
+ -- we have a user-written @a@ but GHC introduces a kind variable @k@
+ -- as well. See #23734.
+ , ifiqtv_reason :: InvalidFamInstQTvReason
+ -- ^ For what reason was the quantified type variable invalid?
+ }
+
+data InvalidFamInstQTvReason
+ -- | A dodgy binder, i.e. a variable that syntactically appears in
+ -- LHS patterns but only in non-injective positions.
+ --
+ -- See Note [Dodgy binding sites in type family instances]
+ -- in GHC.Tc.Validity.
+ = InvalidFamInstQTvDodgy
+ -- | A quantified type variable in a type or data family equation
+ -- that is not bound in any LHS patterns.
+ | InvalidFamInstQTvNotBoundInPats
+ -- | A quantified type variable in a type or data family equation
+ -- that is not used on the RHS.
+ | InvalidFamInstQTvNotUsedInRHS
+
+-- The 'check_tvs' function in 'GHC.Tc.Validity.checkFamPatBinders'
+-- uses 'getSrcSpan', so this 'NamedThing' instance is convenient.
+instance NamedThing InvalidFamInstQTv where
+ getName = getName . ifiqtv
+
data InvalidAssoc
-- | An invalid associated family instance.
--
=====================================
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
@@ -2783,7 +2796,13 @@ tcDefaultAssocDecl fam_tc
-- simply create an empty substitution and let GHC fall
-- over later, in GHC.Tc.Validity.checkValidAssocTyFamDeflt.
-- See Note [Type-checking default assoc decls].
- ; pure $ Just (substTyUnchecked subst rhs_ty, ATVI (locA loc) pats)
+
+ ; 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.
}
@@ -2886,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
@@ -2915,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
@@ -2926,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
@@ -2946,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
@@ -2958,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
@@ -2978,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
@@ -3186,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
@@ -3205,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 =
@@ -3295,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)
@@ -3353,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
@@ -3368,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
@@ -4182,7 +4215,7 @@ names, for example, this would be simplified. This change would almost
certainly degrade error messages a bit, though.
-}
--- ^ From information about a source datacon definition, extract out
+-- | From information about a source datacon definition, extract out
-- what the universal variables and the GADT equalities should be.
-- See Note [mkGADTVars].
mkGADTVars :: [TyVar] -- ^ The tycon vars
@@ -4244,7 +4277,7 @@ mkGADTVars tmpl_tvs dc_tvs subst
eqs' = (t_tv', r_ty) : eqs
| otherwise
- = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
+ = choose (t_tv:univs) eqs t_sub r_sub t_tvs
-- choose an appropriate name for a univ tyvar.
-- This *must* preserve the Unique of the result tv, so that we
@@ -4712,7 +4745,7 @@ checkValidDataCon dflags existential_ok tc con
-- See Note [DataCon user type variable binders] in GHC.Core.DataCon
-- checked here because we sometimes build invalid DataCons before
-- erroring above here
- ; when debugIsOn $
+ ; when debugIsOn $ whenNoErrs $
massertPpr (checkDataConTyVars con) $
ppr con $$ ppr (dataConFullSig con) $$ ppr (dataConUserTyVars con)
@@ -4884,14 +4917,19 @@ checkValidClass cls
-- since there is no possible ambiguity (#10020)
-- Check that any default declarations for associated types are valid
- ; whenIsJust m_dflt_rhs $ \ (rhs, at_validity_info) ->
+ ; whenIsJust m_dflt_rhs $ \ (_, at_validity_info) ->
case at_validity_info of
- NoATVI -> pure ()
- ATVI loc pats ->
+ 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 fam_tvs (mkTyVarTys fam_tvs) rhs }}
+ ; checkFamPatBinders fam_tc qtvs non_user_tvs pats orig_rhs
+ ; checkValidTyFamEqn fam_tc pats orig_rhs }}
where
fam_tvs = tyConTyVars fam_tc
=====================================
compiler/GHC/Tc/TyCl/Build.hs
=====================================
@@ -4,7 +4,6 @@
-}
-
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.TyCl.Build (
=====================================
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
=====================================
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
@@ -82,6 +84,8 @@ import Control.Monad
import Data.Foldable
import Data.Function
import Data.List ( (\\) )
+import qualified Data.List.NonEmpty as NE
+import Data.List.NonEmpty ( NonEmpty(..) )
{-
************************************************************************
@@ -2161,28 +2165,32 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
-- Check that a "type instance" is well-formed (which includes decidability
-- unless -XUndecidableInstances is given).
--
+-- See also the separate 'checkFamPatBinders' which performs scoping checks
+-- on a type family equation.
+-- (It's separate because it expects 'TyFamEqnValidityInfo', which comes from a
+-- separate place e.g. for associated type defaults.)
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
+--
+-- See also the separate 'checkFamPatBinders' which performs scoping checks
+-- on a type family equation.
+-- (It's separate because it expects 'TyFamEqnValidityInfo', which comes from a
+-- separate place e.g. for associated type defaults.)
+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]
@@ -2284,19 +2292,47 @@ 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
+
+-- | Check binders for a type or data family declaration.
+--
+-- Specifically, this function checks for:
+--
+-- - type variables used on the RHS but not bound (explicitly or implicitly)
+-- in the LHS,
+-- - variables bound by a forall in the LHS but not used in the RHS.
+--
+-- See Note [Check type family instance binders].
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)
+ , text "rhs:" <+> ppr rhs
, text "qtvs:" <+> ppr qtvs
- , text "rhs_tvs:" <+> ppr (fvVarSet rhs_fvs)
+ , text "rhs_fvs:" <+> ppr (fvVarSet rhs_fvs)
, text "cpt_tvs:" <+> ppr cpt_tvs
- , text "inj_cpt_tvs:" <+> ppr inj_cpt_tvs ]
+ , text "inj_cpt_tvs:" <+> ppr inj_cpt_tvs
+ , text "bad_rhs_tvs:" <+> ppr bad_rhs_tvs
+ , text "bad_qtvs:" <+> ppr (map ifiqtv bad_qtvs) ]
-- Check for implicitly-bound tyvars, mentioned on the
-- RHS but not bound on the LHS
@@ -2304,17 +2340,19 @@ checkFamPatBinders fam_tc qtvs pats rhs
-- data family D Int = MkD (forall (a::k). blah)
-- In both cases, 'k' is not bound on the LHS, but is used on the RHS
-- We catch the former in kcDeclHeader, and the latter right here
- -- See Note [Check type-family instance binders]
+ -- See Note [Check type family instance binders]
; check_tvs (FamInstRHSOutOfScopeTyVars (Just (fam_tc, pats, dodgy_tvs)))
- bad_rhs_tvs
+ (map tyVarName bad_rhs_tvs)
-- Check for explicitly forall'd variable that is not bound on LHS
-- data instance forall a. T Int = MkT Int
-- See Note [Unused explicitly bound variables in a family pattern]
- -- See Note [Check type-family instance binders]
+ -- See Note [Check type family instance binders]
; check_tvs FamInstLHSUnusedBoundTyVars bad_qtvs
}
where
+ rhs_fvs = tyCoFVsOfType rhs
+
cpt_tvs = tyCoVarsOfTypes pats
inj_cpt_tvs = fvVarSet $ injectiveVarsOfTypes False pats
-- The type variables that are in injective positions.
@@ -2325,18 +2363,41 @@ checkFamPatBinders fam_tc qtvs pats rhs
-- NB: It's OK to use the nondeterministic `fvVarSet` function here,
-- since the order of `inj_cpt_tvs` is never revealed in an error
-- message.
- rhs_fvs = tyCoFVsOfType rhs
- used_tvs = cpt_tvs `unionVarSet` fvVarSet rhs_fvs
- bad_qtvs = filterOut (`elemVarSet` used_tvs) qtvs
- -- Bound but not used at all
- bad_rhs_tvs = filterOut (`elemVarSet` inj_cpt_tvs) (fvVarList rhs_fvs)
- -- Used on RHS but not bound on LHS
+
+ -- Bound but not used at all
+ bad_qtvs = mapMaybe bad_qtv_maybe qtvs
+
+ bad_qtv_maybe qtv
+ | not_bound_in_pats
+ = let reason
+ | dodgy
+ = InvalidFamInstQTvDodgy
+ | used_in_rhs
+ = InvalidFamInstQTvNotBoundInPats
+ | otherwise
+ = InvalidFamInstQTvNotUsedInRHS
+ in Just $ InvalidFamInstQTv
+ { ifiqtv = qtv
+ , ifiqtv_user_written = not $ qtv `elemVarSet` non_user_tvs
+ , ifiqtv_reason = reason
+ }
+ | otherwise
+ = Nothing
+ where
+ not_bound_in_pats = not $ qtv `elemVarSet` inj_cpt_tvs
+ dodgy = not_bound_in_pats && qtv `elemVarSet` cpt_tvs
+ used_in_rhs = qtv `elemVarSet` fvVarSet rhs_fvs
+
+ -- Used on RHS but not bound on LHS
+ bad_rhs_tvs = filterOut ((`elemVarSet` inj_cpt_tvs) <||> (`elem` qtvs)) (fvVarList rhs_fvs)
+
dodgy_tvs = cpt_tvs `minusVarSet` inj_cpt_tvs
check_tvs mk_err tvs
- = unless (null tvs) $ addErrAt (getSrcSpan (head tvs)) $
+ = for_ (NE.nonEmpty tvs) $ \ ne_tvs@(tv0 :| _) ->
+ addErrAt (getSrcSpan tv0) $
TcRnIllegalInstance $ IllegalFamilyInstance $
- mk_err (map tyVarName tvs)
+ mk_err ne_tvs
-- | Checks that a list of type patterns is valid in a matching (LHS)
-- position of a class instances or type/data family instance.
@@ -2442,7 +2503,7 @@ checkConsistentFamInst (InClsInst { ai_class = clas
| otherwise = BindMe
-{- Note [Check type-family instance binders]
+{- Note [Check type family instance binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a type family instance, we require (of course), type variables
used on the RHS are matched on the LHS. This is checked by
=====================================
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,
=====================================
compiler/GHC/Utils/Outputable.hs
=====================================
@@ -52,6 +52,7 @@ module GHC.Utils.Outputable (
ppWhen, ppUnless, ppWhenOption, ppUnlessOption,
speakNth, speakN, speakNOf, plural, singular,
isOrAre, doOrDoes, itsOrTheir, thisOrThese, hasOrHave,
+ itOrThey,
unicodeSyntax,
coloured, keyword,
@@ -1546,6 +1547,15 @@ itsOrTheir :: [a] -> SDoc
itsOrTheir [_] = text "its"
itsOrTheir _ = text "their"
+-- | 'it' or 'they', depeneding on the length of the list.
+--
+-- > itOrThey [x] = text "it"
+-- > itOrThey [x,y] = text "they"
+-- > itOrThey [] = text "they" -- probably avoid this
+itOrThey :: [a] -> SDoc
+itOrThey [_] = text "it"
+itOrThey _ = text "they"
+
-- | Determines the form of subject appropriate for the length of a list:
--
=====================================
testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr
=====================================
@@ -1,12 +1,12 @@
ExplicitForAllFams4a.hs:8:12: error: [GHC-30337]
- • Type variable ‘b’ is bound by a forall,
- but not used in the family instance.
+ • The type variable ‘b’ is bound by a forall,
+ but it isn't used in the family instance.
• In the equations for closed type family ‘H’
In the type family declaration for ‘H’
-ExplicitForAllFams4a.hs:9:10: 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.
+ExplicitForAllFams4a.hs:9:10: error: [GHC-30337]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• In the equations for closed type family ‘H’
In the type family declaration for ‘H’
=====================================
testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
=====================================
@@ -1,7 +1,7 @@
ExplicitForAllFams4b.hs:8:24: error: [GHC-30337]
- • Type variable ‘b’ is bound by a forall,
- but not used in the family instance.
+ • The type variable ‘b’ is bound by a forall,
+ but it isn't used in the family instance.
• In the type instance declaration for ‘J’
ExplicitForAllFams4b.hs:8:27: error: [GHC-34447]
@@ -9,14 +9,14 @@ ExplicitForAllFams4b.hs:8:27: error: [GHC-34447]
J [a] = Float -- Defined at ExplicitForAllFams4b.hs:8:27
J _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:9:27
-ExplicitForAllFams4b.hs:9:22: 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:9:22: error: [GHC-30337]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• 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]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• In the data instance declaration for ‘K’
ExplicitForAllFams4b.hs:12:27: error: [GHC-34447]
@@ -24,14 +24,14 @@ ExplicitForAllFams4b.hs:12:27: error: [GHC-34447]
K (a, Bool) -- Defined at ExplicitForAllFams4b.hs:12:27
K _ -- Defined at ExplicitForAllFams4b.hs:13:27
-ExplicitForAllFams4b.hs:13:22: 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:13:22: error: [GHC-30337]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of 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]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• In the newtype instance declaration for ‘L’
ExplicitForAllFams4b.hs:16:30: error: [GHC-34447]
@@ -39,9 +39,9 @@ ExplicitForAllFams4b.hs:16:30: error: [GHC-34447]
L (a, Bool) -- Defined at ExplicitForAllFams4b.hs:16:30
L _ -- Defined at ExplicitForAllFams4b.hs:17:30
-ExplicitForAllFams4b.hs:17:25: 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:17:25: error: [GHC-30337]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• In the newtype instance declaration for ‘L’
ExplicitForAllFams4b.hs:24:3: error: [GHC-95424]
@@ -52,8 +52,8 @@ ExplicitForAllFams4b.hs:24:3: error: [GHC-95424]
In the instance declaration for ‘C Int’
ExplicitForAllFams4b.hs:24:17: error: [GHC-30337]
- • Type variable ‘b’ is bound by a forall,
- but not used in the family instance.
+ • The type variable ‘b’ is bound by a forall,
+ but it isn't used in the family instance.
• In the type instance declaration for ‘CT’
In the instance declaration for ‘C Int’
@@ -64,32 +64,32 @@ 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]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C Int’
-ExplicitForAllFams4b.hs:28: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:28:15: error: [GHC-30337]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• In the type instance declaration for ‘CT’
In the instance declaration for ‘C Bool’
-ExplicitForAllFams4b.hs:29: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:29:15: error: [GHC-30337]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C Bool’
ExplicitForAllFams4b.hs:32:15: error: [GHC-30337]
- • Type variable ‘b’ is bound by a forall,
- but not used in the family instance.
+ • The type variable ‘b’ is bound by a forall,
+ but it isn't used in the family instance.
• 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]
+ • The type variable ‘b’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C Double’
=====================================
testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
=====================================
@@ -4,7 +4,19 @@ SimpleFail13.hs:9:15: error: [GHC-73138]
D [C a]
• In the data instance declaration for ‘D’
+SimpleFail13.hs:9:17: error: [GHC-30337]
+ • Dodgy type variable ‘a’ in the LHS of a family instance:
+ the type variable ‘a’ syntactically appears in LHS patterns,
+ but it doesn't appear in an injective position.
+ • In the data instance declaration for ‘D’
+
SimpleFail13.hs:13:15: error: [GHC-73138]
• Illegal type synonym family application ‘C a’ in instance:
E [C a]
• In the type instance declaration for ‘E’
+
+SimpleFail13.hs:13:17: error: [GHC-30337]
+ • Dodgy type variable ‘a’ in the LHS of a family instance:
+ the type variable ‘a’ syntactically appears in LHS patterns,
+ but it doesn't appear in an injective position.
+ • In the type instance declaration for ‘E’
=====================================
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.
- All such variables must be bound on the LHS.
- The real LHS (expanding synonyms) is: F @a1 x
+T17008a.hs:12:5: error: [GHC-30337]
+ • Dodgy type variable ‘a’ in the LHS of a family instance:
+ the type variable ‘a’ syntactically appears in LHS patterns,
+ but it doesn't appear in an injective position.
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’
=====================================
testsuite/tests/indexed-types/should_fail/T7536.stderr
=====================================
@@ -1,6 +1,6 @@
-T7536.hs:8:18: error: [GHC-53634]
- • 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: TF Int
+T7536.hs:8:18: error: [GHC-30337]
+ • Dodgy type variable ‘a’ in the LHS of a family instance:
+ the type variable ‘a’ syntactically appears in LHS patterns,
+ but it doesn't appear in an injective position.
• In the type instance declaration for ‘TF’
=====================================
testsuite/tests/typecheck/should_fail/T23734.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies, ExplicitForAll, PolyKinds #-}
+module T23734 where
+
+import Data.Kind
+
+type family F
+type instance forall a. F = ()
+
+type family G where
+ forall b. G = ()
+
+class C where
+ type family H
+ type forall c. H = ()
+
+data family D :: Type
+data instance forall (d :: Type). D = MkD
=====================================
testsuite/tests/typecheck/should_fail/T23734.stderr
=====================================
@@ -0,0 +1,22 @@
+
+T23734.hs:7:25: error: [GHC-30337]
+ • The type variable ‘a’ is bound by a forall,
+ but it isn't used in the family instance.
+ • In the type instance declaration for ‘F’
+
+T23734.hs:10:3: error: [GHC-30337]
+ • The type variable ‘b’ is bound by a forall,
+ but it isn't used in the family instance.
+ • In the equations for closed type family ‘G’
+ In the type family declaration for ‘G’
+
+T23734.hs:14:3: error: [GHC-30337]
+ • The type variable ‘c’ is bound by a forall,
+ but it isn't 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]
+ • The type variable ‘d’ is bound by a forall,
+ but does not appear in any of the LHS patterns of the family instance.
+ • In the data instance declaration for ‘D’
=====================================
testsuite/tests/typecheck/should_fail/T23778.hs
=====================================
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies, NoPolyKinds #-}
+module T23778 where
+
+import Data.Kind
+
+data family D :: Type -> Type
+data instance forall d u v. D u = MkD1 | MkD2 u
=====================================
testsuite/tests/typecheck/should_fail/T23778.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T23778.hs:7:22: error: [GHC-30337]
+ • The type variables ‘d’, ‘v’ are bound by a forall,
+ but do not appear in any of the LHS patterns of the family instance.
+ • In the data instance declaration for ‘D’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -684,6 +684,8 @@ test('CommonFieldResultTypeMismatch', normal, compile_fail, [''])
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, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/86d2971e3cf194d23b483a7cd9466d928e104ca5...1eed645c8b03b19a14cf58d9be5317cb81cbd30a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/86d2971e3cf194d23b483a7cd9466d928e104ca5...1eed645c8b03b19a14cf58d9be5317cb81cbd30a
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230919/20f3ed79/attachment-0001.html>
More information about the ghc-commits
mailing list