GADT type equality issue

[radeusgd]

minimized code

final abstract class Z
final abstract class S[N]

sealed abstract class Vec[Len, ElemT]
final case class VNil[E]() extends Vec[Z, E]
final case class VCons[N, E](head: E, tail: Vec[N, E]) extends Vec[S[N], E]

object Vec {
  def vhead[E, N](v: Vec[Succ[N], E]): E = v match {
    case VCons(h, _) => h
  }
}

expectation

The code should compile, instead it gives the following error:

[error] -- [E007] Type Mismatch Error: /home/radeusgd/Projekty/GADTPlayground1/gadt1/Vector.scala:12:24 
[error] 12 |    case VCons(h, _) => h
[error]    |                        ^
[error]    |                        Found:    E$1(h)
[error]    |                        Required: E
[error] one error found
[error] (Compile / compileIncremental) Compilation failed
[error] Total time: 1 s, completed 20 wrz 2019, 13:33:47

[abgruszecki]

@radeusgd I tried to reproduce this and couldn't. The example you pasted here compiles (save for the misspelling in definition of vhead, Succ should be S).

Could you try and reproduce your problem in the REPL of Dotty's current master? You can start it with sbt repl.

[radeusgd]

I tried reproducing it and indeed after changing Succ to S it works. The cause for the issue we discussed was that I had both S[N] and Succ[N] defined and they were mismatched. So it's not a type equality issue, but still the error message is very cryptic. Given

final abstract class Z
final abstract class S[N]
final abstract class Succ[N]

sealed abstract class Vec[Len, ElemT]
final case class VNil[E]() extends Vec[Z, E]
final case class VCons[N, E](head: E, tail: Vec[N, E]) extends Vec[S[N], E]

object Vec {
  def vhead[E, N](v: Vec[Succ[N], E]): E = v match {
    case VCons(h, _) => h
  }
}

the error

10 |    case VCons(h, _) => h
   |                        ^
   |                        Found:    E$1(h)
   |                        Required: E

gives no clue about what's going on (first type argument in Vec[_,_] is mismatched, because VCons gives a Vec[S[N], E] and we are matching a Vec[Succ[N], E], I guess that's why the two E's are instantiated to different types, because the first arguments cannot be unified), but that's probably a different issue?

[abgruszecki]

You're right that the reason for E$1 being created is that it's impossible to make VCons[E$1, N$1] a subtype of Vec[Succ[N], E]. I agree that we should emit a warning here - I'll take a look at it.