Allow types with the same name at different kinds.

[odersky]

I'd like Scala to allow abstract and alias types with the same name but different kinds. E.g.

class C {
  type This
}
class D[A] {
  type This[X]
}
object O extends C with D {
   type This = o.type
   type This[X] = o.type
}

Benefits:

• It gives us a way to address IndexOutOfBoundsException when attempting to reduce ill-kinded types #2887, because ill-kinded types in that issue would translate to overloaded types, so no conflicting kinds can arise.
• It could avoid namespace pollution in high-level encodings such as the encodings of type classes that we study.

The proposal would be to distinguish same-named types by their kind class, where the kind class in this case only talks about arities, but not about bounds and variances. So

type T
type T[_]
type T[_, _]
type T[_[_]]

are all in different kind classes (and therefore can be defined in the same scope), but

type T[X]
type T[+X]
type T[X <: AnyRef]

are all in the same kind class, so defining them all in the same scope gives double definition errors. The reason for this distinction is that there is no subtype relation between types in different kind classes, so we can use the kind class as a partition criterion.

One tempting generalization of this scheme is to extend it to traits and classes. E.g. where we write Function1, ..., Function22 now, maybe we should allow instead:

trait Function[-T1, R] { ... }
trait Function[-T1, -T2, R] { ... }

and so on. But that one is much harder to define and implement. First, what about the companion object? Of which trait is object Function { ... } the companion? Second, what about binary names? What are the names of the Java interfaces that these Function traits map to? So for the moment, this generalization is not considered as part of this issue.

Besides, one can get a long way already with overloaded aliases. I.e. keep the definitions of the traits Function1, ..., Function22 as they are now, but add aliases:

type Function[-T1, R] = Function1[T1, R]
type Function[-T1, -T2, R] = Function2[T1, T2, R]

and so on.

[sjrd]

Aren't you constantly saying that overloading is a pain to deal with in a compiler? And now you want to add type overloading?

Also,

[...] But that one is much harder to define and implement. First, what about the companion object?

With opaque type aliases, types are about to gain companion objects too. What then?

[Blaisorblade]

are all in the same kind class, so defining them all in the same scope gives double definition errors.

And what if they're defined in different scopes and merged by intersection? What should be the resulting variance?

Also, FWIW, addressing #2887 doesn't require making overloading usable — just that overloads are kept distinct during typechecking.

[odersky]

Also, FWIW, addressing #2887 doesn't require making overloading usable — just that overloads are kept distinct during typechecking.

I believe that's pretty much the same thing! Once they are kept distinct, you could argue that it would require additional effort to prevent them from being used.

@sjrd Sure, overloading is hard to deal with, but it seems to be the most straightforward way to deal with #2887. I have not seen an alternative solution yet that's more palatable. Btw, this was originally proposed by @DarkDimius and together with @sstucki we agreed that this might be one of the more promising ways to solve this (meaning, we cannot rule it out as impractical immediately).

Regarding opaque types, that's easy: Only version of the type may be labelled opaque, and that's the one with the companion object (companion objects are not defined for non-opaque types).

[Blaisorblade]

Once they are kept distinct, you could argue that it would require additional effort to prevent them from being used.

Agreed; I had in mind doing that extra effort to prevent people from (ab)using this feature. If v: C with D, I'm fine with (v: C).This being a proper type and (v: D).This being a type constructor (much like in C++). But I'd be tempted to forbid v.This even if it were more work than implementing overload resolution, just to avoid wondering about all the possible puzzlers and issues needed to support overloading properly.

This would allow "kind classes" to include the whole kind. If you only include arities, how sure are we the compiler handles well the intersection of type members with different arities, or that the result is sound?

But I admit that right now, playing with intersections a bit, I could only implement unsafeCoerce under unrealizable contexts (which we know is possible), not crash the compiler (yet) or implement unsafeCoerce under realizable contexts.

trait A {
  type T[-X]
}
trait B {
  type T[+X]
}
trait C { type M <: A }
trait D { type M >: B }
object Test {
  // this should not be callable.
  def coerceTArg(x: A with B)(v: x.T[Int]): x.T[String] = {  // what's the variance of x.K?
    def downcastT[X, Y <: X](a: A)(x: a.T[X]): a.T[Y] = x
    def upcastT[X, Y <: X](b: B)(x: b.T[Y]): b.T[X] = x
    upcastT[String, Nothing](x)(downcastT[Int, Nothing](x)(v))
  }

  def test(x: C with D): Unit = {
    // XXX try to get funkier behavior following ideas from #2887
  }
}

[Blaisorblade]

not crash the compiler (yet)

Famous last words, and I wasn't trying to get a crash, just to exploit a soundness hole (members on lazy vals) where we already have a fix (this was on branch add-kind-poly, on 14253af).

$ dotr -repl
scala> object Test {
         trait A {
           type T[-X]
         }
         trait B {
           type T[+X]
         }
         trait C { type M <: A }
         trait D { type M >: B }
           // this should not be callable.
           def coerceTArg(x: A with B)(v: x.T[Int]): x.T[String] = {  // what's the variance of x.K?
             def downcastT[X, Y <: X](a: A)(x: a.T[X]): a.T[Y] = x
             def upcastT[X, Y <: X](b: B)(x: b.T[Y]): b.T[X] = x
             upcastT[String, Nothing](x)(downcastT[Int, Nothing](x)(v))
           }

           def test(x: C with D): Unit = {
             // XXX try to get funkier behavior following ideas from #2887
           }
         }
// defined object Test
scala> import Test._
scala> lazy val v: C with D = v
val v: Test.C & Test.D = <lazy>
scala> Test.coerceTArg(v.M)
Exception in thread "main" java.lang.AssertionError: assertion failed: leak: <error value `M` is not a member of Test.C & Test.D>(x$1) in {
  val x$1: <error value `M` is not a member of Test.C & Test.D> = v.M
  {
    def $anonfun(v: x$1.T[Int]): x$1.T[String] = Test.coerceTArg(x$1)(v)
    closure($anonfun): (x$1.T[Int] => x$1.T[String])
  }
}
	at dotty.DottyPredef$.assertFail(DottyPredef.scala:36)
	at dotty.tools.dotc.typer.Typer.ensureNoLocalRefs(Typer.scala:705)
	at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:667)
	at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1779)
	at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1823)
	at dotty.tools.dotc.typer.Typer.op1$2(Typer.scala:1854)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1850)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1862)
	at dotty.tools.dotc.typer.Typer.adaptNoArgsUnappliedMethod$1(Typer.scala:2301)
	at dotty.tools.dotc.typer.Typer.adaptNoArgs$1(Typer.scala:2389)
	at dotty.tools.dotc.typer.Typer.adapt1(Typer.scala:2522)
	at dotty.tools.dotc.typer.Typer.adapt(Typer.scala:2064)
	at dotty.tools.dotc.typer.Typer.op1$2(Typer.scala:1854)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1850)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1862)
	at dotty.tools.dotc.typer.Namer.typedAheadExpr$$anonfun$1(Namer.scala:1003)
	at dotty.tools.dotc.typer.Namer.typedAheadImpl(Namer.scala:993)
	at dotty.tools.dotc.typer.Namer.typedAheadExpr(Namer.scala:1003)
	at dotty.tools.dotc.typer.Namer.rhsType$2(Namer.scala:1121)
	at dotty.tools.dotc.typer.Namer.cookedRhsType$1(Namer.scala:1133)
	at dotty.tools.dotc.typer.Namer.lhsType$lzyINIT1$1(Namer.scala:1134)
	at dotty.tools.dotc.typer.Namer.lhsType$1(Namer.scala:1134)
	at dotty.tools.dotc.typer.Namer.inferredType$1(Namer.scala:1147)
	at dotty.tools.dotc.typer.Namer.valOrDefDefSig(Namer.scala:1155)
	at dotty.tools.dotc.typer.Namer$Completer.typeSig(Namer.scala:792)
	at dotty.tools.dotc.typer.Namer$Completer.completeInCreationContext(Namer.scala:843)
	at dotty.tools.dotc.typer.Namer$Completer.complete(Namer.scala:821)
	at dotty.tools.dotc.core.SymDenotations$SymDenotation.completeFrom(SymDenotations.scala:247)
	at dotty.tools.dotc.core.SymDenotations$SymDenotation.completeInfo$1(SymDenotations.scala:210)
	at dotty.tools.dotc.core.SymDenotations$SymDenotation.info(SymDenotations.scala:212)
	at dotty.tools.dotc.core.SymDenotations$SymDenotation.ensureCompleted(SymDenotations.scala:353)
	at dotty.tools.dotc.typer.Typer.retrieveSym(Typer.scala:1725)
	at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:1750)
	at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1822)
	at dotty.tools.dotc.typer.Typer.op1$2(Typer.scala:1854)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1850)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1862)
	at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:1881)
	at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:1910)
	at dotty.tools.dotc.typer.Typer.typedClassDef(Typer.scala:1451)
	at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:1763)
	at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1822)
	at dotty.tools.dotc.typer.Typer.op1$2(Typer.scala:1854)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1850)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1862)
	at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:1881)
	at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:1910)
	at dotty.tools.dotc.typer.Typer.typedPackageDef(Typer.scala:1623)
	at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1803)
	at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1823)
	at dotty.tools.dotc.typer.Typer.op1$2(Typer.scala:1854)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1850)
	at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1862)
	at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:1922)
	at dotty.tools.dotc.typer.FrontEnd.typeCheck$$anonfun$1(FrontEnd.scala:66)
	at scala.compat.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
	at dotty.tools.dotc.typer.FrontEnd.monitor(FrontEnd.scala:34)
	at dotty.tools.dotc.typer.FrontEnd.typeCheck(FrontEnd.scala:70)
	at dotty.tools.repl.REPLFrontEnd.runOn(ReplFrontEnd.scala:25)
	at dotty.tools.dotc.Run.runPhases$4$$anonfun$4(Run.scala:170)
	at scala.compat.java8.JProcedure1.apply(JProcedure1.java:18)
	at scala.compat.java8.JProcedure1.apply(JProcedure1.java:10)
	at scala.collection.IndexedSeqOptimized.foreach(IndexedSeqOptimized.scala:32)
	at scala.collection.IndexedSeqOptimized.foreach$(IndexedSeqOptimized.scala:29)
	at scala.collection.mutable.ArrayOps$ofRef.foreach(ArrayOps.scala:191)
	at dotty.tools.dotc.Run.runPhases$5(Run.scala:185)
	at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:193)
	at scala.compat.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
	at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:88)
	at dotty.tools.dotc.Run.compileUnits(Run.scala:200)
	at dotty.tools.dotc.Run.compileUnits(Run.scala:141)
	at dotty.tools.repl.ReplCompiler.runCompilationUnit(ReplCompiler.scala:188)
	at dotty.tools.repl.ReplCompiler.compile(ReplCompiler.scala:197)
	at dotty.tools.repl.ReplDriver.compile(ReplDriver.scala:229)
	at dotty.tools.repl.ReplDriver.interpret(ReplDriver.scala:202)
	at dotty.tools.repl.ReplDriver.loop$1(ReplDriver.scala:150)
	at dotty.tools.repl.ReplDriver.runUntilQuit$$anonfun$1(ReplDriver.scala:154)
	at dotty.tools.repl.ReplDriver.withRedirectedOutput$$anonfun$2$$anonfun$1(ReplDriver.scala:163)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
	at scala.Console$.withErr(Console.scala:192)
	at dotty.tools.repl.ReplDriver.withRedirectedOutput$$anonfun$1(ReplDriver.scala:163)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
	at scala.Console$.withOut(Console.scala:163)
	at dotty.tools.repl.ReplDriver.withRedirectedOutput(ReplDriver.scala:163)
	at dotty.tools.repl.ReplDriver.runUntilQuit(ReplDriver.scala:154)
	at dotty.tools.repl.Main$.main(Main.scala:6)
	at dotty.tools.repl.Main.main(Main.scala)

[sstucki]

And what if they're defined in different scopes and merged by intersection? What should be the resulting variance?

If two types are in the same "kind class", they are ordered by subtyping (as alluded to by @odersky) and similarly for their variances. Both types and variances form a bounded lattice (at least in theory), so there's always a good candidate for the GLB and LUB of the kinds of types in the same "kind class".

In your example, the type members T declared in A and B

trait A { type T[-X] }
trait B { type T[+X] }

are in the same "kind class" * -> * and hence they should have a common signature. Theory tells us that the declared kinds (-*) -> * and (+*) -> * should have both a LUB and a GLB, but unfortunately, Scala doesn't have a name for the LUB of + and -. In the literature, that variance is often called "constant" (see e.g. Martin Steffen's thesis on polarized higher-order subtyping). This makes sense intuitively: any concrete instance (v: A & B) must implement v.T in such a way that v.T[X] varies both co- and contravariantly in X, which is clearly true if v.T[X] does not depend on X at all.

(...) This would allow "kind classes" to include the whole kind. If you only include arities, how sure are we the compiler handles well the intersection of type members with different arities, or that the result is sound?

Types with different arities are in different "kind classes", and hence distinguished by overloading resolution. Because they are distinct, there is no intersection — that's precisely the point.

The bug you found seems unrelated. The line that causes the error is Test.coerceTArg(v.M), i.e. you're trying to pass a type member v.M where a value is expected. Of course the compiler should flag this more gracefully, you probably want to report this as a separate issue.

A note on terminology. I'm really not a fan the term "kind class" because it sounds like it's the analogue of a "type class" on the kind level, which it is definitely not. Personally, I prefer the terms "simple kind" and "simplified kind", i.e. the analogues of "simple types" (as in "the simply typed lambda calculus"), which is precisely what they are. The process of computing the simplified version of a kind is then just "simplification" (though others call it "erasure"). Just my 5cents.

[LPTK]

@sstucki

A note on terminology. [...] I prefer the terms "simple kind" and "simplified kind" [...] The process of computing the simplified version of a kind is then just "simplification"

The concept of simplification does not normally involve a loss of information (the simplified form should be equivalent), but there is a loss of information here. So this seems closer to an "erasure" process indeed. In fact, the analogy is very apt: just like you can't overload two methods with the same type erasure, you cannot overload two types with the same kind erasure!

[smarter]

Closing as I think this proposal has been abandoned, but feel free to reopen if there's still interest.