The fact that we are unable to do that is a direct consequence of the semantics of opaque type aliases. Given that named tuples are opaque type aliases, we cannot distinguish them that way, since they are not provably disjoint from anything else.

Could you elaborate on why you would need this? You said:

Assume you have a type level algorithm over named tuples that needs to recurse when the value type is a named tuple, otherwise do something else. (e.g. check a named tuple is substructually equivalent to another)

That sounds a lot like the type-level equivalent of "arbitrary-depth flattening of lists". IIUC I could write the same idea of deep structural equivalence of lists this way:

def deepSameListShape(x: Any, y: Any): Boolean = (x, y) match {
  case (xHead :: xTail, yHead :: yTail) =>
    deepSameListShape(xHead, yHead) && deepSameListShape(xTail, yTail)
  case (Nil, _ :: _) | (_ :: _, Nil) =>
    false
  case _ =>
    true // neither are lists, or both are Nil
}

That's usually considered a big code smell. The user of deepSameListShape could be surprised that user-level deep elements actually happen to be lists themselves, defeating the intended logic.

Dispatching on whether an arbitrary type is a named tuple or not seems very similar in spirit to the above. Based on that, it seems like a code smell as well.

@sjrd the use case is to say that Context[(siteMap: (articles: Pages, about: Pages))] can be provided to a use site that expects Context[(siteMap: (articles: Pages))] because of structural equivalence, so when you reach a non-named tuple you should compare the types.

Another one is path type where you can keep looking within a named tuple for a chain of nested keys - however when you go to some depth that is no longer a named tuple then its not possible to compare to a named tuple type pattern and match type refuses to reduce

Is the argument to Context a phantom type? Because named tuples don't have that subtyping relationship, so values of the former can definitely not be assigned to the latter.

So, I guess you're using named tuples for their type syntax only, without using value?

its using Selectable Fields - and so there would be some operation using an evidence parameter that the substructure proof exists between the types to do a "Safe cast"

I imagine the same sort of thing could be used to convert between two similar named tuples - e.g. to swap order - or drop/add fields

Usually for this sort of thing, you would statically know the expected depth of tupling. And so you wouldn't need to "dynamically" (at the type-level) test whether a type is a named tuple or not.

Likewise with lists of lists. You would statically know whether you need to do xs.map(...) or xss.map(_.map(...))).

but for derivation you dont know, it comes from the structure of types, if you can only inspect 1 level deep that is very limited.

I guess you are suggesting for this context example, basically each level should then be boxed in a new Context - but to construct the initial context from e.g. a raw arbitrarily nested named tuple value then you need to traverse the type - perhaps this would work in the way such that you NamedTuple.Map each level starting from the outside, but as you enter the inner levels maybe this would not reduce, id have to try

Given that summon[scala.util.NotGiven[Int <:< AnyNamedTuple]] works (so i can probably generate the substructural proof the long winded way with implicit induction), why can there not be a way to do this without implicit search?

if not a general subtyping compiletime op, then an alternative mode to match types that is static dispatch? (is that inline match)?

scala> summon[scala.util.NotGiven[Int <:< NamedTuple.AnyNamedTuple]]
val res1: scala.util.NotGiven[Nothing] = scala.util.NotGiven@23eb7e28