Skip to content

Regression since 3.0.0-M1: implicit evidence using result of match types is not found #12093

@MaximeKjaer

Description

@MaximeKjaer

Compiler version

3.0.0-RC1 and 3.0.0-RC2

Minimized code

import scala.compiletime.ops.int.{`*`, +}

// HList
sealed trait Shape
final case class #:[H <: Int & Singleton, T <: Shape](head: H, tail: T) extends Shape
case object Ø extends Shape
type Ø = Ø.type

// Reduce
def reduce[T, S <: Shape, A <: Shape](shape: S, axes: A): Reduce[S, A, 0] = ???
type Reduce[S, Axes <: Shape, I <: Int] <: Shape = S match {
  case head #: tail => Contains[Axes, I] match {
    case true => Reduce[tail, Remove[Axes, I], I + 1]
    case false => head #: Reduce[tail, Axes, I + 1]
  }
  case Ø => Axes match {
    case Ø => Ø
    // otherwise, do not reduce further
  }
}
type Contains[Haystack <: Shape, Needle <: Int] <: Boolean = Haystack match {
  case Ø => false
  case head #: tail => head match {
    case Needle => true
    case _ => Contains[tail, Needle]
  }
}
type Remove[From <: Shape, Value <: Int] <: Shape = From match {
  case Ø => Ø
  case head #: tail => head match {
    case Value => Remove[tail, Value]
    case _ => head #: Remove[tail, Value]
  }
}

// Reshape
def reshape[From <: Shape, To <: Shape](from: From, to: To)
  (using ev: NumElements[From] =:= NumElements[To]): To = ???
type NumElements[X <: Shape] <: Int = X match {
  case Ø => 1
  case head #: tail => head * NumElements[tail]
}

// Test cases
val input = #:(25, #:(256, #:(256, #:(3, Ø))))
val reduced = reduce(input, #:(3, #:(1, #:(2, Ø))))
val reshaped: 5 #: 5 #: Ø = reshape(reduced, #:(5, #:(5, Ø)))

Output

[error] -- Error: /home/maxime/code/dotty-bug-report/implicit-ev-not-found/src/main/scala/ImplicitEvNotFound.scala:47:61 
[error] 47 |val reshaped: 5 #: 5 #: Ø = reshape(reduced, #:(5, #:(5, Ø)))
[error]    |                                                             ^
[error]    |Cannot prove that NumElements[
[error]    |  ((25 : Int) #: 
[error]    |    Reduce[(256 : Int) #: (256 : Int) #: (3 : Int) #: 
[error]    |      ImplicitEvNotFound$package.Ø.type
[error]    |    , (3 : Int) #: (1 : Int) #: (2 : Int) #: ImplicitEvNotFound$package.Ø.type, 
[error]    |      (0 : Int)
[error]    |     + (1 : Int)]
[error]    |  )
[error]    |] =:= NumElements[((5 : Int) #: (5 : Int) #: Ø)].
[error] one error found

Expectation

The above code compiles in 3.0.0-M1. It should also compile in 3.0.0-RC1 and 3.0.0-RC2.

Metadata

Metadata

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions