Inlining still breaks type checking

[LPTK]

Compiler version

3.0.0-RC2-bin-20210325-ab2664f-NIGHTLY

Problem

It is not enough to special-case Nothing (type-ascribing only trees of this type as in #11917). In principle, all inlined parameters may require a type annotation. This is because removing type annotations in Scala can break type checking, as subtyping is not transitive.

Minimized code

type A
class B { def foo = 0 }
trait Ev { type T >: A <: B }

inline  // commenting this fixes the error
def test(ev: Ev)(x: ev.T): Int = x.foo

def trial(ev: Ev, a: A) = {
  test(ev)(a)  // foo cannot be accessed as a member of (a : A) from module class main$package$.
}

Expectation

If it type-checks without inline, it should type-check with inline too. In particular, I assume that non-transparent inline is not supposed to interfere with type checking in any way. Is that a correct assumption?

[odersky]

I think we might have to compromise here, at least for inline parameters. If we type ascribe everything it will be a huge pain for meta programming, and the errors we can expect from that will far outweigh the (very rare) breakages we would entail otherwise.

[LPTK]

Is it really necessary to compromise? IMHO mere type ascriptions should never break metaprogramming usages, especially if the ascribed type is the intersection of the expression's type with the expected type. I don't quite see why that would break inline matches or match types. Perhaps the breakage we can see in my PR exposes bugs in these? (I have not had time to investigate, and TBH I probably won't in the near future.)

I know the scope of Squid's metaprogramming was smaller and easier to reason about, but in Squid, type ascriptions were always added upon substitutions (unless the types matched already), and code transformations, including quote pattern matching, transparently saw through them.

[odersky]

They break any use of meta programming that expects (say) a constructor application or a constant, instead of a type ascrption.

[LPTK]

But surely this could be fixed in the implementation, no?

Here is an example of how it works in Squid, from the REPL:

scala> val c = code"List.fill(42: Int)(0): List[Int]"
c: squid.IR.ClosedCode[List[Int]] = code"scala.collection.immutable.List.fill[scala.Int](((42): scala.Int))(0)"

scala> c match { case code"List.fill(${Const(n)})($e: Int)" => (n, e) }
res8: (Int, squid.IR.Code[Int,Any]) = (42,code"0")

Notice that 42: Int can be matched as Const(n) without trouble, and the same goes for the whole expression, which is ascribed type List[Int] in the scrutinee but is not ascribed in the pattern. Moreover, $e: Int matches any expression of integer type, even if that expression is not ascribed, in the source code.

Basically, I treat type ascription as a transparent piece of metadata that never gets in the way of metaprogramming use cases. This way, we retain type-preserving substitution in all cases.

[odersky]

But surely this could be fixed in the implementation, no?

If we change the implementation's API contract, yes. That's something to consider for the next iteration.

[odersky]

I think the crucial thing to make progress is really to make type ascriptions transparent in the quoted APIs. So let me reassign to @nicolasstucki.

[nicolasstucki]

Ascriptions are already transparent in the quoted patterns.