Incorrect GADT pattern exhaustivity warning

[bishabosha]

A simplification of #6088

minimized code

object GADT {
  import =:=._

  enum =:=[A, B] {
    case Refl[C]() extends (C =:= C)
  }

  def unwrap[A,B](opt: Option[A])(using ev: A =:= Option[B]): Option[B] = ev match {
    case Refl() => opt.flatMap(identity[Option[B]])
  }
}

error:

-- [E029] Pattern Match Exhaustivity Warning: GADT.scala:7:74 
7 |  def unwrap[A,B](opt: Option[A])(given ev: A =:= Option[B]): Option[B] = ev match {
  |                                                                          ^^
  |                               match may not be exhaustive.
  |
  |                               It would fail on pattern case: =:=.Refl()

The warning goes away if you make A contravariant.

expectation

No warning

[bishabosha]

This one works for the type pattern

object GADT {
  import =:=._

  enum =:=[A, B] {
    case Refl[C]() extends (C =:= C)
  }

  def unwrap[A,B](opt: Option[A])(using ev: A =:= Option[B]): Option[B] = ev match {
    case _: Refl[?] => opt.flatMap(identity[Option[B]])
  }
}

[smarter]

@abgruszecki abgruszecki self-assigned this on Mar 19, 2020

@abgruszecki Did you have an angle of attack for this issue? Maybe @liufengyun could help?

[abgruszecki]

I think I just assigned this issue to myself because otherwise it'd simply get lost.

[bishabosha]

another example in 3.0.1-RC1:

object Main extends App:
   enum Extends[A, B]:
     case Ev[B, A <: B]() extends (A Extends B)

     def cast(a: A): B = this match {
       case Extends.Ev() => a
     }

[liufengyun]

This seems to be related to #9682. We need to rethink whether using wildApprox is appropriate in TypeOps.instantiateToSubtype. It also interferes with the changes we did in #8698 to support #8690.