enum EQ[A, B]:
case Refl[A]() extends (A `EQ` A)
object EQ:
given [A]: (A `EQ` A) = Refl()
import EQ.*
// Case 1
def f[A, B, C]: (A, A `EQ` B, B `EQ` C) => C =
case (a, Refl(), Refl()) => a // ok
def g[F[_], A, B]: (A, A `EQ` F[B]) => F[B] =
case (a, Refl()) => a // ok
def h[F[_], A, B, C]: (A, A `EQ` F[B], F[B] `EQ` F[C]) => F[C] =
case (a, Refl(), Refl()) => a // error
// Case 2
enum Nat:
case Z
case S[N <: Nat](n: N)
object Nat:
type Z = Z.type
enum Foo[A]:
case Bar extends Foo[Nat.Z]
def check[M <: Nat, N <: Nat](m: Foo[M], n: Foo[N]): Option[M `EQ` N] = (m, n) match
case (Foo.Bar, Foo.Bar) => Some(Refl()) // ok
def check[M <: Nat, N <: Nat](m: M, n: N): Option[M `EQ` N] = (m, n) match
case (Nat.Z, Nat.Z) => Some(Refl()) // error
After doing some research, I will try to answer my own questions here, so that it can help others who have similar experiences.
It is important to note that all of the above compilation successes are due to GADT-style reasoning.[1] This allows compiler to record some GADT constraints from pattern matching.[2] Then, these constraints will be an important basis for compiler to insert type casting,[3] and it’s similar to the following[4]:
def g[F[_], A, B]: (A, A `EQ` F[B]) => F[B] =
case (a, Refl()) => a.asInstanceOf[F[B]] // ok
From the above, we can see that the compilation failure in the two cases is due to the lack of valid GADT constraints as a basis, and the compiler fails to insert type casting. Specifically,
In the second case, Nat is not a GADT, and no GADT constraints can be recorded[5];
The first case is more complicated. When the compiler checks whether EQ.Refl[A] is a subclass of EQ[F[B], F[C]], it gets a negative result, see the details from the DEBUG CONSOLE[6]:
"debug
==> EQ.Refl[A] <: EQ[F[B], F[C]]
==> EQ[A, A] <: EQ[F[B], F[C]]
==> F[C] <: F[B]
==> B <: C
==> B <: Nothing in frozen constraint
==> Any <: Nothing in frozen constraint = false
==> Any <: Nothing in frozen constraint = false
==> Any <: C
==> Any <: Nothing in frozen constraint = false
==> Any <: C in frozen constraint
==> Any <: Nothing in frozen constraint = false
==> Any <: F[B] = false
==> Any <: F[B] = false
==> Any <: F[B] = false
==> Any <: F[B] = false"
So, no constraints can be recorded either.
As for why the result is negative, and more specifically, why it is necessary to check B <: C, I still don’t quite understand it. I hope someone with knowledge can give me an answer.
At least this makes me know that the more appropriate solution for the first case is:
def h[F[_], A, B, C]: (A, A `EQ` F[B], B `EQ` C) => F[C] =
case (a, Refl(), Refl()) => a // ok