Understanding the limits of Scala GADT support

问题:

The error in Test.test seems unjustified:

sealed trait A[-K, +V]
case class B[+V]() extends A[Option[Unit], V]

case class Test[U]() { 
  def test[V](t: A[Option[U], V]) = t match {
    case B() => null // constructor cannot be instantiated to expected type; found : B[V] required: A[Option[U],?V1] where type ?V1 <: V (this is a GADT skolem)
  }
  def test2[V](t: A[Option[U], V]) = Test2.test2(t)
}

object Test2 {
  def test2[U, V](t: A[Option[U], V]) = t match {
    case B() => null // This works
  }
}

There are a couple ways to make the error change, or go away:

If we remove the V parameter on trait A (and case class B), the 'GADT-skolem' part of the error goes away but the 'constructor cannot be instantiated' part remains.

If we move the U parameter of the Test class to the Test.test method, the error goes away. Why ? (Similarly, the error is not present in Test2.test2)

The following link also identifies that problem, but I do not understand the provided explanation. http://lambdalog.seanseefried.com/tags/GADTs.html

Is this an error in the compiler ? (2.10.2-RC2)

Thank you for any help with clarifying that.

---

2014/08/05: I have managed to further simplify the code, and provide another example where U is bound outside the immediate function without causing a compilation error. I still observe this error in 2.11.2.

sealed trait A[U]
case class B() extends A[Unit]

case class Test[U]() {
  def test(t: A[U]) = t match {
    case B() => ??? // constructor cannot be instantiated to expected type; found : B required: A[U]
  }
}

object Test2 {
  def test2[U](t: A[U]) = t match {
    case B() => ??? // This works
  }
  def test3[U] = {
    def test(t: A[U]) = t match {
      case B() => ??? // This works
    }
  }
}

Simplified like that this looks more like a compiler bug or limitation. Or am I missing something ?

回答1:

Constructor patterns must conform to the expected type of the pattern, which means B <: A[U], a claim which is true if U is a type parameter of the method presently being called (because it can be instantiated to the appropriate type argument) but untrue if U is a previously bound class type parameter.

You can certainly question the value of the "must conform" rule. I know I have. We generally evade this error by upcasting the scrutinee until the constructor pattern conforms. Specifically,

// Instead of this
def test1(t: A[U]) = t match { case B() => ??? }

// Write this
def test2(t: A[U]) = (t: A[_]) match { case B() => ??? }

Addendum: in a comment the questioner says "The question is simple on why it doesn't works with type parameter at class level but works with at method level." Instantiated class type parameters are visible externally and have an indefinite lifetime, neither of which is true for instantiated method type parameters. This has implications for type soundness. Given Foo[A], once I'm in possession of a Foo[Int] then A must be Int when referring to that instance, always and forever.

In principle you could treat class type parameters similarly inside a constructor call, because the type parameter is still unbound and can be inferred opportunistically. That's it, though. Once it's out there in the world, there's no room to renegotiate.

One more addendum: I see people doing this a lot, taking as a premise that the compiler is a paragon of correctness and all that's left for us to do is ponder its output until our understanding has evolved far enough to match it. Such mental gymnastics have taken place under that tent, we could staff Cirque de Soleil a couple times over.

scala> case class Foo[A](f: A => A)
defined class Foo

scala> def fail(foo: Any, x: Any) = foo match { case Foo(f) => f(x) }
fail: (foo: Any, x: Any)Any

scala> fail(Foo[String](x => x), 5)
java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
  at $anonfun$1.apply(<console>:15)
  at .fail(<console>:13)
  ... 33 elided

That's the current version of scala - this is still what it does. No warnings. So maybe ask yourselves whether it's wise to be offering the presumption of correctness to a language and implementation which are so trivially unsound after more than ten years of existence.

回答2:

Looks like it is a compiler caveat. From this, martin odersky puts it as:

In the method case, what you have here is a GADT: 
Patterns determine the type parameters of an corresponding methods in the scope of a pattern case.     
GADTs are not available for class parameters.    

As far as I know, nobody has yet explored this combination, and it looks like it would be quite tricky to get this right.

PS: Thanks to @retronym who provided the reference from discussion here

---

On why it throws an error in case of class:

This works:

sealed trait A[-K, +V]
case class B[+V]() extends A[Option[Unit], V]
case class Test[U]() {

   def test[V, X <: Unit](t: A[Option[X], V]) = t match {
     case B() => null
   }
   def test2[V](t: A[Option[U], V]) = Test2.test2(t)
}

object Test2 {
      def test2[U, V](t: A[Option[U], V]) = t match {
         case B() => null // This works
       }
 }

To examplain why the compiler threw an error: Try doing this:

scala> :paste
// Entering paste mode (ctrl-D to finish)

abstract class Exp[A]{
        def eval:A = this match {
            case Temp(i) => i     //line-a
          }
        }
case class Temp[A](i:A) extends Exp[A]

// Exiting paste mode, now interpreting.

To understand this, from §8.1.6: above Temp is a polymorphic type. If the case class is polymorphic then:

If the case class is polymorphic, then its type parameters are instantiated so that the instantiation of c conforms to the expected type of the pattern. The instantiated formal parameter types of c’s primary constructor are then taken as the expected types of the component patterns p 1 , . . . , p n . The pattern matches all objects created from constructor invocations c(v1 , . . . , v n ) where each element pattern p i matches the corresponding value v i .

i.e. the compiler smartly tries to instantiate Temp in line-a such that it conforms to the primary constructor of this( which if above compiled successfully then in case of Temp(1) would be something like Exp[Int] and hence compiler instantiates Temp in line-a with parameter as Int.

---

Now in our case: the compiler is trying to instantiate B. It sees that t is of type A[Option[U],V] where U is already fixed and obtained from class parameter and V is generic type of method. On trying to initialize B it tries to create in such a way that it ultimately gets A[Option[U],V]. So with B() it is somehow trying to get A[Option[U],V]. But it cant as B is A[Option[Unit],V]. Hence it ultimately cannot initialize B. Fixing this makes it work

---

Its not required in case of test-2 because: The compiler as explained in above process is trying to initialize type parameter of B. It knows t has type parameter [Option[U], V] where U and V are both generic wrt method and are obtained from argument. It tries to initialize B based on the agrument. If the argument was new B[String] it tries deriving B[String] and hence U is automatically obtained as Option[Unit]. If the argument was new A[Option[Int],String] then it obviously it wont match.

回答3:

The difference has to do with what information the compiler and runtime have in each case, combined with what the restrictions on the types are. Below the ambiguity is clarified by having U be the trait and class parameter, and X be the method type paramter.

sealed trait A[U]
case class B(u: Unit) extends A[Unit]

class Test[U]() {
  def test(t: A[U]) = t match {
    case B(u) => u // constructor cannot be instantiated to expected type; found : B required: A[U]
  }
}

object Test2 {
  def test2[X](t: A[X]) = t match {
    case B(x) => x // This works
  }
  def test3[X] = {
    def test(t: A[X]) = t match {
      case B(x) => x // This works
    }
  }
}

Test2.test2(new B(println("yo")))

In Test2.test2, the compiler knows that an instance of A[X] will be provided, with no limits on X.It can generate code that inspects the parameter provided to see if it is B, and handle the case.

In class Test method test, the compiler knows not that some A[X] is provided when called, but that some specific type, U, is presented. This type U can be anything. However, the pattern match is on an algebraic data type. This data type has exactly one valid variation, of type A[Unit]. But this signature is for A[U] where U is not limited do Unit. This is a contradiction. The class definition says that U is a free type parameter, the method says it is Unit.

Imagine you instantiate Test:

val t = new Test[Int]()

Now, at the use site, the method is:

def test(t: A[Int])

There is no such type A[Int]. Pattern matching on B is when the compiler inspects this condition. A[U] for any U is incompatible with the type, hence "constructor cannot be instantiated to expected type; found : B required: A[U]"

The difference with the method versus class type parameter is that one is bound while one is free, at the time the method is called in the runtime.

Another way to think about it is that defining the method

def test(t: A[U])

implies that U is Unit, which is inconsistent with the class declaration that U is anything.

回答4:

Edit: this is not an answer to the question. I'm keeping it for reference (and the comments).

---

The link you provided already gives the answer.

In the case of the parameterised method, U is infered from the argument of the actual method call. So, the fact that the case B() was chosen implies that U >: Unit (otherwise the method could not have been called with a B) and the compiler is happy.

In the case of the parameterized class, U is independent from the method argument. So, the fact that the case B() was chosen tells the compiler nothing about U and it can not confirm that U >: Unit. I think if you add such a type bound to U it should work. I haven't tried it, though.

回答5:

The compiler is absolutely correct with its error message. An easy example should describe the issue well:

sealed trait A[U]
class B extends A[Unit]

class T[U] {
  val b: A[Unit] = new B
  f(b) // invalid, the compiler can't know which types are valid for `U`
  g(b) // valid, the compiler can choose an arbitrary type for `V`

  def f(t: A[U]) = g(t)
  def g[V](t: A[V]) = ???
}

f and g have different type signatures. g takes an A[V] where V is an arbitrary type parameter. On the other hand, f takes an A[U] where U is not arbitrary but dependent from the outer class T.

The compiler does not know what type U can be at the moment when it typechecks T - it needs to typecheck an instantiation of T to find out which types are used. One can say that U is a concrete type inside of T, but a generic type outside of it. This means it has to reject every code fragment that gets inside of T more concrete about the type of U.

Calling g from inside f is clearly allowed - after all an arbitrary type for V can be chosen, which is U in this case. Because U is never again referenced in g it doesn't matter what type it may have.

Your other code example underlies the same limitations - it is just an example that is more complex.

Btw, that this code

def test3[U] = {
  def test(t: A[U]) = t match {
    case B() => ??? // This works
  }
}

is valid looks weird to me. It doesn't matter if U is bound by a class or a method - from inside of the binding scope we can't give any guarantees about its type, therefore the compiler should reject this pattern match too.