[Git][ghc/ghc][wip/int-index/emb-type] Some edit to the Note

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/int-index/emb-type at Glasgow Haskell Compiler / GHC


Commits:
52f16a58 by Simon Peyton Jones at 2023-07-21T13:48:23+01:00
Some edit to the Note

done in a call with Vlad

- - - - -


1 changed file:

- compiler/GHC/Tc/Gen/App.hs


Changes:

=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -892,8 +892,9 @@ evolved over time, and is based on the following papers and proposals:
   - "Visible forall in types of terms"
     https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst
 
-The proposals have not been fully implemented at the time of writing this Note,
-so we offer an overview of the design mixed with commentary on the implementation status.
+Here we offer an overview of the design mixed with commentary on the
+implementation status.  The proposals have not been fully implemented at the
+time of writing this Note (see "non implemented" in the rest of this Note).
 
 Now consider functions
     fi :: forall {a}. a -> t     -- Inferred:  type argument cannot be supplied
@@ -939,26 +940,27 @@ The moving parts are as follows:
 Syntax of types
 ---------------
 * The types are all initially represented with HsForAllTy (c.o. HsType).
+  The binders are in the (hst_tele :: HsForAllTelescope pass) field of the HsForAllTy
   At this stage, we have
       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)
 
-* By the time we get to checking applications/abstractions,
-  the types have been desugared into ForAllTy (c.o. Type).
+* By the time we get to checking applications/abstractions (e.g. GHC.Tc.Gen.App)
+  the types have been kind-checked (e.g. by tcHsType) into ForAllTy (c.o. Type).
   At this stage, we have:
       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)
 
-Syntax of applications
-----------------------
-* Type applications are represented with the following constructors
-      f True     -- HsApp      (c.o. HsExpr, plain function application)
-      f @True    -- HsAppType  (c.o. HsExpr, function application with `@`)
-      type True  -- HsEmbTy    (c.o. HsExpr, embed a type into an expression with `type`)
+Syntax of applications in HsExpr
+--------------------------------
+* We represent applications like this (ignoring parameterisation)
+    data HsExpr = HsApp HsExpr HsExpr    -- (f True)  plain function application)
+                | HsTyApp HsExpr HsType  -- (f @True) function application with `@`)
+                | HsEmbType HsType       -- (type ty) embed a type into an expression with `type`)
 
-* The HsAppType constructor is only used with Specified type variables
+* The HsAppType constructor is only used for Specified type variables
       f @True         -- only valid for f :: forall a. t
 
 * The HsApp constructor without HsEmbTy is used with ordinary function application
@@ -976,9 +978,17 @@ Syntax of applications
       g (Either (type Int) (type Bool))  -- valid for g :: forall (a :: Type) -> t     (NB. not implemented)
 
   This nesting makes `type` rather different from `@`.
+  The HsEmbTy mainly just switches name-space, and affects the term-to-type transformation.
+
+Syntax of abstractions in Pat
+-----------------------------
+similary...
+
+
+data HsPat = ConPat [HsTyPat] [HsPat]
+
+           | EmbPat HsTyPat
 
-Syntax of abstractions
-----------------------
 * Type abstractions are represented with the following constructors
       \ (MkT @a  (x :: a)) -> rhs    -- ConPat (c.o. Pat) and HsConPatTyArg (c.o. HsConPatTyArg)
       \ (type a) (x :: a)  -> rhs    -- EmbTyPat (c.o. Pat)
@@ -994,6 +1004,8 @@ Syntax of abstractions
       \ (P @(a -> Either b c)) -> rhs
   All these forms are represented with HsTP (c.o. HsTyPat).
 
+
+
 Renaming type applications
 --------------------------
 rnExpr delegates renaming of type arguments to rnHsWcType if possible:



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/52f16a585c2ba651aa663430464816ad47d4abc0

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/52f16a585c2ba651aa663430464816ad47d4abc0
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/20230721/7e6d2a13/attachment-0001.html>