summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc')
-rw-r--r--compiler/GHC/Tc/Errors/Hole.hs10
-rw-r--r--compiler/GHC/Tc/Gen/Arrow.hs2
-rw-r--r--compiler/GHC/Tc/Gen/Bind.hs19
-rw-r--r--compiler/GHC/Tc/Gen/Expr.hs4
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs136
-rw-r--r--compiler/GHC/Tc/Gen/Match.hs10
-rw-r--r--compiler/GHC/Tc/Gen/Rule.hs9
-rw-r--r--compiler/GHC/Tc/Gen/Sig.hs55
-rw-r--r--compiler/GHC/Tc/Gen/Splice.hs80
-rw-r--r--compiler/GHC/Tc/Module.hs6
-rw-r--r--compiler/GHC/Tc/Solver.hs6
-rw-r--r--compiler/GHC/Tc/TyCl.hs113
-rw-r--r--compiler/GHC/Tc/TyCl/Build.hs16
-rw-r--r--compiler/GHC/Tc/TyCl/Instance.hs4
-rw-r--r--compiler/GHC/Tc/TyCl/PatSyn.hs38
-rw-r--r--compiler/GHC/Tc/TyCl/Utils.hs4
-rw-r--r--compiler/GHC/Tc/Types.hs10
-rw-r--r--compiler/GHC/Tc/Utils/TcMType.hs84
-rw-r--r--compiler/GHC/Tc/Utils/TcType.hs17
19 files changed, 368 insertions, 255 deletions
diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs
index c764d7d3e3..0639e79073 100644
--- a/compiler/GHC/Tc/Errors/Hole.hs
+++ b/compiler/GHC/Tc/Errors/Hole.hs
@@ -441,10 +441,12 @@ pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) (HoleFit {..}) =
where name = getName hfCand
tyApp = sep $ zipWithEqual "pprHoleFit" pprArg vars hfWrap
where pprArg b arg = case binderArgFlag b of
- Specified -> text "@" <> pprParendType arg
- -- Do not print type application for inferred
- -- variables (#16456)
- Inferred -> empty
+ -- See Note [Explicit Case Statement for Specificity]
+ (Invisible spec) -> case spec of
+ SpecifiedSpec -> text "@" <> pprParendType arg
+ -- Do not print type application for inferred
+ -- variables (#16456)
+ InferredSpec -> empty
Required -> pprPanic "pprHoleFit: bad Required"
(ppr b <+> ppr arg)
tyAppVars = sep $ punctuate comma $
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 6ac42a76d0..ef60b3cea7 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -307,7 +307,7 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty)
= addErrCtxt (cmdCtxt cmd) $
do { (cmd_args', cmd_tys) <- mapAndUnzipM tc_cmd_arg cmd_args
-- We use alphaTyVar for 'w'
- ; let e_ty = mkInvForAllTy alphaTyVar $
+ ; let e_ty = mkInfForAllTy alphaTyVar $
mkVisFunTys cmd_tys $
mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty
; expr' <- tcCheckExpr expr e_ty
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index c2af14b93d..1870531f60 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -907,7 +907,7 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
; (binders, theta') <- chooseInferredQuantifiers inferred_theta
(tyCoVarsOfType mono_ty') qtvs mb_sig_inst
- ; let inferred_poly_ty = mkForAllTys binders (mkPhiTy theta' mono_ty')
+ ; let inferred_poly_ty = mkInvisForAllTys binders (mkPhiTy theta' mono_ty')
; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta'
, ppr inferred_poly_ty])
@@ -926,13 +926,13 @@ chooseInferredQuantifiers :: TcThetaType -- inferred
-> TcTyVarSet -- tvs free in tau type
-> [TcTyVar] -- inferred quantified tvs
-> Maybe TcIdSigInst
- -> TcM ([TyVarBinder], TcThetaType)
+ -> TcM ([InvisTVBinder], TcThetaType)
chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
= -- No type signature (partial or complete) for this binder,
do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
-- Include kind variables! #7916
my_theta = pickCapturedPreds free_tvs inferred_theta
- binders = [ mkTyVarBinder Inferred tv
+ binders = [ mkTyVarBinder InferredSpec tv
| tv <- qtvs
, tv `elemVarSet` free_tvs ]
; return (binders, my_theta) }
@@ -943,7 +943,8 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
, sig_inst_theta = annotated_theta
, sig_inst_skols = annotated_tvs }))
= -- Choose quantifiers for a partial type signature
- do { psig_qtv_prs <- zonkTyVarTyVarPairs annotated_tvs
+ do { psig_qtvbndr_prs <- zonkTyVarTyVarPairs annotated_tvs
+ ; let psig_qtv_prs = mapSnd binderVar psig_qtvbndr_prs
-- Check whether the quantified variables of the
-- partial signature have been unified together
@@ -957,7 +958,8 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs
, not (tv `elem` qtvs) ]
- ; let psig_qtvs = mkVarSet (map snd psig_qtv_prs)
+ ; let psig_qtvbndrs = map snd psig_qtvbndr_prs
+ psig_qtvs = mkVarSet (map snd psig_qtv_prs)
; annotated_theta <- zonkTcTypes annotated_theta
; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx
@@ -966,8 +968,9 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
final_qtvs = [ mkTyVarBinder vis tv
| tv <- qtvs -- Pulling from qtvs maintains original order
, tv `elemVarSet` keep_me
- , let vis | tv `elemVarSet` psig_qtvs = Specified
- | otherwise = Inferred ]
+ , let vis = case lookupVarBndr tv psig_qtvbndrs of
+ Just spec -> spec
+ Nothing -> InferredSpec ]
; return (final_qtvs, my_theta) }
where
@@ -1447,7 +1450,7 @@ tcExtendTyVarEnvFromSig :: TcIdSigInst -> TcM a -> TcM a
tcExtendTyVarEnvFromSig sig_inst thing_inside
| TISI { sig_inst_skols = skol_prs, sig_inst_wcs = wcs } <- sig_inst
= tcExtendNameTyVarEnv wcs $
- tcExtendNameTyVarEnv skol_prs $
+ tcExtendNameTyVarEnv (mapSnd binderVar skol_prs) $
thing_inside
tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 3a89daac0b..2d6b25df10 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -1709,7 +1709,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
do { (tclvl, wanted, (expr', sig_inst))
<- pushLevelAndCaptureConstraints $
do { sig_inst <- tcInstSig sig
- ; expr' <- tcExtendNameTyVarEnv (sig_inst_skols sig_inst) $
+ ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $
tcExtendNameTyVarEnv (sig_inst_wcs sig_inst) $
tcCheckExprNC expr (sig_inst_tau sig_inst)
; return (expr', sig_inst) }
@@ -1730,7 +1730,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta
tau_tvs qtvs (Just sig_inst)
; let inferred_sigma = mkInfSigmaTy qtvs inferred_theta tau
- my_sigma = mkForAllTys binders (mkPhiTy my_theta tau)
+ my_sigma = mkInvisForAllTys binders (mkPhiTy my_theta tau)
; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis.
then return idHsWrapper -- Fast path; also avoids complaint when we infer
-- an ambiguous type and have AllowAmbiguousType
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index cd48e5416f..328ed43d65 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -304,7 +304,7 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
tc_lvl wanted
- ; return (insolubleWC wanted, mkInvForAllTys kvs ty1) }
+ ; return (insolubleWC wanted, mkInfForAllTys kvs ty1) }
tcTopLHsType :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
-- tcTopLHsType is used for kind-checking top-level HsType where
@@ -325,7 +325,7 @@ tcTopLHsType mode hs_sig_type ctxt_kind
; spec_tkvs <- zonkAndScopedSort spec_tkvs
; let ty1 = mkSpecForAllTys spec_tkvs ty
; kvs <- kindGeneralizeAll ty1 -- "All" because it's a top-level type
- ; final_ty <- zonkTcTypeToType (mkInvForAllTys kvs ty1)
+ ; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)
; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty])
; return final_ty}
@@ -717,23 +717,35 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
--------- Foralls
tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
, hst_body = ty }) exp_kind
- = do { (tclvl, wanted, (tvs', ty'))
+ = do { (tclvl, wanted, (inv_tv_bndrs, ty'))
<- pushLevelAndCaptureConstraints $
bindExplicitTKBndrs_Skol hs_tvs $
tc_lhs_type mode ty exp_kind
-- Do not kind-generalise here! See Note [Kind generalisation]
-- Why exp_kind? See Note [Body kind of HsForAllTy]
- ; let argf = case fvf of
- ForallVis -> Required
- ForallInvis -> Specified
- bndrs = mkTyVarBinders argf tvs'
- skol_info = ForAllSkol (ppr forall)
+ ; let skol_info = ForAllSkol (ppr forall)
m_telescope = Just (sep (map ppr hs_tvs))
- ; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted
- -- See Note [Skolem escape and forall-types]
+ ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs
- ; return (mkForAllTys bndrs ty') }
+ ; emitResidualTvConstraint skol_info m_telescope (binderVars tv_bndrs) tclvl wanted
+
+ ; return (mkForAllTys tv_bndrs ty') }
+ where
+ construct_bndr :: TcInvisTVBinder -> TcM TcTyVarBinder
+ construct_bndr (Bndr tv spec) = do { argf <- spec_to_argf spec
+ ; return $ mkTyVarBinder argf tv }
+
+ -- See Note [Variable Specificity and Forall Visibility]
+ spec_to_argf :: Specificity -> TcM ArgFlag
+ spec_to_argf SpecifiedSpec = case fvf of
+ ForallVis -> return Required
+ ForallInvis -> return Specified
+ spec_to_argf InferredSpec = case fvf of
+ ForallVis -> do { addErrTc (hang (text "Unexpected inferred variable in visible forall binder:")
+ 2 (ppr forall))
+ ; return Required }
+ ForallInvis -> return Inferred
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
| null (unLoc ctxt)
@@ -865,6 +877,29 @@ tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type _ wc@(HsWildCardTy _) ek = tcAnonWildCardOcc wc ek
+{-
+Note [Variable Specificity and Forall Visibility]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A HsForAllTy contains a ForAllVisFlag to denote the visibility of the forall
+binder. Furthermore, each bound variable also has a Specificity. Together these
+determine the variable binders (ArgFlag) for each variable in the generated
+ForAllTy type.
+
+This table summarises this relation:
+--------------------------------------------------------------------------
+| User-written type ForAllVisFlag Specificity ArgFlag
+|-------------------------------------------------------------------------
+| f :: forall a. type ForallInvis SpecifiedSpec Specified
+| f :: forall {a}. type ForallInvis InferredSpec Inferred
+| f :: forall a -> type ForallVis SpecifiedSpec Required
+| f :: forall {a} -> type ForallVis InferredSpec /
+| This last form is non-sensical and is thus rejected.
+--------------------------------------------------------------------------
+
+For more information regarding the interpretation of the resulting ArgFlag, see
+Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
+-}
+
------------------------------------------
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
-> TcM TcType
@@ -2204,8 +2239,8 @@ kcCheckDeclHeader_sig kisig name flav
check_zipped_binder (ZippedBinder _ Nothing) = return ()
check_zipped_binder (ZippedBinder tb (Just b)) =
case unLoc b of
- UserTyVar _ _ -> return ()
- KindedTyVar _ v v_hs_ki -> do
+ UserTyVar _ _ _ -> return ()
+ KindedTyVar _ _ v v_hs_ki -> do
v_ki <- tcLHsKindSig (TyVarBndrKindCtxt (unLoc v)) v_hs_ki
discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
unifyKind (Just (HsTyVar noExtField NotPromoted v))
@@ -2228,14 +2263,14 @@ kcCheckDeclHeader_sig kisig name flav
-- A quantifier from a kind signature zipped with a user-written binder for it.
data ZippedBinder =
- ZippedBinder TyBinder (Maybe (LHsTyVarBndr GhcRn))
+ ZippedBinder TyBinder (Maybe (LHsTyVarBndr () GhcRn))
-- See Note [Arity inference in kcCheckDeclHeader_sig]
zipBinders
:: Kind -- kind signature
- -> [LHsTyVarBndr GhcRn] -- user-written binders
+ -> [LHsTyVarBndr () GhcRn] -- user-written binders
-> ([ZippedBinder], -- zipped binders
- [LHsTyVarBndr GhcRn], -- remaining user-written binders
+ [LHsTyVarBndr () GhcRn], -- remaining user-written binders
Kind) -- remainder of the kind signature
zipBinders = zip_binders []
where
@@ -2249,15 +2284,14 @@ zipBinders = zip_binders []
| otherwise = (ZippedBinder tb Nothing, b:bs)
zippable =
case tb of
- Named (Bndr _ Specified) -> False
- Named (Bndr _ Inferred) -> False
- Named (Bndr _ Required) -> True
+ Named (Bndr _ (Invisible _)) -> False
+ Named (Bndr _ Required) -> True
Anon InvisArg _ -> False
Anon VisArg _ -> True
in
zip_binders (zb:acc) ki' bs'
-tooManyBindersErr :: Kind -> [LHsTyVarBndr GhcRn] -> SDoc
+tooManyBindersErr :: Kind -> [LHsTyVarBndr () GhcRn] -> SDoc
tooManyBindersErr ki bndrs =
hang (text "Not a function kind:")
4 (ppr ki) $$
@@ -2664,9 +2698,10 @@ cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar
--------------------------------------
bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
- :: [LHsTyVarBndr GhcRn]
+ :: (OutputableBndrFlag flag)
+ => [LHsTyVarBndr flag GhcRn]
-> TcM a
- -> TcM ([TcTyVar], a)
+ -> TcM ([VarBndr TyVar flag], a)
bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr newSkolemTyVar)
bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr cloneTyVarTyVar)
@@ -2675,21 +2710,30 @@ bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr cloneTyVarTyVar)
bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv
:: ContextKind
- -> [LHsTyVarBndr GhcRn]
+ -> [LHsTyVarBndr () GhcRn]
-> TcM a
-> TcM ([TcTyVar], a)
-bindExplicitTKBndrs_Q_Skol ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newSkolemTyVar)
-bindExplicitTKBndrs_Q_Tv ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newTyVarTyVar)
+bindExplicitTKBndrs_Q_Skol ctxt_kind = bindExplicitTKBndrsX_Q (tcHsQTyVarBndr ctxt_kind newSkolemTyVar)
+bindExplicitTKBndrs_Q_Tv ctxt_kind = bindExplicitTKBndrsX_Q (tcHsQTyVarBndr ctxt_kind newTyVarTyVar)
-- See Note [Non-cloning for tyvar binders]
-
-bindExplicitTKBndrsX
- :: (HsTyVarBndr GhcRn -> TcM TcTyVar)
- -> [LHsTyVarBndr GhcRn]
+bindExplicitTKBndrsX_Q
+ :: (HsTyVarBndr () GhcRn -> TcM TcTyVar)
+ -> [LHsTyVarBndr () GhcRn]
-> TcM a
-> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
-- with the passed-in [LHsTyVarBndr]
+bindExplicitTKBndrsX_Q tc_tv hs_tvs thing_inside
+ = do { (tv_bndrs,res) <- bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
+ ; return ((binderVars tv_bndrs),res) }
+
+bindExplicitTKBndrsX :: (OutputableBndrFlag flag)
+ => (HsTyVarBndr flag GhcRn -> TcM TcTyVar)
+ -> [LHsTyVarBndr flag GhcRn]
+ -> TcM a
+ -> TcM ([VarBndr TyVar flag], a) -- Returned [TcTyVar] are in 1-1 correspondence
+ -- with the passed-in [LHsTyVarBndr]
bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
= do { traceTc "bindExplicTKBndrs" (ppr hs_tvs)
; go hs_tvs }
@@ -2705,33 +2749,33 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
-- See GHC.Tc.Utils.TcMType Note [Cloning for tyvar binders]
; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
go hs_tvs
- ; return (tv:tvs, res) }
+ ; return ((Bndr tv (hsTyVarBndrFlag hs_tv)):tvs, res) }
-----------------
tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
- -> HsTyVarBndr GhcRn -> TcM TcTyVar
-tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
+ -> HsTyVarBndr flag GhcRn -> TcM TcTyVar
+tcHsTyVarBndr new_tv (UserTyVar _ _ (L _ tv_nm))
= do { kind <- newMetaKindVar
; new_tv tv_nm kind }
-tcHsTyVarBndr new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
+tcHsTyVarBndr new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind)
= do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
; new_tv tv_nm kind }
-----------------
tcHsQTyVarBndr :: ContextKind
-> (Name -> Kind -> TcM TyVar)
- -> HsTyVarBndr GhcRn -> TcM TcTyVar
+ -> HsTyVarBndr () GhcRn -> TcM TcTyVar
-- Just like tcHsTyVarBndr, but also
-- - uses the in-scope TyVar from class, if it exists
-- - takes a ContextKind to use for the no-sig case
-tcHsQTyVarBndr ctxt_kind new_tv (UserTyVar _ (L _ tv_nm))
+tcHsQTyVarBndr ctxt_kind new_tv (UserTyVar _ _ (L _ tv_nm))
= do { mb_tv <- tcLookupLcl_maybe tv_nm
; case mb_tv of
Just (ATyVar _ tv) -> return tv
_ -> do { kind <- newExpectedKind ctxt_kind
; new_tv tv_nm kind } }
-tcHsQTyVarBndr _ new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
+tcHsQTyVarBndr _ new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind)
= do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
; mb_tv <- tcLookupLcl_maybe tv_nm
; case mb_tv of
@@ -3156,7 +3200,7 @@ tcHsPartialSigType
-> LHsSigWcType GhcRn -- The type signature
-> TcM ( [(Name, TcTyVar)] -- Wildcards
, Maybe TcType -- Extra-constraints wildcard
- , [(Name,TcTyVar)] -- Original tyvar names, in correspondence with
+ , [(Name,InvisTVBinder)] -- Original tyvar names, in correspondence with
-- the implicitly and explicitly bound type variables
, TcThetaType -- Theta part
, TcType ) -- Tau part
@@ -3167,7 +3211,7 @@ tcHsPartialSigType ctxt sig_ty
, hsib_body = hs_ty } <- ib_ty
, (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTyInvis hs_ty
= addSigCtxt ctxt hs_ty $
- do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
+ do { (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau)))
<- solveLocalEqualities "tcHsPartialSigType" $
-- This solveLocalEqualiltes fails fast if there are
-- insoluble equalities. See GHC.Tc.Solver
@@ -3183,9 +3227,11 @@ tcHsPartialSigType ctxt sig_ty
; return (wcs, wcx, theta, tau) }
- -- No kind-generalization here, but perhaps some promotion
- ; kindGeneralizeNone (mkSpecForAllTys implicit_tvs $
- mkSpecForAllTys explicit_tvs $
+ ; let implicit_tvbndrs = map (mkTyVarBinder SpecifiedSpec) implicit_tvs
+
+ -- No kind-generalization here:
+ ; kindGeneralizeNone (mkInvisForAllTys implicit_tvbndrs $
+ mkInvisForAllTys explicit_tvbndrs $
mkPhiTy theta $
tau)
@@ -3197,16 +3243,14 @@ tcHsPartialSigType ctxt sig_ty
-- Zonk, so that any nested foralls can "see" their occurrences
-- See Note [Checking partial type signatures], in
-- the bullet on Nested foralls.
- ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
- ; explicit_tvs <- mapM zonkTcTyVarToTyVar explicit_tvs
; theta <- mapM zonkTcType theta
; tau <- zonkTcType tau
- -- We return a proper (Name,TyVar) environment, to be sure that
+ -- We return a proper (Name,InvisTVBinder) environment, to be sure that
-- we bring the right name into scope in the function body.
-- Test case: partial-sigs/should_compile/LocalDefinitionBug
- ; let tv_prs = (implicit_hs_tvs `zip` implicit_tvs)
- ++ (hsLTyVarNames explicit_hs_tvs `zip` explicit_tvs)
+ ; let tv_prs = (implicit_hs_tvs `zip` implicit_tvbndrs)
+ ++ (hsLTyVarNames explicit_hs_tvs `zip` explicit_tvbndrs)
-- NB: checkValidType on the final inferred type will be
-- done later by checkInferredPolyId. We can't do it
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index 857470b155..350be10236 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -513,7 +513,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
tup_ty = mkBigCoreVarTupTy bndr_ids
poly_arg_ty = m_app alphaTy
poly_res_ty = m_app (n_app alphaTy)
- using_poly_ty = mkInvForAllTy alphaTyVar $
+ using_poly_ty = mkInfForAllTy alphaTyVar $
by_arrow $
poly_arg_ty `mkVisFunTy` poly_res_ty
@@ -654,7 +654,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
using_arg_ty = m1_ty `mkAppTy` tup_ty
poly_res_ty = m2_ty `mkAppTy` n_app alphaTy
using_res_ty = m2_ty `mkAppTy` n_app tup_ty
- using_poly_ty = mkInvForAllTy alphaTyVar $
+ using_poly_ty = mkInfForAllTy alphaTyVar $
by_arrow $
poly_arg_ty `mkVisFunTy` poly_res_ty
@@ -694,8 +694,8 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
; fmap_op' <- case form of
ThenForm -> return noExpr
_ -> fmap unLoc . tcCheckExpr (noLoc fmap_op) $
- mkInvForAllTy alphaTyVar $
- mkInvForAllTy betaTyVar $
+ mkInfForAllTy alphaTyVar $
+ mkInfForAllTy betaTyVar $
(alphaTy `mkVisFunTy` betaTy)
`mkVisFunTy` (n_app alphaTy)
`mkVisFunTy` (n_app betaTy)
@@ -759,7 +759,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside
= do { m_ty <- newFlexiTyVarTy typeToTypeKind
- ; let mzip_ty = mkInvForAllTys [alphaTyVar, betaTyVar] $
+ ; let mzip_ty = mkInfForAllTys [alphaTyVar, betaTyVar] $
(m_ty `mkAppTy` alphaTy)
`mkVisFunTy`
(m_ty `mkAppTy` betaTy)
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index 3ed75ac49b..c788f15437 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -180,7 +180,7 @@ tcRule (HsRule { rd_ext = ext
, rd_lhs = mkHsDictLet lhs_binds lhs'
, rd_rhs = mkHsDictLet rhs_binds rhs' } }
-generateRuleConstraints :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn]
+generateRuleConstraints :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
-> LHsExpr GhcRn -> LHsExpr GhcRn
-> TcM ( [TcId]
, LHsExpr GhcTc, WantedConstraints
@@ -204,11 +204,12 @@ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs
; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
-- See Note [TcLevel in type checking rules]
-tcRuleBndrs :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn]
+tcRuleBndrs :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
-> TcM ([TcTyVar], [Id])
tcRuleBndrs (Just bndrs) xs
- = do { (tys1,(tys2,tms)) <- bindExplicitTKBndrs_Skol bndrs $
- tcRuleTmBndrs xs
+ = do { (tybndrs1,(tys2,tms)) <- bindExplicitTKBndrs_Skol bndrs $
+ tcRuleTmBndrs xs
+ ; let tys1 = binderVars tybndrs1
; return (tys1 ++ tys2, tms) }
tcRuleBndrs Nothing xs
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 2c716f1826..fb313d9297 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -42,7 +42,7 @@ import GHC.Tc.Types.Evidence( HsWrapper, (<.>) )
import GHC.Core.Type ( mkTyVarBinders )
import GHC.Driver.Session
-import GHC.Types.Var ( TyVar, tyVarKind )
+import GHC.Types.Var ( TyVar, Specificity(..), tyVarKind, binderVars )
import GHC.Types.Id ( Id, idName, idType, idInlinePragma, setInlinePragma, mkLocalId )
import GHC.Builtin.Names( mkUnboundName )
import GHC.Types.Basic
@@ -293,11 +293,11 @@ no_anon_wc lty = go lty
gos = all go
-no_anon_wc_bndrs :: [LHsTyVarBndr GhcRn] -> Bool
+no_anon_wc_bndrs :: [LHsTyVarBndr flag GhcRn] -> Bool
no_anon_wc_bndrs ltvs = all (go . unLoc) ltvs
where
- go (UserTyVar _ _) = True
- go (KindedTyVar _ _ ki) = no_anon_wc ki
+ go (UserTyVar _ _ _) = True
+ go (KindedTyVar _ _ _ ki) = no_anon_wc ki
{- Note [Fail eagerly on bad signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -374,15 +374,15 @@ tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
tcPatSynSig name sig_ty
| HsIB { hsib_ext = implicit_hs_tvs
, hsib_body = hs_ty } <- sig_ty
- , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTyInvis hs_ty
- , (ex_hs_tvs, hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1
+ , (univ_hs_tvbndrs, hs_req, hs_ty1) <- splitLHsSigmaTyInvis hs_ty
+ , (ex_hs_tvbndrs, hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1
= do { traceTc "tcPatSynSig 1" (ppr sig_ty)
- ; (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
+ ; (implicit_tvs, (univ_tvbndrs, (ex_tvbndrs, (req, prov, body_ty))))
<- pushTcLevelM_ $
solveEqualities $ -- See Note [solveEqualities in tcPatSynSig]
bindImplicitTKBndrs_Skol implicit_hs_tvs $
- bindExplicitTKBndrs_Skol univ_hs_tvs $
- bindExplicitTKBndrs_Skol ex_hs_tvs $
+ bindExplicitTKBndrs_Skol univ_hs_tvbndrs $
+ bindExplicitTKBndrs_Skol ex_hs_tvbndrs $
do { req <- tcHsContext hs_req
; prov <- tcHsContext hs_prov
; body_ty <- tcHsOpenType hs_body_ty
@@ -390,8 +390,8 @@ tcPatSynSig name sig_ty
-- e.g. pattern Zero <- 0# (#12094)
; return (req, prov, body_ty) }
- ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvs
- req ex_tvs prov body_ty
+ ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvbndrs
+ req ex_tvbndrs prov body_ty
-- Kind generalisation
; kvs <- kindGeneralizeAll ungen_patsyn_ty
@@ -401,8 +401,8 @@ tcPatSynSig name sig_ty
-- unification variables. Do this after kindGeneralize which may
-- default kind variables to *.
; implicit_tvs <- zonkAndScopedSort implicit_tvs
- ; univ_tvs <- mapM zonkTyCoVarKind univ_tvs
- ; ex_tvs <- mapM zonkTyCoVarKind ex_tvs
+ ; univ_tvbndrs <- mapM zonkTyCoVarKindBinder univ_tvbndrs
+ ; ex_tvbndrs <- mapM zonkTyCoVarKindBinder ex_tvbndrs
; req <- zonkTcTypes req
; prov <- zonkTcTypes prov
; body_ty <- zonkTcType body_ty
@@ -421,15 +421,15 @@ tcPatSynSig name sig_ty
body_ty' = substTy env3 body_ty
-}
; let implicit_tvs' = implicit_tvs
- univ_tvs' = univ_tvs
- ex_tvs' = ex_tvs
+ univ_tvbndrs' = univ_tvbndrs
+ ex_tvbndrs' = ex_tvbndrs
req' = req
prov' = prov
body_ty' = body_ty
-- Now do validity checking
; checkValidType ctxt $
- build_patsyn_type kvs implicit_tvs' univ_tvs' req' ex_tvs' prov' body_ty'
+ build_patsyn_type kvs implicit_tvs' univ_tvbndrs' req' ex_tvbndrs' prov' body_ty'
-- arguments become the types of binders. We thus cannot allow
-- levity polymorphism here
@@ -439,27 +439,28 @@ tcPatSynSig name sig_ty
; traceTc "tcTySig }" $
vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs'
, text "kvs" <+> ppr_tvs kvs
- , text "univ_tvs" <+> ppr_tvs univ_tvs'
+ , text "univ_tvs" <+> ppr_tvs (binderVars univ_tvbndrs')
, text "req" <+> ppr req'
- , text "ex_tvs" <+> ppr_tvs ex_tvs'
+ , text "ex_tvs" <+> ppr_tvs (binderVars ex_tvbndrs')
, text "prov" <+> ppr prov'
, text "body_ty" <+> ppr body_ty' ]
; return (TPSI { patsig_name = name
- , patsig_implicit_bndrs = mkTyVarBinders Inferred kvs ++
- mkTyVarBinders Specified implicit_tvs'
- , patsig_univ_bndrs = univ_tvs'
+ , patsig_implicit_bndrs = mkTyVarBinders InferredSpec kvs ++
+ mkTyVarBinders SpecifiedSpec implicit_tvs'
+ , patsig_univ_bndrs = univ_tvbndrs'
, patsig_req = req'
- , patsig_ex_bndrs = ex_tvs'
+ , patsig_ex_bndrs = ex_tvbndrs'
, patsig_prov = prov'
, patsig_body_ty = body_ty' }) }
where
ctxt = PatSynCtxt name
- build_patsyn_type kvs imp univ req ex prov body
- = mkInvForAllTys kvs $
- mkSpecForAllTys (imp ++ univ) $
+ build_patsyn_type kvs imp univ_bndrs req ex_bndrs prov body
+ = mkInfForAllTys kvs $
+ mkSpecForAllTys imp $
+ mkInvisForAllTys univ_bndrs $
mkPhiTy req $
- mkSpecForAllTys ex $
+ mkInvisForAllTys ex_bndrs $
mkPhiTy prov $
body
@@ -479,7 +480,7 @@ tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
-- Instantiate a type signature; only used with plan InferGen
tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
= setSrcSpan loc $ -- Set the binding site of the tyvars
- do { (tv_prs, theta, tau) <- tcInstType newMetaTyVarTyVars poly_id
+ do { (tv_prs, theta, tau) <- tcInstTypeBndrs newMetaTyVarTyVars poly_id
-- See Note [Pattern bindings and complete signatures]
; return (TISI { sig_inst_sig = sig
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index 99806ff820..aa792ee6b7 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -15,6 +15,8 @@
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
@@ -1618,7 +1620,7 @@ reifyThing (AGlobal (AConLike (RealDataCon dc)))
reifyThing (AGlobal (AConLike (PatSynCon ps)))
= do { let name = reifyName ps
- ; ty <- reifyPatSynType (patSynSig ps)
+ ; ty <- reifyPatSynType (patSynSigBndr ps)
; return (TH.PatSynI name ty) }
reifyThing (ATcId {tct_id = id})
@@ -1673,7 +1675,7 @@ reifyTyCon tc
Just name ->
let thName = reifyName name
injAnnot = tyConInjectivityInfo tc
- sig = TH.TyVarSig (TH.KindedTV thName kind')
+ sig = TH.TyVarSig (TH.KindedTV thName () kind')
inj = case injAnnot of
NotInjective -> Nothing
Injective ms ->
@@ -1737,7 +1739,7 @@ reifyDataCon isGadtDataCon tys dc
(ex_tvs, theta, arg_tys)
= dataConInstSig dc tys
-- used for GADTs data constructors
- g_user_tvs' = dataConUserTyVars dc
+ g_user_tvs' = dataConUserTyVarBinders dc
(g_univ_tvs, _, g_eq_spec, g_theta', g_arg_tys', g_res_ty')
= dataConFullSig dc
(srcUnpks, srcStricts)
@@ -1753,7 +1755,7 @@ reifyDataCon isGadtDataCon tys dc
-- See Note [Freshen reified GADT constructors' universal tyvars]
<- freshenTyVarBndrs $
filterOut (`elemVarSet` eq_spec_tvs) g_univ_tvs
- ; let (tvb_subst, g_user_tvs) = substTyVarBndrs univ_subst g_user_tvs'
+ ; let (tvb_subst, g_user_tvs) = subst_tv_binders univ_subst g_user_tvs'
g_theta = substTys tvb_subst g_theta'
g_arg_tys = substTys tvb_subst g_arg_tys'
g_res_ty = substTy tvb_subst g_res_ty'
@@ -1786,14 +1788,23 @@ reifyDataCon isGadtDataCon tys dc
; let (ex_tvs', theta') | isGadtDataCon = (g_user_tvs, g_theta)
| otherwise = ASSERT( all isTyVar ex_tvs )
-- no covars for haskell syntax
- (ex_tvs, theta)
+ (map mk_specified ex_tvs, theta)
ret_con | null ex_tvs' && null theta' = return main_con
| otherwise = do
{ cxt <- reifyCxt theta'
- ; ex_tvs'' <- reifyTyVars ex_tvs'
+ ; ex_tvs'' <- reifyTyVarBndrs ex_tvs'
; return (TH.ForallC ex_tvs'' cxt main_con) }
; ASSERT( r_arg_tys `equalLength` dcdBangs )
ret_con }
+ where
+ mk_specified tv = Bndr tv SpecifiedSpec
+
+ subst_tv_binders subst tv_bndrs =
+ let tvs = binderVars tv_bndrs
+ flags = map binderArgFlag tv_bndrs
+ (subst', tvs') = substTyVarBndrs subst tvs
+ tv_bndrs' = map (\(tv,fl) -> Bndr tv fl) (zip tvs' flags)
+ in (subst', tv_bndrs')
{-
Note [Freshen reified GADT constructors' universal tyvars]
@@ -1868,9 +1879,9 @@ reifyClass cls
= (n, map bndrName args)
tfNames d = pprPanic "tfNames" (text (show d))
- bndrName :: TH.TyVarBndr -> TH.Name
- bndrName (TH.PlainTV n) = n
- bndrName (TH.KindedTV n _) = n
+ bndrName :: TH.TyVarBndr flag -> TH.Name
+ bndrName (TH.PlainTV n _) = n
+ bndrName (TH.KindedTV n _ _) = n
------------------------------
-- | Annotate (with TH.SigT) a type if the first parameter is True
@@ -2113,16 +2124,18 @@ reifyType ty@(CoercionTy {})= noTH (sLit "coercions in types") (ppr ty)
reify_for_all :: TyCoRep.ArgFlag -> TyCoRep.Type -> TcM TH.Type
-- Arg of reify_for_all is always ForAllTy or a predicate FunTy
reify_for_all argf ty = do
- tvs' <- reifyTyVars tvs
+ tvbndrs' <- reifyTyVarBndrs tvbndrs
case argToForallVisFlag argf of
ForallVis -> do phi' <- reifyType phi
- pure $ TH.ForallVisT tvs' phi'
+ let tvs = map (() <$) tvbndrs'
+ -- see Note [Specificity in HsForAllTy] in GHC.Hs.Types
+ pure $ TH.ForallVisT tvs phi'
ForallInvis -> do let (cxt, tau) = tcSplitPhiTy phi
cxt' <- reifyCxt cxt
tau' <- reifyType tau
- pure $ TH.ForallT tvs' cxt' tau'
+ pure $ TH.ForallT tvbndrs' cxt' tau'
where
- (tvs, phi) = tcSplitForAllTysSameVis argf ty
+ (tvbndrs, phi) = tcSplitForAllTysSameVis argf ty
reifyTyLit :: TyCoRep.TyLit -> TcM TH.TyLit
reifyTyLit (NumTyLit n) = return (TH.NumTyLit n)
@@ -2132,14 +2145,14 @@ reifyTypes :: [Type] -> TcM [TH.Type]
reifyTypes = mapM reifyType
reifyPatSynType
- :: ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type) -> TcM TH.Type
+ :: ([InvisTVBinder], ThetaType, [InvisTVBinder], ThetaType, [Type], Type) -> TcM TH.Type
-- reifies a pattern synonym's type and returns its *complete* type
-- signature; see NOTE [Pattern synonym signatures and Template
-- Haskell]
reifyPatSynType (univTyVars, req, exTyVars, prov, argTys, resTy)
- = do { univTyVars' <- reifyTyVars univTyVars
+ = do { univTyVars' <- reifyTyVarBndrs univTyVars
; req' <- reifyCxt req
- ; exTyVars' <- reifyTyVars exTyVars
+ ; exTyVars' <- reifyTyVarBndrs exTyVars
; prov' <- reifyCxt prov
; tau' <- reifyType (mkVisFunTys argTys resTy)
; return $ TH.ForallT univTyVars' req'
@@ -2154,18 +2167,37 @@ reifyCxt = mapM reifyType
reifyFunDep :: ([TyVar], [TyVar]) -> TH.FunDep
reifyFunDep (xs, ys) = TH.FunDep (map reifyName xs) (map reifyName ys)
-reifyTyVars :: [TyVar] -> TcM [TH.TyVarBndr]
-reifyTyVars tvs = mapM reify_tv tvs
+class ReifyFlag flag flag' | flag -> flag' where
+ reifyFlag :: flag -> flag'
+
+instance ReifyFlag () () where
+ reifyFlag () = ()
+
+instance ReifyFlag Specificity TH.Specificity where
+ reifyFlag SpecifiedSpec = TH.SpecifiedSpec
+ reifyFlag InferredSpec = TH.InferredSpec
+
+instance ReifyFlag ArgFlag TH.Specificity where
+ reifyFlag Required = TH.SpecifiedSpec
+ reifyFlag (Invisible s) = reifyFlag s
+
+reifyTyVars :: [TyVar] -> TcM [TH.TyVarBndr ()]
+reifyTyVars = reifyTyVarBndrs . map mk_bndr
+ where
+ mk_bndr tv = Bndr tv ()
+
+reifyTyVarBndrs :: ReifyFlag flag flag'
+ => [VarBndr TyVar flag] -> TcM [TH.TyVarBndr flag']
+reifyTyVarBndrs = mapM reify_tvbndr
where
-- even if the kind is *, we need to include a kind annotation,
-- in case a poly-kind would be inferred without the annotation.
-- See #8953 or test th/T8953
- reify_tv tv = TH.KindedTV name <$> reifyKind kind
- where
- kind = tyVarKind tv
- name = reifyName tv
+ reify_tvbndr (Bndr tv fl) = TH.KindedTV (reifyName tv)
+ (reifyFlag fl)
+ <$> reifyKind (tyVarKind tv)
-reifyTyVarsToMaybe :: [TyVar] -> TcM (Maybe [TH.TyVarBndr])
+reifyTyVarsToMaybe :: [TyVar] -> TcM (Maybe [TH.TyVarBndr ()])
reifyTyVarsToMaybe [] = pure Nothing
reifyTyVarsToMaybe tys = Just <$> reifyTyVars tys
@@ -2289,7 +2321,7 @@ reifyTypeOfThing th_name = do
AGlobal (AConLike (RealDataCon dc)) ->
reifyType (idType (dataConWrapId dc))
AGlobal (AConLike (PatSynCon ps)) ->
- reifyPatSynType (patSynSig ps)
+ reifyPatSynType (patSynSigBndr ps)
ATcId{tct_id = id} -> zonkTcType (idType id) >>= reifyType
ATyVar _ tctv -> zonkTcTyVar tctv >>= reifyType
-- Impossible cases, supposedly:
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 095fd1c7cc..94402c0989 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -2444,7 +2444,7 @@ getGhciStepIO = do
step_ty = noLoc $ HsForAllTy
{ hst_fvf = ForallInvis
- , hst_bndrs = [noLoc $ UserTyVar noExtField (noLoc a_tv)]
+ , hst_bndrs = [noLoc $ UserTyVar noExtField SpecifiedSpec (noLoc a_tv)]
, hst_xforall = noExtField
, hst_body = nlHsFunTy ghciM ioM }
@@ -2507,7 +2507,7 @@ tcRnExpr hsc_env mode rdr_expr
_ <- perhaps_disable_default_warnings $
simplifyInteractive residual ;
- let { all_expr_ty = mkInvForAllTys qtvs $
+ let { all_expr_ty = mkInfForAllTys qtvs $
mkPhiTy (map idType dicts) res_ty } ;
ty <- zonkTcType all_expr_ty ;
@@ -2608,7 +2608,7 @@ tcRnType hsc_env flexi normalise rdr_type
; return ty' }
else return ty ;
- ; return (ty', mkInvForAllTys kvs (tcTypeKind ty')) }
+ ; return (ty', mkInfForAllTys kvs (tcTypeKind ty')) }
{- Note [TcRnExprMode]
~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 134b230c06..b1017de024 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -745,7 +745,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
= do { -- When quantifying, we want to preserve any order of variables as they
-- appear in partial signatures. cf. decideQuantifiedTyVars
let psig_tv_tys = [ mkTyVarTy tv | sig <- partial_sigs
- , (_,tv) <- sig_inst_skols sig ]
+ , (_,Bndr tv _) <- sig_inst_skols sig ]
psig_theta = [ pred | sig <- partial_sigs
, pred <- sig_inst_theta sig ]
@@ -1056,7 +1056,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
-- If possible, we quantify over partial-sig qtvs, so they are
-- not mono. Need to zonk them because they are meta-tyvar TyVarTvs
- ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
+ ; psig_qtvs <- mapM zonkTcTyVarToTyVar $ binderVars $
concatMap (map snd . sig_inst_skols) psigs
; psig_theta <- mapM TcM.zonkTcType $
@@ -1222,7 +1222,7 @@ decideQuantifiedTyVars name_taus psigs candidates
-- See Note [Quantification and partial signatures]
-- Wrinkles 2 and 3
; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
- , (_,tv) <- sig_inst_skols sig ]
+ , (_,Bndr tv _) <- sig_inst_skols sig ]
; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
, pred <- sig_inst_theta sig ]
; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 5da467d770..144021caea 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -1365,8 +1365,8 @@ get_fam_decl_initial_kind mb_parent_tycon
, fdInfo = info }
= kcDeclHeader InitialKindInfer name flav ktvs $
case resultSig of
- KindSig _ ki -> TheKind <$> tcLHsKindSig ctxt ki
- TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> TheKind <$> tcLHsKindSig ctxt ki
+ KindSig _ ki -> TheKind <$> tcLHsKindSig ctxt ki
+ TyVarSig _ (L _ (KindedTyVar _ _ _ ki)) -> TheKind <$> tcLHsKindSig ctxt ki
_ -- open type families have * return kind by default
| tcFlavourIsOpen flav -> return (TheKind liftedTypeKind)
-- closed type families have their return kind inferred
@@ -1601,10 +1601,8 @@ kcConDecl new_or_data res_kind (ConDeclH98
}
kcConDecl new_or_data res_kind (ConDeclGADT
- { con_names = names, con_qvars = qtvs, con_mb_cxt = cxt
- , con_args = args, con_res_ty = res_ty })
- | HsQTvs { hsq_ext = implicit_tkv_nms
- , hsq_explicit = explicit_tkv_nms } <- qtvs
+ { con_names = names, con_qvars = explicit_tkv_nms, con_mb_cxt = cxt
+ , con_args = args, con_res_ty = res_ty, con_g_ext = implicit_tkv_nms })
= -- Even though the GADT-style data constructor's type is closed,
-- we must still kind-check the type, because that may influence
-- the inferred kind of the /type/ constructor. Example:
@@ -2854,10 +2852,10 @@ a very similar design when generalising over the type of a rewrite rule.
--------------------------
tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo
- -> [Name] -> [LHsTyVarBndr GhcRn] -- Implicit and explicicit binder
- -> HsTyPats GhcRn -- Patterns
- -> LHsType GhcRn -- RHS
- -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs)
+ -> [Name] -> [LHsTyVarBndr () GhcRn] -- Implicit and explicicit binder
+ -> HsTyPats GhcRn -- Patterns
+ -> LHsType GhcRn -- RHS
+ -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs)
-- Used only for type families, not data families
tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
= do { traceTc "tcTyFamInstEqnGuts {" (ppr fam_tc)
@@ -3116,7 +3114,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
- ; (exp_tvs, (ctxt, arg_tys, field_lbls, stricts))
+ ; (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts))
<- pushTcLevelM_ $
solveEqualities $
bindExplicitTKBndrs_Skol explicit_tkv_nms $
@@ -3128,12 +3126,14 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
; return (ctxt, arg_tys, field_lbls, stricts)
}
+ ; let tmpl_tvs = binderVars tmpl_bndrs
+
-- exp_tvs have explicit, user-written binding sites
-- the kvs below are those kind variables entirely unmentioned by the user
-- and discovered only by generalization
- ; kvs <- kindGeneralizeAll (mkSpecForAllTys (binderVars tmpl_bndrs) $
- mkSpecForAllTys exp_tvs $
+ ; kvs <- kindGeneralizeAll (mkSpecForAllTys tmpl_tvs $
+ mkInvisForAllTys exp_tvbndrs $
mkPhiTy ctxt $
mkVisFunTys arg_tys $
unitTy)
@@ -3145,20 +3145,21 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
-- quantify over, and this type is fine for that purpose.
-- Zonk to Types
- ; (ze, qkvs) <- zonkTyBndrs kvs
- ; (ze, user_qtvs) <- zonkTyBndrsX ze exp_tvs
- ; arg_tys <- zonkTcTypesToTypesX ze arg_tys
- ; ctxt <- zonkTcTypesToTypesX ze ctxt
+ ; (ze, qkvs) <- zonkTyBndrs kvs
+ ; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs
+ ; let user_qtvs = binderVars user_qtvbndrs
+ ; arg_tys <- zonkTcTypesToTypesX ze arg_tys
+ ; ctxt <- zonkTcTypesToTypesX ze ctxt
; fam_envs <- tcGetFamInstEnvs
-- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
; let
- univ_tvbs = tyConTyVarBinders tmpl_bndrs
+ univ_tvbs = tyConInvisTVBinders tmpl_bndrs
univ_tvs = binderVars univ_tvbs
- ex_tvbs = mkTyVarBinders Inferred qkvs ++
- mkTyVarBinders Specified user_qtvs
+ ex_tvbs = mkTyVarBinders InferredSpec qkvs ++
+ user_qtvbndrs
ex_tvs = qkvs ++ user_qtvs
-- For H98 datatypes, the user-written tyvar binders are precisely
-- the universals followed by the existentials.
@@ -3184,17 +3185,16 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
-- NB: don't use res_kind here, as it's ill-scoped. Instead, we get
-- the res_kind by typechecking the result type.
- (ConDeclGADT { con_names = names
- , con_qvars = qtvs
+ (ConDeclGADT { con_g_ext = implicit_tkv_nms
+ , con_names = names
+ , con_qvars = explicit_tkv_nms
, con_mb_cxt = cxt, con_args = hs_args
, con_res_ty = hs_res_ty })
- | HsQTvs { hsq_ext = implicit_tkv_nms
- , hsq_explicit = explicit_tkv_nms } <- qtvs
= addErrCtxt (dataConCtxtName names) $
do { traceTc "tcConDecl 1 gadt" (ppr names)
; let (L _ name : _) = names
- ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
+ ; (imp_tvs, (exp_tvbndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
<- pushTcLevelM_ $ -- We are going to generalise
solveEqualities $ -- We won't get another crack, and we don't
-- want an error cascade
@@ -3217,32 +3217,26 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
}
; imp_tvs <- zonkAndScopedSort imp_tvs
- ; let user_tvs = imp_tvs ++ exp_tvs
- ; tkvs <- kindGeneralizeAll (mkSpecForAllTys user_tvs $
+ ; tkvs <- kindGeneralizeAll (mkSpecForAllTys imp_tvs $
+ mkInvisForAllTys exp_tvbndrs $
mkPhiTy ctxt $
mkVisFunTys arg_tys $
res_ty)
+ ; let tvbndrs = (mkTyVarBinders InferredSpec tkvs)
+ ++ (mkTyVarBinders SpecifiedSpec imp_tvs)
+ ++ exp_tvbndrs
+
-- Zonk to Types
- ; (ze, tkvs) <- zonkTyBndrs tkvs
- ; (ze, user_tvs) <- zonkTyBndrsX ze user_tvs
- ; arg_tys <- zonkTcTypesToTypesX ze arg_tys
- ; ctxt <- zonkTcTypesToTypesX ze ctxt
- ; res_ty <- zonkTcTypeToTypeX ze res_ty
-
- ; let (univ_tvs, ex_tvs, tkvs', user_tvs', eq_preds, arg_subst)
- = rejigConRes tmpl_bndrs res_tmpl tkvs user_tvs res_ty
- -- NB: this is a /lazy/ binding, so we pass six thunks to
- -- buildDataCon without yet forcing the guards in rejigConRes
- -- See Note [Checking GADT return types]
+ ; (ze, tvbndrs) <- zonkTyVarBinders tvbndrs
+ ; arg_tys <- zonkTcTypesToTypesX ze arg_tys
+ ; ctxt <- zonkTcTypesToTypesX ze ctxt
+ ; res_ty <- zonkTcTypeToTypeX ze res_ty
- -- Compute the user-written tyvar binders. These have the same
- -- tyvars as univ_tvs/ex_tvs, but perhaps in a different order.
- -- See Note [DataCon user type variable binders] in GHC.Core.DataCon.
- tkv_bndrs = mkTyVarBinders Inferred tkvs'
- user_tv_bndrs = mkTyVarBinders Specified user_tvs'
- all_user_bndrs = tkv_bndrs ++ user_tv_bndrs
+ ; let (univ_tvs, ex_tvs, tvbndrs', eq_preds, arg_subst)
+ = rejigConRes tmpl_bndrs res_tmpl tvbndrs res_ty
+ -- See Note [Checking GADT return types]
ctxt' = substTys arg_subst ctxt
arg_tys' = substTys arg_subst arg_tys
@@ -3261,7 +3255,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
; buildDataCon fam_envs name is_infix
rep_nm
stricts Nothing field_lbls
- univ_tvs ex_tvs all_user_bndrs eq_preds
+ univ_tvs ex_tvs tvbndrs' eq_preds
ctxt' arg_tys' res_ty' rep_tycon tag_map
-- NB: we put data_tc, the type constructor gotten from the
-- constructor type signature into the data constructor;
@@ -3388,22 +3382,18 @@ errors reported in one pass. See #7175, and #10836.
rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type -- Template for result type; e.g.
-- data instance T [a] b c ...
-- gives template ([a,b,c], T [a] b c)
- -> [TyVar] -- The constructor's inferred type variables
- -> [TyVar] -- The constructor's user-written, specified
- -- type variables
+ -> [InvisTVBinder] -- The constructor's type variables (both inferred and user-written)
-> KnotTied Type -- res_ty
-> ([TyVar], -- Universal
[TyVar], -- Existential (distinct OccNames from univs)
- [TyVar], -- The constructor's rejigged, user-written,
- -- inferred type variables
- [TyVar], -- The constructor's rejigged, user-written,
- -- specified type variables
- [EqSpec], -- Equality predicates
- TCvSubst) -- Substitution to apply to argument types
+ [InvisTVBinder], -- The constructor's rejigged, user-written
+ -- type variables
+ [EqSpec], -- Equality predicates
+ TCvSubst) -- Substitution to apply to argument types
-- We don't check that the TyCon given in the ResTy is
-- the same as the parent tycon, because checkValidDataCon will do it
-- NB: All arguments may potentially be knot-tied
-rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
+rejigConRes tmpl_bndrs res_tmpl dc_tvbndrs res_ty
-- E.g. data T [a] b c where
-- MkT :: forall x y z. T [(x,y)] z z
-- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs
@@ -3430,14 +3420,12 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
-- since the dcUserTyVarBinders invariant guarantees that the
-- substitution has *all* the tyvars in its domain.
-- See Note [DataCon user type variable binders] in GHC.Core.DataCon.
- subst_user_tvs = map (getTyVar "rejigConRes" . substTyVar arg_subst)
- substed_inferred_tvs = subst_user_tvs dc_inferred_tvs
- substed_specified_tvs = subst_user_tvs dc_specified_tvs
+ subst_user_tvs = mapVarBndrs (getTyVar "rejigConRes" . substTyVar arg_subst)
+ substed_tvbndrs = subst_user_tvs dc_tvbndrs
substed_eqs = map (substEqSpec arg_subst) raw_eqs
in
- (univ_tvs, substed_ex_tvs, substed_inferred_tvs, substed_specified_tvs,
- substed_eqs, arg_subst)
+ (univ_tvs, substed_ex_tvs, substed_tvbndrs, substed_eqs, arg_subst)
| otherwise
-- If the return type of the data constructor doesn't match the parent
@@ -3450,10 +3438,9 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
-- albeit bogus, relying on checkValidDataCon to check the
-- bad-result-type error before seeing that the other fields look odd
-- See Note [Checking GADT return types]
- = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, dc_inferred_tvs, dc_specified_tvs,
- [], emptyTCvSubst)
+ = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, dc_tvbndrs, [], emptyTCvSubst)
where
- dc_tvs = dc_inferred_tvs ++ dc_specified_tvs
+ dc_tvs = binderVars dc_tvbndrs
tmpl_tvs = binderVars tmpl_bndrs
{- Note [mkGADTVars]
diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs
index cf490075af..af49e9e28c 100644
--- a/compiler/GHC/Tc/TyCl/Build.hs
+++ b/compiler/GHC/Tc/TyCl/Build.hs
@@ -106,7 +106,7 @@ buildDataCon :: FamInstEnvs
-> [FieldLabel] -- Field labels
-> [TyVar] -- Universals
-> [TyCoVar] -- Existentials
- -> [TyVarBinder] -- User-written 'TyVarBinder's
+ -> [InvisTVBinder] -- User-written 'TyVarBinder's
-> [EqSpec] -- Equality spec
-> KnotTied ThetaType -- Does not include the "stupid theta"
-- or the GADT equalities
@@ -170,12 +170,12 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
------------------------------------------------------
buildPatSyn :: Name -> Bool
-> (Id,Bool) -> Maybe (Id, Bool)
- -> ([TyVarBinder], ThetaType) -- ^ Univ and req
- -> ([TyVarBinder], ThetaType) -- ^ Ex and prov
- -> [Type] -- ^ Argument types
- -> Type -- ^ Result type
- -> [FieldLabel] -- ^ Field labels for
- -- a record pattern synonym
+ -> ([InvisTVBinder], ThetaType) -- ^ Univ and req
+ -> ([InvisTVBinder], ThetaType) -- ^ Ex and prov
+ -> [Type] -- ^ Argument types
+ -> Type -- ^ Result type
+ -> [FieldLabel] -- ^ Field labels for
+ -- a record pattern synonym
-> PatSyn
buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
(univ_tvs, req_theta) (ex_tvs, prov_theta) arg_tys
@@ -298,7 +298,7 @@ buildClass tycon_name binders roles fds
op_names = [op | (op,_,_) <- sig_stuff]
arg_tys = sc_theta ++ op_tys
rec_tycon = classTyCon rec_clas
- univ_bndrs = tyConTyVarBinders binders
+ univ_bndrs = tyConInvisTVBinders binders
univ_tvs = binderVars univ_bndrs
; rep_nm <- newTyConRepName datacon_name
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 22849451bf..734ec05512 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -836,7 +836,7 @@ TyVarEnv will simply be empty, and there is nothing to worry about.
-----------------------
tcDataFamInstHeader
- :: AssocInstInfo -> TyCon -> [Name] -> Maybe [LHsTyVarBndr GhcRn]
+ :: AssocInstInfo -> TyCon -> [Name] -> Maybe [LHsTyVarBndr () GhcRn]
-> LexicalFixity -> LHsContext GhcRn
-> HsTyPats GhcRn -> Maybe (LHsKind GhcRn) -> [LConDecl GhcRn]
-> NewOrData
@@ -1306,7 +1306,7 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls))
; sc_ev_id <- newEvVar sc_pred
; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
- ; let sc_top_ty = mkInvForAllTys tyvars $
+ ; let sc_top_ty = mkInfForAllTys tyvars $
mkPhiTy (map idType dfun_evs) sc_pred
sc_top_id = mkLocalId sc_top_name sc_top_ty
export = ABE { abe_ext = noExtField
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 00e0beb5e1..957506c7c5 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -98,7 +98,7 @@ recoverPSB (PSB { psb_id = L _ name
(_arg_names, _rec_fields, is_infix) = collectPatSynArgInfo details
mk_placeholder matcher_name
= mkPatSyn name is_infix
- ([mkTyVarBinder Specified alphaTyVar], []) ([], [])
+ ([mkTyVarBinder SpecifiedSpec alphaTyVar], []) ([], [])
[] -- Arg tys
alphaTy
(matcher_id, True) Nothing
@@ -185,9 +185,9 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
; tc_patsyn_finish lname dir is_infix lpat'
- (mkTyVarBinders Inferred univ_tvs
+ (mkTyVarBinders InferredSpec univ_tvs
, req_theta, ev_binds, req_dicts)
- (mkTyVarBinders Inferred ex_tvs
+ (mkTyVarBinders InferredSpec ex_tvs
, mkTyVarTys ex_tvs, prov_theta, prov_evs)
(map nlHsVar args, map idType args)
pat_ty rec_fields } }
@@ -345,17 +345,17 @@ tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
-> TcM (LHsBinds GhcTc, TcGblEnv)
tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
, psb_def = lpat, psb_dir = dir }
- TPSI{ patsig_implicit_bndrs = implicit_tvs
- , patsig_univ_bndrs = explicit_univ_tvs, patsig_prov = prov_theta
- , patsig_ex_bndrs = explicit_ex_tvs, patsig_req = req_theta
+ TPSI{ patsig_implicit_bndrs = implicit_bndrs
+ , patsig_univ_bndrs = explicit_univ_bndrs, patsig_prov = prov_theta
+ , patsig_ex_bndrs = explicit_ex_bndrs, patsig_req = req_theta
, patsig_body_ty = sig_body_ty }
= addPatSynCtxt lname $
do { let decl_arity = length arg_names
(arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
; traceTc "tcCheckPatSynDecl" $
- vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta
- , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ]
+ vcat [ ppr implicit_bndrs, ppr explicit_univ_bndrs, ppr req_theta
+ , ppr explicit_ex_bndrs, ppr prov_theta, ppr sig_body_ty ]
; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
Right stuff -> return stuff
@@ -364,7 +364,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
-- Complain about: pattern P :: () => forall x. x -> P x
-- The existential 'x' should not appear in the result type
-- Can't check this until we know P's arity
- ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) explicit_ex_tvs
+ ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) $ binderVars explicit_ex_bndrs
; checkTc (null bad_tvs) $
hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
, text "namely" <+> quotes (ppr pat_ty) ])
@@ -373,10 +373,10 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
-- See Note [The pattern-synonym signature splitting rule] in GHC.Tc.Gen.Sig
; let univ_fvs = closeOverKinds $
- (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs)
- (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_tvs
- univ_bndrs = extra_univ ++ mkTyVarBinders Specified explicit_univ_tvs
- ex_bndrs = extra_ex ++ mkTyVarBinders Specified explicit_ex_tvs
+ (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` (binderVars explicit_univ_bndrs))
+ (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_bndrs
+ univ_bndrs = extra_univ ++ explicit_univ_bndrs
+ ex_bndrs = extra_ex ++ explicit_ex_bndrs
univ_tvs = binderVars univ_bndrs
ex_tvs = binderVars ex_bndrs
@@ -594,8 +594,8 @@ tc_patsyn_finish :: Located Name -- ^ PatSyn Name
-> HsPatSynDir GhcRn -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
-> Bool -- ^ Whether infix
-> LPat GhcTc -- ^ Pattern of the PatSyn
- -> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
- -> ([TcTyVarBinder], [TcType], [PredType], [EvTerm])
+ -> ([TcInvisTVBinder], [PredType], TcEvBinds, [EvVar])
+ -> ([TcInvisTVBinder], [TcType], [PredType], [EvTerm])
-> ([LHsExpr GhcTcId], [TcType]) -- ^ Pattern arguments and
-- types
-> TcType -- ^ Pattern type
@@ -782,8 +782,8 @@ isUnidirectional ExplicitBidirectional{} = False
-}
mkPatSynBuilderId :: HsPatSynDir a -> Located Name
- -> [TyVarBinder] -> ThetaType
- -> [TyVarBinder] -> ThetaType
+ -> [InvisTVBinder] -> ThetaType
+ -> [InvisTVBinder] -> ThetaType
-> [Type] -> Type
-> TcM (Maybe (Id, Bool))
mkPatSynBuilderId dir (L _ name)
@@ -796,8 +796,8 @@ mkPatSynBuilderId dir (L _ name)
; let theta = req_theta ++ prov_theta
need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
builder_sigma = add_void need_dummy_arg $
- mkForAllTys univ_bndrs $
- mkForAllTys ex_bndrs $
+ mkInvisForAllTys univ_bndrs $
+ mkInvisForAllTys ex_bndrs $
mkPhiTy theta $
mkVisFunTys arg_tys $
pat_ty
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 249f08beea..00a4c01493 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -784,7 +784,7 @@ mkDefaultMethodType cls _ (GenericDM dm_ty) = mkSigmaTy tv_bndrs [pred] dm_ty
where
pred = mkClassPred cls (mkTyVarTys (binderVars cls_bndrs))
cls_bndrs = tyConBinders (classTyCon cls)
- tv_bndrs = tyConTyVarBinders cls_bndrs
+ tv_bndrs = tyVarSpecToBinders $ tyConInvisTVBinders cls_bndrs
-- NB: the Class doesn't have TyConBinders; we reach into its
-- TyCon to get those. We /do/ need the TyConBinders because
-- we need the correct visibility: these default methods are
@@ -877,7 +877,7 @@ mkOneRecordSelector all_cons idDetails fl
data_tv_set= tyCoVarsOfTypes inst_tys
is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set)
sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors]
- | otherwise = mkForAllTys data_tvbs $
+ | otherwise = mkForAllTys (tyVarSpecToBinders data_tvbs) $
mkPhiTy (conLikeStupidTheta con1) $ -- Urgh!
-- req_theta is empty for normal DataCon
mkPhiTy req_theta $
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index deafb5539d..6e60efd4d5 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -1516,7 +1516,7 @@ sig_extra_cts is Nothing.
data TcIdSigInst
= TISI { sig_inst_sig :: TcIdSigInfo
- , sig_inst_skols :: [(Name, TcTyVar)]
+ , sig_inst_skols :: [(Name, InvisTVBinder)]
-- Instantiated type and kind variables, TyVarTvs
-- The Name is the Name that the renamer chose;
-- but the TcTyVar may come from instantiating
@@ -1602,12 +1602,12 @@ Here we get
data TcPatSynInfo
= TPSI {
patsig_name :: Name,
- patsig_implicit_bndrs :: [TyVarBinder], -- Implicitly-bound kind vars (Inferred) and
- -- implicitly-bound type vars (Specified)
+ patsig_implicit_bndrs :: [InvisTVBinder], -- Implicitly-bound kind vars (Inferred) and
+ -- implicitly-bound type vars (Specified)
-- See Note [The pattern-synonym signature splitting rule] in GHC.Tc.TyCl.PatSyn
- patsig_univ_bndrs :: [TyVar], -- Bound by explicit user forall
+ patsig_univ_bndrs :: [InvisTVBinder], -- Bound by explicit user forall
patsig_req :: TcThetaType,
- patsig_ex_bndrs :: [TyVar], -- Bound by explicit user forall
+ patsig_ex_bndrs :: [InvisTVBinder], -- Bound by explicit user forall
patsig_prov :: TcThetaType,
patsig_body_ty :: TcSigmaType
}
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index bbd52bd059..90598e42c4 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -59,7 +59,7 @@ module GHC.Tc.Utils.TcMType (
newMetaTyVarTyVars, newMetaTyVarTyVarX,
newTyVarTyVar, cloneTyVarTyVar,
newPatSigTyVar, newSkolemTyVar, newWildCardX,
- tcInstType,
+ tcInstType, tcInstTypeBndrs,
tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
@@ -79,7 +79,7 @@ module GHC.Tc.Utils.TcMType (
zonkAndSkolemise, skolemiseQuantifiedTyVar,
defaultTyVar, quantifyTyVars, isQuantifiableTv,
zonkTcType, zonkTcTypes, zonkCo,
- zonkTyCoVarKind,
+ zonkTyCoVarKind, zonkTyCoVarKindBinder,
zonkEvVar, zonkWC, zonkSimples,
zonkId, zonkCoVar,
@@ -507,23 +507,55 @@ inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
* *
********************************************************************* -}
+tc_inst_internal :: ([VarBndr TyVar flag] -> TcM (TCvSubst, [VarBndr TcTyVar flag]))
+ -- ^ How to instantiate the type variables
+ -> [VarBndr TyVar flag] -- ^ Type variable to instantiate
+ -> Type -- ^ rho
+ -> TcM ([(Name, VarBndr TcTyVar flag)], TcThetaType, TcType) -- ^ Result
+ -- (type vars, preds (incl equalities), rho)
+tc_inst_internal _inst_tyvars [] rho =
+ let -- There may be overloading despite no type variables;
+ -- (?x :: Int) => Int -> Int
+ (theta, tau) = tcSplitPhiTy rho
+ in
+ return ([], theta, tau)
+tc_inst_internal inst_tyvars tyvars rho =
+ do { (subst, tyvars') <- inst_tyvars tyvars
+ ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
+ tv_prs = map (tyVarName . binderVar) tyvars `zip` tyvars'
+ ; return (tv_prs, theta, tau) }
+
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
-- ^ How to instantiate the type variables
- -> Id -- ^ Type to instantiate
- -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
+ -> Id -- ^ Type to instantiate
+ -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
-- (type vars, preds (incl equalities), rho)
-tcInstType inst_tyvars id
- = case tcSplitForAllTys (idType id) of
- ([], rho) -> let -- There may be overloading despite no type variables;
- -- (?x :: Int) => Int -> Int
- (theta, tau) = tcSplitPhiTy rho
- in
- return ([], theta, tau)
-
- (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
- ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
- tv_prs = map tyVarName tyvars `zip` tyvars'
- ; return (tv_prs, theta, tau) }
+tcInstType inst_tyvars id =
+ do { let (tyvars, rho) = splitForAllTys (idType id)
+ tyvars' = mkTyVarBinders () tyvars
+ ; (tv_prs, preds, rho) <- tc_inst_internal inst_tyvar_bndrs tyvars' rho
+ ; let tv_prs' = map (\(name, bndr) -> (name, binderVar bndr)) tv_prs
+ ; return (tv_prs', preds, rho) }
+ where
+ inst_tyvar_bndrs :: [VarBndr TyVar ()] -> TcM (TCvSubst, [VarBndr TcTyVar ()])
+ inst_tyvar_bndrs bndrs = do { (subst, tvs) <- inst_tyvars $ binderVars bndrs
+ ; let tvbnds = map (\tv -> Bndr tv ()) tvs
+ ; return (subst, tvbnds) }
+
+tcInstTypeBndrs :: ([VarBndr TyVar Specificity] -> TcM (TCvSubst, [VarBndr TcTyVar Specificity]))
+ -- ^ How to instantiate the type variables
+ -> Id -- ^ Type to instantiate
+ -> TcM ([(Name, VarBndr TcTyVar Specificity)], TcThetaType, TcType) -- ^ Result
+ -- (type vars, preds (incl equalities), rho)
+tcInstTypeBndrs inst_tyvars id =
+ let (tyvars, rho) = splitForAllVarBndrs (idType id)
+ tyvars' = map argf_to_spec tyvars
+ in tc_inst_internal inst_tyvars tyvars' rho
+ where
+ argf_to_spec :: VarBndr TyCoVar ArgFlag -> VarBndr TyCoVar Specificity
+ argf_to_spec (Bndr tv Required) = Bndr tv SpecifiedSpec
+ -- see Note [Specificity in HsForAllTy] in GHC.Hs.Types
+ argf_to_spec (Bndr tv (Invisible s)) = Bndr tv s
tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type signature with skolem constants.
@@ -1000,12 +1032,16 @@ newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- an existing TyVar. We substitute kind variables in the kind.
newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
-newMetaTyVarTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+newMetaTyVarTyVars :: [VarBndr TyVar Specificity]
+ -> TcM (TCvSubst, [VarBndr TcTyVar Specificity])
newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst
-newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+newMetaTyVarTyVarX :: TCvSubst -> (VarBndr TyVar Specificity)
+ -> TcM (TCvSubst, VarBndr TcTyVar Specificity)
-- Just like newMetaTyVarX, but make a TyVarTv
-newMetaTyVarTyVarX subst tyvar = new_meta_tv_x TyVarTv subst tyvar
+newMetaTyVarTyVarX subst (Bndr tv spec) =
+ do { (subst', tv') <- new_meta_tv_x TyVarTv subst tv
+ ; return (subst', (Bndr tv' spec)) }
newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newWildCardX subst tv
@@ -1972,6 +2008,10 @@ zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
; return (setTyVarKind tv kind') }
+zonkTyCoVarKindBinder :: (VarBndr TyCoVar fl) -> TcM (VarBndr TyCoVar fl)
+zonkTyCoVarKindBinder (Bndr tv fl) = do { kind' <- zonkTcType (tyVarKind tv)
+ ; return $ Bndr (setTyVarKind tv kind') fl }
+
{-
************************************************************************
* *
@@ -2178,12 +2218,12 @@ zonkTcTyVarToTyVar tv
(ppr tv $$ ppr ty)
; return tv' }
-zonkTyVarTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
+zonkTyVarTyVarPairs :: [(Name,VarBndr TcTyVar Specificity)] -> TcM [(Name,VarBndr TcTyVar Specificity)]
zonkTyVarTyVarPairs prs
= mapM do_one prs
where
- do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
- ; return (nm, tv') }
+ do_one (nm, Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv
+ ; return (nm, Bndr tv' spec) }
-- zonkId is used *during* typechecking just to zonk the Id's type
zonkId :: TcId -> TcM TcId
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 2ee00a88dc..fb1d6f432b 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -21,7 +21,7 @@ module GHC.Tc.Utils.TcType (
-- Types
TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
- TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcTyCon,
+ TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcTyCon,
KnotTied,
ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
@@ -130,8 +130,9 @@ module GHC.Tc.Utils.TcType (
Type, PredType, ThetaType, TyCoBinder,
ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
- mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys, mkTyCoInvForAllTy,
- mkInvForAllTy, mkInvForAllTys,
+ mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys,
+ mkSpecForAllTys, mkTyCoInvForAllTy,
+ mkInfForAllTy, mkInfForAllTys,
mkVisFunTy, mkVisFunTys, mkInvisFunTy, mkInvisFunTys,
mkTyConApp, mkAppTy, mkAppTys,
mkTyConTy, mkTyVarTy, mkTyVarTys,
@@ -337,8 +338,9 @@ type TcTyCoVar = Var -- Either a TcTyVar or a CoVar
-- a cannot occur inside a MutTyVar in T; that is,
-- T is "flattened" before quantifying over a
-type TcTyVarBinder = TyVarBinder
-type TcTyCon = TyCon -- these can be the TcTyCon constructor
+type TcTyVarBinder = TyVarBinder
+type TcInvisTVBinder = InvisTVBinder
+type TcTyCon = TyCon -- these can be the TcTyCon constructor
-- These types do not have boxy type variables in them
type TcPredType = PredType
@@ -1213,8 +1215,9 @@ tcSplitForAllTys ty
-- @'sameVis' argf supplied_argf@ is 'True', where @argf@ is the visibility
-- of the @ForAllTy@'s binder and @supplied_argf@ is the visibility provided
-- as an argument to this function.
-tcSplitForAllTysSameVis :: ArgFlag -> Type -> ([TyVar], Type)
-tcSplitForAllTysSameVis supplied_argf ty = ASSERT( all isTyVar (fst sty) ) sty
+-- All split tyvars are annotated with their argf.
+tcSplitForAllTysSameVis :: ArgFlag -> Type -> ([TyVarBinder], Type)
+tcSplitForAllTysSameVis supplied_argf ty = ASSERT( all (isTyVar . binderVar) (fst sty) ) sty
where sty = splitForAllTysSameVis supplied_argf ty
-- | Like 'tcSplitForAllTys', but splits off only named binders.
View Lorry Controller Status