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?

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)