Home > Software design >  Scala Type Inference Not Working for GADTs in IntelliJ
Scala Type Inference Not Working for GADTs in IntelliJ

Time:08-20

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
    }
  }

CodePudding user response:

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.

  • Related