diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 8078b5da6e24..65c83caaf999 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -715,6 +715,9 @@ class Definitions {
 
     def Not_value(implicit ctx: Context): TermSymbol = NotModule.requiredMethod(nme.value)
 
+  lazy val ValueOfType: TypeRef = ctx.requiredClassRef("scala.ValueOf")
+  def ValueOfClass(implicit ctx: Context): ClassSymbol = ValueOfType.symbol.asClass
+
   lazy val XMLTopScopeModuleRef: TermRef = ctx.requiredModuleRef("scala.xml.TopScope")
 
   lazy val TupleTypeRef: TypeRef = ctx.requiredClassRef("scala.Tuple")
diff --git a/compiler/src/dotty/tools/dotc/typer/Implicits.scala b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
index e9a18e09380a..e75ed134a11b 100644
--- a/compiler/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Implicits.scala
@@ -690,6 +690,29 @@ trait Implicits { self: Typer =>
       }
     }
 
+    /** Creates a tree that will produce a ValueOf instance for the requested type.
+      * An EmptyTree is returned if materialization fails.
+      */
+    def synthesizedValueOf(formal: Type)(implicit ctx: Context): Tree = {
+      def success(t: Tree) = New(defn.ValueOfClass.typeRef.appliedTo(t.tpe), t :: Nil).withPos(pos)
+
+      formal.argTypes match {
+        case arg :: Nil =>
+          fullyDefinedType(arg.dealias, "ValueOf argument", pos) match {
+            case ConstantType(c: Constant) =>
+              success(Literal(c))
+            case TypeRef(_, sym) if sym == defn.UnitClass =>
+              success(Literal(Constant(())))
+            case n: NamedType =>
+              success(ref(n))
+            case tp =>
+              EmptyTree
+          }
+        case _ =>
+          EmptyTree
+      }
+    }
+
     def hasEq(tp: Type): Boolean =
       inferImplicit(defn.EqType.appliedTo(tp, tp), EmptyTree, pos).isSuccess
 
@@ -714,7 +737,8 @@ trait Implicits { self: Typer =>
           trySpecialCase(defn.ClassTagClass, synthesizedClassTag,
             trySpecialCase(defn.QuotedTypeClass, synthesizedTypeTag,
               trySpecialCase(defn.TastyReflectionClass, synthesizedTastyContext,
-                trySpecialCase(defn.EqClass, synthesizedEq, failed))))
+                trySpecialCase(defn.EqClass, synthesizedEq,
+                  trySpecialCase(defn.ValueOfClass, synthesizedValueOf, failed)))))
     }
   }
 
diff --git a/library/src/dotty/DottyPredef.scala b/library/src/dotty/DottyPredef.scala
index 9cc046127317..0a1276e1958e 100644
--- a/library/src/dotty/DottyPredef.scala
+++ b/library/src/dotty/DottyPredef.scala
@@ -40,4 +40,19 @@ object DottyPredef {
   @forceInline final def implicitly[T](implicit ev: T): T = ev
 
   @forceInline def locally[T](body: => T): T = body
+
+  /**
+   * Retrieve the single value of a type with a unique inhabitant.
+   *
+   * @example {{{
+   * object Foo
+   * val foo = valueOf[Foo.type]
+   * // foo is Foo.type = Foo
+   *
+   * val bar = valueOf[23]
+   * // bar is 23.type = 23
+   * }}}
+   * @group utilities
+   */
+  @forceInline def valueOf[T](implicit vt: ValueOf[T]): T = vt.value
 }
diff --git a/library/src/scala/ValueOf.scala b/library/src/scala/ValueOf.scala
new file mode 100644
index 000000000000..2d9a1e72b340
--- /dev/null
+++ b/library/src/scala/ValueOf.scala
@@ -0,0 +1,52 @@
+/*
+ * Scala (https://www.scala-lang.org)
+ *
+ * Copyright EPFL and Lightbend, Inc.
+ *
+ * Licensed under Apache License 2.0
+ * (http://www.apache.org/licenses/LICENSE-2.0).
+ *
+ * See the NOTICE file distributed with this work for
+ * additional information regarding copyright ownership.
+ */
+
+package scala
+
+/**
+ * `ValueOf[T]` provides the unique value of the type `T` where `T` is a type which has a
+ * single inhabitant. Eligible types are singleton types of the form `stablePath.type`,
+ * Unit and singleton types corresponding to value literals.
+ *
+ * Instances of `ValueOf[T]` are provided implicitly for all eligible types. Typically
+ * an instance would be required where a runtime value corresponding to a type level
+ * computation is needed.
+
+ * For example, we might define a type `Residue[M <: Int]` corresponding to the group of
+ * integers modulo `M`. We could then mandate that residues can be summed only when they
+ * are parameterized by the same modulus,
+ *
+ * {{{
+ * 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])
+ * }
+ *
+ * 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]
+ * }}}
+ *
+ * Notice that here the modulus is encoded in the type of the values and so does not
+ * incur any additional per-value storage cost. When a runtime value of the modulus
+ * is required in the implementation of `+` it is provided at the call site via the
+ * implicit argument `m` of type `ValueOf[M]`.
+ */
+@scala.annotation.implicitNotFound(msg = "No singleton value available for ${T}.")
+final class ValueOf[T](val value: T) extends AnyVal
diff --git a/tests/pos/sip23-aliasing.scala b/tests/pos/sip23-aliasing.scala
new file mode 100644
index 000000000000..de434e042e9c
--- /dev/null
+++ b/tests/pos/sip23-aliasing.scala
@@ -0,0 +1,32 @@
+object Test {
+  trait Foo0 {
+    type T0
+  }
+
+  object Foo0 {
+    type Aux[T] = Foo0 {type T0 = T}
+    implicit def apply[T](implicit v: ValueOf[T]): Aux[T] = new Foo0 {
+      type T0 = T
+    }
+  }
+
+  type Foo[T] = Foo0 { type T0 = T }
+  val Foo = Foo0
+
+  Foo[5]
+  implicitly[Foo.Aux[5]]
+  implicitly[Foo[5]]
+
+
+  val three: 3 = 3
+  type Three = three.type
+  Foo[Three]
+  implicitly[Foo.Aux[Three]]
+  implicitly[Foo[Three]]
+
+  final object bar
+  type Bar = bar.type
+  Foo[Bar]
+  implicitly[Foo.Aux[Bar]]
+  implicitly[Foo[Bar]]
+}
diff --git a/tests/run/sip23-valueof.scala b/tests/run/sip23-valueof.scala
new file mode 100644
index 000000000000..684257c3b001
--- /dev/null
+++ b/tests/run/sip23-valueof.scala
@@ -0,0 +1,26 @@
+object Test extends App {
+  object Foo
+  val foo = "foo"
+
+  implicitly[ValueOf[1]]
+  implicitly[ValueOf[1L]]
+  implicitly[ValueOf[1.0]]
+  implicitly[ValueOf[1.0F]]
+  implicitly[ValueOf[true]]
+  implicitly[ValueOf['f']]
+  implicitly[ValueOf["foo"]]
+  implicitly[ValueOf[Unit]]
+  implicitly[ValueOf[Foo.type]]
+  implicitly[ValueOf[foo.type]]
+
+  assert((valueOf[1]: 1) == 1)
+  assert((valueOf[1L]: 1L) == 1L)
+  assert((valueOf[1.0]: 1.0) == 1.0)
+  assert((valueOf[1.0F]: 1.0F) == 1.0F)
+  assert((valueOf[true]: true) == true)
+  assert((valueOf['f']: 'f') == 'f')
+  assert((valueOf["foo"]: "foo") == "foo")
+  assert((valueOf[Unit]: Unit) == ((): Any))
+  assert((valueOf[Foo.type]: Foo.type) eq Foo)
+  assert((valueOf[foo.type]: foo.type) eq foo)
+}