Ah, I think what's been confusing me is that in the paper they use numeric literals at the type level, but they're singleton types for numeric terms. So it looks like they're matching on terms at the type level, but they're not.

Thread renamed from "Ah, I think what's been confusing me is that in the paper they use numeric literals at the type level..." to "Confused by term-like type literals" by deleted user

OK I think this is because n in MyTuple is necessarily a singleton type, whereas in myfn it's both an Int and a singleton type, which doesn't work as is, but the only way to make it work would be to make it a singleton type everywhere, at which point n is no longer a term, but a type, which is clearly not dependent.

Nope, I still don't get how this is different from the paper example def random_normal[S <: Shape](shape: S): NDArray[Float, S] = ???

I don't know what paper you're referencing, but in general, S doesn't contain all of the information in the value shape. A type that depends on S can therefore only use the information in the S variable, and not the information in the shape variable. A dependently-typed language could use both.

Type-level programming with match types, the original match types paper. I bring up this example because if their random_normal is implementable, I imagine sth effectively the same as myfn is too (with singletons), though I didn't figure out how to implement it

NDArray appears to be defined as a trait, not as a match type, so I don't think the two examples are analogous. There are lots of ways to potentially define that trait and implement it in random_normal, and the ones that come to my mind don't require any of the recent advances in Scala 3. How easy or difficult a trait is to instantiate depends entirely on the signatures of its members, and we aren't given that.

You'll notice that later in the paper, when match types come into play, there are examples of type-level arithmetic being performed on the Int singletons encoded in Shape. The fact that these are compiler-provided operators distinct from their value-level counterparts is another demonstration that this isn't a fully dependently-typed language. In Agda, for example, after defining a multiplication operator on terms, the operator is also usable in types. Dependently-typed languages largely collapse the distinction between terms and types as separate categories of thing.