Further GADT issues

[Blaisorblade]

So here's an example with a bunch of GADT issues; they should be diagnosed and minimized.

import scala.collection.generic.CanBuildFrom

sealed trait Exp[T]
case class IntLit(n: Int) extends Exp[Int]

case class GenLit[T](t: T) extends Exp[T]
case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int]
case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T]
case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]

case class MapS[S, T](xs: Exp[List[S]], f: Exp[S => T]) extends Exp[List[T]]
case class Map[S, T, That](xs: Exp[List[S]], f: Exp[S => T])(implicit val cbf: CanBuildFrom[List[S], T, That]) extends Exp[That]
//def map[B, That](f: (A) ⇒ B)(implicit bf: CanBuildFrom[List[A], B, That]): That

object Interpreter {
  def eval[T](e: Exp[T]): T = e match {
    case IntLit(n) => // Here T = Int and n: Int
      n

    case gl: GenLit[_]     => // Here in fact gl: GenLit[T]

      // the next line was incorrectly allowed before the fix to https://github.com/lampepfl/dotty/issues/1754:
      //val gl1: GenLit[Nothing] = gl

      gl.t

    case Plus(e1, e2) =>
      // Here T = Int and e1, e2: Exp[Int]
      eval(e1) + eval(e2)

    // The next cases triggered warnings before the fix to
    // https://github.com/lampepfl/dotty/issues/3666

    case f: Fun[s, t]  => // Here T = s => t
      //val f1: Exp[Nothing] => Exp[Nothing] = f.f
      (v: s) => eval(f.f(GenLit(v)))

    case App(f, e)     => // Here f: Exp[s, T] and e: Exp[s]
      eval(f)(eval(e))

    case m @ Map(xs, f)    =>
      //val f1: Exp[Any => Any] = f // spuriously accepted by Scalac, rejected by Dotty.
      eval(xs).map(eval(f))(m.cbf)
    // case MapS(xs, f) =>
    //   eval(xs) map eval(f) // accepted by Scalac, spuriously (?) rejected by Dotty
    case m: MapS[s, t] =>
      //(eval(m.xs) map eval(m.f))(List.canBuildFrom) //fails in Dotty
      (eval(m.xs) map eval(m.f))(List.canBuildFrom[t]) //succeeds in Dotty
  }

  def betaReduce[T](e: Exp[T]): Exp[T] = e match {
    case App(Fun(f), arg) => f(arg)
    case _ => e
  }
}

• eval(xs) map eval(f) seems to fail because of GADT bounds are not precise enough #4075

• I wild-guess that (eval(m.xs) map eval(m.f))(List.canBuildFrom) might not be able to infer t because it's not "frozen" yet — errors in Add test to close #3666, problems with typechecking GADTs #4069 complain about that.

• the body of eval(Fun(...)) must give a type annotation to v, writing (v: s) => eval(f.f(GenLit(v))). Since the typechecker knows the result type is T and that T = s => t, this annotation should not be necessary; @smarter suggested this might be because the GADT bounds are stored separately and the typechecker would have to look at them, which should be doable.

  I'd expect to be able to write instead:

case Fun(f) =>
  v => eval(f(GenLit(v)))

[Blaisorblade]

See also #4176.

[abgruszecki]

Notes about eval(xs) map eval(f):

Implicit search does not appear to look in GADT bounds. Correct bound is inferred on the side of GADTMap (that T := List[MapS#T]). Making MapS#T an explicit member and explicitly annotating the result of map as List[MapS#T] lets the code compile.

Here's a much smaller example, which does not compile in Dotty either, but is compiled by Scalac:

 sealed trait Expr[T]
object IntExpr extends Expr[Int]
implicit val i: Int = 0

def test[T](e: Expr[T]): T = e match { case IntExpr => implicitly }