Lack of type refinement for match case #15958
Description
Compiler version
3.1.3
Minimized code
sealed trait NatT case class Zero() extends NatT case class Succ[N<: NatT](n: N) extends NatT trait IsLessThan[M <: NatT, N <: NatT] object IsLessThan: given base[M <: NatT]: IsLessThan[M, Succ[M]]() given weakening[N <: NatT, M <: NatT] (using IsLessThan[N, M]): IsLessThan[N, Succ[M]]() given reduction[N <: NatT, M <: NatT] (using IsLessThan[Succ[N], Succ[M]]): IsLessThan[N, M]() sealed trait UniformTuple[Length <: NatT, T]: def apply[M <: NatT](m: M)(using IsLessThan[M, Length]): T case class Empty[T]() extends UniformTuple[Zero, T]: def apply[M <: NatT](m: M)(using IsLessThan[M, Zero]): T = throw new AssertionError("Uncallable") case class Cons[N <: NatT, T](head: T, tail: UniformTuple[N, T]) extends UniformTuple[Succ[N], T]: def apply[M <: NatT](m: M)(using proof: IsLessThan[M, Succ[N]]): T = m match case Zero() => head case Succ(predM): Succ[predM] => tail(predM)(using IsLessThan.reduction(using proof))Output
Found: (proof : IsLessThan[M, Succ[N]]) Required: IsLessThan[Succ[predM], Succ[N]]Expectation
The code is expected to compile, as within that case branch, M is identified with Succ[predM].
I opened a discussion thread on contributors.scala-lang.org about this, but didn't get any answer. So I'm tentatively filing this as a bug.