Understanding the limits of Scala GADT support

Question

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 ?

Ideation

Have you tried reformulating your implementation in terms of type classes? see GADT vs. Type Classes @ Lambda the Ultimate. – Lutestring

I have not, but I suspect this would not help in Scala. Scala's encoding of type classes would still result in a GADT. – Pooch

I meant that perhaps Scala's type classes don't suffer from the compiler limitations you seemed to be struggling with. – Lutestring

Answer 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.

Gettysburg

Thanks. The upcast trick is interesting, but gaining information on the class type parameter was my actual goal here, so I'll have to look for a different approach. – Pooch

You've helped clarify to some degree why the class parameter is different, yet I still do not fully appreciate the soundness risk. This is going beyond the original question, but any further pointers on the issue would be interesting. It seems to me that the class type parameters can easily be made less precise by upcasting, and as long as pattern matching discovers valid evidence, it should be possible to make them more precise. – Pooch

That is a "covariance-centric" perspective. Type parameters move in both directions. A more specific type in a positive position is a less specific type in a negative position. You can't pattern match your way back to static types. For instance, class Foo[A](f: A => A). That A can't move even a little, and you can't recover it by throwing pattern matching at it since there is nothing tangible to inspect. – Gettysburg

By the way, martin saying something doesn't mean it's true, and it definitely doesn't mean it's sound. – Gettysburg

Point taken, this feels safe to me so I'm working around the limitation, simply by calling a function outside the class as shown in my original example. Although the restriction on the class case seems unnecessary because this workaround is available, I'm not complaining that scalac errs on the side of caution in this case. I will assume there is no problem, but I remain very interested in any argument about the unsound nature of this workaround. Thanks again for the upcast trick, it has been useful elsewhere in my code. – Pooch

About the unsound example: it's indeed a baffling flaw in the current system, and it does create a lot of problems in relation to implicits; the compiler infers Any for type parameters of values extracted with a pattern if there is nothing to guide it. For information, the correct way to make the compiler reason about this is the following (and it will rightfully not compile): foo match { case foo: Foo[t] => foo match { case Foo(f) => f(x) } } The error is type mismatch; found: x.type (with underlying type Any); required: t (one can also write _ instead of t) – Guerdon

Answer 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 a 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

---

It's 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 won't match.

Krieger

Why is the bound U <: Unit not required on Test2.test2? – Levina

It doesn't make sense to add an upper bound of Unit to U. This way it is impossible to instantiate it with any other type than Unit, you can leave out the type parameter altogether. – Prothrombin

@sschaef the idea was to show that a bound can help. It can obviously be put at method level instead of class level as edited. But then test can only be called with B then and is a major restriction. – Krieger

Answer 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.

Vouvray

Answer 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.

Levina

Thanks, and sorry for the year-long delay. I do not understand this. It seems to me that type-inference is only relevant for the caller of Test.test, and may not happen at all if explicit types are provided. The implementation just receives a U type, and a value t. Why should the place when U is bound matter ? If Test was covariant in U it might be a more complex argument, but it is not. – Pooch

A is contravariant in K. Therefore, B[V] is only a subtype of A[Option[U], V] if U >: Unit. But in class Test[U], U is not bounded at all, so it does not follow that U >: Unit. This has nothing to do with inference. – Levina

In the second case (Test2.test2), if the method is called with some B[U], then obviously U >: Unit. – Levina

Thanks again. Still puzzled. Somehow the compiler doesn't want to learn more information about U (when presented with evidence) if it is a parameter of the class, but accepts it if it is a parameter of the method. I do not see the soundness risk in accepting the evidence in both cases, but perhaps there is. Or perhaps this is only a temporary limitation ? – Pooch

What happens if you instantiate Test[Int]? Now the test[V] method is trying to match an A[Option[Int], V] against a B[V] which is a type error. – Levina

I would have guessed the only consequence to be that you wouldn't be able to provide the B to call into Test.test. That would be analogous to not being able to call Test2.test2[Int, V]. – Pooch

You're right, my answer is nonsense. It has nothing to do with U! For some reason, the V in test[V] cannot be unified with the (implicit) V in the pattern match on B. The compiler thinks the latter could be some supertype of the parameter V (hence the error message). I don't know the answer to your question, unfortunately. – Levina

Answer 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.

Prothrombin

-1. This answer absolutely does not explain the reason for it. The question is simple on why it doesn't works with type parameter at class level but works with at method level. Moreover there is no reasoning on why it fails at B() in one of the case (has got to do with pattern finder as mentioned by @jatin) – Transnational