Nested transparent call does not refine the type

[nicolasstucki]

Minimized code

trait HList
case object HNil extends HList
case class HCons[H, T <: HList](h: H, t: T) extends HList

transparent inline def concat(inline x: HList, inline y: HList): HList =
  inline x match
    case HNil => y
    case HCons(h, t) =>
      val tail = concat(t, y)
      HCons(h, tail)

val d: HCons[Int, HCons[String, HNil.type]] = concat(HCons(1, HNil), HCons("2", HNil))

Output

12 |val d: HCons[Int, HCons[String, HNil.type]] = concat(HCons(1, HNil), HCons("2", HNil))
   |                                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |                          Found:    HCons[Int, HList]
   |                          Required: HCons[Int, HCons[String, HNil.type]]

After typer the code is

    val d: HCons[Int, HCons[String, HNil.type]] = 
      {
        {
          val h: (1 : Int) = 1
          val $elem2: HNil$ = HNil
          val t: HNil$ = $elem2
          val tail: HList = // this type should have beein refined to HCons[String, HNil.type]
            {
              {
                {
                  HCons.apply[String, HNil.type]("2", HNil)
                }
              }
            }
          HCons.apply[Int, HList](h, tail)
        }
      }

Expectation

It should compile

[nicolasstucki]

Minimized to

trait Nat
case object Zero extends Nat
case class Succ[N <: Nat](pred: N) extends Nat

transparent inline def s(inline y: Nat): Nat = Succ(y)

val d: Succ[Zero.type]= s(Zero)

   val d: Succ[Zero.type] = 
      {
        Succ.apply[Nat]( // This type should be refined to Zero.type without modifying the initial elaboration
          {
            Zero
          }
        )
      }

[odersky]

This is a consequence of the fact that nested calls to transparent inline functions are typed with their declared return type, and thereby fix type inference in the enclosing method. After thinking hard about it I believe there's nothing we can do about this, short of going all the way back to untyped transparent functions, which are not semantics preserving and which can fail on expansion.

We should be able to use match types to give a better type to these functions. Unfortunately, that does not work either:

trait HList
case object HNil extends HList
case class HCons[H, T <: HList](h: H, t: T) extends HList

object test:
  type Concat[Xs, Ys <: HList] <: HList = Xs match
    case HNil.type => Ys
    case HCons[x, xs1] => HCons[x, Concat[xs1, Ys]]

  transparent inline def concat[Xs <: HList, Ys <: HList]
      (inline xs: Xs, inline ys: Ys): Concat[Xs, Ys] =
    inline xs match
      case HNil => ys
      case HCons(x, xs1) =>
        val tail = concat(xs1, ys)
        HCons(x, tail)

gives

-- [E007] Type Mismatch Error: i8739-match-types2.scala:13:19 ------------------
13 |      case HNil => ys
   |                   ^^
   |Found:    (ys : Ys)
   |Required: test.Concat[Xs, Ys]
   |
   |where:    Xs is a type in method concat with bounds >: (?1 : HNil.type) and <: HList
   |          Ys is a type in method concat with bounds <: HList
-- [E007] Type Mismatch Error: i8739-match-types2.scala:16:13 ------------------
16 |        HCons(x, tail)
   |        ^^^^^^^^^^^^^^
   |Found:    HCons[H$1, test.Concat[T$1, Ys]]
   |Required: test.Concat[Xs, Ys]
   |
   |where:    T$1 is a type in method concat with bounds <: HList
   |          Xs  is a type in method concat with bounds >: (?2 : HCons[H$1, T$1]) and <: HList
   |          Ys  is a type in method concat with bounds <: HList
2 errors found

@OlivierBlanvillain do you see a way to fix this (either change the code, or improve the match type checking to accept the code?)

[odersky]

An alternative strategy would be to make inferred types be more flexible, using some of the ideas of Georg and Olivier.

The reason the concat example does not work is that it gets augmented with inferred types like this:

transparent inline def concat(inline x: HList, inline y: HList): HList =
  inline x match
    case HNil => y
    case HCons(h, t) =>
      val tail: HList = concat(t, y)
      HCons[h, Hlist](h, tail)  // <--- HList is the problem here

We could fix this if instead of the declared type of a transparent def we pick a type that refers to the call. E.g.

transparent inline def concat(inline x: HList, inline y: HList): HList =
  inline x match
    case HNil => y
    case HCons(h, t) =>
      val tail: TypeOf(concat(t, y)) = concat(t, y)
      HCons[h, TypeOf(concat(t, y))](h, tail) 

Then these TypeOfs can be expanded to the actual type of the expansion of the call, not the declared type. (In practice, the TypeOfs would just contain a pointer to the concat(t, y) tree, not a copy).

It does not stop there. We'd then also have to track these types through (at least) if-then-else, match expressions, and local bindings, which is what Georg and Olivier do(*). Basically, everything that depends on a TypeOf has to become a TypeOf.

If we do this, there are still other questions:

• Overloading resolution: Can it depend on a TypeOf type, which means it might need to be redone on expansion?
• Implicit search: Same question - if it can depend on TypeOf type, it needs to be redone on expansion

In the TypeOf approach I believe the answer to both questions must be no, since we would push far too much complexity into the types.

Overall we can now discern three possible strategies:

• What we have: Inferred types stay as they are. This means that recursive whitebox macros by themselves work only if their declared type is precise enough (e.g. an appropriate match type)
• Using TypeOf. Some examples work, but we cannot rely on overloading resolution or implicit search to be redone. (In fact, for implicit search summonFrom can often provide a solution).
• Redo everything. This is what my previous approach to transparent did. It expanded inline defs as untyped trees, and redid the typechecking on expansion. This is very powerful, but also less predictable.

(*) In fact their work does this tracking also through recursive calls which means that they can compute precise TypeOf types even without expanding the function. The difference is whether TypeOf types
are local to the body a transparent function, or whether they can be the result types of such functions.

There's also a difference how TypeOf is defined. In the scheme sketched here TypeOf(t) would mean "the type of the expansion of t". Since Georg and Olivier do not need to expand, they define TypeOf directly. But the end result is the same.

[odersky]

In fact, the TypeOf approach is not a free lunch either. Consider

transparent inline def f(): Any = 
  ... 
  val h = g(f)
  ...

def g[X](x: X): X => X = ???

What is the type of h? Is it Any => Any or TypeOf(g(f)) => TypeOf(g(f))? Neither of these types is better than the other. If we pick the first, we lose precision in the result. If we pick the second, then
we might have a follow-on call h(1) in the body f that would fail, since we cannot prove that Int <: TypeOf(g(f)). But note that this call would typecheck with the current rules.

A similar problem is for implicit search. Searching an implicit with TypeOf types will often fail when we typecheck the inline def. But if we pick the upper bound for the implicit search instead, this might introduce type errors on expansion.

I think the only feasible strategy is to own up to the TypeOf business immediately. I.e when typechecking a transparent function body, the result of a call to a transparent function f with computed return type F is an abstract type Fx <: F, which is associated with the call. So Fx represents the TypeOf of the call. In the same way, we introduce abstract types for all tree nodes that contain a call to a transparent function. Each abstract type is bounded from above by the type computed normally.

Then we use these types normally in type-checking and type inference.

This might produce errors when typechecking transparent functions. For instance, we might search an implicit of computed type T but since T is the direct or indirect result of a transparent function call we use the abstract type Tx <: T instead. Then implicit search will likely fail, since there will be no implicit matching that abstract type.

This stricter type checking could be annoying but I believe it's better than the alternative. In essence, we tighten the rules for transparent functions to ensure that their expansions will not produce surprisingly weak types. That's better than accepting the transparent function as is and then asking the user to figure out why it did not produce the right type.

[gsps]

Indeed, that's an interesting issue.

I think the only feasible strategy is to own up to the TypeOf business immediately. I.e when typechecking a transparent function body, the result of a call to a transparent function f with computed return type F is an abstract type Fx <: F, which is associated with the call. So Fx represents the TypeOf of the call. In the same way, we introduce abstract types for all tree nodes that contain a call to a transparent function. Each abstract type is bounded from above by the type computed normally.

To clarify, when you say the "type computed normally" you mean F, and, in the above example, it would be "Any => Any"?

Switching to Dotty-internal notation for a second, I'm a bit confused why a tpe = '[ TypeOf(t) ] with tpe.superType == '[ F ] isn't as good as Fx <: F. It seems that Fx wouldn't have any better lower bound than itself anyways, and it'd be more useful to have access to the structure of t, since that at least allows us to decide equality structurally, no? Or does the abstract type interact with the rest of type inference in some beneficial way?

This might produce errors when typechecking transparent functions. For instance, we might search an implicit of computed type T but since T is the direct or indirect result of a transparent function call we use the abstract type Tx <: T instead. Then implicit search will likely fail, since there will be no implicit matching that abstract type.

Agreed, that sounds tricky. Have you considered the option that such singleton types not take part in implicit resolution at all, and we always use the upper bound (T) instead? One could still use singletons to compute Reflect boxes with some type member .S and use that to search for implicits of some computed type.

[OlivierBlanvillain]

The match type version compiles on master when using type test patterns (the only type of pattern that is currently expressible in match types):

sealed trait HList
case class HCons[H, T <: HList](h: H, t: T) extends HList
sealed trait HNil extends HList
case object HNil extends HNil

object Test {
  type Concat[Xs <: HList, Ys <: HList] <: HList = Xs match {
    case HNil => Ys
    case HCons[x, xs1] => HCons[x, Concat[xs1, Ys]]
  }

  def concat[Xs <: HList, Ys <: HList](xs: Xs, ys: Ys): Concat[Xs, Ys] =
    xs match {
      case _: HNil => ys
      case c: HCons[x, xs1] =>
        val tail = concat(c.t, ys)
        HCons(c.h, tail)
    }
}

[odersky]

Ah, OK. Good that it works with type tests! Can we make it support other patterns as well? Or, alternatively, tell the user that only type tests are supported? Right now one is left in the dark why it fails.

[OlivierBlanvillain]

Can we make it support other patterns as well?

Yes that might work for certain types unapplies, such as the ones generated for case classes. It's already on the TODO list :)

Or, alternatively, tell the user that only type tests are supported?

We discarded the idea of giving verbose warnings in this case because would requires type checking the expression twice, first in "match type" mode to emit the warning, then fallback to normal mode if that didn't go through.

[odersky]

Agreed, that sounds tricky. Have you considered the option that such singleton types not take part in implicit resolution at all, and we always use the upper bound (T) instead? One could still use singletons to compute Reflect boxes with some type member .S and use that to search for implicits of some computed type.

I think that would not work. Here's a problematic example:

class A
class B extends A
given a as A
def f[X](c: Boolean, x: X)(using y: X): X = 
  if c then x else y

transparent inline def foo(n: A): A = 
  val b = f(false, foo(n-1))

Here the call would expand to

  val b: TypeOf(foo(n-1)) = f[TypeOf(foo(n-1))](false, foo(n-1))(using a)

If the recursive call foo(n-1) gives type B, we get

  val b: B = f[B](false, foo(n-1))(using a)

but that call will give an a at runtime, so we get a CCE.

[odersky]

We discarded the idea of giving verbose warnings in this case because would requires type checking the expression twice, first in "match type" mode to emit the warning, then fallback to normal mode if that didn't go through.

But we could do a simple pass on what the match was, and if it uses unsupported elements, tell the user, no?

[gsps]

I think that would not work. Here's a problematic example: ...

Ah, yes, that's a pretty glaring issue. I guess to achieve both soundness and legibility, we could just be honest about the type of y in the syntax, i.e., provide an explicit way of referring to the upper bound as in ...(using y: X.nonSingletonSuperType).

What's our goal here anyways? Do we only want to maintain existing use cases of implicits, which would suddenly start failing, because some terms carry more precise types now?