Inconsistent type inferences about GADT constraints

Compiler
1 
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

Is there something I’m not getting?

1 Like
2

I don’t know why some work and not others, but these might help you figure it out (including if it is or not a compiler bug):

  • Check what gets inferred for the type parameter of Refl in those pattern matches
  • Use the compiler option -Xprint:all to see how the program gets transformed
  • Use the compiler option -explain-types and possibly -Yexplain-lowlevel (“When explaining type errors, show types at a lower level.”)
3

Thanks for the advice, but it doesn’t help me to figure out the inconsistent type inferences.

4

It might, for example there might be a Nothing that gets inferred somewhere, and in one case it still works through sub-typing, but not in the other

Apart from that, I can’t help you more (but others might)

5

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

  1. https://abgruszecki.github.io/publication/case-for-dot/ ↩︎

  2. https://github.com/scala/scala3/blob/dbd49886b9c885089e54dd0e98ebeb9a32734387/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L2234 ↩︎

  3. https://github.com/scala/scala3/blob/dbd49886b9c885089e54dd0e98ebeb9a32734387/compiler/src/dotty/tools/dotc/typer/Typer.scala#L4459-L4468 ↩︎

  4. A more precise intermediate state can be observed by scalac -Xprint:typer ... ↩︎

  5. https://dotty.epfl.ch/docs/internals/gadts.html#what-abstract-types-can-have-gadt-constraints-1 ↩︎

  6. Set a breakpoint at PatternTypeConstrainer.scala, then input explained(_.isSubType(pat, scrut), "debug", true) in DEBUG CONSOLE. ↩︎