EDIT: the TLDR is that nobody has shown that kind polymorphism is sound, but it indeed does not seem to be more impredicative than current Scala, and we don’t have strong evidence against it, although I initially feared otherwise, and I can articulate a bit what leads me to this current best guess. I’m not certain, but I have thought about this for a while before today.
DOT indeed doesn’t support higher kinds yet; the first Dotty versions actually translated higher kinds into core DOT*, but that encoding turned out to not work well enough. Getting to higher kinds should be the next step in my current efforts, and hopefully AnyKind would also be in scope, but I haven’t looked at it closely enough. The first question, in such an effort, would be whether one can formalize an intuition similar to what @milessabin presents, at least in the semantics.
But at present, kind polymorphism falls (not alone) among the features that haven’t been formalized, and for which we don’t have strong evidence of either soundness or unsoundness — as opposed to e.g. type projections (for which we have evidence of unsoundness and of multiple failed attempts at fixes).
In the absence of formal proofs, what’s our best guess?
Speculating on the chance of paradoxes
First, why not just try encoding them? Because it’s extremely hard, even when those paradoxes arise. Here’s the shortest version I know (in Agda with unsafe options):
But in other systems that takes much longer:
Beyond the length, this is extremely dense and infamously difficult code. I still don’t fully understand the Agda version, and I only got halfway in the cited paper (“A simplification of Girard’s paradox”) before running out of time.
And BTW, I must admit that if we only had problems of that sort, it might not be a significant type safety problem. However, the risk is always that we’d get much simpler violations.
How much do we care about paradoxes
First of all, usually Girard’s paradox just lets you write programs that loop. That’s bad for a proof assistant based on Curry-Howard, like Agda or Coq, because looping programs are also looping proofs, which let you prove False; that it, programs that loop are a problem for logical soundness.
However, for Scala we only need type soundness: Scala’s not a proof assistant, and it anyway doesn’t ask users to prove that programs terminate. That only requires only a limited sort of logical soundness: a value v with type member A >: L <: U serves as evidence that L <: U, and this evidence must be logically sound. Otherwise, you could prove that Any <: Nothing and implement unchecked casts. And indeed, @sstucki has managed to adapt existing paradoxes (related to Russell’s) to violate type soundness using this avenue (tho the example doesn’t translate to Scala). Strawman of a DOT calculus with higher-kinded types · GitHub
“X <: AnyKind”, or polykinded bounded quantification
I have also wondered whether “kind polymorphism” is too impredicative, but when I talked @sstucki was relatively confident that this was not a danger. And I think I now understand why.
With or without AnyKind, types can only quantify over other types; notwithstanding the name, AnyKind does not give you “parametric kind polymorphism”: you cannot express a type like ∀ (K : Kind). F K, which would be dangerous because it’s a type quantifying over something bigger (a kind). Haskell’s kind polymorphism allows exactly that, so it might suffer from Girard’s paradox — but in Haskell there’s no known way to go from there to violations of type soundness (and in fact they have proved type soundness).
How a soundness proof could start
In my ongoing soundness proofs for DOT, the key step is defining values that can contain type members, represented as semantic types (that is, predicates on values). Theorem provers forbid doing that naively, because doing that lets you encode Russell’s paradox in the theorem prover; one must use instead a more complicated sort of predicate. However, once values can contain semantic types, higher-kinded semantic types seem a smaller step — and the union of higher-kinded semantic types for different kinds should also work.
It’s trickier to interpret T <: AnyKind: if T and U have “kind *”, then T <: U means that all values in T are also in U; one can extend this definition pointwise to higher kinds, so that T <: U at kind * -> * iff for all X : * then T[X] <: U[X], but the definition depends on the kind. For T <: AnyKind, you can use the actual kind of T for a variant of this definition (or just demand that T is a “reasonable” type in the appropriate sense).
*Implementing Higher-Kinded Types in Dotty, Scala Symposium 2016, https://infoscience.epfl.ch/record/222780/files/p51-odersky.pdf