New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

GADT pattern matching produces conformance constraints instead of equality (HKTs) #5068

Open
alexknvl opened this Issue Sep 2, 2018 · 1 comment

Comments

Projects
None yet
2 participants
@alexknvl

alexknvl commented Sep 2, 2018

object App {
  case class Box[F[_]](value: F[Int])
  sealed trait IsK[F[_], G[_]]
  final case class ReflK[F[_]]() extends IsK[F, F]

  def foo[F[_], G[_]](r: F IsK G, a: Box[F]): Box[G] = r match { case ReflK() => a }
  
  def main(args: Array[String]): Unit = {
    println(foo(ReflK(), Box(Option(10))))
  }
}
-- [E007] Type Mismatch Error: foo.scala:6:81 ----------------------------------
6 |  def foo[F[_], G[_]](r: F IsK G, a: Box[F]): Box[G] = r match { case ReflK() => a }
  |                                                                                 ^
  |                   found:    App.Box[F](a)
  |                   required: App.Box[G]
  |                   
  |                   where:    F is a type in method foo with bounds <: G[_]
  |                             G is a type in method foo with bounds <: F[_]
one error found

@alexknvl alexknvl changed the title from GADT pattern matching produces conformance constraints instead of equality to GADT pattern matching produces conformance constraints instead of equality (HKTs) Sep 2, 2018

@Blaisorblade

This comment has been minimized.

Show comment
Hide comment
@Blaisorblade

Blaisorblade Sep 6, 2018

Contributor

In Dotty type equality is just type conformance twice: A = B means A <: B and B <: A. But then constraint solving should unify variables if A <: B and B <: A.

So this seems a variant of #4176:

We end up with GADT constraints foo >:> S and S >:> foo but we don't have a mechanism to unify GADT constraints, so we end up with a loop in subtyping checks.

except that even with that bug, we should have F <: G or F <: [X] => G[X], and F <: G[_] looks wrong or misleading.

Contributor

Blaisorblade commented Sep 6, 2018

In Dotty type equality is just type conformance twice: A = B means A <: B and B <: A. But then constraint solving should unify variables if A <: B and B <: A.

So this seems a variant of #4176:

We end up with GADT constraints foo >:> S and S >:> foo but we don't have a mechanism to unify GADT constraints, so we end up with a loop in subtyping checks.

except that even with that bug, we should have F <: G or F <: [X] => G[X], and F <: G[_] looks wrong or misleading.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment