Scala Type Inference Not Working for GADTs in IntelliJ

user_337546 0
Viewed 56

Following code does not appear as compiling in IntelliJ. It is complaining that the type returned from the eval should be A where I would expect it to infer during usage. The code compiles fine using sbt but does not compile on IntelliJ with both Scala version 2 and 3 (it runs fine but shows error message in code). Is there a special configuration (e.g. sbt params, jvm args etc) that is required for code below to appear as compiled on IntelliJ?

  object Solution1 {
    trait Expr[A]
    case class B(bool: Boolean) extends Expr[Boolean]
    case class I(i: Int) extends Expr[Int]

    def eval[A](expr: Expr[A]): A = expr match {
      case B(b) => b
      case I(i) => i
    }
  }
gadt intellij-idea scala
1 Answers

Generalized algebraic data types (GADTs) are known to be extremely difficult to implement correctly in Scala. AFAIK both the scalac and dotty compilers currently have type soundness holes, particularly using covariant GADTs.

Your eval should return a value of type T, but since i has type Int and b has type Boolean, it seems the compiler is able to see that because I is a subtype of Expr[Int], T must be equal to Int and then T must be equal to Boolean in the same way.

I am surprised this type checks. It's odd because one would expect T to keep it's meaning. It seems Scala 2's GATDs implementation is still faulty.

I'm not surprised Intellij's Scala Plugin flags it red. You can report this, but I'm not sure whether they can do anything about it as it seems Scala is flawed here for the time being. It needs special treatment for them.

user_22050890
Related