diff --git a/_sips/sips/2014-06-27-42.type.md b/_sips/sips/2014-06-27-42.type.md
index e03c3a97c1..f39232f7ba 100644
--- a/_sips/sips/2014-06-27-42.type.md
+++ b/_sips/sips/2014-06-27-42.type.md
@@ -7,7 +7,10 @@ vote-status: pending
permalink: /sips/:title.html
---
-**By: George Leontiev, Eugene Burmako, Jason Zaugg, Adriaan Moors, Paul Phillips, Oron Port**
+**Authors: George Leontiev, Eugene Burmako, Jason Zaugg, Adriaan Moors, Paul Phillips, Oron Port, Miles
+Sabin**
+
+**Supervisor and advisor: Adriaan Moors**
## History
@@ -17,294 +20,665 @@ permalink: /sips/:title.html
| Jul 15th 2014 | Last update to SIP before declared dormant |
| TBD | Dormant because original authors are not available for its review |
| Feb 9th 2017 | New author volunteered to update the SIP for review |
-
-### Current status
-Literal types were implemented in both Typelevel Scala and Dotty.
-SIP pending for committee review.
-
----
-
-Champion: Adriaan Moors
-
-## Motivation
-
-Singleton types bridge the gap between the value level and the type level and hence allow the exploration in Scala of techniques which would typically only be available in languages with support for full-spectrum dependent types.
-
-Scala's type system can model constants (e.g. `42`, `"foo"`, `classOf[String]`). These are inferred in cases like `object O { final val x = 42 }`. They are used to denote and propagate compile time constants (See [6.24 Constant Expressions](http://www.scala-lang.org/files/archive/spec/2.11/06-expressions.html) and discussion of "constant value definition" in [4.1 Value Declarations and Definitions](http://www.scala-lang.org/files/archive/spec/2.11/04-basic-declarations-and-definitions.html)). However, there is no surface syntax to express such types. This makes people who need them, create macros that would provide workarounds to do just that (e.g. [shapeless](https://github.com/milessabin/shapeless/blob/master/core/src/main/scala/shapeless/singletons.scala)). This can be changed in a relatively simple way, as the whole machinery to enable this is already present in the scala compiler.
-
-Another motivation for adding this functionality is the fact that it is already partially available in scala, but the way it is available makes interaction with this feature a bit inconsistent. Here’s what is possible in the current version of scala:
-
- scala> val t = "test"
- t: String = test
-
- scala> val r: t.type = t
- r: t.type = test
-
-But:
-
- scala> val r: "test".type = "test"
- :1: error: identifier expected but string literal found.
- val r: "test".type = "test"
- ^
-
-And:
-
- scala> val r: 42.type = 42
- :1: error: identifier expected but integer literal found.
- val r: 42.type = 42
- ^
-
-Or even:
-
- scala> val t = 42
- t: Int = 42
-
- scala> val r: t.type = t
- :8: error: type mismatch;
- found : t.type (with underlying type Int)
- required: AnyRef
- val r: t.type = t
- ^
-
-This looks like an inconsistency, which should be fixed. The proposed change fixes exactly that:
-
- scala> val r: "test".type = "test"
- r: "test".type = test
-
- scala> val r: 42.type = 42
- r: 42.type = 42
-
-or even:
-
- scala> val r: 42 = 42
- r: 42.type = 42
-
- scala> val t = 42
- t: Int = 42
-
- scala> val r: t.type = t
- r: t.type = 42
-
-To summarize, scala has full support for literal-based singleton types, but language user has very limited possibilities for creating and using them. Two possible ways currently are asking the compiler to infer the singleton type by marking value as `final`, or use `.type` syntax, which is only available for stable identifiers pointing to values that conform to `AnyRef`.
-
-## Prerequisites
-
-### Any vs AnyRef
-
-Currently there is a possibility to use singleton types in some contexts, but only on identifiers which point to a constant that conforms to `AnyRef`. This restriction is due to `Any` not having an `eq` method, which is what’s used for singleton type-equality check and pattern matching [https://github.com/scala/scala/pull/3558](https://github.com/scala/scala/pull/3558). This has been discussed on the mailing list [here](https://groups.google.com/forum/#!msg/scala-internals/12h2TgDFnDM/Sq-EYi7VD7IJ) and [here](https://groups.google.com/forum/#!msg/scala-internals/jsVlJI4H5OQ/BwdZT5hpKtsJ), and there is a consent that this needs to be done.
-
-### Inhabitants of the type
-
-Getting the inhabitant of a singleton type, as described by [Travis Brown](http://meta.plasm.us/posts/2013/06/28/singleton-types-for-literals-in-scala/), can be done with a macro, which is a part of the [proposed implementation](https://github.com/folone/scala/commit/094883efb4d1c50981cea41f049c3930c8efbc3c).
-
-**Note:** This is one of the many parts of this SIP that are in flux, and are likely to change in the future. We might not need to generate instances of `SingleInhabitant` typeclass, but instead only use `<: Singleton` type bound for this. See [SI-5103](https://issues.scala-lang.org/browse/SI-5103). The name is also likely to change to `valueOf[T]`.
-
-## Possible use cases
-
-There are quite a few use cases we’ve collected on the [mailing list](https://groups.google.com/forum/#!topic/scala-language/9VEnFZImyJI). Some of them are as follows.
-
-### Spire
-
-Singleton types will be useful for defining a type like `Residue[13.type]` (Z/13Z, the group of integers modulo 13). We could then mandate that residues can be added only when they are parameterized on the same number. Possibly something like:
-
- case class Residue[N <: Int : SingleInhabitant](n: Long) { lhs =>
- def +(rhs: Residue[N]): Residue[N] =
- Residue((lhs.n + rhs.n) % inhabitant[N])
- }
-
-Another use is to help with property based testing. In Spire, there is a Ranged type that makes it easy to ask for numbers in a particular range in ScalaCheck:
-
- forAll { x: Ranged[Int, 1, 100] =>
- val n: Int = x.value // guaranteed to be 1 to 100
- }
-
-Currently Spire just builds some of the most common number literals and uses boilerplate to define the end points of `Ranged`. But this is another place where singleton types could really help make things clear. Here’s what `Ranged` could look like:
-
- class Ranged[From <: Int : SingleInhabitant, To <: Int : SingleInhabitant] {
- def value = {
- val rnd = new scala.util.Random
- val from = inhabitant[From]
- val to = inhabitant[To]
- (from + rnd.nextInt(to - from + 1))
- }
- }
-
-There is also all kinds of length/dimension checking and other standard cases where singleton types will help.
-
-### Scala.js
-
-There is an important use case for literal-based singleton types in Scala.js. In particular for Strings: declaring several overloads of a method that differ only in the actual strings in parameters, for example:
-
- trait HTMLCanvasElement extends HTMLElement {
- def getContext(contextId: String): Any
- def getContext(contextId: "2d".type): CanvasRenderingContext2D
- }
-
-so that at call-site:
-
- val anyContext = canvas.getContext("webgl")
- val context2D = canvas.getConttext("2d")
-
-`anyContext` is an `Any` but `context2D` is statically known to be a `CanvasRenderingContext2D`.
-
-Note: The way this currently works:
-
- scala> :t canvas.getContext("webgl")
- Any
-
- scala> :t canvas.getContext("2d")
- Any
-
-But
-
- scala> :t canvas.getContext("2d": "2d".type)
- CanvasRenderingContext2D
-
-### Shapeless
-
-[Shapeless](https://github.com/milessabin/shapeless/) is a project that makes heavy use of singleton types already. It has all the machinery in place to make working with them nicer. Hence, it is a source of inspiration for working on this SIP. This change does not bring much to the table for shapeless though. One of the useful cases would be an ability to explicitly specify types for e.g. records in a more convenient way than possible with the current version of scala:
-
- val book: "author" ->> String ::
- "title" ->> String ::
- "id" ->> Int ::
- "price" ->> Double :: HNil =
- ("author" ->> "Benjamin Pierce") ::
- ("title" ->> "Types and Programming Languages") ::
- ("id" ->> 262162091) ::
- ("price" ->> 44.11) ::
- HNil
-
-### Others
-
-Quite a few other projects find this feature relevant for more efficient work on the tasks they are solving: Slick, Spark, Scala RX, Scalding, Breeze.
+| Nov 16th 2017 | Updated following implementation experience in Typelevel Scala |
+
+## Introduction
+
+Singleton types, types which have a unique inhabitant, have been a fundamental component of Scala's
+semantics dating back to the earliest published work on its type system. They are ubiquitous in
+ordinary Scala code, typically as the types of Scala object definitions understood as modules, where
+their role is to give the meaning of paths selecting types and terms from nested values. Selector
+paths have an intuitive meaning to programmers from a wide range of backgrounds which belies their
+underpinning by a somewhat "advanced" concept in type theory.
+
+Nevertheless, by pairing a type with it's unique inhabitant, singleton types bridge the gap between
+types and values, and their presence in Scala has over the years allowed Scala programmers to explore
+techniques which would typically only be available in languages, such as Agda or Idris, with support
+for full-spectrum dependent types.
+
+Scala's semantics have up until now been richer than its syntax. The only singleton types which are
+currently _directly_ expressible are those of the form `p.type` where `p` is a path pointing to a
+value of some subtype of `AnyRef`. Interally the Scala compiler also represents singleton types for
+individual values of subtypes of `AnyVal`, such as `Int` or values of type `String` which don't
+correspond to paths. These types are inferred in some circumstances, notably as the types of `final`
+vals. Their primary purpose has been to represent compile time constants (see [6.24 Constant
+Expressions](http://scala-lang.org/files/archive/spec/2.12/06-expressions.html#constant-expressions)
+and the discussion of "constant value definitions" in [4.1 Value Declarations and
+Definitions](http://scala-lang.org/files/archive/spec/2.12/04-basic-declarations-and-definitions.html#value-declarations-and-definitions)).
+The types here correspond to _literal_ values (ie. values which programmers can directly write as
+terms, see [1.3
+Literals](http://scala-lang.org/files/archive/spec/2.12/01-lexical-syntax.html#literals)) such as
+`23`, `true` or `"foo"` of the larger non-singleton types they inhabit (`Int`, `Boolean` or `String`
+respectively). However, there is no suface syntax to express these types.
+
+As we will see in the motivation section of the proposal below, singleton types corresponding to
+literal values (henceforth _literal types_) have many important uses and are already widely used in
+many important Scala libraries. The lack of first class syntax for literal types has forced library
+authors to use the experimental Scala macro system to provide a means to express them. Whilst this
+has proved to be extremely successful, it has poor ergonimics (although this can typically be hidden
+from library _users_) and is not portable -- because Scala macros in general and the mechanisms used
+to expose literal types to Scala programmes in particular depend on internal implementation details
+of the current Scala compiler.
+
+The poor ergonomics of macro-based exposure of literal types was the original motivation for this
+SIP. The development of Dotty and other Scala dialects since then has made the portability issue
+more urgent.
+
+### Implementation status
+
+Literal types have been implemented in both [Typelevel Scala](https://github.com/typelevel/scala)
+and [Dotty](http://dotty.epfl.ch/).
+
+There has been a great deal of useful experience with the Typelevel Scala implementation in
+[a variety of projects](https://github.com/search?p=1&q=-Yliteral-types&type=Code) which has
+resulted in several improvements which are incorporated in the latest iteration of this document. A
+full implementation of this proposal exists as a pull request relative to the 2.13.x branch of the
+Lightbend Scala compiler.
## Proposal
-This document proposes to extend an existing very limited syntax for singleton types to a more general one. That is, possibility to use syntax for singleton types, as well as raw literals, in any type position. Here are several examples (taken from the [tests](https://github.com/folone/scala/blob/topic/42.type/test/files/run/42.type.scala)):
-
-### Simple examples:
-
- type _42 = 42.type
- type Unt = ().type
- type _1 = 1 // .type is optional for literals
- final val x = 1
- type one = x.type // … but mandatory for identifiers
-
-This is not allowed for the reason that we will have problems bootstrapping this
-
- scala> type _2 = (1+1).type
- :1: error: '.' expected but identifier found.
- type _2 = (1+1).type
- ^
-
-### Using it with vars:
-
- scala> var x: 3.type = 3
-
- scala> x = 42
- :8: error: type mismatch;
- found : 42.type (with underlying type Int)
- required: 3.type
- x = 42
- ^
-
-### Pattern-matching
-
- val y: 5 = 5
-
- def g(x: Int) = x match {
- case _: y.type => 0
- case _: 7.type => 1
- case _ => 2
- }
-
-### Etc.
-
- trait Succ[T] {
- type Out
- def apply(x: T): Out
- }
-
- implicit object One extends Succ[1.type] {
- type Out = 2.type
- def apply(x: 1.type) = 2
- }
-
- def f[T](x: T)(implicit succ: Succ[T]) = succ(x)
-
- def main(args: Array[String]): Unit = {
- println(f(1))
- // println(f(5))
- println((g(1), g(5), g(7)))
- }
-
-## Formalization
-
-The proposed change is essentially as follows (adding on the [language reference](http://iainmcgin.github.io/scala-ref-markdown/ScalaReference.html#scala-syntax-summary)):
-
- SimpleType ::= SimpleType TypeArgs
- | SimpleType ‘#’ id
- | StableId
- | Path ‘.’ ‘type’
- | Literal [‘.’ type]
- | ‘(’ Types ‘)’
-
-A singleton type is of the form `p.type`, where `p` is a path pointing to a value. Or `literal[.type]` (in this case `.type` is optional, because when using a literal we always know if we are in a type- or term-parsing mode). The type denotes set of values consisting of a single value denoted by path `p`, or a `literal`.
-
-## Implementation
-
-The singleton type part (not including `eq` on `Any`) is implemented on [github](https://github.com/folone/scala/tree/topic/42.type). There are currently several outstanding issues that need to be looked into. Namely, `ConstantType` folding and inlining of functions with singleton type result.
-
-The places where those issues might present themselves are marked with `TODO (folone)`, and can be found like this:
-
- $ ack “TODO \(folone\)” src/
-
-Other places where `ConstantType` is used can be found like this:
-
- $ grep -r --include="*.scala" "ConstantType" src/
-
-## Some details on the optionality of .type
-
-While discussing this document, the agreement was that we should keep the mandatory `.type` for identifiers, to avoid situations described by Adriaan Moors:
-
- type T = Int
- final val T = 1
- val x: T = 2 // Which T is this: T, or T.type?
-
-but make it optional for literals, e.g. both `42.type` and `42` in type position are valid.
-
-This change is implemented in the branch, and needs a careful update of all the failed check files (partest can do that automatically: `partest --update-check`).
-
-## Dependencies on other SIPs
-
-This project needs an `eq` method on `Any`.
-
-## Related open tickets
-
-* [https://issues.scala-lang.org/browse/SI-8323](https://issues.scala-lang.org/browse/SI-8323)
-* [https://issues.scala-lang.org/browse/SI-8564](https://issues.scala-lang.org/browse/SI-8564)
-* [https://issues.scala-lang.org/browse/SI-7656](https://issues.scala-lang.org/browse/SI-7656)
-* [https://issues.scala-lang.org/browse/SI-5103](https://issues.scala-lang.org/browse/SI-5103)
-
-## Weird behaviour collected so far
-
-### Inlining of functions
-
- scala> def test: 7.type = {
- | println("PANDA!")
- | 7
- | }
- test: 7.type
-
- scala> test
- res0: 7.type = 7
-
-[Suspected culprit](https://github.com/folone/scala/blob/topic/42.type/src/compiler/scala/tools/nsc/transform/Constructors.scala#L643-L644)
-
-Can hopefully be fixed by verifying that the body is pure (by means of SI-7656) before inlining it.
-
-## Useful links
+### Proposal summary
+
++ Literals can now appear in type position, designating the corresponding singleton type.
+ ```
+ val one: 1 = 1 // val declaration
+ def foo(x: 1): Option[1] = Some(x) // param type, type arg
+ def bar[T <: 1](t: T): T = t // type parameter bound
+ foo(1: 1) // type ascription
+ ```
+
++ The `.type` singleton type forming operator can be applied to values of all subtypes of `Any`.
+ ```
+ def foo[T](t: T): t.type = t
+ foo(23) // result is 23: 23
+ ```
+
++ The presence of an upper bound of `Singleton` on a formal type parameter indicates that
+ singleton types should be inferred for type parameters at call sites.
+ ```
+ def wide[T](t: T): T = t
+ wide(13) // result is 13: Int
+ def narrow[T <: Singleton](t: T): T = t
+ narrow(23) // result is 23: 23
+ ```
+
++ Pattern matching against literal types and `isInstanceOf`/`asInstanceOf` tests/conversions are
+ implemented via equality/identity tests of the corresponding values.
+ ```
+ (1: Any) match {
+ case one: 1 => true
+ case _ => false
+ } // result is true
+ (1: Any).isInstanceOf[1] // result is true
+ (1: Any).asInstanceOf[1] // result is 1: 1
+ (1: Any).asInstanceOf[2] // ClassCastException
+ ```
+
++ A `scala.ValueOf[T]` type class and corresponding `scala.Predef.valueOf[T]` operator has been
+ added yielding the unique value of types with a single inhabitant.
+ ```
+ def foo[T](implicit v: ValueOf[T]): T = v.value
+ foo[13] // result is 13: 13
+ ```
+
++ Support for `scala.Symbol` literal types has been added.
+ ```
+ valueOf['foo] // result is 'foo: 'foo
+ ```
+
+### Motivating examples
+
+Many of the examples below use primitives provided by the Scala generic programming library
+[shapeless](https://github.com/milessabin/shapeless/). It provides a `Witness` type class and a
+family of Scala macro based methods and conversions for working with singleton types and shifting
+from the value to the type level and vice versa. One of the goals of this SIP is to enable Scala
+programmers to achieve similar results without having to rely on a third party library or fragile
+and non-portable macros.
+
+The relevant parts of shapeless are excerpted in [Appendix 1](#appendix-1--shapeless-excerpts).
+Given the definitions there, some of forms summarized above can be expressed in current Scala,
+```
+val wOne = Witness(1)
+val one: wOne.T = wOne.value // wOne.T is the type 1
+ // wOne.value is 1: 1
+
+def foo[T](implicit w: Witness[T]): w.T = w.value
+foo[wOne.T] // result is 1: 1
+
+"foo" ->> 23 // shapeless record field constructor
+ // result type is FieldType["foo", Int]
+```
+The syntax is awkward and hiding it from library users is challenging. Nevertheless they enable many
+constructs which have proven valuable in practice.
+
+#### shapeless records
+
+shapeless models records as HLists (essentially nested pairs) of record values with their types
+tagged with the singleton types of their keys. The library provides user friendly mechanisms for
+constructing record _values_, however it is extremely laborious to express the corresponding _types_.
+Consider the following record value,
+```
+val book =
+ ("author" ->> "Benjamin Pierce") ::
+ ("title" ->> "Types and Programming Languages") ::
+ ("id" ->> 262162091) ::
+ ("price" ->> 44.11) ::
+ HNil
+```
+
+Using shapeless and current Scala the following would be required to give `book` an explicit type
+annotation,
+```
+val wAuthor = Witness("author")
+val wTitle = Witness("title")
+val wId = Witness("id")
+val wPrice = Witness("price")
+type Book =
+ (wAuthor.T ->> String) ::
+ (wTitle.T ->> String) ::
+ (wId.T ->> Int) ::
+ (wPrice.T ->> Double) ::
+ HNil
+
+val book: Book =
+ ("author" ->> "Benjamin Pierce") ::
+ ("title" ->> "Types and Programming Languages") ::
+ ("id" ->> 262162091) ::
+ ("price" ->> 44.11) ::
+ HNil
+```
+Notice that here the `val` definitions are essential -- they are needed to create the stable path
+required for selection of the member types `T`.
+
+Under this proposal we can express the record type directly,
+```
+type Book =
+ ("author" ->> String) ::
+ ("title" ->> String) ::
+ ("id" ->> Int) ::
+ ("price" ->> Double) ::
+ HNil
+
+val book: Book =
+ ("author" ->> "Benjamin Pierce") ::
+ ("title" ->> "Types and Programming Languages") ::
+ ("id" ->> 262162091) ::
+ ("price" ->> 44.11) ::
+ HNil
+```
+
+shapeless enables generic programming and type class derivation by providing a mechanism for mapping
+a value of a standard Scala algebraic data type onto a sum of products representation type,
+essentially nested labelled `Either`'s of the records discussed above. Techniques of this sort are
+widely used, and removing the incidental complexity that comes with encoding via macros will improve
+the experience for many users across a wide variety of domains.
+
+#### refined and singleton-ops
+
+[refined](https://github.com/fthomas/refined) and
+[singleton-ops](https://github.com/fthomas/singleton-ops) are two libraries which build on
+shapeless's `Witness` to support refinement types for Scala. A refinement is a type-level predictate
+which constrains a set of values relative to some base type, for example, the type of integers
+greater thar 5.
+
+refined allows such types to be expressed in Scala using shapeless's `Witness`,
+```
+val w5 = Witness(5)
+val a: Int Refined Greater[w5.T] = 10
+
+// Since every value greater than 5 is also greater than 4,
+// `a` can be ascribed the type Int Refined Greater[w4.T]:
+val w4 = Witness(4)
+val b: Int Refined Greater[w4.T] = a
+
+// An unsound ascription leads to a compile error:
+val w6 = Witness(6)
+val c: Int Refined Greater[w6.T] = a
+
+//:23: error: type mismatch (invalid inference):
+// Greater[Int(5)] does not imply
+// Greater[Int(6)]
+// val c: Int Refined Greater[W.`6`.T] = a
+ ^
+```
+
+Under this proposal we can express these refinements much more succinctly,
+```
+val a: Int Refined Greater[5] = 10
+
+val b: Int Refined Greater[4] = a
+```
+
+Type level predicates of this kind have proved to be useful in practice and are supported by modules
+of a [number of important libraries](https://github.com/fthomas/refined#external-modules).
+
+Experience with those libraries has led to a desire to compute directly over singleton types, in
+effect to lift whole term-level expressions to the type-level which has resulted in the development
+of the [singleton-ops](https://github.com/fthomas/singleton-ops) library. singleton-ops is built
+with Typelevel Scala which allows it to use literal types as discussed in this SIP.
+
+```
+import singleton.ops._
+
+class MyVec[L] {
+ def doubleSize = new MyVec[2 * L]
+ def nSize[N] = new MyVec[N * L]
+ def getLength(implicit length : SafeInt[L]) : Int = length
+}
+object MyVec {
+ implicit def apply[L]
+ (implicit check : Require[L > 0]) : MyVec[L] =
+ new MyVec[L]()
+}
+val myVec : MyVec[10] = MyVec[4 + 1].doubleSize
+val myBadVec = MyVec[-1] //fails compilation, as required
+```
+
+singleton-ops is used by a number of libraries, most notably our next motivating example, Libra.
+
+#### Libra
+
+[Libra](https://github.com/to-ithaca/libra) is a a dimensional analysis library based on shapeless,
+spire and singleton-ops. It support SI units at the type level for all numeric types. Like
+singleton-ops Libra is built using Typelevel Scala and so is able to use literal types as discussed
+in this SIP.
+
+Libra allows numeric computations to be checked for dimensional correctness as follows,
+```
+import spire.implicits._
+// import spire.implicits._
+
+import libra._, libra.si._
+// import libra._
+// import libra.si._
+
+(3.m + 2.m).show
+// res0: String = 5 m [L]
+
+(3.m * 2.m).show
+// res1: String = 6 m^2 [L^2]
+
+(1.0.km.to[Metre] + 2.0.m + 3.0.mm.to[Metre]).show
+// res2: String = 1002.003 m [L]
+
+(3.0.s.to[Millisecond] / 3.0.ms).show
+// res3: String = 1000.0 []
+
+3.m + 2.kg //this should fail
+// :22: error: These quantities can't be added!
+// 3.m + 2.kg //this should fail
+// ^
+```
+
+#### Spire
+
+The Scala numeric library [Spire](https://github.com/non/spire) provides us with another example
+where it is useful to be able to use literal types as a constraint.
+
+Spire has an open issue to add a `Residue` type to model modular arithmetic. An implementation might
+look something like this,
+
+```
+case class Residue[M <: Int](n: Int) extends AnyVal {
+ def +(rhs: Residue[M])(implicit m: ValueOf[M]): Residue[M] =
+ Residue((this.n + rhs.n) % valueOf[M])
+}
+```
+
+Given this definition we can work with modular numbers without any danger of mixing numbers with
+different modulii,
+
+```
+val fiveModTen = Residue[10](5)
+val nineModTen = Residue[10](9)
+
+fiveModTen + nineModTen // OK == Residue[10](4)
+
+val fourModEleven = Residue[11](4)
+
+fiveModTen + fourModEleven
+// compiler error: type mismatch;
+// found : Residue[11]
+// required: Residue[10]
+```
+
+Also note that the use of `ValueOf` as an implicit argument of `+` means that the modulus does not
+need to be stored along with the `Int` in the `Residue` value which could be beneficial in
+applications which work with large datasets.
+
+### Proposal details
+
++ Literals can now appear in type position, designating the corresponding singleton type. The
+ [`SimpleType`](http://scala-lang.org/files/archive/spec/2.12/03-types.html) production is extended
+ to include syntactic literals.
+
+ ```
+ SimpleType ::= SimpleType TypeArgs
+ | SimpleType ‘#’ id
+ | StableId
+ | Path ‘.’ ‘type’
+ | Literal
+ | ‘(’ Types ‘)’
+ ```
+
+ Examples,
+ ```
+ val one: 1 = 1 // val declaration
+ def foo(x: 1): Option[1] = Some(x) // param type, type arg
+ def bar[T <: 1](t: T): T = t // type parameter bound
+ foo(1: 1) // type ascription
+ ```
+
++ The restriction that the singleton type forming operator `.type` can only be appended to
+ stable paths designating a value which conforms to `AnyRef` is dropped -- the path may now conform
+ to `Any`. Section
+ [3.2.1](http://scala-lang.org/files/archive/spec/2.12/03-types.html#singleton-types) of the SLS is
+ updated as follows,
+
+ > **Singleton Types**
+ >
+ > ```ebnf
+ > SimpleType ::= Path ‘.’ ‘type’
+ > ```
+ >
+ > A **singleton type** is of the form `p.type`. Where `p` is a path pointing to a value which
+ > conforms to `scala.AnyRef`, the type denotes the set of values consisting of `null` and the value
+ > denoted by `p` (i.e., the value `v` for which `v eq p`). Where the path does not conform to
+ > `scala.AnyRef` the type denotes the set consisting of only the value denoted by `p`.
+
+ Example,
+ ```
+ def foo[T](t: T): t.type = t
+ foo(23) // result is 23: 23
+ ```
+
++ The presence of an upper bound of `Singleton` on a formal type parameter indicates that
+ singleton types should be inferred for type parameters at call sites.
+
+ This SIP aims to leave the meaning of all currently valid programmes unchanged, which entails that
+ it must not alter type inference in currently valid programmes. Current Scala will generally widen
+ the types of literal values from their singleton type to their natural non-singleton type when
+ they occur in expressions. For example in,
+
+ ```
+ val foo = 23
+ def id[T](t: T): T = t
+ id(23)
+ ```
+
+ we expect the inferred type of `foo` and the actual type parameter inferred for `T` in the
+ application of `id` to both be `Int` rather than `23`. This behaviour seems to be natural and
+ appropriate in circumstances where the programmer is not deliberately working with singleton
+ types.
+
+ With the introduction of literal types, however, we do want to be able to infer singleton types in
+ cases such as these,
+
+ ```
+ case class Show[T](val s: String)
+ object Show {
+ implicit val showTrue: Show[true] = Show[true]("yes")
+ implicit val showFalse: Show[false] = Show[false]("no")
+ }
+
+ def show[T](t: T)(implicit st: Show[T]): String = st.s
+ show(true) // currently rejected
+ ```
+
+ The proposal in this SIP is that we use an upper bound of `Singleton` on a formal type parameter
+ to indicate that a singleton type should be inferred. The above example would then be written
+ as,
+
+ ```
+ def show[T <: Singleton](t: T)
+ (implicit st: Show[T]): String = st.s
+ show(true) // compiles and yields "yes"
+ ```
+
+ This change will not affect the meaning of currently valid programmes, because the widened types
+ inferred for literal values at call sites do not currently conform to `Singleton`, hence all call
+ sites of the form in the above example would currently be rejected as invalid.
+
+ Whilst type inference in Scala is not fully specified, section [6.26.4 Local Type
+ Inference](http://scala-lang.org/files/archive/spec/2.12/06-expressions.html#local-type-inference)
+ contains language which explicitly excludes the inference of singleton types (see cases 2 and 3,
+ "None of the inferred types Ti is a singleton type"). This does not match the current Scala or
+ Dotty compiler implementations, where singleton types are inferred where a definition is final,
+ specifically non-lazy final val definitions and object definitions. Where a definition has had a
+ singleton type inferred for it, singleton types will be inferred from its uses,
+
+ ```
+ final val narrow = 23 // inferred type of narrow: 23
+
+ class Widen
+ object Narrow extends Wide
+ def id[T](t: T): T = t
+ id(Narrow) // result is Narrow: Narrow.type
+ ```
+
+ This SIP updates the specification to match the current implementation and then adds the further
+ refinement that an explict upper bound of `Singleton` indicates that a singleton type should be
+ inferred.
+
+ Given,
+
+ > A **singleton-apt** definition is
+ > 1. An object definition, or
+ > 2. A non-lazy final val definition
+
+ the relevant clauses of 6.26.4 are revised as follows,
+
+ > None of the inferred types Ti is a singleton type unless, (1) Ti is a singleton type
+ > corresponding to a singleton-apt definition, or (2) The upper bound Ui of Ti conforms to
+ > `Singleton`.
+
+ Example,
+ ```
+ def wide[T](t: T): T = t
+ wide(13) // result is 13: Int
+ def narrow[T <: Singleton](t: T): T = t
+ narrow(23) // result is 23: 23
+ ```
+
++ A `scala.ValueOf[T]` type class and corresponding `scala.Predef.valueOf[T]` operator has been
+ added yielding the unique value of types with a single inhabitant.
+
+ Type inference allows us to infer a singleton type from a literal value. It is natural to want to
+ be able to go in the other direction and infer a value from a singleton type. This latter
+ capability was exploited in the motivating `Residue` example given earlier, and is widely relied
+ on in current Scala in uses of shapeless's records, and `LabelledGeneric` based type class
+ derivation.
+
+ Implicit resolution is Scala's mechanism for inferring values from types and in current Scala
+ shapeless provides a macro-based materialier for instances of its `Witness` type class. This SIP
+ adds a directly compiler supported type class as a replacement,
+
+ ```
+ final class ValueOf[T](val value: T) extends AnyVal
+ ```
+
+ Instances are automatically provided for all types with a single inhabitant, which includes
+ literal and non-literal singleton types and `Unit`.
+
+ Example,
+ ```
+ def foo[T](implicit v: ValueOf[T]): T = v.value
+ foo[13] // result is 13: 13
+ ```
+
+ A method `valueOf` is also added to `scala.Predef` analogously to existing operators such as
+ `classOf`, `typeOf` etc.
+
+ ```
+ def valueOf[T](implicit vt: ValueOf[T]): T = vt.value
+ ```
+
+ Example,
+ ```
+ object Foo
+ valueOf[Foo.type] // result is Foo: Foo.type
+
+ valueOf[23] // result is 23: 23
+ ```
+
++ Pattern matching against literal types and `isInstanceOf`/`asInstanceOf` tests/conversions are
+ implemented via equality/identity tests of the corresponding values.
+
+ Pattern matching against typed patterns (see [8.1.2 Typed
+ Patterns](http://scala-lang.org/files/archive/spec/2.12/08-pattern-matching.html#typed-patterns))
+ where the `TypePat` is a literal type is translated as a match against the subsuming non-singleton
+ type followed by an equality test with the value corresponding to the literal type.
+
+ Where applied to literal types `isInstanceOf` and `asInstanceOf` are translated to a test against
+ the subsuming non-singleton type and an equality test with the value corresponding to the literal
+ type. In the case of `asInstanceOf` a `ClassCastException` is thrown if the test fails.
+
+ Examples,
+ ```
+ (1: Any) match {
+ case one: 1 => true
+ case _ => false
+ } // result is true
+ (1: Any).isInstanceOf[1] // result is true
+ (1: Any).asInstanceOf[1] // result is 1: 1
+ (1: Any).asInstanceOf[2] // ClassCastException
+ ```
+
++ Default initialization for vars with literal types is forbidden.
+
+ The default initializer for a var is already mandated to be it's natural zero element (`0`,
+ `false`, `null` etc.). This is inconsistent with the var being given a non-zero literal type,
+
+ ```
+ var bad: 1 = _
+ ```
+ Whilst we could, in principle, provide an implicit non-default initializer for cases such as these
+ it is the view of the authors of this SIP that there is nothing to be gained from enabling this
+ construction and that default initializer should be forbidden.
+
++ Support for `scala.Symbol` literal types has been added.
+
+ The `scala.Symbol` type has first class syntax support, like `String`. Despite having syntactic
+ literals, it does not have semantic literals in the same way that `String` does. This SIP adds
+ semantic literal types corresponding to the syntactic literals in the interest of consistency and
+ on the grounds that if a type is important enough to warrant first class syntax it is important
+ enough to warrant first class singleton types.
+
+ Note that shapeless in current Scala provides an encoding of singleton types for `Symbol` as the
+ type `Symbol` tagged with the literal type of its corresponding `String`.
+
+ Example,
+ ```
+ valueOf['foo] // result is 'foo: 'foo
+ ```
+
+## Follow on work from this SIP
+
+Whilst the authors of this SIP believe that it stands on its own merits, we think that there are two
+areas where follow on work is desirable.
+
+### Infix and prefix types
+
+[SIP-33 Match Infix and Prefix Types to Meet Expression Rules](http://docs.scala-lang.org/sips/make-types-behave-like-expressions.html)
+has emerged from the work on refined types and computation over singleton types mentioned in the
+motivation section above.
+
+Once literal types are available it is natural to want to lift entire expressions to the type level
+as is done already in libraries such as [singleton-ops](https://github.com/fthomas/singleton-ops).
+However, the precedence and associativity of symbolic infix _type constructors_ don't match the
+precedence and associativity of symbolic infix _value operators_, and prefix type constructors don't
+exist at all. It would be valuable to continue the process of aligning the form of the types and
+terms.
+
+### Byte and short literals
+
+As discussed in the proposal above, an important motivation for including first class literal
+types for Scala `Symbol` literals is that they have first class syntax -- if something is important
+enough to warrant syntax then it should be important enough to warrant a corresponding literal type.
+
+The converse also holds, and here we have two notable missing cases: `Byte` and `Short`. These have
+singleton types, but lack any corresponding syntax either at the type or at the term level. These
+types are important in libraries which deal with low level numerics and protocol implementation
+(see eg. [Spire](https://github.com/non/spire) and [Scodec](https://github.com/scodec/scodec)) and
+elsewhere, and the ability to, for instance, index a type class by a byte or short literal would be
+valuable.
+
+A prototype of this syntax extension existed at an early stage in the development of Typelevel Scala
+but never matured. The possibility of useful literal types adds impetus.
+
+## Related Scala issues resolved by the literal types implementation
+
++ [SI-1273](https://github.com/scala/bug/issues/1273) Singleton type has wrong bounds
++ [SI-5103](https://github.com/scala/bug/issues/5103) Singleton types not inferred in all places they should be
++ [SI-8323](https://github.com/scala/bug/issues/8323) Duplicate method name & signature with singleton type parameters over constant types
++ [SI-8564](https://github.com/scala/bug/issues/8564) Methods with ConstantType results get the inhabitant of ConstantType as their body
+
+## Appendix 1 -- shapeless excerpts
+
+Extracts from shapeless relevant to the motivating examples for this SIP,
+
+```
+trait Witness {
+ type T // the singleton type represented by this Witness
+ val value: T {} // the unique inhabitant of that type
+}
+
+object Witness extends Dynamic {
+ type Aux[T0] = Witness { type T = T0 }
+ type Lt[Lub] = Witness { type T <: Lub }
+
+ /**
+ * Materialize the Witness for singleton type T
+ */
+ implicit def apply[T]: Witness.Aux[T] = macro ...
+
+ /**
+ * Convert a literal value to its Witness
+ */
+ implicit def apply[T](t: T): Witness.Lt[T] = macro ...
+}
+
+object labelled {
+ /**
+ * The type of fields with keys of singleton type `K` and value type `V`.
+ */
+ type FieldType[K, +V] = V with KeyTag[K, V]
+ trait KeyTag[K, +V]
+
+ /**
+ * Yields a result encoding the supplied value with the singleton type `K' as its key.
+ */
+ def field[K] = new FieldBuilder[K]
+
+ class FieldBuilder[K] {
+ def apply[V](v : V): FieldType[K, V] = v.asInstanceOf[FieldType[K, V]]
+ }
+}
+
+object singleton {
+ implicit def mkSingletonOps(t: Any): SingletonOps = macro ...
+}
+
+trait SingletonOps {
+ import labelled._
+
+ type T
-* Implementation: [https://github.com/folone/scala/tree/topic/42.type](https://github.com/folone/scala/tree/topic/42.type)
-* Initial announcement: [https://groups.google.com/forum/#!topic/scala-language/9VEnFZImyJI](https://groups.google.com/forum/#!topic/scala-language/9VEnFZImyJI)
-* SIP discussion: [https://groups.google.com/forum/#!topic/scala-sips/YRHd8WW0V40](https://groups.google.com/forum/#!topic/scala-sips/YRHd8WW0V40)
+ /**
+ * Returns a Witness of the singleton type of this value.
+ */
+ val witness: Witness.Aux[T]
+
+ /**
+ * Narrows this value to its singleton type.
+ */
+ def narrow: T {} = witness.value
+
+ /**
+ * Returns the provided value tagged with the singleton type
+ * of this value as its key in a record-like structure.
+ */
+ def ->>[V](v: V): FieldType[T, V] = field[T](v)
+}
+
+```