Problem with type checking GADTs

[odersky]

Here's an interpreter for simply typed lambda calculus:

sealed trait Exp[T]
case class Num(n: Int) extends Exp[Int]
case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int]
case class Var[T](name: String) extends Exp[T]
case class Lambda[T, U](x: Var[T], e: Exp[U]) extends Exp[T => U]
case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]

abstract class Env { outer =>
  def apply[T](x: Var[T]): T

  def + [T](xe: (Var[T], T)) = new Env {
    def apply[T](x: Var[T]): T =
      if (x == xe._1) xe._2.asInstanceOf[T]
      else outer(x)
  }
}

object Env {
  val empty = new Env {
    def apply[T](x: Var[T]): T = ???
  }
}

object Test {

  val exp = App(Lambda(Var[Int]("x"), Plus(Var[Int]("x"), Num(1))), Var[Int]("2"))

  def eval[T](e: Exp[T])(env: Env): T = e match {
    case Num(n) => n
    case Plus(e1, e2) => eval(e1)(env) + eval(e2)(env)
    case v: Var[T] => env(v)
    case Lambda(x: Var[s], e) => ((y: s) => eval(e)(env + (x -> y)))
    case App(f, e) => eval(f)(env)(eval(e)(env))
  }

  eval(exp)(Env.empty)
}

When we compile that, we get two mysterious warnings:

-- Warning: STL.scala:32:19 ----------------------------------------------------
32 |        case Lambda(x: Var[s], e) => ((y: s) => eval(e)(env + (x -> y)))
   |             ^^^^^^^^^^^^^^^^^^^^
   |         There is no best instantiation of pattern type Lambda[Any, Any]
   |         that makes it a subtype of selector type Exp[T].
   |         Non-variant type variable U cannot be uniquely instantiated.
   |         (This would be an error under strict mode)
-- Warning: STL.scala:33:16 ----------------------------------------------------
33 |        case App(f, e) => eval(f)(env)(eval(e)(env))
   |             ^^^^^^^^^
   |           There is no best instantiation of pattern type App[Any, T]
   |           that makes it a subtype of selector type Exp[T].
   |           Non-variant type variable T' cannot be uniquely instantiated.
   |           
   |           where:    T  is a type in method eval
   |                     T' is a type variable
   |           
   |           (This would be an error under strict mode)
two warnings found

If we look under the hood we find that these stem from the fact that we somehow miss the right subtype constraints for the Lambda and App cases. I suspect something fundamental is wrong here. I don't have the time to look into it now, but maybe someone who is up-to-speed with GADT matching can?

[odersky]

Just verified that scalac has the same behavior. Specifically, it infers the types of the Lambda arguments to Any, Any, which seems wrong - at least the body argument e should have type T. i.e. the U in the Lambda case should be inferred to be the same as Exp's T.

[allanrenucci]

Related: #2675, #1870. Scalac: scala/bug#6680

[liufengyun]

Maybe I miss something here, it seems to me the compiler is justifiable in both of the two cases above.

In the Lambda case, we only know T = S => U, but we don't know what's the S and U here. Inferring U to T is type-incorrect.

In the App case, we only know the result type of application, but we don't know the argument type.

[ctongfei]

I've been plagued by this for a long time.
Shouldn't we infer an existential type (type member)? For example,

  case f @ Lambda(t, u) =>

should infer t: Var[f.T] and u: Exp[f.U]. (use path-dependent types!)

or if e has type Exp[U],

  case e @ App(f, x) =>

should infer f: Exp[e.T => U] and x: Exp[e.T].

[Blaisorblade]

In the Lambda case, we only know T = S => U, but we don't know what's the S and U here. Inferring U to T is type-incorrect.

In the App case, we only know the result type of application, but we don't know the argument type.

In both cases, GADT pattern matching requires synthesizing fresh type variables (with possible equality or subtyping constraints) and using them to refine the types of members. We don’t need those type variables to be made into type members as @ctongfei proposes, at least not to handle such examples, even though that would be sound. Maybe I can give a hand?

[ctongfei]

@Blaisorblade If I recalled correctly, under Dotty, the encoding of generics for

case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]

would create type member T and U for the class App. (http://guillaume.martres.me/publications/dotty-hk.pdf, Section 2.1)
So why not just use <instance>.T and <instance>.U as the inferred type for the pattern-matched type variables? I guess that they are readily available in the compiler.

[Blaisorblade]

In both cases, GADT pattern matching requires synthesizing fresh type variables (with possible equality or subtyping constraints) and using them to refine the types of members.

Forgot to mention: as usual, such constraints would have to be sound even if we extend the case classes. Here all type parameters are invariant, so this should be easier since we can't write class BadVar[T](x: String) extends Var[T] with Exp[Nothing]; but Dotty must be careful.

@ctongfei Using standard existentials (type variables) over type members seems as easy and more standard for GADTs (http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.119.8094&rep=rep1&type=pdf); Dotty already started doing this I think.

What you say makes some sense and I'm familiar with that work, but in fact, Sec. 8 of that paper explains clearly Dotty actually uses the direct representation in Sec. 4, not the simple encoding in Sec. 3. Sec. 2.1 is about the encoding in core DOT; it also mentions dotty in "The problem is solved in DOT and dotty by a radical reduction", but I wouldn't take that too literally given the rest of the paper. And those type members don't seem to be actually available to the user (see below).

Your proposal sounds plausible, and maybe it would be more expressive (I don't see evidence of that); it's also plausible that it's sound, but to know for sure some theorist would need to look at it for more than 5 minutes (there's one tricky question involved). Using type variables has fewer problems.

> console
scala> trait Exp[T] 
// defined trait Exp
scala> case class Var[T](name: String) extends Exp[T] 
// defined case class Var
scala> Var[Int]("a").T 
1 |Var[Int]("a").T
  |^^^^^^^^^^^^^^^
  |value `T` is not a member of Var[Int]
scala> val i : Var[Int]("a").T = 1 
1 |val i : Var[Int]("a").T = 1
  |                 ^^^
  |                 ';' expected, but string literal found
scala> val v = Var[Int]("a") 
val v: Var[Int] = Var(a)
scala> val i : v.T = 1 
1 |val i : v.T = 1
  |        ^^^
  |type T in class Var cannot be accessed as a member of Var[Int](v) from object rs$line$4.

[liufengyun]

Sure @Blaisorblade , I haven't started working on this, I've assigned to you 👍

[Blaisorblade]

@liufengyun Implementing the ideas in dotty will take a while, but yeah I'd like to give it a serious try. (Assigning to me didn't quite work not sure why). Thanks!

[ctongfei]

@Blaisorblade I'm not an expert on compiler design but I think that my proposal does make it more expressive. I'll show with the following example.

I've been working on a typesafe deep learning system and the core part is backward differentiation, which is a traversal over a computation graph.

Nodes in the computation graph, (i.e. symbolic expressions) are defined here as a GADT:
https://github.com/ctongfei/nexus/blob/master/core/src/main/scala/nexus/Expr.scala

To be brief,

sealed trait Expr[X]
case class Input[X]() extends Expr[X]
case class Param[X](var value: X)(implicit val tag: Grad[X]) extends Expr[X]
case class Const[X](value: X)(implicit val tag: Type[X]) extends Expr[X]
case class App1[X, Y](op: Op1[X, Y], x: Expr[X]) extends Expr[Y]
case class App2[X1, X2, Y](op: Op2[X1, X2, Y], x1: Expr[X1], x2: Expr[X2]) extends Expr[Y]
case class App3[X1, X2, X3, Y](op: Op3[X1, X2, X3, Y], x1: Expr[X1], x2: Expr[X2], x3: Expr[X3]) extends Expr[Y]

When doing backpropagation, we do pattern matching on symbolic expressions.
https://github.com/ctongfei/nexus/blob/master/core/src/main/scala/nexus/exec/Backward.scala#L28

// type of e: Expr[Y]
case e @ App2(o, x1, x2) => o match {  
          case o: Op2[e.Input1, e.Input2, _] =>

Naturally, the un-applied variables o, x1 and x2 should have the following type:

o: Op2[e.X1, e.X2, Y]
x1: Expr[e.X1]
x2: Expr[e.X2]

However Scala 2 currently gives existential types (Expr[_]). The type equality constraint o: Op2[e1, e2, Y]; x1: Expr[e3]; e1 =:= e3 is lost.

I have to use another pattern matching on the second line to make it typecheck, without falling back to using the evil asInstanceOf. Patmat GADT with dependent types solves this kind of problem.

[Blaisorblade]

@ctongfei

The current handling is indeed insufficient, I’ve run into similar issues years ago.
This example doesn't seem to need type members. I think using fresh type variables X1 and X2 instead of type members, with the same type equalities, would give the same result as you want.

One issue would be with writing those type variables explicitly (as you're doing in part) would require type patterns; it would probably non-linear ones (that is, patterns with repeated type variables), which aren’t supported yet. That seems still a smaller extension, though it motivates maybe looking a bit more into members. But I’d still prefer using the standard approach as far as possible.

[ctongfei]

Can we use the same fresh type variables in different type patterns in Dotty? E.g.

case e @ App2(o: Op2[e1, e2, Y], x1: Expr[e1], x2: Expr[e2]) => ....

where fresh type variable e1 and e2 both occurred twice.

[Blaisorblade]

@ctongfei In the second occurrence, I expect you’d need to use e1 with literal backquotes in the current syntax, otherwise you’d bind e1 again. Haven’t tried with Dotty, but that’s indeed a non-linear type pattern, the extension I was hinting at — thanks for adding an example. Scalac didn’t support those last I checked, but we’d need Dotty to accept them — it should both generate such patterns and accept the same ones from the user; and it should notice if the user writes patterns that aren’t implied by GADT constraints. I agree with you we need either this or using the extra type members, but the first looks more localized.

For instance, Dotty can’t (without manifests) check a match against

case e @ App2(o: Op2[e1, e1, Y], x1: Expr[e1], x2: Expr[e1]) =>

and ideally, if you write instead

case e @ App2(o: Op2[e1, e2, Y], x1: Expr[e3], x2: Expr[e4]) =>

we might want to either (kindly) figure out that e1 = e3 and e2 = e4 or (more draconianly) give an error and tell the user to do that in the source (not sure the second will scale to subtyping).

[ctongfei]

Thanks @Blaisorblade for the explanation. Now I understand the issues behind these.

I wonder why Dotty doesn't make the type member accessible to users. If not I would simply do something like

case class App2[_X1, _X2, Y](f: Op2[_X1, _X2, Y], x1: _X1, x2: _X2) extends Expr[Y] {
  type X1 = _X1
  type X2 = _X2
}

to force it to become visible.

[Blaisorblade]

I remember people proposing case class App[type X1, type X2, Y]... to achieve that effect. Not sure on the plans on it.

But adding such type members by default instead of requiring type there would be a breaking change relative to Scala2: something like class FunnyApp extends App2[...] {type X1 = Int} works in Scala2 but wouldn’t work as intended if App2 had type member X1.

[ctongfei]

Thanks. I'd like to see the [type X1, type X2, Y] proposal baked into the language.

[smarter]

I believe this issue has been fixed by #3918, but I'll leave it open until someone makes a PR to turn the example code into positive and negative testcases.

[Blaisorblade]

So #3666 typechecks but causes tons of assertion failures in checks — for instance (http://dotty-ci.epfl.ch/lampepfl/dotty/3469/4):

assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
assertion failure for T <:< T, frozen = false
assertion failure for T <:< T, frozen = false