当使用scala路径依赖类型作为函数共域时，为什么无法为该函数添加别名？

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）

所以我们甚至不能声明单个类型的变量P#Repr。

它看起来与错误类似：

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

• 11910. 当使用具体子类型V参数化时，使用A包含成员类型的类型参数化的类型构造T函数无法解析TA

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

它来自存在主义类型的斯科莱姆化

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)