Pattern matching exhaustivity warnings on higher kinded types

[remi-delmas-3000]

Experimenting with higher-kinded recursion schemes and dotty, I got exhaustivity and unchecked type warnings with the attached code, and I can't make up my mind they are right or spurious

  /** Natural transformation. */
  trait ~>[F[_], G[_]] {
    def apply[A](fa: F[A]): G[A]
  }

  /** Higher-kinded pattern functor typeclass. */
  trait HFunctor[H[f[_], i]] {
    def hmap[A[_], B[_]](nt: A ~> B): ([x] => H[A,x]) ~> ([x] => H[B,x]) 
  }

  /** Some HK pattern functor. */
  enum ExprF[R[_],I] {
    case Const[R[_]](i: Int) extends ExprF[R,Int]
    case Neg[R[_]](l: R[Int]) extends ExprF[R,Int]
    case Eq[R[_]](l: R[Int], r: R[Int]) extends ExprF[R,Boolean]
  }

  /** Companion. */
  object ExprF {
    implied hfunctor for HFunctor[ExprF] {
      def hmap[A[_], B[_]](nt: A ~> B): ([x] => ExprF[A,x]) ~> ([x] => ExprF[B,x]) = {
        new ~>[[x] => ExprF[A,x], [x] => ExprF[B,x]] {
          def apply[I](fa: ExprF[A,I]): ExprF[B,I] = fa match {
            case Const(i) => Const(i)
            case Neg(l) => Neg(nt(l))
            case Eq(l, r) => Eq(nt(l), nt(r))
          }
        }
      }
    } 
  }

[warn] -- [E029] Pattern Match Exhaustivity Warning: /fixpoint-dotty/src/main/scala/HK.scala:25:53 
[warn] 25 |          def apply[I](fa: ExprF[A,I]): ExprF[B,I] = fa match {
[warn]    |                                                     ^^
[warn]    |match may not be exhaustive.
[warn]    |
[warn]    |It would fail on pattern case: ExprF.Const(_), ExprF.Neg(_), ExprF.Eq(_, _)
[warn] -- Warning: /fixpoint-dotty/src/main/scala/HK.scala:26:17 
[warn] 26 |            case Const(i) => Const(i)
[warn]    |                 ^^^^^^^^
[warn]    |        the type test for HK.ExprF.Const[A] cannot be checked at runtime
[warn] -- Warning: /fixpoint-dotty/src/main/scala/HK.scala:27:17 
[warn] 27 |            case Neg(l) => Neg(nt(l))
[warn]    |                 ^^^^^^
[warn]    |          the type test for HK.ExprF.Neg[A] cannot be checked at runtime
[warn] -- Warning: /fixpoint-dotty/src/main/scala/HK.scala:28:17 
[warn] 28 |            case Eq(l, r) => Eq(nt(l), nt(r))
[warn]    |                 ^^^^^^^^
[warn]    |           the type test for HK.ExprF.Eq[A] cannot be checked at runtime
[warn] four warnings found
[info] Done compiling.

The enum is sealed and all cases are matched so the exhaustivity warning seems spurious.

If the exhaustivity warning is due to the fact that ExprF[_[_], _] is a higher-kinded GADT, well it seems that incorrect uses of a natural transformation
A ~> B lifted to [x] => ExprF[A, x] ~> [x] => ExprF[B, x] using ExprF.hfunctor will be caught anyway as demonstrated below:

//a natural transformation from List to Option
val l2opt = new ~>[List, Option] {
    def apply[A](in: List[A]): Option[A] = {
      in match {
        case Nil => None
        case h :: _ => Some(h)
      }
    }
  }
// lifted to [x] => ExprF[List,x] ~> [x] => ExprF[Option,x]
val nt  = ExprF.hfunctor.hmap(l2opt)
// applied on a wrong ExprF value 
nt(ExprF.Neg(Set(12)))

[error] -- [E007] Type Mismatch Error: /fixpoint/fixpoint-dotty/src/main/scala/HK.scala:45:18 
[error] 45 |  nt(ExprF.Neg(Set(12)))
[error]    |               ^^^^^^^
[error]    |               Found:    Set[Int]
[error]    |               Required: List[Int]
[error] one error found
[error] (Compile / compileIncremental) Compilation failed

So it seems to me that the pattern match is exhaustive and that unchecked warnings are kind of noisy as I see no way of providing wrong input to nt that would get uncaught by the type system beforehand.

Any how, dotty seems super nice for generic programming !

Attached is a fully working example of higher-kinded catamorphism, only issue are these warnings.

Best regards.

HK.scala.gz

[abgruszecki]

As of #6398, the runtime check warnings are no longer emitted. The only remaining problem is the exhaustivity warning:

scala>   /** Natural transformation. */
     |   trait ~>[F[_], G[_]] {
     |     def apply[A](fa: F[A]): G[A]
     |   }
     | 
     |   /** Higher-kinded pattern functor typeclass. */
     |   trait HFunctor[H[f[_], i]] {
     |     def hmap[A[_], B[_]](nt: A ~> B): ([x] =>> H[A,x]) ~> ([x] =>> H[B,x]) 
     |   }
     | 
     |   /** Some HK pattern functor. */
     |   enum ExprF[R[_],I] {
     |     case Const[R[_]](i: Int) extends ExprF[R,Int]
     |     case Neg[R[_]](l: R[Int]) extends ExprF[R,Int]
     |     case Eq[R[_]](l: R[Int], r: R[Int]) extends ExprF[R,Boolean]
     |   }
     | 
     |   /** Companion. */
     |   object ExprF {
     |     implied hfunctor for HFunctor[ExprF] {
     |       def hmap[A[_], B[_]](nt: A ~> B): ([x] =>> ExprF[A,x]) ~> ([x] =>> ExprF[B,x]) = {
     |         new ~>[[x] =>> ExprF[A,x], [x] =>> ExprF[B,x]] {
     |           def apply[I](fa: ExprF[A,I]): ExprF[B,I] = fa match {
     |             case Const(i) => Const(i)
     |             case Neg(l) => Neg(nt(l))
     |             case Eq(l, r) => Eq(nt(l), nt(r))
     |           }
     |         }
     |       }
     |     } 
     |   }
23 |          def apply[I](fa: ExprF[A,I]): ExprF[B,I] = fa match {
   |                                                     ^^
   |match may not be exhaustive.
   |
   |It would fail on pattern case: ExprF.Const(_), ExprF.Neg(_), ExprF.Eq(_, _)
// defined trait ~>
// defined trait HFunctor
// defined class ExprF
// defined object ExprF