(this is the Scala version, for Rust version, please go to In Rust, which type declaration is closest to a type declaration nested in a generic class in C# or C++?)

When writing a library that relies heavily on generic/template in C# or C++, one trick I often use is to declare several structs that uses the same generic type arguments as nested types under a static class.

e.g. these declaration (using C# as an example):

    public struct Gen1<T1, T2, T3>
    {
    }

    public struct Gen2<T1, T2, T3>
    {
    }

is functionally equivalent to this:

    public static class Ts<T1, T2, T3>
    {
        public struct Gen1
        {
        }

        public struct Gen2
        {
        }
    }

Namely, Ts<int, int, string>.Gen1 is converted to a specialised class by the compiler, with its own static members. Ts<int, int, String> and Ts<int, int, int> becomes 2 different classes that shares nothing except names.

This is different from JVM compiler with type erasure, where type arguments are removed during the compilation. As a result, the same static nested class declaration translated to Java only has 1 type and has to be initialised without type arguments.

To my knowledge, no other JVM language has transcended this limitation (namely, Kotlin compiler doesn’t support specialising a generic type like C#/C++, Scala compiler doesn’t have static declaration and template/generic type argument for object type). In fact, most other languages don’t have similar abstraction (the only exception is LEAN4, where the static generic class becomes a section: https://lean-lang.org/lean4/doc/sections.html).

I’m looking for a minimal extension to the type system of Scala/Kotlin that can reproduce this abstraction line-by-line. Given that Scala has path-dependent type and GADT, it will be my first choice. But how should I do this?

(One way to implement this without compiler plugin is to introduce a type equality axiom, I don’t know how to do this, but if you answered In Scala 3 with DOT calculus, how to extend the equality of 2 path dependent types for obviously cases?, it should be easy to include the solution to this problem as a special case)