[Git][ghc/ghc][wip/T25647] 2 commits: move [FamArgFlavour] to tyCon
Patrick (@soulomoon)
gitlab at gitlab.haskell.org
Tue Mar 4 19:37:08 UTC 2025
Patrick pushed to branch wip/T25647 at Glasgow Haskell Compiler / GHC
Commits:
90e97f12 by Patrick at 2025-03-04T23:42:18+08:00
move [FamArgFlavour] to tyCon
- - - - -
dbe81ead by Patrick at 2025-03-05T03:36:49+08:00
add note
- - - - -
5 changed files:
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
Changes:
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -17,6 +17,7 @@ module GHC.Core.TyCon(
AlgTyConFlav(..), isNoParent,
FamTyConFlav(..), Role(..), Injectivity(..),
PromDataConInfo(..), TyConFlavour(..),
+ FamArgFlavour(..),
-- * TyConBinder
TyConBinder, TyConBndrVis(..),
@@ -109,6 +110,7 @@ module GHC.Core.TyCon(
tcTyConScopedTyVars, isMonoTcTyCon,
tyConHasClosedResKind,
mkTyConTagMap,
+ tyConFamArgFlavours,
-- ** Manipulating TyCons
ExpandSynResult(..),
@@ -740,6 +742,7 @@ instance Binary TyConBndrVis where
-}
+
-- | TyCons represent type constructors. Type constructors are introduced by
-- things such as:
--
@@ -881,7 +884,7 @@ data TyConDetails =
-- abstract, built-in. See comments for
-- FamTyConFlav
- famTcParent :: Maybe TyCon, -- ^ For *associated* type/data families
+ famTcParent :: Maybe (TyCon, [FamArgFlavour]), -- ^ For *associated* type/data families
-- The class tycon in which the family is declared
-- See Note [Associated families and their parent class]
@@ -1948,8 +1951,17 @@ mkFamilyTyCon name binders res_kind resVar flav parent inj
= mkTyCon name binders res_kind (constRoles binders Nominal) $
FamilyTyCon { famTcResVar = resVar
, famTcFlav = flav
- , famTcParent = classTyCon <$> parent
+ , famTcParent = genfamTcParent <$> parent
, famTcInj = inj }
+ where
+ genfamTcParent cls = (classTyCon cls, argFlavours)
+ where clsArgs = classTyVars cls
+ argFlavours = [if b `elem` clsArgs then ClassArg else FreeArg | b <- binderVars binders]
+
+tyConFamArgFlavours :: TyCon -> [FamArgFlavour]
+tyConFamArgFlavours (TyCon { tyConDetails = details })
+ | FamilyTyCon { famTcParent = Just (_, argFlavours) } <- details = argFlavours
+ | otherwise = []
-- | Create a promoted data constructor 'TyCon'
-- Somewhat dodgily, we give it the same Name
@@ -2846,8 +2858,8 @@ tyConFlavour (TyCon { tyConDetails = details })
| FamilyTyCon { famTcFlav = flav, famTcParent = parent } <- details
= case flav of
- DataFamilyTyCon{} -> OpenFamilyFlavour (IAmData DataType) parent
- OpenSynFamilyTyCon -> OpenFamilyFlavour IAmType parent
+ DataFamilyTyCon{} -> OpenFamilyFlavour (IAmData DataType) (fst <$> parent)
+ OpenSynFamilyTyCon -> OpenFamilyFlavour IAmType (fst <$> parent)
ClosedSynFamilyTyCon{} -> ClosedTypeFamilyFlavour
AbstractClosedSynFamilyTyCon -> ClosedTypeFamilyFlavour
BuiltInSynFamTyCon{} -> ClosedTypeFamilyFlavour
@@ -2965,3 +2977,55 @@ tyConSkolem = isHoleName . tyConName
--
-- This is why the test is on the original name of the TyCon,
-- not whether it is abstract or not.
+
+
+
+{- Note [FamArgFlavour and family instance decl type checking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The FamArgFlavour is used to distinguish the different kinds of arguments that may
+appear in an associated type family declaration/instance. In an associated type family,
+some arguments come directly from the parent class (the “class arguments”) while
+others are provided freely by the user (the “free arguments”). For example, consider:
+
+ class C a b c where
+ type F x y a -- Here, 'x' and 'y' are free arguments, while 'a' comes from the class.
+ type G p c b -- Here, 'p' is free and both 'c' and 'b' are class arguments.
+
+We can conceptually view the kinds of arguments for a type family as a famArgFlavour–vector,
+with one flavour per argument of the family. Each flavour indicates whether the corresponding
+argument is a ClassArg or a FreeArg. We also introduce a third flavour, SigArg,
+to flag arguments that appear only in a kind signature for a type instance (i.e. when
+a wildcard is provided along with a kind annotation, as in @(_ :: _)@).
+
+Under the current design, when type-checking an instance the interpretation of wildcards
+depends on their position:
+
+ - In free arguments, a wildcard is interpreted as a TyVarTv-variable type variable.
+ - In class arguments, a wildcard is interpreted as a Tau–variable.
+ - In signature arguments, a wildcard is similarly treated as a Tau–variable.
+
+For instance, for an instance declaration like
+
+ instance C Int [x] Bool where
+ type F _ _ (_ :: _) = Int
+
+the first two underscores (free arguments) would yield TyVarTv’s while the last two underscores (a class
+argument and a signature argument) would produce TauTv's.
+
+This design provides flexibility in handling wildcards in type families.
+
+Side note:
+we maintain diffirent flavours between class arguments and signature arguments because
+we might want to be able to flip only the class arguments to use TyVarTv without affecting
+the signature arguments.
+
+For more discussion, see #13908.
+-}
+
+-- see Note [FamArgFlavour and family instance decl type checking]
+data FamArgFlavour = ClassArg | FreeArg | SigArg deriving (Eq, Show)
+
+instance Outputable FamArgFlavour where
+ ppr ClassArg = text "ClassArg"
+ ppr FreeArg = text "FreeArg"
+ ppr SigArg = text "SigArg"
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -142,8 +142,6 @@ import Data.List ( mapAccumL )
import Control.Monad
import Data.Tuple( swap )
import GHC.Types.SourceText
-import GHC.Tc.Instance.Class (AssocInstInfo (..), FamArgType (..),
- buildPatsArgTypes, buildPatsModeTypes)
{-
----------------------------
@@ -781,20 +779,22 @@ There is also the possibility of mentioning a wildcard
tcFamTyPats :: TyCon
-> HsFamEqnPats GhcRn -- Patterns
- -> AssocInstInfo -- Associated instance info
-> TcM (TcType, TcKind) -- (lhs_type, lhs_kind)
-- Check the LHS of a type/data family instance
-- e.g. type instance F ty1 .. tyn = ...
-- Used for both type and data families
-tcFamTyPats fam_tc hs_pats mb_clsinfo
+tcFamTyPats fam_tc hs_pats
= do { traceTc "tcFamTyPats {" $
- vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity, text "pats:" <+> ppr hs_pats ]
+ vcat [ ppr fam_tc,
+ text "arity:" <+> ppr fam_arity,
+ text "pats:" <+> ppr hs_pats
+ ]
; mode <- mkHoleMode TypeLevel (HM_FamPat FreeArg)
-- HM_FamPat: See Note [Wildcards in family instances] in
-- GHC.Rename.Module
; let fun_ty = mkTyConApp fam_tc []
- ; (fam_app, res_kind) <- tcInferTyApps mode lhs_fun fun_ty (buildPatsArgTypes mb_clsinfo hs_pats)
+ ; (fam_app, res_kind) <- tcInferTyApps mode lhs_fun fun_ty hs_pats (tyConFamArgFlavours fam_tc ++ cycle [FreeArg])
-- Hack alert: see Note [tcFamTyPats: zonking the result kind]
; res_kind <- liftZonkM $ zonkTcType res_kind
@@ -888,14 +888,14 @@ tcInferLHsTypeUnsaturated hs_ty
; case splitHsAppTys_maybe (unLoc hs_ty) of
Just (hs_fun_ty, hs_args)
-> do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
- ; tcInferTyApps_nosat mode hs_fun_ty fun_ty (buildPatsModeTypes (tcTyModeFamArgType mode) hs_args) }
+ ; tcInferTyApps_nosat mode hs_fun_ty fun_ty hs_args (cycle [FreeArg])}
-- Notice the 'nosat'; do not instantiate trailing
-- invisible arguments of a type family.
-- See Note [Dealing with :kind]
Nothing -> tc_infer_lhs_type mode hs_ty }
-tcTyModeFamArgType :: TcTyMode -> FamArgType
-tcTyModeFamArgType (TcTyMode { mode_holes = mh })
+tcTyModeFamArgFlavour :: TcTyMode -> FamArgFlavour
+tcTyModeFamArgFlavour (TcTyMode { mode_holes = mh })
= case mh of
Just (_, HM_FamPat artType) -> artType
_ -> FreeArg
@@ -976,7 +976,7 @@ type HoleInfo = Maybe (TcLevel, HoleMode)
-- HoleMode says how to treat the occurrences
-- of anonymous wildcards; see tcAnonWildCardOcc
data HoleMode = HM_Sig -- Partial type signatures: f :: _ -> Int
- | HM_FamPat FamArgType -- Family instances: F _ Int = Bool
+ | HM_FamPat FamArgFlavour -- Family instances: F _ Int = Bool
| HM_VTA -- Visible type and kind application:
-- f @(Maybe _)
-- Maybe @(_ -> _)
@@ -998,8 +998,8 @@ mkHoleMode tyki hm
; return (TcTyMode { mode_tyki = tyki
, mode_holes = Just (lvl,hm) }) }
-updateFamArgType :: FamArgType -> TcTyMode -> TcTyMode
-updateFamArgType fam_arg m at TcTyMode { mode_tyki = tyki, mode_holes = mh }
+updateFamArgFlavour :: FamArgFlavour -> TcTyMode -> TcTyMode
+updateFamArgFlavour fam_arg m at TcTyMode { mode_tyki = tyki, mode_holes = mh }
|Just (lvl, HM_FamPat _) <- mh
= (TcTyMode { mode_tyki = tyki
, mode_holes = Just (lvl,HM_FamPat fam_arg) })
@@ -1285,7 +1285,7 @@ tcHsType mode rn_ty@(HsAppKindTy{}) exp_kind = tc_app_ty mode rn_ty exp_kind
tcHsType mode rn_ty@(HsOpTy{}) exp_kind = tc_app_ty mode rn_ty exp_kind
tcHsType mode rn_ty@(HsKindSig _ ty sig) exp_kind
- = do { let mode' = (updateFamArgType SigArg $ mode { mode_tyki = KindLevel})
+ = do { let mode' = (updateFamArgFlavour SigArg $ mode { mode_tyki = KindLevel})
; sig' <- tc_lhs_kind_sig mode' KindSigCtxt sig
-- We must typecheck the kind signature, and solve all
-- its equalities etc; from this point on we may do
@@ -1555,7 +1555,7 @@ tc_app_ty :: TcTyMode -> HsType GhcRn -> ExpKind -> TcM TcType
tc_app_ty mode rn_ty exp_kind
= do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
; (ty, infered_kind) <- tcInferTyApps mode hs_fun_ty fun_ty
- (buildPatsModeTypes (tcTyModeFamArgType mode) hs_args)
+ hs_args (cycle [FreeArg])
; checkExpKind rn_ty ty infered_kind exp_kind }
where
(hs_fun_ty, hs_args) = splitHsAppTys rn_ty
@@ -1576,15 +1576,16 @@ tcInferTyApps, tcInferTyApps_nosat
:: TcTyMode
-> LHsType GhcRn -- ^ Function (for printing only)
-> TcType -- ^ Function
- -> [(LHsTypeArg GhcRn, FamArgType)] -- ^ Args
+ -> [LHsTypeArg GhcRn] -- ^ Args
+ -> [FamArgFlavour] -- ^ Args
-> TcM (TcType, TcKind) -- ^ (f args, result kind)
-tcInferTyApps mode hs_ty fun hs_args
- = do { (f_args, res_k) <- tcInferTyApps_nosat mode hs_ty fun hs_args
+tcInferTyApps mode hs_ty fun hs_args famArgFlvs
+ = do { (f_args, res_k) <- tcInferTyApps_nosat mode hs_ty fun hs_args famArgFlvs
; saturateFamApp f_args res_k }
-tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
+tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args fam_arg_flvs
= do { traceTc "tcInferTyApps {" (ppr orig_hs_ty $$ ppr orig_hs_args)
- ; (f_args, res_k) <- go_init 1 fun orig_hs_args
+ ; (f_args, res_k) <- go_init 1 fun orig_hs_args fam_arg_flvs
; traceTc "tcInferTyApps }" (ppr f_args <+> dcolon <+> ppr res_k)
; return (f_args, res_k) }
where
@@ -1608,7 +1609,8 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
-> TcType -- Function applied to some args
-> Subst -- Applies to function kind
-> TcKind -- Function kind
- -> [(LHsTypeArg GhcRn, FamArgType)] -- Un-type-checked args
+ -> [LHsTypeArg GhcRn] -- Un-type-checked args
+ -> [FamArgFlavour] -- Un-type-checked args
-> TcM (TcType, TcKind) -- Result type and its kind
-- INVARIANT: in any call (go n fun subst fun_ki args)
-- typeKind fun = subst(fun_ki)
@@ -1621,14 +1623,14 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
-- is apply 'fun' to an argument type.
-- Dispatch on all_args first, for performance reasons
- go n fun subst fun_ki all_args = case (all_args, tcSplitPiTy_maybe fun_ki) of
-
+ go n fun subst fun_ki all_args [] = error "tcInferTyApps_nosat: empty all_args"
+ go n fun subst fun_ki all_args arg_flvs@(arg_flv:rest_arg_flvs) = case (all_args, tcSplitPiTy_maybe fun_ki) of
---------------- No user-written args left. We're done!
([], _) -> return (fun, substTy subst fun_ki)
- ((arg,famArgTy):argtys, kb) -> do
+ (arg:argtys, kb) -> do
case (arg, kb) of
---------------- HsArgPar: We don't care about parens here
- (HsArgPar _, _) -> go n fun subst fun_ki argtys
+ (HsArgPar _, _) -> go n fun subst fun_ki argtys arg_flvs
---------------- HsTypeArg: a kind application (fun @ki)
(HsTypeArg _ hs_ki_arg, Just (ki_binder, inner_ki)) ->
@@ -1640,6 +1642,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
Named (Bndr _ Specified) -> -- Visible kind application
do { traceTc "tcInferTyApps (vis kind app)"
(vcat [ ppr ki_binder, ppr hs_ki_arg
+ , ppr arg_flv
, ppr (piTyBinderType ki_binder)
, ppr subst ])
@@ -1651,7 +1654,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
; traceTc "tcInferTyApps (vis kind app)" (ppr exp_kind)
; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg
- ; go (n+1) fun' subst' inner_ki argtys }
+ ; go (n+1) fun' subst' inner_ki argtys rest_arg_flvs }
-- Attempted visible kind application (fun @ki), but fun_ki is
-- forall k -> blah or k1 -> k2
@@ -1674,20 +1677,20 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
-> do { traceTc "tcInferTyApps (vis normal app)"
(vcat [ ppr ki_binder
, ppr arg
- , ppr famArgTy
+ , ppr arg_flv
, ppr (piTyBinderType ki_binder)
, ppr subst ])
; let exp_kind = substTy subst $ piTyBinderType ki_binder
; arg' <- addErrCtxt (FunAppCtxt (FunAppCtxtTy orig_hs_ty arg) n) $
- tc_check_lhs_type (updateFamArgType famArgTy mode) arg exp_kind
+ tc_check_lhs_type (updateFamArgFlavour arg_flv mode) arg exp_kind
; traceTc "tcInferTyApps (vis normal app) 2" (ppr exp_kind)
; (subst', fun') <- mkAppTyM subst fun ki_binder arg'
- ; go (n+1) fun' subst' inner_ki argtys }
+ ; go (n+1) fun' subst' inner_ki argtys rest_arg_flvs}
-- no binder; try applying the substitution, or infer another arrow in fun kind
(HsValArg _ _, Nothing)
-> try_again_after_substing_or $
- do { let arrows_needed = n_initial_val_args (fst <$> all_args)
+ do { let arrows_needed = n_initial_val_args all_args
; co <- matchExpectedFunKind (HsTypeRnThing $ unLoc hs_ty) arrows_needed substed_fun_ki
; fun' <- liftZonkM $ zonkTcType (fun `mkCastTy` co)
@@ -1699,27 +1702,27 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
, ppr arrows_needed
, ppr co
, ppr fun' <+> dcolon <+> ppr (typeKind fun')]
- ; go_init n fun' all_args }
+ ; go_init n fun' all_args arg_flvs}
-- Use go_init to establish go's INVARIANT
where
instantiate ki_binder inner_ki
= do { traceTc "tcInferTyApps (need to instantiate)"
- (vcat [ ppr ki_binder, ppr subst])
+ (vcat [ ppr ki_binder, ppr arg_flv, ppr subst ])
; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder
- ; go n (mkAppTy fun arg') subst' inner_ki all_args }
+ ; go n (mkAppTy fun arg') subst' inner_ki all_args rest_arg_flvs}
-- Because tcInvisibleTyBinder instantiate ki_binder,
-- the kind of arg' will have the same shape as the kind
-- of ki_binder. So we don't need mkAppTyM here.
try_again_after_substing_or fallthrough
| not (isEmptyTCvSubst subst)
- = go n fun zapped_subst substed_fun_ki all_args
+ = go n fun zapped_subst substed_fun_ki all_args arg_flvs
| otherwise
= fallthrough
zapped_subst = zapSubst subst
substed_fun_ki = substTy subst fun_ki
- hs_ty = appTypeToArg orig_hs_ty (take (n-1) $ fst <$> orig_hs_args)
+ hs_ty = appTypeToArg orig_hs_ty (take (n-1) orig_hs_args)
n_initial_val_args :: [HsArg p tm ty] -> Arity
-- Count how many leading HsValArgs we have
@@ -2258,7 +2261,7 @@ tcAnonWildCardOcc is_extra (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) }
HM_TyAppPat -> fsLit "_"
mk_wc_details = case hole_mode of
HM_FamPat FreeArg -> newTyVarMetaVarDetailsAtLevel
- HM_FamPat ClassArg -> newTyVarMetaVarDetailsAtLevel
+ HM_FamPat ClassArg -> newTauTvDetailsAtLevel
HM_FamPat SigArg -> newTauTvDetailsAtLevel
_ -> newTauTvDetailsAtLevel
emit_holes = case hole_mode of
=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -6,9 +6,7 @@ module GHC.Tc.Instance.Class (
ClsInstResult(..),
InstanceWhat(..), safeOverlap, instanceReturnsDictCon,
AssocInstInfo(..), isNotAssociated,
- lookupHasFieldLabel, FamArgType(..), PartialAssocInstInfo,
- buildAssocInstInfo, buildPatsArgTypes,
- assocInstInfoPartialAssocInstInfo, buildPatsModeTypes
+ lookupHasFieldLabel
) where
import GHC.Prelude
@@ -92,33 +90,7 @@ data AssocInstInfo
-- 'GHC.Tc.Validity.checkConsistentFamInst'
, ai_inst_env :: VarEnv Type -- ^ Maps /class/ tyvars to their instance types
-- See Note [Matching in the consistent-instantiation check]
- , ai_arg_types :: [FamArgType] -- ^ The types of the arguments to the associated type
}
-type PartialAssocInstInfo = Maybe (Class, [TyVar], VarEnv Type)
-
-assocInstInfoPartialAssocInstInfo :: AssocInstInfo -> PartialAssocInstInfo
-assocInstInfoPartialAssocInstInfo NotAssociated = Nothing
-assocInstInfoPartialAssocInstInfo (InClsInst {..}) = Just (ai_class, ai_tyvars, ai_inst_env)
-
-buildAssocInstInfo :: TyCon -> PartialAssocInstInfo -> AssocInstInfo
-buildAssocInstInfo _fam_tc Nothing = NotAssociated
-buildAssocInstInfo fam_tc (Just (cls, tvs, env))
- = InClsInst cls tvs env
- [ if elemVarEnv fam_tc_tv env then ClassArg else FreeArg | fam_tc_tv <- tyConTyVars fam_tc]
-
-buildPatsArgTypes :: (Outputable x) => AssocInstInfo -> [x] -> [(x, FamArgType)]
-buildPatsArgTypes NotAssociated xs = buildPatsModeTypes FreeArg xs
-buildPatsArgTypes (InClsInst {..}) xs = zip xs (ai_arg_types ++ cycle [FreeArg])
-
-buildPatsModeTypes :: FamArgType -> [x] -> [(x, FamArgType)]
-buildPatsModeTypes fa xs = (,fa) <$> xs
-
-data FamArgType = ClassArg | FreeArg | SigArg deriving (Eq, Show)
-
-instance Outputable FamArgType where
- ppr ClassArg = text "ClassArg"
- ppr FreeArg = text "FreeArg"
- ppr SigArg = text "SigArg"
isNotAssociated :: AssocInstInfo -> Bool
isNotAssociated (NotAssociated {}) = True
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -49,7 +49,7 @@ import {-# SOURCE #-} GHC.Tc.TyCl.Instance( tcInstDecls1 )
import {-# SOURCE #-} GHC.Tc.Module( checkBootDeclM )
import GHC.Tc.Deriv (DerivInfo(..))
import GHC.Tc.Gen.HsType
-import GHC.Tc.Instance.Class( AssocInstInfo(..), PartialAssocInstInfo)
+import GHC.Tc.Instance.Class( AssocInstInfo(..))
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.TcType
import GHC.Tc.Instance.Family
@@ -2659,68 +2659,79 @@ tcClassDecl1 :: RolesInfo -> Name -> Maybe (LHsContext GhcRn)
-> [LFamilyDecl GhcRn] -> [LTyFamDefltDecl GhcRn]
-> TcM Class
tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
- = fixM $ \ clas -> -- We need the knot because 'clas' is passed into tcClassATs
- bindTyClTyVars class_name $ \ tc_bndrs res_kind ->
- do { checkClassKindSig res_kind
- ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr tc_bndrs)
- ; let tycon_name = class_name -- We use the same name
- roles = roles_info tycon_name -- for TyCon and Class
-
- ; (ctxt, fds, sig_stuff, at_stuff)
- <- pushLevelAndSolveEqualities skol_info tc_bndrs $
- -- The (binderVars tc_bndrs) is needed bring into scope the
- -- skolems bound by the class decl header (#17841)
- do { ctxt <- tcHsContext hs_ctxt
- ; fds <- mapM (addLocM tc_fundep) fundeps
- ; sig_stuff <- tcClassSigs class_name sigs meths
- ; at_stuff <- tcClassATs class_name clas ats at_defs
- ; return (ctxt, fds, sig_stuff, at_stuff) }
-
- -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
- -- Example: (typecheck/should_fail/T17562)
- -- type C :: Type -> Type -> Constraint
- -- class (forall a. a b ~ a c) => C b c
- -- The kind of `a` is unconstrained.
- ; dvs <- candidateQTyVarsOfTypes ctxt
- ; let err_ctx tidy_env = do { (tidy_env2, ctxt) <- zonkTidyTcTypes tidy_env ctxt
- ; return (tidy_env2, UninfTyCtx_ClassContext ctxt) }
- ; doNotQuantifyTyVars dvs err_ctx
-
- -- The pushLevelAndSolveEqualities will report errors for any
- -- unsolved equalities, so these zonks should not encounter
- -- any unfilled coercion variables unless there is such an error
- -- The zonk also squeeze out the TcTyCons, and converts
- -- Skolems to tyvars.
- ; (bndrs, ctxt, sig_stuff) <- initZonkEnv NoFlexi $
- runZonkBndrT (zonkTyVarBindersX tc_bndrs) $ \ bndrs ->
- do { ctxt <- zonkTcTypesToTypesX ctxt
- ; sig_stuff <- mapM zonkTcMethInfoToMethInfoX sig_stuff
- -- ToDo: do we need to zonk at_stuff?
- ; return (bndrs, ctxt, sig_stuff) }
-
- -- TODO: Allow us to distinguish between abstract class,
- -- and concrete class with no methods (maybe by
- -- specifying a trailing where or not
-
- ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
- ; is_boot <- tcIsHsBootOrSig
- ; let body | is_boot, isNothing hs_ctxt, null at_stuff, null sig_stuff
- -- We use @isNothing hs_ctxt@ rather than @null ctxt@,
- -- so that a declaration in an hs-boot file such as:
- --
- -- class () => C a b | a -> b
- --
- -- is not considered abstract; it's sometimes useful
- -- to be able to declare such empty classes in hs-boot files.
- -- See #20661.
- = Nothing
- | otherwise
- = Just (ctxt, at_stuff, sig_stuff, mindef)
-
- ; clas <- buildClass class_name bndrs roles fds body
- ; traceTc "tcClassDecl" (ppr fundeps $$ ppr bndrs $$
- ppr fds)
- ; return clas }
+ = do { cls <-
+ fixM $ \ clas -> -- We need the knot because 'clas' is passed into tcClassATs
+ bindTyClTyVars class_name $ \ tc_bndrs res_kind ->
+ do { checkClassKindSig res_kind
+ ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr tc_bndrs)
+ ; let tycon_name = class_name -- We use the same name
+ roles = roles_info tycon_name -- for TyCon and Class
+
+ ; (ctxt, fds, sig_stuff, at_stuff)
+ <- pushLevelAndSolveEqualities skol_info tc_bndrs $
+ -- The (binderVars tc_bndrs) is needed bring into scope the
+ -- skolems bound by the class decl header (#17841)
+ do { ctxt <- tcHsContext hs_ctxt
+ ; fds <- mapM (addLocM tc_fundep) fundeps
+ ; sig_stuff <- tcClassSigs class_name sigs meths
+ ; at_stuff <- tcClassATs class_name clas ats at_defs
+ ; return (ctxt, fds, sig_stuff, at_stuff) }
+
+ -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
+ -- Example: (typecheck/should_fail/T17562)
+ -- type C :: Type -> Type -> Constraint
+ -- class (forall a. a b ~ a c) => C b c
+ -- The kind of `a` is unconstrained.
+ ; dvs <- candidateQTyVarsOfTypes ctxt
+ ; let err_ctx tidy_env = do { (tidy_env2, ctxt) <- zonkTidyTcTypes tidy_env ctxt
+ ; return (tidy_env2, UninfTyCtx_ClassContext ctxt) }
+ ; doNotQuantifyTyVars dvs err_ctx
+
+ -- The pushLevelAndSolveEqualities will report errors for any
+ -- unsolved equalities, so these zonks should not encounter
+ -- any unfilled coercion variables unless there is such an error
+ -- The zonk also squeeze out the TcTyCons, and converts
+ -- Skolems to tyvars.
+ ; (bndrs, ctxt, sig_stuff) <- initZonkEnv NoFlexi $
+ runZonkBndrT (zonkTyVarBindersX tc_bndrs) $ \ bndrs ->
+ do { ctxt <- zonkTcTypesToTypesX ctxt
+ ; sig_stuff <- mapM zonkTcMethInfoToMethInfoX sig_stuff
+ -- ToDo: do we need to zonk at_stuff?
+ ; return (bndrs, ctxt, sig_stuff) }
+
+ -- TODO: Allow us to distinguish between abstract class,
+ -- and concrete class with no methods (maybe by
+ -- specifying a trailing where or not
+
+ ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
+ ; is_boot <- tcIsHsBootOrSig
+ ; let body | is_boot, isNothing hs_ctxt, null at_stuff, null sig_stuff
+ -- We use @isNothing hs_ctxt@ rather than @null ctxt@,
+ -- so that a declaration in an hs-boot file such as:
+ --
+ -- class () => C a b | a -> b
+ --
+ -- is not considered abstract; it's sometimes useful
+ -- to be able to declare such empty classes in hs-boot files.
+ -- See #20661.
+ = Nothing
+ | otherwise
+ = Just (ctxt, at_stuff, sig_stuff, mindef)
+
+ ; clas <- buildClass class_name bndrs roles fds body
+ ; traceTc "tcClassDecl" (ppr fundeps $$ ppr bndrs $$ ppr fds)
+ ; return clas }
+ ; mapM_
+ (\tc ->
+ traceTc "tcClassDecl assoc type class:"
+ (vcat
+ [ ppr tc
+ , text "tyConBinders:" <+> ppr (tyConBinders tc)
+ , text "tyConTyVars:" <+> ppr (tyConTyVars tc)
+ , text "tyConFamArgFlavours:" <+> ppr (tyConFamArgFlavours tc)
+ ]))
+ $ map (\(ATI ty _) -> ty) $ classATItems cls
+ ; return cls }
where
skol_info = TyConSkol ClassFlavour class_name
@@ -3253,7 +3264,7 @@ kcTyFamInstEqn tc_fam_tc
; discardResult $
bindOuterFamEqnTKBndrs_Q_Tv outer_bndrs $
- do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats NotAssociated
+ do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats
; tcCheckLHsTypeInContext hs_rhs_ty (TheKind res_kind) }
-- Why "_Tv" here? Consider (#14066)
-- type family Bar x y where
@@ -3279,7 +3290,7 @@ tcTyFamInstEqn fam_tc mb_clsinfo
, text "fam tc bndrs" <+> pprTyVars (tyConTyVars fam_tc)
, case mb_clsinfo of
NotAssociated {} -> empty
- InClsInst { ai_class = cls, ai_arg_types = arg_types } -> text "class" <+> ppr cls <+> pprTyVars (classTyVars cls) <+> ppr arg_types]
+ InClsInst { ai_class = cls } -> text "class" <+> ppr cls <+> pprTyVars (classTyVars cls) ]
; checkTyFamInstEqn fam_tc eqn_tc_name hs_pats
@@ -3430,7 +3441,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
; (tclvl, wanted, (outer_bndrs, (lhs_ty, rhs_ty)))
<- pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $
bindOuterFamEqnTKBndrs skol_info outer_hs_bndrs $
- do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats mb_clsinfo
+ do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats
-- Ensure that the instance is consistent with its
-- parent class (#16008)
; addConsistencyConstraints mb_clsinfo lhs_ty
@@ -5539,19 +5550,19 @@ tcAddDeclCtxt :: TyClDecl GhcRn -> TcM a -> TcM a
tcAddDeclCtxt decl thing_inside
= addErrCtxt (tcMkDeclCtxt decl) thing_inside
-tcAddOpenTyFamInstCtxt :: PartialAssocInstInfo -> TyFamInstDecl GhcRn -> TcM a -> TcM a
+tcAddOpenTyFamInstCtxt :: AssocInstInfo -> TyFamInstDecl GhcRn -> TcM a -> TcM a
tcAddOpenTyFamInstCtxt mb_assoc decl
= tcAddFamInstCtxt flav (tyFamInstDeclName decl)
where
assoc = case mb_assoc of
- Nothing -> Nothing
- Just (cls,_,_) -> Just $ classTyCon cls
+ NotAssociated -> Nothing
+ InClsInst { ai_class = cls } -> Just $ classTyCon cls
flav = TyConInstFlavour
{ tyConInstFlavour = OpenFamilyFlavour IAmType assoc
, tyConInstIsDefault = False
}
-tcMkDataFamInstCtxt :: PartialAssocInstInfo -> NewOrData -> DataFamInstDecl GhcRn -> ErrCtxtMsg
+tcMkDataFamInstCtxt :: AssocInstInfo -> NewOrData -> DataFamInstDecl GhcRn -> ErrCtxtMsg
tcMkDataFamInstCtxt mb_assoc new_or_data (DataFamInstDecl { dfid_eqn = eqn })
= TyConInstCtxt (unLoc (feqn_tycon eqn))
(TyConInstFlavour
@@ -5560,10 +5571,10 @@ tcMkDataFamInstCtxt mb_assoc new_or_data (DataFamInstDecl { dfid_eqn = eqn })
})
where
assoc = case mb_assoc of
- Nothing -> Nothing
- Just (cls,_,_) -> Just $ classTyCon cls
+ NotAssociated -> Nothing
+ InClsInst { ai_class = cls } -> Just $ classTyCon cls
-tcAddDataFamInstCtxt :: PartialAssocInstInfo -> NewOrData -> DataFamInstDecl GhcRn -> TcM a -> TcM a
+tcAddDataFamInstCtxt :: AssocInstInfo -> NewOrData -> DataFamInstDecl GhcRn -> TcM a -> TcM a
tcAddDataFamInstCtxt assoc new_or_data decl
= addErrCtxt (tcMkDataFamInstCtxt assoc new_or_data decl)
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -43,7 +43,7 @@ import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.TyCl.Build
import GHC.Tc.Utils.Instantiate
-import GHC.Tc.Instance.Class( AssocInstInfo(..), isNotAssociated, PartialAssocInstInfo, buildAssocInstInfo, assocInstInfoPartialAssocInstInfo )
+import GHC.Tc.Instance.Class( AssocInstInfo(..), isNotAssociated )
import GHC.Core.Multiplicity
import GHC.Core.InstEnv
import GHC.Tc.Instance.Family
@@ -472,11 +472,11 @@ tcLocalInstDecl :: LInstDecl GhcRn
--
-- We check for respectable instance type, and context
tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
- = do { fam_inst <- tcTyFamInstDecl Nothing (L loc decl)
+ = do { fam_inst <- tcTyFamInstDecl NotAssociated (L loc decl)
; return ([], [fam_inst], []) }
tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
- = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl Nothing emptyVarEnv (L loc decl)
+ = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl NotAssociated emptyVarEnv (L loc decl)
; return ([], [fam_inst], maybeToList m_deriv_info) }
tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
@@ -515,7 +515,9 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_ext = lwarn
<- tcExtendNameTyVarEnv tv_skol_prs $
do { let mini_env = mkVarEnv (classTyVars clas `zip` substTys subst inst_tys)
mini_subst = mkTvSubst (mkInScopeSet (mkVarSet skol_tvs)) mini_env
- mb_info = Just (clas, visible_skol_tvs, mini_env)
+ mb_info = InClsInst { ai_class = clas
+ , ai_tyvars = visible_skol_tvs
+ , ai_inst_env = mini_env }
; df_stuff <- mapAndRecoverM (tcDataFamInstDecl mb_info tv_skol_env) adts
; tf_insts1 <- mapAndRecoverM (tcTyFamInstDecl mb_info) ats
@@ -585,16 +587,15 @@ lot of kinding and type checking code with ordinary algebraic data types (and
GADTs).
-}
-tcTyFamInstDecl :: PartialAssocInstInfo
+tcTyFamInstDecl :: AssocInstInfo
-> LTyFamInstDecl GhcRn -> TcM FamInst
-- "type instance"; open type families only
-- See Note [Associated type instances]
-tcTyFamInstDecl partial_mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
+tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
= setSrcSpanA loc $
- tcAddOpenTyFamInstCtxt partial_mb_clsinfo decl $
+ tcAddOpenTyFamInstCtxt mb_clsinfo decl $
do { let fam_lname = feqn_tycon eqn
; fam_tc <- tcLookupLocatedTyCon fam_lname
- ; let mb_clsinfo = buildAssocInstInfo fam_tc partial_mb_clsinfo
; tcFamInstDeclChecks mb_clsinfo IAmType fam_tc
-- (0) Check it's an open type family
@@ -681,7 +682,7 @@ than type family instances
-}
tcDataFamInstDecl ::
- PartialAssocInstInfo
+ AssocInstInfo
-> TyVarEnv Name -- If this is an associated data family instance, maps the
-- parent class's skolemized type variables to their
-- original Names. If this is a non-associated instance,
@@ -689,7 +690,7 @@ tcDataFamInstDecl ::
-- See Note [Associated data family instances and di_scoped_tvs].
-> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
-- "newtype instance" and "data instance"
-tcDataFamInstDecl partial_mb_clsinfo tv_skol_env
+tcDataFamInstDecl mb_clsinfo tv_skol_env
(L loc decl@(DataFamInstDecl { dfid_eqn =
FamEqn { feqn_bndrs = outer_bndrs
, feqn_pats = hs_pats
@@ -701,9 +702,9 @@ tcDataFamInstDecl partial_mb_clsinfo tv_skol_env
, dd_kindSig = m_ksig
, dd_derivs = derivs } }}))
= setSrcSpanA loc $
- tcAddDataFamInstCtxt partial_mb_clsinfo new_or_data decl $
+ tcAddDataFamInstCtxt mb_clsinfo new_or_data decl $
do { fam_tc <- tcLookupLocatedTyCon lfam_name
- ; let mb_clsinfo = buildAssocInstInfo fam_tc partial_mb_clsinfo
+
; tcFamInstDeclChecks mb_clsinfo (IAmData new_or_data) fam_tc
-- Check that the family declaration is for the right kind
@@ -843,7 +844,7 @@ tcDataFamInstDecl partial_mb_clsinfo tv_skol_env
Just $ DerivInfo { di_rep_tc = rep_tc
, di_scoped_tvs = scoped_tvs
, di_clauses = preds
- , di_ctxt = tcMkDataFamInstCtxt (assocInstInfoPartialAssocInstInfo mb_clsinfo) new_or_data decl
+ , di_ctxt = tcMkDataFamInstCtxt mb_clsinfo new_or_data decl
}
; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
@@ -933,7 +934,7 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
<- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
bindOuterFamEqnTKBndrs skol_info hs_outer_bndrs $ -- Binds skolem TcTyVars
do { stupid_theta <- tcHsContext hs_ctxt
- ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats mb_clsinfo
+ ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
; (lhs_applied_ty, lhs_applied_kind)
<- tcInstInvisibleTyBinders lhs_ty lhs_kind
-- See Note [Data family/instance return kinds]
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9869fe5d2bda18d7d5624ebeeff7ab6e7ff0b0ac...dbe81ead0bf274ecd7039be8df39624a9e2b1aa3
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9869fe5d2bda18d7d5624ebeeff7ab6e7ff0b0ac...dbe81ead0bf274ecd7039be8df39624a9e2b1aa3
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/20250304/abe66a3c/attachment-0001.html>
More information about the ghc-commits
mailing list