[Git][ghc/ghc][wip/jbruenker/foreach] 2 commits: wip add Erasure to ppr functions
Jakob Brünker (@JakobBruenker)
gitlab at gitlab.haskell.org
Mon Dec 4 05:15:02 UTC 2023
Jakob Brünker pushed to branch wip/jbruenker/foreach at Glasgow Haskell Compiler / GHC
Commits:
ba4ffaf6 by Jakob Bruenker at 2023-12-02T22:59:04+01:00
wip add Erasure to ppr functions
- - - - -
d6113cc3 by Jakob Bruenker at 2023-12-04T06:13:32+01:00
wip split off foreach added function type in tcSplit functions
- - - - -
14 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/PatSyn.hs
- compiler/GHC/Core/TyCo/Ppr.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/CoreToIface.hs-boot
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Types/TyThing/Ppr.hs
- compiler/GHC/Types/Var.hs
- compiler/Language/Haskell/Syntax/Pat.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -2,6 +2,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
{-
(c) The University of Glasgow 2006
@@ -252,7 +253,7 @@ ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc)
-> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch ppr_rhs fam_tc branch
= foldr1 (flip hangNotEmpty 2)
- [ pprUserForAll (mkForAllTyBinders Inferred bndrs')
+ [ pprUserForAll (map (Erased,) $ mkForAllTyBinders Inferred bndrs')
-- See Note [Printing foralls in type family instances] in GHC.Iface.Type
, pp_lhs <+> ppr_rhs tidy_env ee_rhs
, vcat [ text "-- Defined" <+> pp_loc
=====================================
compiler/GHC/Core/PatSyn.hs
=====================================
@@ -1,3 +1,5 @@
+{-# LANGUAGE TupleSections #-}
+
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1998
@@ -6,7 +8,6 @@
-}
-
module GHC.Core.PatSyn (
-- * Main data types
PatSyn, PatSynMatcher, PatSynBuilder, mkPatSyn,
@@ -502,7 +503,7 @@ pprPatSynType :: PatSyn -> SDoc
pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
, psExTyVars = ex_tvs, psProvTheta = prov_theta
, psArgs = orig_args, psResultTy = orig_res_ty })
- = sep [ pprForAll $ tyVarSpecToBinders univ_tvs
+ = sep [ pprForAll $ map (Erased,) $ tyVarSpecToBinders univ_tvs
, pprThetaArrowTy req_theta
, ppWhen insert_empty_ctxt $ parens empty <+> darrow
, pprType sigma_ty ]
=====================================
compiler/GHC/Core/TyCo/Ppr.hs
=====================================
@@ -1,4 +1,5 @@
{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TupleSections #-}
-- | Pretty-printing types and coercions.
module GHC.Core.TyCo.Ppr
@@ -27,7 +28,7 @@ module GHC.Core.TyCo.Ppr
import GHC.Prelude
import {-# SOURCE #-} GHC.CoreToIface
- ( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndrs
+ ( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr
, toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX )
import {-# SOURCE #-} GHC.Core.DataCon
@@ -161,13 +162,13 @@ pprThetaArrowTy = pprIfaceContextArr . map tidyToIfaceType
pprSigmaType :: Type -> SDoc
pprSigmaType = pprIfaceSigmaType ShowForAllWhen . tidyToIfaceType
-pprForAll :: [ForAllTyBinder] -> SDoc
-pprForAll tvs = pprIfaceForAll (toIfaceForAllBndrs tvs)
+pprForAll :: [(Erasure, ForAllTyBinder)] -> SDoc
+pprForAll = pprIfaceForAll . (map . fmap) toIfaceForAllBndr
-- | Print a user-level forall; see @Note [When to print foralls]@ in
-- "GHC.Iface.Type".
-pprUserForAll :: [ForAllTyBinder] -> SDoc
-pprUserForAll = pprUserIfaceForAll . toIfaceForAllBndrs
+pprUserForAll :: [(Erasure, ForAllTyBinder)] -> SDoc
+pprUserForAll = pprUserIfaceForAll . (map . fmap) toIfaceForAllBndr
pprTCvBndrs :: [ForAllTyBinder] -> SDoc
pprTCvBndrs tvs = sep (map pprTCvBndr tvs)
@@ -318,7 +319,7 @@ pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc]
where
(_univ_tvs, _ex_tvs, _eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc
user_bndrs = tyVarSpecToBinders $ dataConUserTyVarBinders dc
- forAllDoc = pprUserForAll user_bndrs
+ forAllDoc = pprUserForAll $ map (Erased,) user_bndrs
thetaDoc = pprThetaArrowTy theta
argsDoc = hsep (fmap pprParendType (map scaledThing arg_tys))
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -1437,6 +1437,8 @@ piResultTy ty arg = case piResultTy_maybe ty arg of
piResultTy_maybe :: Type -> Type -> Maybe Type
-- We don't need a 'tc' version, because
-- this function behaves the same for Type and Constraint
+-- XXX JB actually we probably do need a separate tc thing, since foreach is handled differently in tc and core (check if this is still used for tc)
+-- XXX JB same applies to piResultTys below
piResultTy_maybe ty arg = case coreFullView ty of
FunTy { ft_res = res } -> Just res
@@ -1761,7 +1763,7 @@ tyConBindersPiTyBinders :: [TyConBinder] -> [PiTyBinder]
-- Return the tyConBinders in PiTyBinder form
tyConBindersPiTyBinders = map to_tyb
where
- to_tyb (Bndr tv (NamedTCB vis)) = Named Erased (Bndr tv vis) -- XXX JB TyConBinder is this really always Erased?
+ to_tyb (Bndr tv (NamedTCB vis)) = Named Erased (Bndr tv vis) -- XXX JB is this really always Erased? I think since we're dealing with type constructors the answer is yes (this is also never used)
to_tyb (Bndr tv AnonTCB) = Anon (tymult (varType tv)) FTF_T_T
-- | Make a dependent forall over a TyCoVar
=====================================
compiler/GHC/CoreToIface.hs-boot
=====================================
@@ -11,6 +11,7 @@ import GHC.Types.Var.Set( VarSet )
-- For GHC.Core.TyCo.Rep
toIfaceTypeX :: VarSet -> Type -> IfaceType
toIfaceTyLit :: TyLit -> IfaceTyLit
+toIfaceForAllBndr :: VarBndr TyCoVar flag -> VarBndr IfaceBndr flag
toIfaceForAllBndrs :: [VarBndr TyCoVar flag] -> [VarBndr IfaceBndr flag]
toIfaceTyCon :: TyCon -> IfaceTyCon
toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -6,6 +6,7 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TupleSections #-}
module GHC.Iface.Syntax (
module GHC.Iface.Type,
@@ -72,7 +73,7 @@ import GHC.Unit.Module.Warnings
import GHC.Types.SrcLoc
import GHC.Types.SourceText
import GHC.Data.BooleanFormula ( BooleanFormula(..), pprBooleanFormula, isTrue )
-import GHC.Types.Var( VarBndr(..), binderVar, tyVarSpecToBinders, visArgTypeLike )
+import GHC.Types.Var( VarBndr(..), binderVar, tyVarSpecToBinders, visArgTypeLike, Erasure(..) )
import GHC.Core.TyCon ( Role (..), Injectivity(..), tyConBndrVisForAllTyFlag )
import GHC.Core.DataCon (SrcStrictness(..), SrcUnpackedness(..))
import GHC.Builtin.Types ( constraintKindTyConName )
@@ -738,7 +739,7 @@ pprAxBranch pp_tc idx (IfaceAxBranch { ifaxbTyVars = tvs
where
-- See Note [Printing foralls in type family instances] in GHC.Iface.Type
ppr_binders = maybe_index <+>
- pprUserIfaceForAll (map (mkIfaceForAllTvBndr Specified) tvs)
+ pprUserIfaceForAll (map ((Erased,) . mkIfaceForAllTvBndr Specified) tvs)
pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys)
-- See Note [Displaying axiom incompatibilities]
@@ -917,7 +918,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
is_data_instance = isIfaceDataInstance parent
-- See Note [Printing foralls in type family instances] in GHC.Iface.Type
pp_data_inst_forall :: SDoc
- pp_data_inst_forall = pprUserIfaceForAll forall_bndrs
+ pp_data_inst_forall = pprUserIfaceForAll $ map (Erased,) forall_bndrs
forall_bndrs :: [IfaceForAllBndr]
forall_bndrs = [Bndr (binderVar tc_bndr) Specified | tc_bndr <- binders]
@@ -1133,8 +1134,8 @@ pprIfaceDecl _ (IfacePatSyn { ifName = name,
, pprIfaceType $ foldr (IfaceFunTy visArgTypeLike many_ty)
pat_ty arg_tys ])
pat_body = braces $ sep $ punctuate comma $ map ppr pat_fldlbls
- univ_msg = pprUserIfaceForAll $ tyVarSpecToBinders univ_bndrs
- ex_msg = pprUserIfaceForAll $ tyVarSpecToBinders ex_bndrs
+ univ_msg = pprUserIfaceForAll $ map (Erased,) $ tyVarSpecToBinders univ_bndrs
+ ex_msg = pprUserIfaceForAll $ map (Erased,) $ tyVarSpecToBinders ex_bndrs
insert_empty_ctxt = null req_ctxt
&& not (null prov_ctxt && isEmpty sdocCtx ex_msg)
@@ -1262,9 +1263,9 @@ pprIfaceConDecl ss gadt_style tycon tc_binders parent
-- the visibilities of the existential tyvar binders, we can simply drop
-- the universal tyvar binders from user_tvbs.
ex_tvbs = dropList tc_binders user_tvbs
- ppr_ex_quant = pprIfaceForAllPartMust (ifaceForAllSpecToBndrs ex_tvbs) ctxt
+ ppr_ex_quant = pprIfaceForAllPartMust (map (Erased,) $ ifaceForAllSpecToBndrs ex_tvbs) ctxt
pp_gadt_res_ty = mk_user_con_res_ty eq_spec
- ppr_gadt_ty = pprIfaceForAllPart (ifaceForAllSpecToBndrs user_tvbs) ctxt pp_tau
+ ppr_gadt_ty = pprIfaceForAllPart (map (Erased,) $ ifaceForAllSpecToBndrs user_tvbs) ctxt pp_tau
-- A bit gruesome this, but we can't form the full con_tau, and ppr it,
-- because we don't have a Name for the tycon, only an OccName
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -476,7 +476,7 @@ isIfaceLifted (IfaceTyConApp tc args)
= True
isIfaceLifted _ = False
-splitIfaceSigmaTy :: IfaceType -> ([IfaceForAllBndr], [IfacePredType], IfaceType)
+splitIfaceSigmaTy :: IfaceType -> ([(Erasure, IfaceForAllBndr)], [IfacePredType], IfaceType)
-- Mainly for printing purposes
--
-- Here we split nested IfaceSigmaTy properly.
@@ -500,9 +500,9 @@ splitIfaceSigmaTy ty
(theta, tau) = split_rho rho
-- XXX JB Iface do we need to check the erasure here?
- split_foralls (IfaceForAllTy _ bndr ty)
+ split_foralls (IfaceForAllTy eras bndr ty)
| isInvisibleForAllTyFlag (binderFlag bndr)
- = case split_foralls ty of { (bndrs, rho) -> (bndr:bndrs, rho) }
+ = case split_foralls ty of { (bndrs, rho) -> ((eras, bndr):bndrs, rho) }
split_foralls rho = ([], rho)
split_rho (IfaceFunTy af _ ty1 ty2)
@@ -510,11 +510,10 @@ splitIfaceSigmaTy ty
= case split_rho ty2 of { (ps, tau) -> (ty1:ps, tau) }
split_rho tau = ([], tau)
-splitIfaceReqForallTy :: IfaceType -> ([IfaceForAllBndr], IfaceType)
--- XXX JB Iface do we need to check the erasure here?
-splitIfaceReqForallTy (IfaceForAllTy _ bndr ty)
+splitIfaceReqForallTy :: IfaceType -> ([(Erasure, IfaceForAllBndr)], IfaceType)
+splitIfaceReqForallTy (IfaceForAllTy eras bndr ty)
| isVisibleForAllTyFlag (binderFlag bndr)
- = case splitIfaceReqForallTy ty of { (bndrs, rho) -> (bndr:bndrs, rho) }
+ = case splitIfaceReqForallTy ty of { (bndrs, rho) -> ((eras, bndr):bndrs, rho) }
splitIfaceReqForallTy rho = ([], rho)
suppressIfaceInvisibles :: PrintExplicitKinds -> [IfaceTyConBinder] -> [a] -> [a]
@@ -1275,12 +1274,12 @@ ppr_app_arg ctx_prec (t, argf) =
_ -> empty
-------------------
-pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
+pprIfaceForAllPart :: [(Erasure, IfaceForAllBndr)] -> [IfacePredType] -> SDoc -> SDoc
pprIfaceForAllPart tvs ctxt sdoc
= ppr_iface_forall_part ShowForAllWhen tvs ctxt sdoc
-- | Like 'pprIfaceForAllPart', but always uses an explicit @forall at .
-pprIfaceForAllPartMust :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
+pprIfaceForAllPartMust :: [(Erasure, IfaceForAllBndr)] -> [IfacePredType] -> SDoc -> SDoc
pprIfaceForAllPartMust tvs ctxt sdoc
= ppr_iface_forall_part ShowForAllMust tvs ctxt sdoc
@@ -1289,9 +1288,8 @@ pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)]
pprIfaceForAllCoPart tvs sdoc
= sep [ pprIfaceForAllCo tvs, sdoc ]
--- XXX JB HERE printing this needs to be fixed
ppr_iface_forall_part :: ShowForAllFlag
- -> [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
+ -> [(Erasure, IfaceForAllBndr)] -> [IfacePredType] -> SDoc -> SDoc
ppr_iface_forall_part show_forall tvs ctxt sdoc
= sep [ case show_forall of
ShowForAllMust -> pprIfaceForAll tvs
@@ -1300,13 +1298,13 @@ ppr_iface_forall_part show_forall tvs ctxt sdoc
, sdoc]
-- | Render the "forall ... ." or "forall ... ->" bit of a type.
-pprIfaceForAll :: [IfaceForAllBndr] -> SDoc
+pprIfaceForAll :: [(Erasure, IfaceForAllBndr)] -> SDoc
pprIfaceForAll [] = empty
-pprIfaceForAll bndrs@(Bndr _ vis : _)
- = sep [ add_separator (forAllLit <+> fsep docs)
+pprIfaceForAll bndrs@((eras, Bndr _ vis) : _)
+ = sep [ add_separator ((if eras == Erased then forAllLit else forEachLit) <+> fsep docs)
, pprIfaceForAll bndrs' ]
where
- (bndrs', docs) = ppr_itv_bndrs bndrs vis
+ (bndrs', docs) = ppr_itv_bndrs bndrs eras vis
add_separator stuff = case vis of
Required -> stuff <+> arrow
@@ -1316,14 +1314,16 @@ pprIfaceForAll bndrs@(Bndr _ vis : _)
-- | Render the ... in @(forall ... .)@ or @(forall ... ->)@.
-- Returns both the list of not-yet-rendered binders and the doc.
-- No anonymous binders here!
-ppr_itv_bndrs :: [IfaceForAllBndr]
+ppr_itv_bndrs :: [(Erasure, IfaceForAllBndr)]
+ -> Erasure -- ^ erasure of the first binder in the list
-> ForAllTyFlag -- ^ visibility of the first binder in the list
- -> ([IfaceForAllBndr], [SDoc])
-ppr_itv_bndrs all_bndrs@(bndr@(Bndr _ vis) : bndrs) vis1
- | vis `eqForAllVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
+ -> ([(Erasure, IfaceForAllBndr)], [SDoc])
+ppr_itv_bndrs all_bndrs@((eras, bndr@(Bndr _ vis)) : bndrs) eras1 vis1
+ | eras == eras1
+ , vis `eqForAllVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs eras1 vis1 in
(bndrs', pprIfaceForAllBndr bndr : doc)
| otherwise = (all_bndrs, [])
-ppr_itv_bndrs [] _ = ([], [])
+ppr_itv_bndrs [] _ _ = ([], [])
pprIfaceForAllCo :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc
pprIfaceForAllCo [] = empty
@@ -1409,14 +1409,15 @@ ppr_sigma show_forall ctxt_prec iface_ty
in ppr_iface_forall_part show_forall invis_tvs theta $
sep [pprIfaceForAll req_tvs, ppr_ty_nested tau']
-pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
-pprUserIfaceForAll tvs
+pprUserIfaceForAll :: [(Erasure, IfaceForAllBndr)] -> SDoc
+pprUserIfaceForAll etvs
+ | let tvs = map snd etvs
= sdocOption sdocPrintExplicitForalls $ \print_foralls ->
-- See Note [When to print foralls] in this module.
ppWhen (any tv_has_kind_var tvs
|| any tv_is_required tvs
|| print_foralls) $
- pprIfaceForAll tvs
+ pprIfaceForAll etvs
where
tv_has_kind_var (Bndr (IfaceTvBndr (_,kind)) _)
= not (ifTypeIsVarFree kind)
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -637,12 +637,19 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- Rule ITVDQ from the GHC Proposal #281
go1 delta acc so_far fun_ty ((EValArg { eva_arg = ValArg arg }) : rest_args)
- | Just (eras, tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty -- XXX JB HERE
+ | Just (Erased, tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty
, binderFlag tvb == Required
= do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg
; let wrap = mkWpTyApps [ty_arg]
; go delta (addArgWrap wrap acc) so_far inst_body rest_args }
+ go1 delta acc so_far fun_ty ((EValArg { eva_arg = ValArg arg }) : rest_args)
+ | Just (Retained, tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty -- XXX JB HERE
+ , binderFlag tvb == Required -- XXX JB what if it's not required? How is regular forall handled in that case?
+ = do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg
+ ; let wrap = mkWpTyApps [ty_arg]
+ ; go delta (addArgWrap wrap acc) so_far inst_body rest_args }
+
-- Rule IRESULT from Fig 4 of the QL paper
go1 delta acc _ fun_ty []
= do { traceTc "tcInstFun:ret" (ppr fun_ty)
@@ -983,6 +990,7 @@ Syntax of applications in HsExpr
This nesting makes `type` rather different from `@`. Remember, the HsEmbTy mainly just
switches namespace, and is subject to the term-to-type transformation.
+-- XXX JB note update
Syntax of abstractions in Pat
-----------------------------
* Type patterns are represented in Pat roughly like this
=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -1100,7 +1100,7 @@ ty_con_binders_ty_binders' :: [TyConBinder] -> ([PiTyBinder], Bool)
ty_con_binders_ty_binders' = foldr go ([], False)
where
go (Bndr tv (NamedTCB vis)) (bndrs, _)
- = (Named Erased (Bndr tv vis) : bndrs, True) -- XXX JB Named is it really always Erased?
+ = (Named Erased (Bndr tv vis) : bndrs, True) -- XXX JB Named is it really always Erased? I think since we're dealing with type constructors the answer is yes
go (Bndr tv AnonTCB) (bndrs, n)
= (Anon (tymult (tyVarKind tv)) FTF_T_T : bndrs, n)
{-# INLINE go #-}
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -2,6 +2,8 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
{-
(c) The University of Glasgow 2006
@@ -893,7 +895,7 @@ tcTyFamInstsAndVisX = go
| otherwise
= tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys
go _ (LitTy {}) = []
- go is_invis_arg (ForAllTy _ bndr ty) = go is_invis_arg (binderType bndr)
+ go is_invis_arg (ForAllTyWithFun _ bndr ty) = go is_invis_arg (binderType bndr)
++ go is_invis_arg ty
go is_invis_arg (FunTy _ w ty1 ty2) = go is_invis_arg w
++ go is_invis_arg ty1
@@ -972,7 +974,7 @@ any_rewritable role tv_pred tc_pred should_expand
go rl bvs arg || go rl bvs res || go NomEq bvs w
where arg_rep = getRuntimeRep arg -- forgetting these causes #17024
res_rep = getRuntimeRep res
- go rl bvs (ForAllTy _ tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty
+ go rl bvs (ForAllTyWithFun _ tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty
go rl bvs (CastTy ty _) = go rl bvs ty
go _ _ (CoercionTy _) = False
@@ -1328,7 +1330,7 @@ getDFunTyKey (TyConApp tc _) = getOccName tc
getDFunTyKey (LitTy x) = getDFunTyLitKey x
getDFunTyKey (AppTy fun _) = getDFunTyKey fun
getDFunTyKey (FunTy { ft_af = af }) = getOccName (funTyFlagTyCon af)
-getDFunTyKey (ForAllTy _ _ t) = getDFunTyKey t
+getDFunTyKey (ForAllTyWithFun _ _ t) = getDFunTyKey t
getDFunTyKey (CastTy ty _) = getDFunTyKey ty
getDFunTyKey t@(CoercionTy _) = pprPanic "getDFunTyKey" (ppr t)
@@ -1345,13 +1347,35 @@ getDFunTyLitKey (CharTyLit n) = mkOccName Name.varName (show n)
************************************************************************
-}
+-- | Attempts to take a ForAllTy apart, returning the full ForAllTyBinder, but assumes that any coreView stuff is already done
+tcSplitForAllForAllTyBinderNoView_maybe :: Type -> Maybe (Erasure, ForAllTyBinder, Type)
+tcSplitForAllForAllTyBinderNoView_maybe (ForAllTy Erased bndr inner_ty) = Just (Erased, bndr, inner_ty)
+tcSplitForAllForAllTyBinderNoView_maybe (ForAllTy Retained bndr (FunTy FTF_T_T mult arg_ty inner_ty)) =
+ assert (eqType (binderType bndr) arg_ty) . assert (eqType mult manyDataConTy) $
+ Just (Retained, bndr, inner_ty)
+tcSplitForAllForAllTyBinderNoView_maybe (ForAllTy Retained _ _) =
+ panic "tcSplitForAllForAllTyBinderNoView_maybe: Retained binder without matching FunTy"
+tcSplitForAllForAllTyBinderNoView_maybe _ = Nothing
+
+-- | Acts like ForAllTy, but for retained binders additionally removes the function type that is added in Core
+pattern ForAllTyWithFun :: Erasure -> ForAllTyBinder -> Type -> Type
+pattern ForAllTyWithFun eras bndr ty <- (tcSplitForAllForAllTyBinderNoView_maybe -> Just (eras, bndr, ty))
+{-# COMPLETE TyVarTy, AppTy, TyConApp, ForAllTyWithFun, FunTy, LitTy, CastTy, CoercionTy #-}
+
-- | Splits a forall type into a list of 'PiTyVarBinder's and the inner type.
-- Always succeeds, even if it returns an empty list.
tcSplitPiTys :: Type -> ([PiTyVarBinder], Type)
tcSplitPiTys ty
= assert (all isTyBinder (fst sty)) -- No CoVar binders here
sty
- where sty = splitPiTys ty
+ where
+ sty = split ty ty []
+
+ split _ (ForAllTyWithFun eras b res) bs = split res res (Named eras b : bs)
+ split _ (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) bs
+ = split res res (Anon (Scaled w arg) af : bs)
+ split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
+ split orig_ty _ bs = (reverse bs, orig_ty)
-- | Splits a type into a PiTyVarBinder and a body, if possible.
tcSplitPiTy_maybe :: Type -> Maybe (PiTyVarBinder, Type)
@@ -1359,18 +1383,20 @@ tcSplitPiTy_maybe ty
= assert (isMaybeTyBinder sty) -- No CoVar binders here
sty
where
- sty = splitPiTy_maybe ty
+ sty = tc_split_pi_ty_maybe ty
isMaybeTyBinder (Just (t,_)) = isTyBinder t
isMaybeTyBinder _ = True
+ tc_split_pi_ty_maybe :: Type -> Maybe (PiTyBinder, Type)
+ tc_split_pi_ty_maybe ty = case coreFullView ty of
+ ForAllTyWithFun eras bndr ty -> Just (Named eras bndr, ty)
+ FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res}
+ -> Just (Anon (mkScaled w arg) af, res)
+ _ -> Nothing
+
tcSplitForAllTyVarBinder_maybe :: Type -> Maybe (Erasure, TyVarBinder, Type)
tcSplitForAllTyVarBinder_maybe ty | Just ty' <- coreView ty = tcSplitForAllTyVarBinder_maybe ty'
-tcSplitForAllTyVarBinder_maybe (ForAllTy Retained tv (FunTy FTF_T_T mult arg_ty ty)) =
- assert (isTyVarBinder tv) . assert (eqType (binderType tv) arg_ty) . assert (eqType mult manyDataConTy) $
- Just (Retained, tv, ty)
-tcSplitForAllTyVarBinder_maybe (ForAllTy Retained _ _) =
- panic "tcSplitForAllTyVarBinder_maybe: Retained binder without matching FunTy"
-tcSplitForAllTyVarBinder_maybe (ForAllTy Erased tv ty) = assert (isTyVarBinder tv ) Just (Erased, tv, ty)
+tcSplitForAllTyVarBinder_maybe (ForAllTyWithFun eras tv ty) = assert (isTyVarBinder tv ) Just (eras, tv, ty)
tcSplitForAllTyVarBinder_maybe _ = Nothing
-- | Like 'tcSplitPiTys', but splits off only named binders,
@@ -1378,7 +1404,12 @@ tcSplitForAllTyVarBinder_maybe _ = Nothing
tcSplitForAllTyVars :: Type -> ([TyVar], Type)
tcSplitForAllTyVars ty
= assert (all isTyVar (fst sty)) sty
- where sty = splitForAllTyCoVars ty
+ where
+ sty = split ty ty []
+
+ split _ (ForAllTyWithFun _ (Bndr tv _) ty) tvs = split ty ty (tv:tvs)
+ split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
+ split orig_ty _ tvs = (reverse tvs, orig_ty)
-- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible'
-- type variable binders.
@@ -1393,7 +1424,7 @@ tcSplitSomeForAllTyVars :: (ForAllTyFlag -> Bool) -> Type -> ([TyVar], Type)
tcSplitSomeForAllTyVars argf_pred ty
= split ty ty []
where
- split _ (ForAllTy _ (Bndr tv argf) ty) tvs
+ split _ (ForAllTyWithFun _ (Bndr tv argf) ty) tvs
| argf_pred argf = split ty ty (tv:tvs)
split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
split orig_ty _ tvs = (reverse tvs, orig_ty)
@@ -1402,18 +1433,33 @@ tcSplitSomeForAllTyVars argf_pred ty
-- variable binders. All split tyvars are annotated with '()'.
tcSplitForAllReqTVBinders :: Type -> ([TcReqTVBinder], Type)
tcSplitForAllReqTVBinders ty = assert (all isTyVarBinder (fst sty) ) sty
- where sty = splitForAllReqTyBinders ty
+ where
+ sty = split ty ty []
+
+ split _ (ForAllTyWithFun _ (Bndr tv Required) ty) tvs = split ty ty (Bndr tv ():tvs)
+ split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
+ split orig_ty _ tvs = (reverse tvs, orig_ty)
-- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible' type
-- variable binders. All split tyvars are annotated with their 'Specificity'.
tcSplitForAllInvisTVBinders :: Type -> ([TcInvisTVBinder], Type)
tcSplitForAllInvisTVBinders ty = assert (all (isTyVar . binderVar) (fst sty)) sty
- where sty = splitForAllInvisTyBinders ty
+ where
+ sty = split ty ty []
+
+ split _ (ForAllTyWithFun _ (Bndr tv (Invisible spec)) ty) tvs = split ty ty (Bndr tv spec:tvs)
+ split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
+ split orig_ty _ tvs = (reverse tvs, orig_ty)
-- | Like 'tcSplitForAllTyVars', but splits off only named binders.
tcSplitForAllTyVarBinders :: Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders ty = assert (all isTyVarBinder (fst sty)) sty
- where sty = splitForAllForAllTyBinders ty
+ where
+ sty = split ty ty []
+
+ split _ (ForAllTyWithFun _ b res) bs = split res res (b:bs)
+ split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
+ split orig_ty _ bs = (reverse bs, orig_ty)
tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
-- Split off the first predicate argument from a type
@@ -1892,7 +1938,7 @@ isOverloadedTy :: Type -> Bool
-- Yes for a type of a function that might require evidence-passing
-- Used only by bindLocalMethods
isOverloadedTy ty | Just ty' <- coreView ty = isOverloadedTy ty'
-isOverloadedTy (ForAllTy _ _ ty) = isOverloadedTy ty
+isOverloadedTy (ForAllTyWithFun _ _ ty) = isOverloadedTy ty
isOverloadedTy (FunTy { ft_af = af }) = isInvisibleFunArg af
isOverloadedTy _ = False
@@ -2232,7 +2278,7 @@ pSizeTypeX bvs (TyConApp tc tys) = pSizeTyConAppX bvs tc tys
pSizeTypeX bvs (AppTy fun arg) = pSizeTypeX bvs fun `addPSize` pSizeTypeX bvs arg
pSizeTypeX bvs (FunTy _ w arg res) = pSizeTypeX bvs w `addPSize` pSizeTypeX bvs arg `addPSize`
pSizeTypeX bvs res
-pSizeTypeX bvs (ForAllTy _ (Bndr tv _) ty) = pSizeTypeX bvs (tyVarKind tv) `addPSize`
+pSizeTypeX bvs (ForAllTyWithFun _ (Bndr tv _) ty) = pSizeTypeX bvs (tyVarKind tv) `addPSize`
pSizeTypeX (bvs `extendVarSet` tv) ty
pSizeTypeX bvs (CastTy ty _) = pSizeTypeX bvs ty
pSizeTypeX _ (CoercionTy {}) = pSizeOne
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -388,6 +388,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
where
-- Skolemise any /invisible/ foralls /before/ the zero-arg case
-- so that we guarantee to return a rho-type
+ -- XXX JB do we need to do something different here for foreach? E.g. should tcSplitSigma return Erasure for each tv?
go acc_arg_tys n ty
| (tvs, theta, _) <- tcSplitSigmaTy ty -- Invisible binders only!
, not (null tvs && null theta) -- Visible ones handled below
@@ -403,6 +404,13 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
go acc_arg_tys n ty
| Just ty' <- coreView ty = go acc_arg_tys n ty'
+ -- XXX JB these actually aren't here I just need to put this somewhere
+ -- XXX JB HERE HERE: right now \x -> x (or undefined) :: foreach x -> x results in a stack overflow :thinking:
+ -- XXX JB HERE HERE: foo :: foreach x -> Int; foo x = 4 right now has type `forall (x :: k) -> k -> Int`. Should be foreach I guess
+ -- XXX JB HERE HERE: :t undefined :: foreach x -> x results in Couldn't match expected type forall x -> * -> x with actual type a0
+ -- XXX JB HERE example of core lint failure: let foo :: foreach x -> Int; foo (type x) = 4
+ -- XXX JB HERE the above works without -dlint, except when you run `:t foo (type True)", it then says "Bool -> Int"
+ -- XXX JB "foo :: foreach x . Int; foo = 4" fails - and that makes sense, we're not stripping the foreach anywhere, so also not stripping the function type - uhh though actually I guess I see no reason why tcSplitForAllTyVarBinder or some variant wouldn't be called when checking the type, now that I think about it (seems like it might not be useful to have a retained arg on which you don't match, but what if you use pointfree style?)
-- Decompose /visible/ (forall a -> blah), to give an ExpForAllPat
-- NB: invisible binders are handled by tcSplitSigmaTy/tcTopSkolemise above
@@ -410,7 +418,6 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
-- to syntactically visible patterns in the source program
-- See Note [Visible type application and abstraction] in GHC.Tc.Gen.App
go acc_arg_tys n ty
- -- XXX JB HERE Maybe this should use the tc version of splitForAllTys (and then splitForAllTys can stop removing the function type)
| Just (eras, Bndr tv vis, ty') <- tcSplitForAllTyVarBinder_maybe ty
, Required <- vis
= let init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
=====================================
compiler/GHC/Types/TyThing/Ppr.hs
=====================================
@@ -6,6 +6,8 @@
--
-----------------------------------------------------------------------------
+{-# LANGUAGE TupleSections #-}
+
module GHC.Types.TyThing.Ppr (
pprTyThing,
@@ -20,6 +22,7 @@ import GHC.Prelude
import GHC.Types.TyThing ( TyThing(..), tyThingParent_maybe )
import GHC.Types.Name
+import GHC.Types.Var ( Erasure(..) )
import GHC.Core.Type ( ForAllTyFlag(..), mkTyVarBinders )
import GHC.Core.Coercion.Axiom ( coAxiomTyCon )
@@ -120,7 +123,7 @@ pprFamInst (FamInst { fi_flavor = SynFamilyInst, fi_axiom = axiom
, fi_tvs = tvs, fi_tys = lhs_tys, fi_rhs = rhs })
= showWithLoc (pprDefinedAt (getName axiom)) $
hang (text "type instance"
- <+> pprUserForAll (mkTyVarBinders Specified tvs)
+ <+> pprUserForAll (map (Erased,) $ mkTyVarBinders Specified tvs)
-- See Note [Printing foralls in type family instances]
-- in GHC.Iface.Type
<+> pprTypeApp (coAxiomTyCon axiom) lhs_tys)
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -470,6 +470,7 @@ data Specificity = InferredSpec
deriving (Eq, Ord, Data)
-- | Whether a dependent argument is erased at runtime
+-- XXX JB maybe this should be added to ForAllTyFlag?
data Erasure = Erased | Retained
deriving (Eq, Ord, Data)
=====================================
compiler/Language/Haskell/Syntax/Pat.hs
=====================================
@@ -221,6 +221,8 @@ data Pat p
-- Embed the syntax of types into patterns.
-- Used with RequiredTypeArguments or Foreach, e.g. fn (type t) = rhs
+ -- XXX JB Once we allow type patterns without the type herald, we'll probably have to add to the Tc extension point of some other constructor here whether that pattern is retained in some way.
+ -- XXX JB ...and somehow we also need to handle invisible foreach, like... we need to add an extra pattern for it for the retained type argument, even though there's no existing pattern as in `foreach x . 4
| EmbTyPat (XEmbTyPat p)
!(LHsToken "type" p)
(HsTyPat (NoGhcTc p))
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/2f14e085001a9b659b93c2fa7582a67b5d51e57a...d6113cc3de570e52e193e403ca74c87b8a179b2c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/2f14e085001a9b659b93c2fa7582a67b5d51e57a...d6113cc3de570e52e193e403ca74c87b8a179b2c
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/20231204/d0472b52/attachment-0001.html>
More information about the ghc-commits
mailing list