Null lower bound breaks with intersection types

[scabug]

Using 2.7.2.RC1. The problem is that if A is a type variable with a >: Null lower bound, then even if B >: Null, A with B won't be >: Null.

Super-contrived minimal example follows:

scala> trait X { x => type T >: Null; new X { type T = Any with x.T } }
<console>:5: error: error overriding type T in trait X with bounds >: Null <: Any;
 type T has incompatible type Any with X.this.T
       trait X { x => type T >: Null; new X { type T = Any with x.T } }

Replace Null above with any other type, and it works.

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-1280?orig=1
Reporter: Lauri Alanko (lealanko)

[scabug]

@dragos said:
Maybe a bit simpler:

scala> trait T { type U >: Null
     | type V >: Null
     | }
defined trait T

scala> trait T1 extends T { type V = Any with U }
<console>:5: error: error overriding type V in trait T with bounds >: Null <: Any;
 type V has incompatible type Any with T1.this.U
       trait T1 extends T { type V = Any with U }

[scabug]

@odersky said:
That's mandated by the spec. The issue is that in general, a type T with U may be empty, in which case not even null would be a legal value. So we can't assume that
null <:< T with U, unless we know something about T and U. The spec and compiler approximate this by saying that null <:< T with U is no longer true if either T or U is an abstract type. In the particular case, this is too severe because T <: Any, so Any with T is really just T. But fixing this would complicate the simple rule in the spec, for no obvious gain.

[scabug]

Lauri Alanko (lealanko) said:
I'm sorry, but the answer doesn't satisfy me, and I can't avoid the impression that you have misunderstood the problem. The problem is not that Null isn't getting some special treatment, but rather that a general typing rule doesn't apply to Null whereas it seems to apply to all other types (including Nothing). To reiterate:

If A >: L and B >: L then A with B >: L.

This rule should, as far as I can see, be safe for all types, and with the current type system it already seems to be admissible for all the types I tested with... except Null. Obviously, if A >: Null and B >: Null, then null also inhabits A with B, so your concern about empty types is already addressed by the general bounds checking mechanism. I don't see Null being any different from any other lower bound here.

As further proof that this is a compiler bug, consider that the problems in both my and Iulian's example can be worked around by simply parameterizing the lower bound so a literal Null doesn't appear in the code:

trait X[L] { x => type T >: L; new X[L] { type T = Any with x.T } }

trait T[L] { type U >: L; type V >: L }
trait T1[L] extends T[L] { type V = Any with U }

This doesn't yield any compiler errors with 2.7.2.RC1, and there are no problems instantiating L to Null.

So it very very much seems to me that in the compiler there is some special-cased handling for Null that rejects valid code.

[scabug]

@odersky said:
Please trust my experience here. There was a type soundness bug related to exactly this which was filed by either Altherr or Cremet in Aladdin a while ago. I don't have the time to dig this up myself. I am hopelessly overloaded as it is and can't go into this right now. If somebody else feels like analyzing the matter and demonstrating type soundness, fine. But I can't do it right now, and I can't allow a ``fix_ which would most likely break type soundness. If you don't believe me, look up the tickets by Altherr and Cremet in Aladdin.

[scabug]

Geoffrey Alan Washburn (washburn) said:
I was unable to find anything in Aladdin about this. If having subtyping behave correctly means that we lose type soundness, something is seriously wrong with the type system. This with the fact that fixing #1208 would apparently break all sorts of things seems to indicate that we need to step back and really figure out what has gone wrong with the Scala type system before proceeding with additional features.

[scabug]

@DRMacIver said:
For what it's worth, the reason you can't generically infer that if A >: Null then A with B >: Null is because if B is nothing then A with B is Nothing which is not >: Null.

I can't think of a reason it shouldn't work if B >: Null though.

[scabug]

Lauri Alanko (lealanko) said:
Tickets #500 and #501 seem like they might be the ones intended, but if they're directly related to this case, I'm probably a bit slow since I can't see it.

Anyway, if L <: A, L <: B |- L <: A with B would, for some reason, be an unsound rule when L = Null, then the type system is already broken due to the parameterized workaround.

And by my reading the above rule is already contained in the spec, in 3.5.2:

If T <: Ui for i = 1, . . . , n and R is okay then T conforms to the compound type {U1 with . . . with Un {R}.

I don't see any exceptions for T = Null.

[scabug]

@odersky said:
You are right, #500 and #501 are not direct counter-examples. I remember now that we reasoned informally that type intersection would be similar but we never worked out a concrete example. I have done that now. Here it is:

class B
class C(x: String) extends B

class A {
  type A >: Null
  class D { type T >: C <: B }
  val x: D with A = null
  var y: x.T = new C("abc")
}
object Test extends A with Application {
  class C { type T = Int; val x = 1 }
  type A = C
  y = 42
}

(I'll add it to the test suite as null-unsoundness.scala).

If you compile the test with scalac, you get:

 found   : Null(null)
 required: A.this.D with A.this.A
  val x: D with A = null
                    ^
one error found

I then changed the condition which causes the error. It's in symtab/Types, method
isSubType0. One of the cases reads:

      case (_, RefinedType(parents2, ref2)) =>
        (parents2 forall (tp2 => tp1 <:< tp2)) &&
        (ref2.toList forall tp1.specializes) &&
        (tp1.typeSymbol != NullClass ||
        !parents2.exists(_.typeSymbol.isAbstractType))

I removed the last condition. Then the example compiles, but at runtime you see:

Exception in thread "main" java.lang.ExceptionInInitializerError
	at Test.main(nulls.scala)
Caused by: java.lang.ClassCastException: java.lang.Integer cannot be cast to B
	at Test$$.<init>(nulls.scala:13)
	at Test$$.<clinit>(nulls.scala)
	... 1 more

So, here's the type hole.

In summary, ``what's wrong with the Scala type system_ is that the idea of a universal value of null is fundamentally at odds with type abstraction. The cleanest fix would be to eliminate `null'. Failing that, we have to live with the restriction, or design a different scheme. But this should be a SIP; as you can see the issues are tricky and require a lot of study.

[scabug]

Lauri Alanko (lealanko) said:
Thanks for taking the time to explain the issue in detail.

It seems to me that 500, 501 and this case are all various
symptoms of a common problem. The fixes have cured individual
symptoms (at the cost of rejecting some safe programs), but not
the underlying cause.

To my understanding, the underlying cause is the fact that a
stable identifier bound to null can have a singleton type.
With value members this "only" leads to a NullPointerException,
but with type members it leads to the situation that null
is accepted as a witness to prove that some type with given
constraints actually exists. And this is not always the case.

The fix to 501 and this case take different approaches, though:
the 501 fix (requiring bounds to be statically conforming) tries
to prevent us from even expressing "bad" constraints that
null would then illegally prove. In your above example,
however, we can express the impossible constraints in {type T = Int } with { type T <: B }, but we just prevent
null from proving it.

I don't think null is inherently evil, but its interaction
with singleton types seems to be broken. To my understanding, it
would in principle suffice to substitute NotNull in place of AnyRef in section 3.2.1 of the spec, though this would of
course bring enormous practical difficulties. But it seems like
the right thing to do. Then the all the fixes to individual
symptoms could be removed.

It's funny, now I realize that my ticket #1273 is completely
upside down: it's right that Null <: Singleton doesn't
hold. The problem is instead that Null <: p.type holds. :)

Have I understood the situation correctly?

[scabug]

Lauri Alanko (lealanko) said:
As I said previously, if the type system can be broken without the current restrictions on Null, it can be broken even with them, thanks to the parameterization workaround. This turns out to be true, since the following breaks even unmodified RC1. So, once again, Scala is unsound.

  class C[L, A >: L, B >: L](l : L) { 
    val x : A with B = l
  }

  class D[B >: Null] extends C[Null, { type X >: String}, B](null) { 
    var y : x.X = "foo" 
  }

  val v : Int = new D[{type X <: Int}].y

This yields:

java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
	at scala.runtime.BoxesRunTime.unboxToInt(Unknown Source)
	at .<init>(<console>:6)

Abstract type members can also be used instead of type parameters.

I guess it's possible to add some more ad-hoc checks that prevent more of these kinds of problems, but they still can't guarantee that more of the same kind won't turn up. Forbidding null from having a singleton type seems like the only real solution.

[scabug]

Geoffrey Alan Washburn (washburn) said:
I've fixed

[scabug]

Geoffrey Alan Washburn (washburn) said:
This has been fixed as part of the new volatility language change.

I've created a test in r16081 for this particular ticket.

[scabug]

@paulp said:
Reopening because I want to see how the 2013 scala does with these tests.

[scabug]

@adriaanm said:
The sleeping dogs wish not to be disturbed.