The reason I ask is interaction with dependent method types, singleton types. /cc @adriaanm
Assume we had contravariant method subtyping. Given types B <: A <: Object, the following should hold
(x': A)(y': B)T <: (x: B)(y: x.type)T
the lefthand type accepts larger argument types, so it's more specific. Now, the current implementation
for method types does the following:
matchingParams(params1, params2) && // here we'd check contravariant subtyping, instead of equivalence
isSubType(res1, res2.substSym(params2, params1))
So the compiler replaces the parameter symbols in the supertype by the ones of the subtype, and we get
the following test for the result types
(y': B)T <: (y: x'.type)T
This test fails, because x'.type <: B ===> A <: B fails.
If we replaced symbols the other way around, it would have worked in this case. Now, I don't know if it's
good enough to just replace symbols the other way around, or if that can also fail in some cases. I tried
to find a counter-example, but could not. Check the following:
(x': A)x'.type <: (x: B)B
This subtyping statement is in fact true, even though that's non-intuitive at first. Obviously the argument
types are fine, the subtype accepts a larger argument type. It seems at first that the return types would
not conform, because if you expand x'.type <: B to A <: B that fails. Indeed, the lefthand type could
return an A, while the righthand type guarantees to always return a B.
HOWEVER, assume you have a function of the lefthand type
f: (x': A)x.type // note: it can only return the value that it receives as argument
If you are up-casting that function to the righthand type (x: B)B what happens? Now you cannot anymore
pass an argument of type A into the function, you have to give it a B. And since the function will always
return the same value as the one you pass into it, you will also get back a B. So the function f satisfies
the contract of type (x: B)B.
So the subtyping implementation would do the following, which seems correct
B <: B
------------- // expand the singleton to the underlying
x.type <: B
-----------------------
B <: A (x'.type)[x' -> x] <: B
----------------------------------------
(x': A)x'.type <: (x: B)B
Thoughts? Anybody knows papers on the subject?
Lukas