The singleton instance trick used by `=:=` is unsound

[smarter]

In the standard library, =:= is defined as follow:

  // the only instance for <:< and =:=, used to avoid overhead
  private val singleton: =:=[Any, Any] = new =:=[Any,Any] {
    // ...
  }
  implicit def refl[A]: A =:= A = singleton.asInstanceOf[A =:= A]
}

I always thought this was perfectly fine, but thanks to Dotty's world-class GADT support, it isn't anymore :)

object Test {
  def cast[A, B](elem: A, default: B)(implicit x: A =:= A, y: B =:= B): B = x match {
    case x: y.type =>
      elem
    case _ =>
      default
  }

  def main(args: Array[String]): Unit = {
    val x: String = cast(1, "") // ClassCastException
  }
}

The same code also compiles and crashes in scalac, but produces an unchecked erasure warning which I believe is incorrect: if it weren't for the cast used to get an instance of =:=, this code would be perfectly fine.

What can we do about this? In the short-term, either do nothing or special-case the GADT handling of =:= in the compiler. in the long-term, we should rewrite =:= and <:< using an opaque type to some dummy value:

opaque type <:<[-From, +To] = Object
opaque type =:=[From, To] <: <:<[From, To] = Object
private val singleton: =:=[Any, Any] = new Object
implicit def refl[A]: A =:= A = singleton
// ... and a bunch of extension methods on <:< and =:=

There's still a cast (EDIT: actually not needed), but the use of opaque types prevents the bogus inference of GADT bounds:
https://github.com/lampepfl/dotty/blob/b448db2454e003f1448a31746daed11001a2ec86/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L869-L870

(another solution would be to somehow enforce that values of type =:= must always be erased at runtime, and therefore do not have a notion of reference equality)

[abgruszecki]

Can we find a single case where inferring GADT constraints from singleton type checks is actually useful? Taking object identity into account when inferring GADT constraints sounds deeply bogus to me. As we can see, it also prevents useful optimizations such as reusing a single instance of Nil for an invariant list. The simplest fix would then be to just infer no GADT constraints from singleton type checks.

[smarter]

Can we find a single case where inferring GADT constraints from singleton type checks is actually useful?

I don't have a concrete example, but being able to infer constraints from equality sounds like something that'd be useful when writing theorem-prover-style code, maybe @Blaisorblade has an idea ?

it also prevents useful optimizations such as reusing a single instance of Nil

Not at all. List is covariant so Nil is perfectly sound as is. This is really only a problem when people rely on asInstanceOf working because of type erasure.

[Blaisorblade]

Can we find a single case where inferring GADT constraints from singleton type checks is actually useful?

The typing rule makes some sense for objects with type members, tho I’m not sure I can think of a use case there; maybe when you match hlists against null?
Emir et al. (2007) present another use-case (http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.88.5295&rep=rep1&type=pdf), but I’m not sure it’s very convincing...

[neko-kai]

This has been discussed a long time ago in the scalac bug tracker, (and apparently it's the reason why polymorphic, non-specialized zero-arg givens aren't lazy vals by default?..) I can't find the link now but I mentioned it in

EDIT: I don’t think the singleton type cast trick is relevant, unless DOT specifies semantics for reference equality? You MUST opt-in to insanity for it to lead to unsoundness – it can also be detected and require a langauge flag.

[LPTK]

@smarter

There's still a cast

Surely, you could also avoid the cast by putting the appropriate private[scala] methods in the companion objects of the opaque types, no? (Or really just putting refl itself there.)

@AleksanderBG

Can we find a single case where inferring GADT constraints from singleton type checks is actually useful?

I'm sure there are many and we just haven't thought of them yet :^)
Please do not make things worse just to avoid making them right!

[nicolasstucki]

Another way this could be fixed if by using erased

  type =:=[-From, +To]
  type <:<[-From, +To] <: =:=[From, To]

  erased implicit def refl[A]: A =:= A = ???

  extension ops on [From, To](erased ev: =:=[From, To]) {
    def apply(x: From): To = x.asInstanceOf[To]
  }

The upside (performance-wise and soundness-wise) and downside (usability-wise) is that all =:= parameters would need to be annotated with erased. We can also get rid of the annoying singleton instance.

Note: the collective extension do not support erased yet but it should support it.

[LPTK]

@nicolasstucki what if people have code like this?

def test[T: <:<[Int, *]](arr: ArrayBuffer[Int]): ArrayBuffer[T] = arr.map(summon)

[abgruszecki]

@LPTK what we could also do is add a @phantom annotation to type parameters of classes which says "never infer GADT constraints from this type parameter". Then we could annotate both type parameters of =:= with this annotation and be on our merry way, same with the Nil of an invariant list. Additional benefit is I can see how to implement this w/o too much effort.

[Blaisorblade]

@AleksanderBG It seems you never want to mark only one parameter as phantom (also, I'm not sure the name is good). It's a bit annoying that this annotation is specific for singleton type tests and singleton values casted to multiple types, but I'm not sure of an easy way to generalize it.

OTOH, it seems none of the proposals can go in for 3.0 (except a compiler-hardcoded blacklist of types where GADT inference must be avoided), and I'm unsure which can go in for 3.1...

[abgruszecki]

@Blaisorblade This @phantom is basically another view at Haskell's type parameter roles. Both for us and for Haskell, "phantom" means "not reflected in the underlying runtime structure". Contrast this with (https://gitlab.haskell.org/ghc/ghc/wikis/roles):

It is often the case that programmers use type variables simply to constrain the type checker, not to make any statement about the runtime representation of a type.

It's just that we're approaching the issue from another angle, since in Haskell people wanted a safe way of coercing between values of two types, and what we want is not inferring GADT constraints from runtime instance checks on values which were "unsafely" coerced.

[szeiger]

What exactly makes the compiler assume that it can compile this to a runtime equality check instead of producing an unchecked erasure warning (and why would an opaque type avoid it)?

Casting a single instance of an immutable and invariant class to whatever instance is required is commonplace in the standard library and in other Scala code.

[smarter]

What exactly makes the compiler assume that it can compile this to a runtime equality check

That's the semantics of x: foo.type type tests according to the spec.

instead of producing an unchecked erasure warning

there's nothing that is left unchecked, so there's no warning

and why would an opaque type avoid it

opaque types are not injectives like class types, if we have Foo[X] = Foo[Y] we cannot conclude anything about the relationship between X and Y, because we could have defined opaque type Foo[T] = Int for example.

Casting a single instance of an immutable and invariant class to whatever instance is required is commonplace in the standard library and in other Scala code.

Yes, and I wonder if we could get rid of this pattern. For =:= it seems that we can easily using an opaque type. But I don't have a good solution for HashMap.empty:
https://github.com/scala/scala/blob/8f20a7d84924939698717d26b3e0e5a5c0da829c/src/library/scala/collection/immutable/HashMap.scala#L2140-L2146
If HashMap was contravariant in K then this would be fine (as we couldn't infer any kind of equality between types between two instances) but I assume there's a good reason it isn't ?

[Blaisorblade]

FWIW, as I hinted earlier, this match semantics dates back to the paper introducing case classes in 2007 (http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.547.5623&rep=rep1&type=pdf). Check out Fig. 11 of that paper.

[SethTisue]

if HashMap was contravariant in K ... but I assume there's a good reason it isn't

HashMap extends Iterable[(K, V)] (but even if it didn't, consider such methods as keysIterator)