TASTy Checker using tasty-query

Description

The goal of this project is to build a compiler-independent checker for .tasty files, which ensures that .tasty files produced by the compiler adhere to the spec. It will use tasty-query for that purpose.

tasty-query is a library to load Scala 3 .tasty files, as well as Scala 2 pickles and Java class files. It provides semantic information about all the symbols and types in a program's classpath. For TASTy files, it also provides to full Typed Abstract Syntax Trees (typed AST) of all the classes and methods.

For every expression Tree in a program, tasty-query computes a Type. For example, it can compute the type scala.Int for an expression like 1 + 2. However, it does not check that expressions of certain types are only used where those types are valid. Consider for example:

def foo(x: String): Unit = println(x)

foo(1 + 2)

tasty-query will compute the type scala.Int for 1 + 2, and will know that foo expects one parameter of type java.lang.String, but it won't complain that it is an invalid call. That even though tasty-query knows that scala.Int is not a subtype of java.lang.String.

The compiler is supposed to catch these mistakes, so that it never produces .tasty files that are invalid. However, under separate compilation, or if there is a bug in the compiler, it could happen.

The TASTy Checker's job should detect and flag these cases, as well as many others.

Expected outcome

We expect the student to implement a TASTy Checker based on tasty-query. The checker should walk all the trees of TASTy file and validate the invariants of a well-typed program. Here is a non-exhaustive list of these invariants:

Whenever an expression of type A is used where a B is expected, check that A <:< B. That includes method calls, as above, but also Booleans in if conditions, and other specific types required by language features.
Whenever there is A[...Ts], check that the ...Ts conform to the bounds of the type parameters of A.
When A extends B, whenever A.m has the same erasure as B.m, check that A.m indeed overrides B.m.
Whenever A.m overrides B.m, check that the result type of A.m is a subtype of that of B.m.
When A extends B and they both have a type member T, check that A.T conforms to the bounds of B.T.

The first two bullets should definitely be addressed in the project. The extent to which other bullets and other invariants can be covered will be determined based on the progress.

Supervisor

Sébastien Doeraene (sebastien.doeraene@epfl.ch): principal engineer at the Scala Center

scalacenter / student-projects