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（Scala 2.13.6）

所以我们甚至不能声明一个 type 的变量P#Repr。

它似乎类似于错误：

• 2346.类型成员和类型边界中存在类型的类型错误（自 2009 年 9 月 11 日开放，Scala 2.8.0）

• 11910.使用包含成员类型V的类型参数化的类型构造函数在使用具体子类型参数化时无法解析ATTA

---

这(some other)是从哪里来的？

它来自存在类型的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)