Scala 3基于match类型的类型函数类型相等性证明异常

问题根因 #

该异常是3.0.0-RC3预发布版本中match类型实现的特定缺陷，核心逻辑问题如下：

• 纯type关键字声明的无具象实体锚点的抽象类型（无对应trait、类、单例对象作为类型来源），在编译器类型系统中仅带有子类型约束，不存在编译器可自动识别的互不相交子类型边界。
• 该版本的match类型在处理这类无锚点抽象类型时，分支匹配不会做精确的类型相等性校验，仅按分支顺序，只要待匹配类型和分支模式类型同属上层约束的子类型集合，就直接采用该分支的返回类型做规约，不会校验后续精确匹配分支。
• 这就解释了分支顺序和失败场景的强关联：比如Neg的分支顺序为case True => False在前时，编译器遇到Neg[False]的类型规约，会因为False和True同属Bool的子类型集合，模糊将False归入第一个True的匹配分支，最终规约得到Neg[False]为False，自然无法通过Neg[False] =:= True的校验；调换分支顺序后，False分支在前，True的规约就会被错误归入前一分支，导致对应场景失败。
• 更换为trait+类、trait+单例对象类型别名的定义方式后，True和False是带有具象实体锚点、编译器明确判定为互不相交的封闭子类型，match类型的精确匹配逻辑可正常生效，因此不会出现规约错误。

保留原有纯抽象type定义的解决方案 #

• 调整match类型的分支判定逻辑，将原本的裸类型子类型匹配改为强制精确相等匹配，消除模糊判定空间：

  type Neg[B <: Bool] <: Bool = B match
    case b if b =:= True => False
    case b if b =:= False => True
  

  这种写法会强制编译器对每个分支做待匹配类型和模式类型的相等性校验，不会因子类型归属模糊错配分支。
• 绕开编译器的自动match类型规约，显式手写两个场景的等价性隐式证明：

  // 直接提供Neg类型和目标类型的等价实例
  given negTrueProof: Neg[True] =:= False = =:=.tp
  given negFalseProof: Neg[False] =:= True = =:=.tp
  

  由于纯抽象类型本身没有内置的规约规则，编译器会直接使用你提供的隐式证明完成summon操作，完全不会触发match类型的错误分支匹配。
• 给原有抽象类型补全互不相交的约束声明，给编译器明确的类型边界提示：

  type Bool
  type True <: Bool
  type False <: Bool
  
  // 显式声明两个子类型不存在交集，消除模糊判定的可能
  given trueNeqFalse: True =!= False = =!=.tp
  

  该约束会明确告知编译器True和False是完全不相交的类型，match类型的分支匹配就不会将两个类型模糊归为同一类。

内容的提问来源于stack exchange，提问作者Duduk