This has been expressed, but I do not think it is true. Yes, the original linear logic doesn't have anything like a "linear kind", but that's mainly because it's a logic not a type theory. The classic A → B = !A ⊸ B could be interpreted as something like A → B = GC A ⊸ B, i.e. making the ! an in-language type constructor not some sort erased modality.

I'm not expert at this stuff, but when I was interrogating this before, I found the thesis behind https://ncatlab.org/nlab/show/linear-non-linear+logic as a quite old example (1994, only a few years after the first LL paper from Girard in 1987) of separating the linear and non-linear worlds as two categories with an adjudication between them. This is very compatible with linearity in the types.

That all said, I will admit that the "quantitative type theory" line of research gives the current LinearHaskell a big leg up on integrating with dependent types. See https://ncatlab.org/nlab/show/linear-non-linear+logic for the latest plans on that.

I certainly have no retort. My big complaint about the status quo is we can't even have things like Rust's `Box`, but I have no idea what the operational semantics of `f : pi (b : Box<T>) ...` might be, let alone the static semantics!