[Git][ghc/ghc][wip/jbruenker/foreach] wip type desugaring

Jakob Brünker (@JakobBruenker) gitlab at gitlab.haskell.org
Sun Jul 30 21:27:56 UTC 2023



Jakob Brünker pushed to branch wip/jbruenker/foreach at Glasgow Haskell Compiler / GHC


Commits:
1e8dd284 by Jakob Bruenker at 2023-07-30T23:27:43+02:00
wip type desugaring

- - - - -


5 changed files:

- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Types/Var.hs


Changes:

=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -49,7 +49,7 @@ module GHC.Core.TyCo.Rep (
         mkVisFunTy, mkScaledFunTys,
         mkInvisFunTy, mkInvisFunTys,
         tcMkVisFunTy, tcMkInvisFunTy, tcMkScaledFunTys,
-        mkForAllTy, mkForAllTys, mkInvisForAllTys,
+        mkForAllTy, mkForAllTys, mkInvisForAllTys, mkForEachTys,
         mkPiTy, mkPiTys,
         mkVisFunTyMany, mkVisFunTysMany,
         nonDetCmpTyLit, cmpTyLit,
@@ -805,6 +805,11 @@ mkForAllTy bndr body
 mkForAllTys :: [ForAllTyBinder] -> Type -> Type
 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 
+-- | Wraps foralls and function binders over the type using the provided 'TyCoVar's from left to right
+mkForEachTys :: [ForAllTyBinder] -> Type -> Type
+mkForEachTys tyvars ty =
+  foldr (\v t -> mkForAllTy v (mkFunTy FTF_T_T manyDataConTy (binderType v) t)) ty tyvars
+
 -- | Wraps foralls over the type using the provided 'InvisTVBinder's from left to right
 mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
 mkInvisForAllTys tyvars = mkForAllTys (tyVarSpecToBinders tyvars)


=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -133,6 +133,7 @@ dsLHsBind :: LHsBind GhcTc
 dsLHsBind (L loc bind) = do dflags <- getDynFlags
                             putSrcSpanDs (locA loc) $ dsHsBind dflags bind
 
+-- XXX JB Desugar somewhere in here. However we need to add some info during typechecking to the pattern match, maybe, idk, so we can desugar properly
 -- | Desugar a single binding (or group of recursive binds).
 dsHsBind :: DynFlags
          -> HsBind GhcTc


=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -876,6 +876,7 @@ tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty
 
 {- Note [Visible type application and abstraction]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- XXX JB Note update
 GHC supports the types
     forall {a}.  a -> t     -- ForAllTyFlag is Inferred
     forall  a.   a -> t     -- ForAllTyFlag is Specified
@@ -945,20 +946,19 @@ Syntax of types
       forall {a}. t    -- HsForAllInvis (c.o. HsForAllTelescope) and InferredSpec  (c.o. Specificity)
       forall a. t      -- HsForAllInvis (c.o. HsForAllTelescope) and SpecifiedSpec (c.o. Specificity)
       forall a -> t    -- HsForAllVis (c.o. HsForAllTelescope)
-      foreach {a}. t    -- HsForEachInvis (c.o. HsForAllTelescope) and InferredSpec  (c.o. Specificity)
-      foreach a. t      -- HsForEachInvis (c.o. HsForAllTelescope) and SpecifiedSpec (c.o. Specificity)
-      foreach a -> t    -- HsForEachVis (c.o. HsForAllTelescope)
+      foreach {a}. t   -- HsForEachInvis (c.o. HsForAllTelescope) and InferredSpec  (c.o. Specificity)
+      foreach a. t     -- HsForEachInvis (c.o. HsForAllTelescope) and SpecifiedSpec (c.o. Specificity)
+      foreach a -> t   -- HsForEachVis (c.o. HsForAllTelescope)
 
 * By the time we get to checking applications/abstractions (e.g. GHC.Tc.Gen.App)
   the types have been kind-checked (e.g. by tcLHsType) into ForAllTy (c.o. Type).
-  At this stage, we have:
+  At this stage, we have (using t.o. to mean "type of"):
       forall {a}. t    -- ForAllTy (c.o. Type) and Inferred  (c.o. ForAllTyFlag)
       forall a. t      -- ForAllTy (c.o. Type) and Specified (c.o. ForAllTyFlag)
       forall a -> t    -- ForAllTy (c.o. Type) and Required  (c.o. ForAllTyFlag)
-      -- XXX JB fix this. Should be ForAllTy -> FunTy I guess?
-      foreach {a}. t    -- ForAllTy (c.o. Type) and Inferred  (c.o. ForAllTyFlag)
-      foreach a. t      -- ForAllTy (c.o. Type) and Specified (c.o. ForAllTyFlag)
-      foreach a -> t    -- ForAllTy (c.o. Type) and Required  (c.o. ForAllTyFlag)
+      foreach {a}. t.o. a -> t    -- ForAllTy (c.o. Type) and Inferred  (c.o. ForAllTyFlag)
+      foreach a. t.o. a -> t      -- ForAllTy (c.o. Type) and Specified (c.o. ForAllTyFlag)
+      foreach a -> t.o. a -> t    -- ForAllTy (c.o. Type) and Required  (c.o. ForAllTyFlag)
 
 Syntax of applications in HsExpr
 --------------------------------
@@ -1090,6 +1090,7 @@ Proposal #281.
 
 Typechecking type abstractions
 ------------------------------
+-- XXX JB patterns read here!
 Type abstractions are checked alongside ordinary patterns in GHC.Tc.Gen.Pat.tcPats.
 One of its inputs is a list of ExpPatType that has two constructors
   * ExpFunPatTy    ...   -- the type A of a function A -> B


=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1179,9 +1179,8 @@ tc_hs_type mode (HsOpTy _ _ ty1 (L _ op) ty2) exp_kind
   = tc_fun_type mode (HsUnrestrictedArrow noHsUniTok) ty1 ty2 exp_kind
 
 --------- Foralls
--- XXX JB HsForAllTy I think this is where we change things into Core
 tc_hs_type mode (HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
-  = do { (tv_bndrs, ty') <- tcTKTelescope mode tele $
+  = do { (erasure, tv_bndrs, ty') <- tcTKTelescope mode tele $
                             tc_lhs_type mode ty exp_kind
                  -- Pass on the mode from the type, to any wildcards
                  -- in kind signatures on the forall'd variables
@@ -1190,7 +1189,7 @@ tc_hs_type mode (HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
 
        -- Do not kind-generalise here!  See Note [Kind generalisation]
 
-       ; return (mkForAllTys tv_bndrs ty') }
+       ; return ((if erasure == Erased then mkForAllTys else mkForEachTys) tv_bndrs ty') }
 
 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
   | null (unLoc ctxt)
@@ -1382,7 +1381,7 @@ tc_fun_type mode mult ty1 ty2 exp_kind = case mode_tyki mode of
 {- Note [Skolem escape and forall-types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See also Note [Checking telescopes].
--- XXX JB Note update
+-- XX JB Note update
 
 Consider
   f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> ()
@@ -3014,10 +3013,9 @@ checkForDuplicateScopedTyVars scoped_prs
 tcTKTelescope :: TcTyMode
               -> HsForAllTelescope GhcRn
               -> TcM a
-              -> TcM ([TcTyVarBinder], a)
+              -> TcM (Erasure, [TcTyVarBinder], a)
 -- A HsForAllTelescope comes only from a HsForAllTy,
 -- an explicit, user-written forall type
--- XXX JB HsForAllType typechecking, do we need to change this?
 tcTKTelescope mode tele thing_inside = case tele of
   HsForAllVis { hsf_vis_bndrs = bndrs }
     -> do { skol_info <- mkSkolemInfo (ForAllSkol (HsTyVarBndrsRn (unLoc <$> bndrs)))
@@ -3026,7 +3024,7 @@ tcTKTelescope mode tele thing_inside = case tele of
           ; (req_tv_bndrs, thing) <- tcExplicitTKBndrsX skol_mode bndrs thing_inside
             -- req_tv_bndrs :: [VarBndr TyVar ()],
             -- but we want [VarBndr TyVar ForAllTyFlag]
-          ; return (tyVarReqToBinders req_tv_bndrs, thing) }
+          ; return (Erased, tyVarReqToBinders req_tv_bndrs, thing) }
 
   HsForAllInvis { hsf_invis_bndrs = bndrs }
     -> do { skol_info <- mkSkolemInfo (ForAllSkol (HsTyVarBndrsRn (unLoc <$> bndrs)))
@@ -3035,7 +3033,7 @@ tcTKTelescope mode tele thing_inside = case tele of
           ; (inv_tv_bndrs, thing) <- tcExplicitTKBndrsX skol_mode bndrs thing_inside
             -- inv_tv_bndrs :: [VarBndr TyVar Specificity],
             -- but we want [VarBndr TyVar ForAllTyFlag]
-          ; return (tyVarSpecToBinders inv_tv_bndrs, thing) }
+          ; return (Erased, tyVarSpecToBinders inv_tv_bndrs, thing) }
 
   HsForEachVis { hsf_retained_vis_bndrs = bndrs }
     -> do { skol_info <- mkSkolemInfo (ForAllSkol (HsTyVarBndrsRn (unLoc <$> bndrs)))
@@ -3044,7 +3042,7 @@ tcTKTelescope mode tele thing_inside = case tele of
           ; (req_tv_bndrs, thing) <- tcExplicitTKBndrsX skol_mode bndrs thing_inside
             -- req_tv_bndrs :: [VarBndr TyVar ()],
             -- but we want [VarBndr TyVar ForAllTyFlag]
-          ; return (tyVarReqToBinders req_tv_bndrs, thing) }
+          ; return (Retained, tyVarReqToBinders req_tv_bndrs, thing) }
 
   HsForEachInvis { hsf_retained_invis_bndrs = bndrs }
     -> do { skol_info <- mkSkolemInfo (ForAllSkol (HsTyVarBndrsRn (unLoc <$> bndrs)))
@@ -3053,7 +3051,7 @@ tcTKTelescope mode tele thing_inside = case tele of
           ; (inv_tv_bndrs, thing) <- tcExplicitTKBndrsX skol_mode bndrs thing_inside
             -- inv_tv_bndrs :: [VarBndr TyVar Specificity],
             -- but we want [VarBndr TyVar ForAllTyFlag]
-          ; return (tyVarSpecToBinders inv_tv_bndrs, thing) }
+          ; return (Retained, tyVarSpecToBinders inv_tv_bndrs, thing) }
 
 --------------------------------------
 --    HsOuterTyVarBndrs


=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -67,7 +67,7 @@ module GHC.Types.Var (
 
         -- * ForAllTyFlags
         ForAllTyFlag(Invisible,Required,Specified,Inferred),
-        Specificity(..),
+        Specificity(..), Erasure(..),
         isVisibleForAllTyFlag, isInvisibleForAllTyFlag, isInferredForAllTyFlag,
         coreTyLamForAllTyFlag,
 
@@ -472,7 +472,6 @@ data Specificity = InferredSpec
 -- | Whether a dependent argument is erased at runtime
 data Erasure = Erased | Retained
   deriving (Eq, Data)
-  -- XXX JB Erasure flag do we need it?
 
 pattern Inferred, Specified :: ForAllTyFlag
 pattern Inferred  = Invisible InferredSpec



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e8dd284dc334cbb77fa9db21caa8a9491460374

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1e8dd284dc334cbb77fa9db21caa8a9491460374
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/20230730/6b276b5c/attachment-0001.html>


More information about the ghc-commits mailing list