Regression in foldables-io/skunk-tables for match types: with error "selector is uninhabited" but selector is actually inhabited

[WojciechMazur]

Compiler version

Last good release: 3.6.0-RC1-bin-20240719-af933c4-NIGHTLY
First bad release: 3.6.0-RC1-bin-20240723-46ff151-NIGHTLY
Bisect points to b7846c4

Minimized code

import scala.compiletime.constValueTuple

trait IsColumn[A]

final case class TypedColumn[N <: Singleton, A, T, C <: Tuple](name: N, primitive: IsColumn[A])
object TypedColumn:
  enum Constraint:
    case Default
    case Nullable

  final class Insert[N <: Singleton, A, C <: Tuple, In](name: N, isColumn: IsColumn[A])
  final case class Op[A](a: A)

type IfIn[T <: Tuple, A, True, False] <: True | False = T match
  case EmptyTuple => False
  case A *: t     => True
  case ? *: t     => IfIn[t, A, True, False]

type IfInM[T <: Tuple, A <: Tuple, True, False] <: True | False =
  A match
    case EmptyTuple => False
    case a *: tail  => IfIn[T, a, True, IfInM[T, tail, True, False]]

type NonRequiredConstraints =
  (TypedColumn.Constraint.Nullable.type, TypedColumn.Constraint.Default.type)

type Required[C <: NonEmptyTuple] <: Tuple =
  C match
    case TypedColumn.Insert[n, ?, c, ?] *: t =>
      RequiredGo[t, IfInM[c, NonRequiredConstraints, EmptyTuple, n *: EmptyTuple]]
type RequiredGo[C <: Tuple, A <: Tuple] <: Tuple =
  C match
    case EmptyTuple => A
    case TypedColumn.Insert[n, ?, c, ?] *: t =>
      RequiredGo[t, IfInM[c, NonRequiredConstraints, A, scala.Tuple.Append[A, n]]]

@main def Test = {
    type Columns = (TypedColumn.Insert["one", Boolean, EmptyTuple, Nothing],
                  TypedColumn.Insert["two", Int, EmptyTuple, Nothing],
                  TypedColumn.Insert["three", String, EmptyTuple, Nothing])

    assert(constValueTuple[Required[Columns]] == ("one", "two", "three"))
}

Output

[error] ./src/main/scala/usage.scala:42:12
[error] Values of types Required[Columns] and (String, String, String) cannot be compared with == or !=
[error] 
[error] Note: a match type could not be fully reduced:
[error] 
[error]   trying to reduce  Required[Columns]
[error]   failed since selector Columns
[error]   is uninhabited (there are no values of that type).
[error]     assert(constValueTuple[Required[Columns]] == ("one", "two", "three"))

Expectation

Should compile (probably)

[WojciechMazur]

The same commit pointed out by bisect leads to failures in other projects
julianpeeters/dynamical

Reproducer

//> using options -Ykind-projector:underscores 

sealed trait Monomial[A, B, Y]
object Monomial:
  case class Interface[A, B, Y](yᵉˣᵖ: A => Y, coeff: B) extends Monomial[A, B, Y]
  case class Store[S, Y](yᵉˣᵖ: S => Y, coeff: S) extends Monomial[S, S, Y]
  case class StoreF[F[_], S, Y](yᵉˣᵖ: F[S] => Y, coeff: S) extends Monomial[F[S], S, Y]
import Monomial.{Store, Interface, StoreF}

trait Mealy[P[_]]:
  def init[Y]: Init[P, Y]

type ~>[P[_], Q[_]] = PolyMap[P, Q, _]
abstract class PolyMap[P[_], Q[_], Y]

type Init[P[_], Y] = P[Y] match
  case PolyMap[p, q, Y]   => Init[p, Y]
  case Store[s, Y]        => s
  case StoreF[f, s, Y]    => s
  case Interface[a, b, Y] => b
  case Tensor[p, q, Y]    => (Init[p, Y], Init[q, Y]) 

type ⊗[P[_], Q[_]] = Tensor[P, Q, _]
abstract class Tensor[P[_], Q[_], Y]

object tensors:
  extension [S1, S2, A1, B1, A2, B2] (m1: Mealy[Store[S1, _] ~> Interface[A1, A1 => B1, _]])
    def ⊗(m2: Mealy[Store[S2, _] ~> Interface[A2, A2 => B2, _]]): Mealy[(Store[S1, _] ⊗ Store[S2, _]) ~> (Interface[A1, A1 => B1, _] ⊗ Interface[A2, A2 => B2, _])] =
      new Mealy[(Store[S1, _] ⊗ Store[S2, _]) ~> (Interface[A1, A1 => B1, _] ⊗ Interface[A2, A2 => B2, _])]:
        def init[Y]: Init[(Store[S1, _] ⊗ Store[S2, _]) ~> (Interface[A1, A1 => B1, _] ⊗ Interface[A2, A2 => B2, _]), Y] =
          (m1.init, m2.init)

Output

[error] ./src/main/scala/usage.scala:31:12
[error] Found:    Init[
[error]   ([_] =>> Monomial.Store[S1, _]) ~>
[error]     ([_²] =>> Monomial.Interface[A1, A1 => B1, _²]),
[error] Y]
[error] Required: S1
[error] 
[error] where:    Y  is a type variable
[error]           _  is a type variable
[error]           _² is a type variable
[error]           (m1.init, m2.init)
[error]            ^^^^^^^
[error] ./src/main/scala/usage.scala:31:21
[error] Found:    Init[
[error]   ([_] =>> Monomial.Store[S2, _]) ~>
[error]     ([_²] =>> Monomial.Interface[A2, A2 => B2, _²]),
[error] Y]
[error] Required: S2
[error] 
[error] where:    Y  is a type variable
[error]           _  is a type variable
[error]           _² is a type variable
[error]           (m1.init, m2.init)
[error]             

[odersky]

@sjrd Can you take a look to see whether the breakages are inevitable or whether there is some mitigation?

[sjrd]

I'll have a look on Monday.

[smarter]

The match type error "failed since selector is uninhabited" fires when the selector is a parameterized trait applied to Nothing, which is wrong since it doesn't preclude it from being inhabited. Here's a minimization:

sealed trait Foo[A]
final class Bar extends Foo[Nothing]

object Test:
  type Extract[T] = T match
    case Foo[_] => Int

  val x: Extract[Bar] = 1

8 |  val x: Extract[Bar] = 1
  |                        ^
  |                      Found:    (1 : Int)
  |                      Required: Test.Extract[Bar]
  |
  |                      Note: a match type could not be fully reduced:
  |
  |                        trying to reduce  Test.Extract[Bar]
  |                        failed since selector Bar
  |                        is uninhabited (there are no values of that type).

[dwijnand]

Looks like we approximate _ to its upper bound Any and then Any and Nothing are apparently disjoint? Apparently "Nothing ⋔ T and T ⋔ Nothing for all T", 🤔 .

[sjrd]

This is going to be a problem. It shows that provablyDisjoint is in fact incorrect for phantom type parameters. The obvious fix would be to make invariantDisjoint the same as covariantDisjoint at

scala3/compiler/src/dotty/tools/dotc/core/TypeComparer.scala

Lines 3239 to 3244 in a672e05

	def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
	provablyDisjoint(tp1, tp2, pending) && typeparamCorrespondsToField(cls.appliedRef, tparam)
	// In the invariant case, direct type parameter disjointness is enough.
	def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
	provablyDisjoint(tp1, tp2, pending)

However this is bound to destroy other existing use cases. There are existing tests that do not pass anymore if we make that change.

We could also be more surgical and still conclude disjointness if we can show that at least one of the sides cannot be instantiated to Nothing. So something like

    def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
      provablyDisjoint(tp1, tp2, pending)
        && {
          typeparamCorrespondsToField(cls.appliedRef, tparam)
          || cannotBeNothing(tp1) || cannotBeNothing(tp2)
        }

but cannotBeNothing is not an operation that we can reliably implement either.

It looks like this is a dead end for now. A workaround is not to use Nothing in match types, even as type arguments.