Add Precise type class for precise type inference

Author: odersky

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -535,6 +535,8 @@ class Definitions {
   def ConsType: TypeRef                 = ConsClass.typeRef
   @tu lazy val SeqFactoryClass: Symbol  = requiredClass("scala.collection.SeqFactory")
 
+  @tu lazy val PreciseClass: ClassSymbol = requiredClass("scala.Precise")
+
   @tu lazy val SingletonClass: ClassSymbol =
     // needed as a synthetic class because Scala 2.x refers to it in classfiles
     // but does not define it as an explicit class.

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -4941,7 +4941,7 @@ object Types extends TypeUtils {
       initOrigin: TypeParamRef,
       creatorState: TyperState | Null,
       val initNestingLevel: Int,
-      precise: Boolean) extends CachedProxyType with ValueType {
+      val precise: Boolean) extends CachedProxyType with ValueType {
     private var currentOrigin = initOrigin
 
     def origin: TypeParamRef = currentOrigin
@@ -5045,9 +5045,19 @@ object Types extends TypeUtils {
       else
         instantiateWith(tp)
 
+    def isPrecise(using Context) =
+      precise
+      || {
+        val constr = ctx.typerState.constraint
+        constr.upper(origin).exists: tparam =>
+          constr.typeVarOfParam(tparam) match
+            case tvar: TypeVar => tvar.precise
+            case _ => false
+      }
+
     /** Widen unions when instantiating this variable in the current context? */
     def widenPolicy(using Context): Widen =
-      if precise then Widen.None
+      if isPrecise then Widen.None
       else if ctx.typerState.constraint.isHard(this) then Widen.Singletons
       else Widen.Unions
 

compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala

@@ -11,6 +11,7 @@ import Constants.*
 import util.{Stats, SimpleIdentityMap, SimpleIdentitySet}
 import Decorators.*
 import Uniques.*
+import Flags.Method
 import inlines.Inlines
 import config.Printers.typr
 import Inferencing.*
@@ -26,7 +27,7 @@ object ProtoTypes {
   import tpd.*
 
   /** A trait defining an `isCompatible` method. */
-  trait Compatibility {
+  trait Compatibility:
 
     /** Is there an implicit conversion from `tp` to `pt`? */
     def viewExists(tp: Type, pt: Type)(using Context): Boolean
@@ -106,19 +107,34 @@ object ProtoTypes {
       if !res then ctx.typerState.constraint = savedConstraint
       res
 
-    /** Constrain result with special case if `meth` is an inlineable method in an inlineable context.
-     *  In that case, we should always succeed and not constrain type parameters in the expected type,
-     *  because the actual return type can be a subtype of the currently known return type.
-     *  However, we should constrain parameters of the declared return type. This distinction is
-     *  achieved by replacing expected type parameters with wildcards.
+    /** Constrain result with two special cases:
+     *   1. If `meth` is an inlineable method in an inlineable context,
+     *      we should always succeed and not constrain type parameters in the expected type,
+     *      because the actual return type can be a subtype of the currently known return type.
+     *      However, we should constrain parameters of the declared return type. This distinction is
+     *      achieved by replacing expected type parameters with wildcards.
+     *   2. When constraining the result of a primitive value operation against
+     *      a precise typevar, don't lower-bound the typevar with a non-singleton type.
      */
     def constrainResult(meth: Symbol, mt: Type, pt: Type)(using Context): Boolean =
-      if (Inlines.isInlineable(meth)) {
+
+      def constFoldException(pt: Type): Boolean = pt.dealias match
+        case tvar: TypeVar =>
+          tvar.isPrecise
+          && meth.is(Method) && meth.owner.isPrimitiveValueClass
+          && mt.resultType.isPrimitiveValueType && !mt.resultType.isSingleton
+        case tparam: TypeParamRef =>
+          constFoldException(ctx.typerState.constraint.typeVarOfParam(tparam))
+        case _ =>
+          false
+
+      if Inlines.isInlineable(meth) then
         constrainResult(mt, wildApprox(pt))
         true
-      }
-      else constrainResult(mt, pt)
-  }
+      else
+        constFoldException(pt) || constrainResult(mt, pt)
+    end constrainResult
+  end Compatibility
 
   object NoViewsAllowed extends Compatibility {
     override def viewExists(tp: Type, pt: Type)(using Context): Boolean = false
@@ -701,10 +717,18 @@ object ProtoTypes {
       case FunProto((arg: untpd.TypedSplice) :: Nil, _) => arg.isExtensionReceiver
       case _ => false
 
-  object SingletonConstrained:
-    def unapply(tp: Type)(using Context): Option[Type] = tp.dealias match
-      case RefinedType(parent, tpnme.Self, TypeAlias(tp))
-      if parent.typeSymbol == defn.SingletonClass => Some(tp)
+  /** An extractor for Singleton and Precise witness types.
+   *
+   *       Singleton { type Self = T }     returns Some(T, true)
+   *       Precise { type Self = T }       returns Some(T, false)
+   */
+  object PreciseConstrained:
+    def unapply(tp: Type)(using Context): Option[(Type, Boolean)] = tp.dealias match
+      case RefinedType(parent, tpnme.Self, TypeAlias(tp)) =>
+        val tsym = parent.typeSymbol
+        if tsym == defn.SingletonClass then Some((tp, true))
+        else if tsym == defn.PreciseClass then Some((tp, false))
+        else None
       case _ => None
 
   /** Add all parameters of given type lambda `tl` to the constraint's domain.
@@ -728,30 +752,31 @@ object ProtoTypes {
       // hk type lambdas can be added to constraints without typevars during match reduction
     val added = state.constraint.ensureFresh(tl)
 
-    def singletonConstrainedRefs(tp: Type): Set[TypeParamRef] = tp match
+    def preciseConstrainedRefs(tp: Type, singletonOnly: Boolean): Set[TypeParamRef] = tp match
       case tp: MethodType if tp.isContextualMethod =>
         val ownBounds =
-          for case SingletonConstrained(ref: TypeParamRef) <- tp.paramInfos
+          for
+            case PreciseConstrained(ref: TypeParamRef, singleton) <- tp.paramInfos
+            if !singletonOnly || singleton
           yield ref
-        ownBounds.toSet ++ singletonConstrainedRefs(tp.resType)
+        ownBounds.toSet ++ preciseConstrainedRefs(tp.resType, singletonOnly)
       case tp: LambdaType =>
-        singletonConstrainedRefs(tp.resType)
+        preciseConstrainedRefs(tp.resType, singletonOnly)
       case _ =>
         Set.empty
 
-    val singletonRefs = singletonConstrainedRefs(added)
-    def isSingleton(ref: TypeParamRef) = singletonRefs.contains(ref)
-
     def newTypeVars: List[TypeVar] =
+      val preciseRefs = preciseConstrainedRefs(added, singletonOnly = false)
       for paramRef <- added.paramRefs yield
-        val tvar = TypeVar(paramRef, state, nestingLevel, precise = isSingleton(paramRef))
+        val tvar = TypeVar(paramRef, state, nestingLevel, precise = preciseRefs.contains(paramRef))
         state.ownedVars += tvar
         tvar
 
     val tvars = if addTypeVars then newTypeVars else Nil
     TypeComparer.addToConstraint(added, tvars)
+    val singletonRefs = preciseConstrainedRefs(added, singletonOnly = true)
     for paramRef <- added.paramRefs do
-      if isSingleton(paramRef) then paramRef <:< defn.SingletonType
+      if singletonRefs.contains(paramRef) then paramRef <:< defn.SingletonType
     (added, tvars)
   end constrained
 

compiler/src/dotty/tools/dotc/typer/Synthesizer.scala

@@ -238,7 +238,7 @@ class Synthesizer(typer: Typer)(using @constructorOnly c: Context):
   end synthesizedValueOf
 
   val synthesizedSingleton: SpecialHandler = (formal, span) => formal match
-    case SingletonConstrained(tp) =>
+    case PreciseConstrained(tp, true) =>
       if tp.isSingletonBounded(frozen = false) then
         withNoErrors:
           ref(defn.Compiletime_erasedValue).appliedToType(formal).withSpan(span)
@@ -247,6 +247,13 @@ class Synthesizer(typer: Typer)(using @constructorOnly c: Context):
     case _ =>
       EmptyTreeNoError
 
+  val synthesizedPrecise: SpecialHandler = (formal, span) => formal match
+    case PreciseConstrained(tp, false) =>
+      withNoErrors:
+        ref(defn.Compiletime_erasedValue).appliedToType(formal).withSpan(span)
+    case _ =>
+      EmptyTreeNoError
+
   /** Create an anonymous class `new Object { type MirroredMonoType = ... }`
    *  and mark it with given attachment so that it is made into a mirror at PostTyper.
    */
@@ -749,6 +756,7 @@ class Synthesizer(typer: Typer)(using @constructorOnly c: Context):
     defn.ManifestClass        -> synthesizedManifest,
     defn.OptManifestClass     -> synthesizedOptManifest,
     defn.SingletonClass       -> synthesizedSingleton,
+    defn.PreciseClass         -> synthesizedPrecise,
   )
 
   def tryAll(formal: Type, span: Span)(using Context): TreeWithErrors =

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -3027,7 +3027,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
                 cpy.Select(id)(This(cls), id.name)
               case _ =>
                 super.transform(tree)
-          ValDef(impl, anchorParams.transform(rhs))
+          ValDef(impl, anchorParams.transform(rhs)).withSpan(impl.span.endPos)
         end givenImpl
 
         val givenImpls =

compiler/test/dotty/tools/repl/TabcompleteTests.scala

@@ -122,11 +122,11 @@ class TabcompleteTests extends ReplTest {
   }
 
   @Test def moduleCompletion = initially {
-    assertEquals(List("Predef"), tabComplete("object Foo { type T = Pre"))
+    assertEquals(List("Predef"), tabComplete("object Foo { type T = Pred"))
   }
 
   @Test def i6415 = initially {
-    assertEquals(List("Predef"), tabComplete("object Foo { opaque type T = Pre"))
+    assertEquals(List("Predef"), tabComplete("object Foo { opaque type T = Pred"))
   }
 
   @Test def i6361 = initially {

docs/_docs/reference/experimental/typeclasses.md

@@ -444,6 +444,39 @@ This is less of a disruption than it might appear at first:
  - Simplification of the language since a feature is dropped
  - Eliminate non-obvious and misleading syntax.
 
+
+### Bonus: Fixing Singleton
+
+We know the current treatment of `Singleton` as a type bound is broken since
+`x.type | y.type <: Singleton` holds by the subtyping rules for union types, even though `x.type | y.type` is clearly not a singleton.
+
+A better approach is to treat `Singleton` as a type class that is interpreted specially by the compiler.
+
+We can do this in a backwards-compatible way by defining `Singleton` like this:
+
+```scala
+trait Singleton:
+  type Self
+```
+
+Then, instead of using an unsound upper bound we can use a context bound:
+
+```scala
+def f[X: Singleton](x: X) = ...
+```
+
+The context bound is treated specially by the compiler so that no using clause is generated at runtime (this is straightforward, using the erased definitions mechanism).
+
+### Bonus: Precise Typing
+
+This approach also presents a solution to the problem how to express precise type variables. We can introduce another special type class `Precise` and use it like this:
+
+```scala
+def f[X: Precise](x: X) = ...
+```
+Like a `Singleton` bound, a `Precise` bound disables automatic widening of singleton types or union types in inferred instances of type variable `X`. But there is no requirement that the type argument _must_ be a singleton.
+
+
 ## Summary of Syntax Changes
 
 Here is the complete context-free syntax for all proposed features.
@@ -692,38 +725,10 @@ Dimi Racordon tried to [port some core elements](https://github.com/kyouko-taiga
 
 With the improvements proposed here, the library can now be expressed quite clearly and straightforwardly. See tests/pos/hylolib in this PR for details.
 
-## Suggested Improvements unrelated to Type Classes
-
-The following two improvements elsewhere would make sense alongside the suggested changes to type classes. But only the first (fixing singleton) forms a part of this proposal and is implemented.
-
-### Fixing Singleton
-
-We know the current treatment of `Singleton` as a type bound is broken since
-`x.type | y.type <: Singleton` holds by the subtyping rules for union types, even though `x.type | y.type` is clearly not a singleton.
-
-A better approach is to treat `Singleton` as a type class that is interpreted specially by the compiler.
+## Suggested Improvement unrelated to Type Classes
 
-We can do this in a backwards-compatible way by defining `Singleton` like this:
+The following improvement would make sense alongside the suggested changes to type classes. But it does not form part of this proposal and is not yet implemented.
 
-```scala
-trait Singleton:
-  type Self
-```
-
-Then, instead of using an unsound upper bound we can use a context bound:
-
-```scala
-def f[X: Singleton](x: X) = ...
-```
-
-The context bound is treated specially by the compiler so that no using clause is generated at runtime (this is straightforward, using the erased definitions mechanism).
-
-_Aside_: This can also lead to a solution how to express precise type variables. We can introduce another special type class `Precise` and use it like this:
-
-```scala
-def f[X: Precise](x: X) = ...
-```
-This would disable automatic widening of singleton types in inferred instances of type variable `X`.
 
 ### Using `as` also in Patterns
 

library/src/scala/Precise.scala

@@ -0,0 +1,11 @@
+package scala
+import annotation.experimental
+import language.experimental.erasedDefinitions
+
+/** A type class-like trait intended as a context bound for type variables.
+ *  If we have `[X: Precise]`, instances of the type variable `X` are inferred
+ *  in precise mode. This means that singleton types and union types are not
+ *  widened.
+ */
+@experimental erased trait Precise:
+  type Self

tests/neg/singleton-ctx-bound.check

@@ -0,0 +1,34 @@
+-- [E007] Type Mismatch Error: tests/neg/singleton-ctx-bound.scala:7:5 -------------------------------------------------
+7 |  f1(someInt) // error
+  |     ^^^^^^^
+  |     Found:    Int
+  |     Required: Singleton
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg/singleton-ctx-bound.scala:12:5 ------------------------------------------------
+12 |  f2(someInt) // error
+   |     ^^^^^^^
+   |     Found:    Int
+   |     Required: Singleton
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E172] Type Error: tests/neg/singleton-ctx-bound.scala:13:26 --------------------------------------------------------
+13 |  f2(if ??? then 1 else 2)   // error
+   |                          ^
+   |No given instance of type (1 : Int) | (2 : Int) is Singleton was found for parameter x$2 of method f2 in object Test. Failed to synthesize an instance of type (1 : Int) | (2 : Int) is Singleton: (1 : Int) | (2 : Int) is not a singleton
+-- [E007] Type Mismatch Error: tests/neg/singleton-ctx-bound.scala:17:5 ------------------------------------------------
+17 |  f3(someInt) // error
+   |     ^^^^^^^
+   |     Found:    Int
+   |     Required: Singleton
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E172] Type Error: tests/neg/singleton-ctx-bound.scala:18:26 --------------------------------------------------------
+18 |  f3(if ??? then 1 else 2)   // error
+   |                          ^
+   |No given instance of type Singleton{type Self = (1 : Int) | (2 : Int)} was found for a context parameter of method f3 in object Test. Failed to synthesize an instance of type Singleton{type Self = (1 : Int) | (2 : Int)}: (1 : Int) | (2 : Int) is not a singleton
+-- [E172] Type Error: tests/neg/singleton-ctx-bound.scala:33:6 ---------------------------------------------------------
+33 |class D extends A:  // error
+   |^
+   |No given instance of type Singleton{type Self = D.this.Elem} was found for inferring the implementation of the deferred given instance given_Singleton_Elem in trait A. Failed to synthesize an instance of type Singleton{type Self = D.this.Elem}: D.this.Elem is not a singleton
+34 |  type Elem = Int

tests/neg/singleton-ctx-bound.scala

@@ -18,3 +18,18 @@ object Test:
   f3(if ??? then 1 else 2)   // error
   f3(3 * 2) // OK
   f3(6) // OK
+
+import compiletime.*
+
+trait A:
+  type Elem: Singleton
+
+class B extends A:
+  type Elem = 1 // OK
+
+class C[X: Singleton] extends A:
+  type Elem = X // OK
+
+class D extends A:  // error
+  type Elem = Int
+