FT parameter of ErasedProductInstancesN[K, FT] prevents derivation of instances of non-total type families

[tschuchortdev]

Take a look at this snippet that I've been playing around with:

type F1[X] = X match
      case String => String
      case Int => Int

type F2[X] = X match
      case Int => Int
      case String => String
      

case class Foo(a: Int, b: String)

summon[K0.ProductInstances[[A] =>> F1[A] <:< F2[A], Foo]]

To give some background info: The motivation here is to eventually check if for case class FooHK[F[_]](a: F[Int], b: F[String]) we have that FooHK[F1] <: FooHK[F2]. This is the case precisely when for every field type A of Foo we have F1[A] <: F2[A]. Despite F1 and F2 being functionally identical, summoning an instance of K0.ProductInstances fails:

But given instance mkProductInstances in object K0 does not match type shapeless3.deriving.K0.ProductInstances[[A] =>> F1[A] <:< F2[A], Foo].
[error]     |
[error]     |Note: a match type could not be fully reduced:
[error]     |
[error]     |  trying to reduce  F1[A]
[error]     |  failed since selector A
[error]     |  does not match  case String => String
[error]     |  and cannot be shown to be disjoint from it either.
[error]     |  Therefore, reduction cannot advance to the remaining case
[error]     |
[error]     |    case Int => Int

Why is that? The problem here is that F1 and F2 are not total. Their domain covers all the types that appear in Foo fields, so applying them to FooHK is legal, however in Shapeless kinds.scala we have this line:

inline given mkProductInstances[F[_[_]], T[_]](using gen: ProductGeneric[T]): ProductInstances[F, T] =
    ErasedProductInstances[K1.type, F[T], LiftP[F, gen.MirroredElemTypes]](gen)

That applies F[T], i.e. F1[Foo] in our example, a case that is not defined and thus fails to reduce.

ErasedProductInstancesN[K, FT]

Can we get rid of the FT type parameter in ErasedProductInstancesN? What is it needed for?

[joroKr21]

It looks like those type parameters are not used. But I'm also not sure if it would be binary compatible to remove them.

[milessabin]

It's a phantom type argument used to distinguish the instances for different fully applied types. I'm fairly sure it's only used for implicit resolution, and I'm fairly sure it can't simply be removed (which isn't to say we couldn't make some sort of change to accommodate this case).

[tschuchortdev]

Hmm, I see, a regular type alias is used here, allowing ErasedProductInstances to escape:

type ProductInstances[F[_[_[_]]], T[_[_]]] = ErasedProductInstances[K11.type, F[T]]

Perhaps it would be possible to use F[_], T parameters instead of F[T], or use an opaque type, though I suspect that opaque would still require F and T to be used on the RHS for implicit resolution and thus not change anything.

[milessabin]

allowing ErasedProductInstances to escape

It's not really "escaping" per se. The type alias really is just an abbreviation here: the underlying type has to show through to drive implicit resolution. Switching to an opaque type would break things.