You would want for type variable to not be attached directly to a type class on its definition? But still treated as a container type. Something like:
trait Functor:
fun fmap[A, B](f: A -> B, c: Self[A]) -> Self[B];
...
impl Functor for List[A]:
fun fmap[A, B](f: A -> B, l: List[A]) -> List[B]
List::fold(l, Nil[B], (t, h) => Cons(f(h), t))
...
The above would compile, but the Functor wouldn't be treated of a higher kind in the type-system. I'll try to work a flexible solution, thanks for the great callout!† There's an encoding of higher-kinded types in some languages that don't really have them as first-class citizens (e.g. Rust with associated type constructors) that does this by adding a ‘rewrap’ item to the trait: you implement `Functor` for `List<A>`, but also (as part of the trait) includes a type constructor `Rewrap<B> = List<B>`. This lets you encode the fact that the `Functor` instance is defined for `List<A>` for all values of `A`, but you still struggle to prove that some of their items are independent of the choice of `A`.
‡ To see both of these side-by-side, consider the instance for pairs, which are functorial in their right parameter (as well as the left parameter: they are bifunctorial, but that's not relevant here). So if you have a curried pair type constructor `Pair : * → * → *` it really is true that `Pair[A]`, not `Pair`, is a `Functor`:
impl Functor for Pair[A]:
fun fmap[B, C](f: B -> C, self: Pair[A][B]) -> Pair[B][C]):
Pair(self.0, f(self.1))
I think what both I and the sibling comment are getting at is that there is a difference between `Functor : (Self : * → *) → Class` and `Functor : (Self : * → *) → (A : *) → Class`/preapplied `Functor : (Self : *) → Class` and the syntax seems to merge the two (using syntax for the latter that is automatically abstracted to the former). But it's not clear to me that you can do that without losing the ability to express some things. The associated type is a pointed example because the unwanted dependence breaks type equality, but consider also an associated function that should _not_ be parameterized by `A`.