Skip to content
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

Fix unsound injectivity assumption when inferring GADT bounds #13380

Merged
merged 2 commits into from
Aug 26, 2021

Conversation

Linyxus
Copy link
Contributor

@Linyxus Linyxus commented Aug 25, 2021

Current compiler allows the compilation of the following unsound code (as added as a negative test):

/** A modified version of gadt-injectivity-alt.scala. */
object test {

  enum SUB[-F, +G] {
    case Refl[S]() extends SUB[S, S]
  }

  enum KSUB[-F[_], +G[_]] {
    case Refl[S[_]]() extends KSUB[S, S]
  }

  def foo[F[_], G[_], A](
    keq: (F KSUB Option, Option KSUB F),
    ksub: Option KSUB G,
    sub: F[Option[A]] SUB G[Option[Int]],
    a: A
  ) =
    keq._1 match { case KSUB.Refl() =>
      keq._2 match { case KSUB.Refl() =>
        ksub match { case KSUB.Refl() =>
          sub match { case SUB.Refl() =>
            //        F        =  Option
            // &      G       >: Option
            // & F[Option[A]] <: G[Option[Int]]
            // =X=>
            // A <: Int
            //
            // counterexample: G = [T] => Any
            val i: Int = a // error
            ()
          }
        }
      }
    }
}

The soundness problem arises from the implementation of inFrozenGadtIf:

private inline def inFrozenGadtIf[T](cond: Boolean)(inline op: T): T = {
  val savedFrozenGadt = frozenGadt
  frozenGadt = cond
  try op finally frozenGadt = savedFrozenGadt
}

Note that the code will set frozenGadt to cond regardless of its current value. In other words, if we freeze GADT constraints in op1 with inFrozenGadtIf(true)(op1) and in op1 we call inFrozenGadtIf(false)(op2), the GADT constraints will be unfreezed in op2.

In the negative example here, when comparing F[Option[A]] <: G[Option[Int]], we found that the injectivity does not hold, so we will freeze GADT and compare Option[A] <: Option[Int]. However, since the concrete Option constructor has injectivity, we will accidentally unfreeze GADT and infer the constraint A <: Int, which is unsound.

I am not sure whether it is a expected behavior that inFrozenGadtIf(false)(op) unfreezes GADT in op. But after disabling such unfreezing by writing frozenGadt ||= cond in inFrozenGadtIf, the unsound code will be rejected.

@abgruszecki

Copy link
Contributor

@abgruszecki abgruszecki left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@abgruszecki abgruszecki merged commit 2312258 into scala:master Aug 26, 2021
@dwijnand
Copy link
Member

Wow, one boolean slip up and everything goes wrong. Nice fix!

@smarter
Copy link
Member

smarter commented Aug 26, 2021

FWIW, I just checked and #13080 is still reproducible after this.

@Kordyjan Kordyjan added this to the 3.1.0 milestone Aug 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants