When using scala path dependent type as function codomain, why is it impossible to add alias for that function?

Question

Here is a simple example:

trait Proposition[T] {
  type Repr = T
}

trait Scope {

  type OUT

  type Consequent = Proposition[_ <: OUT]

  abstract class Proof[-I, +P <: Consequent] {
    final def instanceFor(v: I): P#Repr = ???
    final def apply(v: I): P#Repr = instanceFor(v)
  }
}

This gives the compilation error:

[Error] ....scala:44: type mismatch;
 found   : _$1(in type Consequent)
 required: (some other)_$1(in type Consequent)

Where does this (some other) come from? Is it a compiler bug caused by a clear rule of type selection (which should be theoretically solved in scala 3)?

UPDATE 1 Sorry I just realised that P#Repr should not be called type selection, which should only refers to val p: P;p.Repr, now it added even more confusion because:

• I don't even know the name of this grammar, yet I kept using it for a long time

• It is not even defined in DOT calculus. So scala 3 support is questionable

Answer 1

Looks like a bug.

I minimized your code till

trait Proposition[T] {
  type Repr = T
}

trait Scope {
  type Consequent = Proposition[_]

  abstract class Proof[P <: Consequent] {
    val instanceFor: P#Repr = ??? // doesn't compile
      // type mismatch;
      // found   : Proof.this.instanceFor.type (with underlying type _$1)
      // required: _$1
  }
}

https://scastie.scala-lang.org/DmytroMitin/DNRby7JGRc2TPZuwIM8ROA/1 (Scala 2.13.6)

So we can't even declare a single variable of type P#Repr.

It seems similar to bugs:

• 2346. Type error with type members and existential types in type bounds (open since 11 Sep 2009, Scala 2.8.0)

• 11910. Type constructor V parameterized with a type A including a member type T does not resolve T when parameterized with a concrete subtype of A

---

Where does this (some other) come from?

It comes from skolemization of an existential type

https://scala-lang.org/files/archive/spec/2.13/03-types.html#existential-types

https://en.wikipedia.org/wiki/Skolem_normal_form

Proposition[_] is a shorthand for Proposition[T] forSome { type T <: OUT }. If you replace Proposition[_] with the latter then the error message will be

type mismatch;
 found   : T(in type Consequent)
 required: (some other)T(in type Consequent)
      final def apply(v: I): P#Repr = instanceFor(v)