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

Soundness issue with type pattern #1754

Closed
smarter opened this issue Nov 29, 2016 · 0 comments
Closed

Soundness issue with type pattern #1754

smarter opened this issue Nov 29, 2016 · 0 comments

Comments

@smarter
Copy link
Member

smarter commented Nov 29, 2016

This doesn't compile, as expected:

case class One[T](fst: T)

object Test {
  def good[T](e: One[T]) = e match {
    case One(_) =>
      val t: T = e.fst
      val nok: Nothing = t // error, as expected
  }
}

But this does:

case class One[T](fst: T)

object Test {
  def bad[T](e: One[T]) = e match {
    case foo: One[a] =>
      val t: T = e.fst
      val nok: Nothing = t // should not compile
  }
}
odersky added a commit to dotty-staging/dotty that referenced this issue Jan 25, 2018
In a type pattern, a wildcard argument and a type variable needs to be treated the same.
I.e. it should make no difference if I have

    C[_ >: L <: H]

or

    C[t >: L <: H]

where `t` is unused. Previously, the two constructs had largely different codepaths with
different things that failed and worked. This fix is necessary to mitigate the fix for
scala#1754. The latter fix uncovered several problems with the way wildcard arguments in
patterns were treated.

The change also uncovered a problem in transforms: FirstTransform eliminates all type
nodes wnd with it any binders bound type symbols. This means that subsequently patVars
is wrong, and therefore a TreeTypeMap over a pattern will no longer duplicate pattern-
bound type variables. This caused Ycheck to fail after TailRec.

The fix is to keep pattern bound type variables around in an internal annotation, which
is understood by patVars.
odersky added a commit to dotty-staging/dotty that referenced this issue Jan 25, 2018
neg/i1754.scala succeeded because a GADT bound for `A` in `A <: B`
was narrowed to the lower bound of `B` (which was nothing) instead of
`B` itself. Fixing this uncovered several other problems that were
hidden by the overly aggressive narrowing "feature".
odersky added a commit to dotty-staging/dotty that referenced this issue Jan 25, 2018
In a type pattern, a wildcard argument and a type variable needs to be treated the same.
I.e. it should make no difference if I have

    C[_ >: L <: H]

or

    C[t >: L <: H]

where `t` is unused. Previously, the two constructs had largely different codepaths with
different things that failed and worked. This fix is necessary to mitigate the fix for
scala#1754. The latter fix uncovered several problems with the way wildcard arguments in
patterns were treated.

The change also uncovered a problem in transforms: FirstTransform eliminates all type
nodes wnd with it any binders bound type symbols. This means that subsequently patVars
is wrong, and therefore a TreeTypeMap over a pattern will no longer duplicate pattern-
bound type variables. This caused Ycheck to fail after TailRec.

The fix is to keep pattern bound type variables around in an internal annotation, which
is understood by patVars.
odersky added a commit to dotty-staging/dotty that referenced this issue Jan 25, 2018
neg/i1754.scala succeeded because a GADT bound for `A` in `A <: B`
was narrowed to the lower bound of `B` (which was nothing) instead of
`B` itself. Fixing this uncovered several other problems that were
hidden by the overly aggressive narrowing "feature".
smarter pushed a commit to dotty-staging/dotty that referenced this issue Feb 1, 2018
In a type pattern, a wildcard argument and a type variable needs to be treated the same.
I.e. it should make no difference if I have

    C[_ >: L <: H]

or

    C[t >: L <: H]

where `t` is unused. Previously, the two constructs had largely different codepaths with
different things that failed and worked. This fix is necessary to mitigate the fix for
scala#1754. The latter fix uncovered several problems with the way wildcard arguments in
patterns were treated.

The change also uncovered a problem in transforms: FirstTransform eliminates all type
nodes wnd with it any binders bound type symbols. This means that subsequently patVars
is wrong, and therefore a TreeTypeMap over a pattern will no longer duplicate pattern-
bound type variables. This caused Ycheck to fail after TailRec.

The fix is to keep pattern bound type variables around in an internal annotation, which
is understood by patVars.
smarter pushed a commit to dotty-staging/dotty that referenced this issue Feb 1, 2018
neg/i1754.scala succeeded because a GADT bound for `A` in `A <: B`
was narrowed to the lower bound of `B` (which was nothing) instead of
`B` itself. Fixing this uncovered several other problems that were
hidden by the overly aggressive narrowing "feature".
odersky added a commit to dotty-staging/dotty that referenced this issue Feb 2, 2018
In a type pattern, a wildcard argument and a type variable needs to be treated the same.
I.e. it should make no difference if I have

    C[_ >: L <: H]

or

    C[t >: L <: H]

where `t` is unused. Previously, the two constructs had largely different codepaths with
different things that failed and worked. This fix is necessary to mitigate the fix for
scala#1754. The latter fix uncovered several problems with the way wildcard arguments in
patterns were treated.

The change also uncovered a problem in transforms: FirstTransform eliminates all type
nodes wnd with it any binders bound type symbols. This means that subsequently patVars
is wrong, and therefore a TreeTypeMap over a pattern will no longer duplicate pattern-
bound type variables. This caused Ycheck to fail after TailRec.

The fix is to keep pattern bound type variables around in an internal annotation, which
is understood by patVars.
odersky added a commit to dotty-staging/dotty that referenced this issue Feb 2, 2018
neg/i1754.scala succeeded because a GADT bound for `A` in `A <: B`
was narrowed to the lower bound of `B` (which was nothing) instead of
`B` itself. Fixing this uncovered several other problems that were
hidden by the overly aggressive narrowing "feature".
odersky added a commit to dotty-staging/dotty that referenced this issue Feb 2, 2018
In a type pattern, a wildcard argument and a type variable needs to be treated the same.
I.e. it should make no difference if I have

    C[_ >: L <: H]

or

    C[t >: L <: H]

where `t` is unused. Previously, the two constructs had largely different codepaths with
different things that failed and worked. This fix is necessary to mitigate the fix for
scala#1754. The latter fix uncovered several problems with the way wildcard arguments in
patterns were treated.

The change also uncovered a problem in transforms: FirstTransform eliminates all type
nodes wnd with it any binders bound type symbols. This means that subsequently patVars
is wrong, and therefore a TreeTypeMap over a pattern will no longer duplicate pattern-
bound type variables. This caused Ycheck to fail after TailRec.

The fix is to keep pattern bound type variables around in an internal annotation, which
is understood by patVars.
@odersky odersky closed this as completed in 4f24531 Feb 3, 2018
odersky added a commit that referenced this issue Feb 3, 2018
Fix #1754: Don't narrow GADTs to lower bounds
Blaisorblade added a commit to dotty-staging/dotty that referenced this issue Mar 4, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant