diff options
Diffstat (limited to 'compiler/GHC/Tc/Gen')
| -rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 80 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Sig.hs | 10 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Splice.hs | 30 |
3 files changed, 64 insertions, 56 deletions
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index e6cad5f4f0..b99cc6365b 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -896,11 +896,10 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind = tc_fun_type mode ty1 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, (inv_tv_bndrs, ty')) - <- pushLevelAndCaptureConstraints $ - bindExplicitTKBndrs_Skol_M mode hs_tvs $ +tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind + = do { (tclvl, wanted, (tv_bndrs, ty')) + <- pushLevelAndCaptureConstraints $ + bindExplicitTKTele_Skol_M mode tele $ -- The _M variant passes on the mode from the type, to -- any wildards in kind signatures on the forall'd variables -- e.g. f :: _ -> Int -> forall (a :: _). blah @@ -909,31 +908,27 @@ tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs -- Do not kind-generalise here! See Note [Kind generalisation] - ; let skol_info = ForAllSkol (ppr forall) (sep (map ppr hs_tvs)) - skol_tvs = binderVars inv_tv_bndrs + ; let skol_info = ForAllSkol (ppr forall) $ sep $ case tele of + HsForAllVis { hsf_vis_bndrs = hs_tvs } -> + map ppr hs_tvs + HsForAllInvis { hsf_invis_bndrs = hs_tvs } -> + map ppr hs_tvs + tv_bndrs' = construct_bndrs tv_bndrs + skol_tvs = binderVars tv_bndrs' ; implic <- buildTvImplication skol_info skol_tvs tclvl wanted ; emitImplication implic -- /Always/ emit this implication even if wanted is empty -- We need the implication so that we check for a bad telescope -- See Note [Skolem escape and forall-types] - ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs - ; return (mkForAllTys tv_bndrs ty') } + ; 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 + construct_bndrs :: Either [TcReqTVBinder] [TcInvisTVBinder] + -> [TcTyVarBinder] + construct_bndrs (Left req_tv_bndrs) = + map (mkTyVarBinder Required . binderVar) req_tv_bndrs + construct_bndrs (Right inv_tv_bndrs) = + map tyVarSpecToBinder inv_tv_bndrs tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind | null (unLoc ctxt) @@ -1068,21 +1063,21 @@ tc_hs_type mode ty@(HsWildCardTy _) ek = tcAnonWildCardOcc mode ty 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. +A HsForAllTy contains an HsForAllTelescope to denote the visibility of the forall +binder. Furthermore, each invisible type variable binder 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 / +---------------------------------------------------------------------------- +| User-written type HsForAllTelescope Specificity ArgFlag +|--------------------------------------------------------------------------- +| f :: forall a. type HsForAllInvis SpecifiedSpec Specified +| f :: forall {a}. type HsForAllInvis InferredSpec Inferred +| f :: forall a -> type HsForAllVis SpecifiedSpec Required +| f :: forall {a} -> type HsForAllVis 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 "GHC.Core.TyCo.Rep". @@ -2863,6 +2858,21 @@ cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar -- Explicit binders -------------------------------------- +-- | Skolemise the 'HsTyVarBndr's in an 'LHsForAllTelescope. +-- Returns 'Left' for visible @forall@s and 'Right' for invisible @forall@s. +bindExplicitTKTele_Skol_M + :: TcTyMode + -> HsForAllTelescope GhcRn + -> TcM a + -> TcM (Either [TcReqTVBinder] [TcInvisTVBinder], a) +bindExplicitTKTele_Skol_M mode tele thing_inside = case tele of + HsForAllVis { hsf_vis_bndrs = bndrs } -> do + (req_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside + pure (Left req_tv_bndrs, thing) + HsForAllInvis { hsf_invis_bndrs = bndrs } -> do + (inv_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside + pure (Right inv_tv_bndrs, thing) + bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv :: (OutputableBndrFlag flag) => [LHsTyVarBndr flag GhcRn] diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs index 2ac2823fb5..df0c7d37f6 100644 --- a/compiler/GHC/Tc/Gen/Sig.hs +++ b/compiler/GHC/Tc/Gen/Sig.hs @@ -279,8 +279,8 @@ no_anon_wc lty = go lty HsRecTy _ flds -> gos $ map (cd_fld_type . unLoc) flds HsExplicitListTy _ _ tys -> gos tys HsExplicitTupleTy _ tys -> gos tys - HsForAllTy { hst_bndrs = bndrs - , hst_body = ty } -> no_anon_wc_bndrs bndrs + HsForAllTy { hst_tele = tele + , hst_body = ty } -> no_anon_wc_tele tele && go ty HsQualTy { hst_ctxt = L _ ctxt , hst_body = ty } -> gos ctxt && go ty @@ -293,8 +293,10 @@ no_anon_wc lty = go lty gos = all go -no_anon_wc_bndrs :: [LHsTyVarBndr flag GhcRn] -> Bool -no_anon_wc_bndrs ltvs = all (go . unLoc) ltvs +no_anon_wc_tele :: HsForAllTelescope GhcRn -> Bool +no_anon_wc_tele tele = case tele of + HsForAllVis { hsf_vis_bndrs = ltvs } -> all (go . unLoc) ltvs + HsForAllInvis { hsf_invis_bndrs = ltvs } -> all (go . unLoc) ltvs where go (UserTyVar _ _ _) = True go (KindedTyVar _ _ _ ki) = no_anon_wc ki diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs index 3a4d0de24f..140299997a 100644 --- a/compiler/GHC/Tc/Gen/Splice.hs +++ b/compiler/GHC/Tc/Gen/Splice.hs @@ -2123,19 +2123,19 @@ 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 - tvbndrs' <- reifyTyVarBndrs tvbndrs - case argToForallVisFlag argf of - ForallVis -> do phi' <- reifyType phi - let tvs = map (() <$) tvbndrs' - -- see Note [Specificity in HsForAllTy] in GHC.Hs.Type - pure $ TH.ForallVisT tvs phi' - ForallInvis -> do let (cxt, tau) = tcSplitPhiTy phi - cxt' <- reifyCxt cxt - tau' <- reifyType tau - pure $ TH.ForallT tvbndrs' cxt' tau' - where - (tvbndrs, phi) = tcSplitForAllTysSameVis argf ty +reify_for_all argf ty + | isVisibleArgFlag argf + = do let (req_bndrs, phi) = tcSplitForAllTysReq ty + tvbndrs' <- reifyTyVarBndrs req_bndrs + phi' <- reifyType phi + pure $ TH.ForallVisT tvbndrs' phi' + | otherwise + = do let (inv_bndrs, phi) = tcSplitForAllTysInvis ty + tvbndrs' <- reifyTyVarBndrs inv_bndrs + let (cxt, tau) = tcSplitPhiTy phi + cxt' <- reifyCxt cxt + tau' <- reifyType tau + pure $ TH.ForallT tvbndrs' cxt' tau' reifyTyLit :: TyCoRep.TyLit -> TcM TH.TyLit reifyTyLit (NumTyLit n) = return (TH.NumTyLit n) @@ -2177,10 +2177,6 @@ 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 |