scala - 当使用 scala 路径依赖类型作为函数 codomain 时，为什么不能为该函数添加别名？

Question

这是一个简单的例子:

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)
  }
}

这给出了编译错误:

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

这个在哪里 (some other)来自？是否是由明确的类型选择规则引起的编译器错误(理论上应该在scala 3中解决)？
更新 1 抱歉，我才意识到 P#Repr不应称为类型选择，应仅指 val p: P;p.Repr ，现在它增加了更多的困惑，因为:

我什至不知道这个语法的名字，但我一直使用它很长时间

它甚至没有在 DOT 演算中定义。所以 Scala 3 的支持是有问题的

Answer 1

看起来像一个错误。
我最小化你的代码直到

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 (斯卡拉 2.13.6)
所以我们甚至不能声明一个 P#Repr 类型的变量.
它似乎类似于错误:

2346. Type error with type members and existential types in type bounds (自 2009 年 9 月 11 日起开放，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?

它来自存在类型的 skolemization
https://scala-lang.org/files/archive/spec/2.13/03-types.html#existential-types
https://en.wikipedia.org/wiki/Skolem_normal_form Proposition[_]是 Proposition[T] forSome { type T <: OUT } 的简写.如果更换 Proposition[_]使用后者，则错误消息将是

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