Hi there 
I’m a Lean4 user myself.
I don’t think Scala can support full dependent types like Idris or Agda or Lean. Because Scala’s DOT (dependent object types) system has a vastly different type calculus, which I assume is incompatible with things like Calculus of Constructions. When you have subtyping, class hierarchies, covariance / contravariance, etc. you leave that world behind.
Scala’s DOT was the result of so many years of work and research, proving its soundness and then rewriting the compiler. Its goal from the start was to fuse OOP and FP, not a fully dependent FP-style type system. Scala’s type calculus is unique in that regard, and is not part of the Hindley-Milner family or the CoC family (to the best of my knowledge). Trying to add Idris-like type systems would require even more years of research and yet another uprooting of the whole language (like Scala 3 did).
So Scala opted to have partial support for certain dependently typed programming patterns that are suitable for its needs, like Match Types and Dependent Function Types for example. This approach seems to be powerful enough for Scala users’ needs.
I think the long-term goal is to stay more practical. This is not related to types, but you can read Evolving Scala which was posted recently (video talk version here by Martin himself). Current research is not about type systems, it’s about effect/capability systems (think of it as a more general version of Rust’s borrow checker, applied to any kind of resource / capability, not just memory management).
One can also ask, does Scala really need a fully dependently typed system? Scala’s use cases are very different than Idris / Agda / Haskell / Lean and it might not make much sense.
A more philosophical question is the meaning of this word “dependent type”. It’s a term that is used very loosely to mean many things. There isn’t a strict formal definition, there are many dependent type systems out there (CoC, Girard’s System F, and so on). From a philosophical standpoint you could argue that Scala’s type system is “fully dependent”, I mean it’s called “dependent object types” isn’t it? 
(Also path dependent types play a fundamental role in DOT.) Even a parameterized type is an example of a “dependent type”: List[T] depends on T; but type parameters are everywhere and people are familiar with it, so nobody calls it “dependent type”. So, what most people mean by “dependent types” is the features and patterns available in one of those languages: Idris, Agda, Lean, etc.
That’s the best of my understanding, hope it helps! 
).