Update specs and internal syntax

Author: natsukagami

docs/_docs/internals/syntax.md

@@ -140,7 +140,7 @@ type      val       var       while     with      yield
 ### Soft keywords
 
 ```
-as  derives  end  extension  infix  inline  opaque  open  throws transparent  using  |  *  +  -
+as  derives  end  erased  extension  infix  inline  opaque  open  throws transparent  using  |  *  +  -
 ```
 
 See the [separate section on soft keywords](../reference/soft-modifier.md) for additional
@@ -180,13 +180,13 @@ Type              ::=  FunType
                     |  FunParamClause ‘=>>’ Type                                TermLambdaTypeTree(ps, t)
                     |  MatchType
                     |  InfixType
-FunType           ::=  FunTypeArgs (‘=>’ | ‘?=>’) Type                          Function(ts, t)
+FunType           ::=  FunTypeArgs (‘=>’ | ‘?=>’) Type                          Function(ts, t) | FunctionWithMods(ts, t, mods, erasedParams)
                     |  HKTypeParamClause '=>' Type                              PolyFunction(ps, t)
 FunTypeArgs       ::=  InfixType
                     |  ‘(’ [ FunArgTypes ] ‘)’
                     |  FunParamClause
 FunParamClause    ::=  ‘(’ TypedFunParam {‘,’ TypedFunParam } ‘)’
-TypedFunParam     ::=  id ‘:’ Type
+TypedFunParam     ::=  [`erased`] id ‘:’ Type
 MatchType         ::=  InfixType `match` <<< TypeCaseClauses >>>
 InfixType         ::=  RefinedType {id [nl] RefinedType}                        InfixOp(t1, op, t2)
 RefinedType       ::=  AnnotType {[nl] Refinement}                              RefinedTypeTree(t, ds)
@@ -207,8 +207,8 @@ Singleton         ::=  SimpleRef
                     |  SimpleLiteral
                     |  Singleton ‘.’ id
 Singletons        ::=  Singleton { ‘,’ Singleton }
-FunArgType        ::=  Type
-                    |  ‘=>’ Type                                                PrefixOp(=>, t)
+FunArgType        ::=  [`erased`] Type
+                    |  [`erased`] ‘=>’ Type                                     PrefixOp(=>, t)
 FunArgTypes       ::=  FunArgType { ‘,’ FunArgType }
 ParamType         ::=  [‘=>’] ParamValueType
 ParamValueType    ::=  [‘into’] ExactParamType                                  Into(t)
@@ -229,7 +229,7 @@ BlockResult       ::=  FunParams (‘=>’ | ‘?=>’) Block
                     |  HkTypeParamClause ‘=>’ Block
                     |  Expr1
 FunParams         ::=  Bindings
-                    |  id
+                    |  [`erased`] id
                     |  ‘_’
 Expr1             ::=  [‘inline’] ‘if’ ‘(’ Expr ‘)’ {nl} Expr [[semi] ‘else’ Expr] If(Parens(cond), thenp, elsep?)
                     |  [‘inline’] ‘if’  Expr ‘then’ Expr [[semi] ‘else’ Expr]    If(cond, thenp, elsep?)
@@ -376,13 +376,13 @@ UsingParamClause  ::=  [nl] ‘(’ ‘using’ (DefTermParams | FunArgTypes) 
 DefImplicitClause ::=  [nl] ‘(’ ‘implicit’ DefTermParams ‘)’
 
 DefTermParams     ::= DefTermParam {‘,’ DefTermParam}
-DefTermParam      ::= {Annotation} [‘inline’] Param                         ValDef(mods, id, tpe, expr) -- point of mods at id.
+DefTermParam      ::= {Annotation} [`erased`] [‘inline’] Param                    ValDef(mods, id, tpe, expr) -- point of mods at id.
 Param             ::=  id ‘:’ ParamType [‘=’ Expr]
 ```
 
 ### Bindings and Imports
 ```ebnf
-Bindings          ::=  ‘(’ [Binding {‘,’ Binding}] ‘)’
+Bindings          ::=  ‘(’[`erased`] [Binding {‘,’ [`erased`] Binding}] ‘)’
 Binding           ::=  (id | ‘_’) [‘:’ Type]                                    ValDef(_, id, tpe, EmptyTree)
 
 Modifier          ::=  LocalModifier

docs/_docs/reference/experimental/erased-defs-spec.md

@@ -19,8 +19,8 @@ TODO: complete
 
     def g(erased x: Int) = ...
 
-    (erased x: Int) => ...
-    def h(x: (erased Int) => Int) = ...
+    (erased x: Int, y: Int) => ...
+    def h(x: (Int, erased Int) => Int) = ...
 
     class K(erased x: Int) { ... }
     erased class E {}
@@ -34,12 +34,12 @@ TODO: complete
 
 3. Functions
    * `(erased x1: T1, x2: T2, ..., xN: TN) => y : (erased T1, T2, ..., TN) => R`
-   * `(given erased x1: T1, x2: T2, ..., xN: TN) => y: (given erased T1, T2, ..., TN) => R`
+   * `(given x1: T1, erased x2: T2, ..., xN: TN) => y: (given T1, erased T2, ..., TN) => R`
    * `(given erased T1) => R  <:<  erased T1 => R`
-   * `(given erased T1, T2) => R  <:< (erased T1, T2) => R`
+   * `(given T1, erased T2) => R  <:< (T1, erased T2) => R`
    *  ...
 
-   Note that there is no subtype relation between `(erased T) => R` and `T => R` (or `(given erased T) => R` and `(given T) => R`)
+   Note that there is no subtype relation between `(erased T) => R` and `T => R` (or `(given erased T) => R` and `(given T) => R`). The `erased` parameters must match exactly in their respective positions.
 
 
 4. Eta expansion
@@ -51,7 +51,8 @@ TODO: complete
    * All `erased` parameters are removed from the function
    * All argument to `erased` parameters are not passed to the function
    * All `erased` definitions are removed
-   * All `(erased T1, T2, ..., TN) => R` and `(given erased T1, T2, ..., TN) => R` become `() => R`
+   * `(erased ET1, erased ET2, T1, ..., erased ETN, TM) => R` are erased to `(T1, ..., TM) => R`.
+   * `(given erased ET1, erased ET2, T1, ..., erased ETN, TM) => R` are erased to `(given T1, ..., TM) => R`.
 
 
 6. Overloading
@@ -60,11 +61,10 @@ TODO: complete
 
 
 7. Overriding
-   * Member definitions overriding each other must both be `erased` or not be `erased`
-   * `def foo(x: T): U` cannot be overridden by `def foo(erased x: T): U` and vice-versa
-   *
-
+   * Member definitions overriding each other must both be `erased` or not be `erased`.
+   * `def foo(x: T): U` cannot be overridden by `def foo(erased x: T): U` and vice-versa.
 
 8. Type Restrictions
    * For dependent functions, `erased` parameters are limited to realizable types, that is, types that are inhabited by non-null values.
      This restriction stops us from using a bad bound introduced by an erased value, which leads to unsoundness (see #4060).
+   * Polymorphic functions with erased parameters are currently not supported, and will be rejected by the compiler. This is purely an implementation restriction, and might be lifted in the future.

docs/_docs/reference/experimental/erased-defs.md

@@ -54,13 +54,13 @@ semantics and they are completely erased.
 ## How to define erased terms?
 
 Parameters of methods and functions can be declared as erased, placing `erased`
-in front of a parameter list (like `given`).
+in front of each erased parameter (like `inline`).
 
 ```scala
-def methodWithErasedEv(erased ev: Ev): Int = 42
+def methodWithErasedEv(erased ev: Ev, x: Int): Int = x + 2
 
-val lambdaWithErasedEv: erased Ev => Int =
-  (erased ev: Ev) => 42
+val lambdaWithErasedEv: (erased Ev, Int) => Int =
+  (erased ev, x) => x + 2
 ```
 
 `erased` parameters will not be usable for computations, though they can be used
@@ -80,7 +80,7 @@ parameters.
 
 ```scala
 erased val erasedEvidence: Ev = ...
-methodWithErasedEv(erasedEvidence)
+methodWithErasedEv(erasedEvidence, 40) // 42
 ```
 
 ## What happens with erased values at runtime?
@@ -89,15 +89,15 @@ As `erased` are guaranteed not to be used in computations, they can and will be
 erased.
 
 ```scala
-// becomes def methodWithErasedEv(): Int at runtime
-def methodWithErasedEv(erased ev: Ev): Int = ...
+// becomes def methodWithErasedEv(x: Int): Int at runtime
+def methodWithErasedEv(x: Int, erased ev: Ev): Int = ...
 
 def evidence1: Ev = ...
 erased def erasedEvidence2: Ev = ... // does not exist at runtime
 erased val erasedEvidence3: Ev = ... // does not exist at runtime
 
-// evidence1 is not evaluated and no value is passed to methodWithErasedEv
-methodWithErasedEv(evidence1)
+// evidence1 is not evaluated and only `x` is passed to methodWithErasedEv
+methodWithErasedEv(x, evidence1)
 ```
 
 ## State machine with erased evidence example