Yes, it also has TypeTags, allowing you to inspect exactly what the compiler saw at compile-time in detail. That's not really what one uses in practice, e.g...

    scala> val list = List(null, 1, 2, "any")
    list: List[Any] = List(null, 1, 2, any)

    scala> list.collect { case x: Int => x }
    res0: List[Int] = List(1, 2)

    scala> Vector(null, "hello", 3).collectFirst { case i: Int => i * 2 }
    res1: Option[Int] = Some(6)

    scala> import collection.immutable.BitSet
    
    scala> BitSet(1,2,3).map(_ + 1)
    res2: immutable.BitSet = BitSet(2, 3, 4)

    scala> BitSet(1,2,3).map(_.toString)
    res3: immutable.SortedSet[String] = TreeSet(1, 2, 3)

To be honest, tags are indeed needed for creating arrays, since they are reified by the JVM:

    scala> import scala.reflect.ClassTag
    scala> def myAwesomeArray[T : ClassTag] = new Array[T](10)

    scala> myAwesomeArray[Int]
    res4: Array[Int] = Array(0, 0, 0, 0, 0, 0, 0, 0, 0, 0)

One common problem is that overriding of parameters doesn't work for containers due to type erasure, so you can't have overrides on type parameters, because the JVM gets in the way (i.e. the following does not work):

    def sum(list: List[String]) = ???
    def sum(list: List[Int]) = ???

However, Scala has something more powerful (type-classes):

    trait Monoid[T] { 
      def plus(x: T, y: T): T
      def zero: T 
    }

    implicit object IntMonoid extends Monoid[Int] { 
      def plus(x: Int, y: Int) = x + y
      val zero = 0 
    }

    implicit object StringMonoid extends Monoid[String] { 
      def plus(x: String, y: String) = x + y
      val zero = "" 
    }

    def sum[T : Monoid](list: List[T]) = {
      val monoid = implicitly[Monoid[T]]
      list.foldLeft(monoid.zero)(monoid.plus)
    }

    scala> sum(List("a", "b", "c", "d"))
    res5: String = abcd

    scala> sum(List(1,2,3,4))
    res6: Int = 10

But wait, we can go much further with implicits that actually dictate the return type:

    trait SetBuilder[T, R] {
      def empty: R
      def buildInstance(param: T): R
      def concat(s1: R, s2: R): R
    }

    implicit object IntSetBuilder extends SetBuilder[Int, BitSet] {
      def empty = BitSet.empty
      def buildInstance(param: Int) = BitSet(param)
      def concat(s1: BitSet, s2: BitSet) = 
        s1 ++ s2
    }

    implicit object StringSetBuilder extends SetBuilder[String, Set[String]] {
      def empty = Set.empty[String]
      def buildInstance(param: String) = Set(param)
      def concat(s1: Set[String], s2: Set[String]) =
        s1 ++ s2
    }

    def buildSetFrom[T,R](params: T*)(implicit builder: SetBuilder[T,R]): R = {
      if (params.nonEmpty)
        builder.concat(
          builder.buildInstance(params.head),
          buildSetFrom(params.tail : _*)
        )
      else
        builder.empty
    }  

    scala> buildSetFrom(1,2,3)
    res7: scala.collection.immutable.BitSet = BitSet(1, 2, 3)

    scala> buildSetFrom("a", "b", "c")
    res8: Set[String] = Set(a, b, c)

Scala in general allows for code that is much more generic than C#, without having the need for reified generics.

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).

This is the first time I've heard of F*. Interesting. Is it usable?

Not really. It basically generates a number of type (in)equalities and outsources finding the solution to Microsoft Z3 theorem prover, which you cannot use for anything commercial.