And F* has dependent typing. I was never claiming that reified generics was necessary for stronger typing, but I'm also not convinced that it's an impediment.

And F* has dependent typing. I was never claiming that reified generics was necessary for stronger typing, but I'm also not convinced that it's an impediment. At worst I could see how it could be a trivial implementation detail, but the fact that Scala went out of their way to use tokens and manifests suggests that the functionality is desired. Whether that's provided by the runtime or by the compiler writer is only a difference in effort (or rather, whose effort).