Skip to content

Fix #7807: Add case for MatchTypes to ApproximatingTypeMap #7835

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.

Sign up for GitHub

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

Merged
merged 2 commits into from
Jan 7, 2020
Merged

Fix #7807: Add case for MatchTypes to ApproximatingTypeMap #7835

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6e60814
Fix #7807: Add case for MatchTypes to ApproximatingTypeMap
odersky Dec 22, 2019
2662cdc
Add extra test cases for #7807
smarter Jan 6, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion compiler/src/dotty/tools/dotc/core/Types.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3966,7 +3966,6 @@ object Types {
* and `X_1,...X_n` are the type variables bound in `patternType`
*/
abstract case class MatchType(bound: Type, scrutinee: Type, cases: List[Type]) extends CachedProxyType with ValueType {

def derivedMatchType(bound: Type, scrutinee: Type, cases: List[Type])(implicit ctx: Context): MatchType =
if (bound.eq(this.bound) && scrutinee.eq(this.scrutinee) && cases.eqElements(this.cases)) this
else MatchType(bound, scrutinee, cases)
Expand Down Expand Up @@ -4945,6 +4944,15 @@ object Types {
override protected def derivedWildcardType(tp: WildcardType, bounds: Type): WildcardType =
tp.derivedWildcardType(rangeToBounds(bounds))

override protected def derivedMatchType(tp: MatchType, bound: Type, scrutinee: Type, cases: List[Type]): Type =
bound match
case Range(lo, hi) =>
range(derivedMatchType(tp, lo, scrutinee, cases), derivedMatchType(tp, hi, scrutinee, cases))
case _ =>
scrutinee match
case Range(lo, hi) => range(bound.bounds.lo, bound.bounds.hi)
case _ => tp.derivedMatchType(bound, scrutinee, cases)

override protected def derivedSkolemType(tp: SkolemType, info: Type): Type = info match {
case Range(lo, hi) =>
range(tp.derivedSkolemType(lo), tp.derivedSkolemType(hi))
Expand Down
3 changes: 3 additions & 0 deletions tests/pos/i7807.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
object Test with

def flip: (x: 0 | 1) => x.type match { case 0 => 1 case 1 => 0 } = ???
Copy link
Contributor

Choose a reason for hiding this comment

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

I would add some more tests:

   flip(0): 1
   flip(1): 0

   flip(if ??? then 0 else 1)
   val n: 0 | 1 = if ??? then 0 else 1
   flip(n)

   val m: n.type match { case 0 => 1 case 1 => 0 } = flip(n)

But I noticed a strange thing: a match type is apparently not a subtype of the union of it branches. So adding flip(m) or flip(flip(n)) for instance does not work:

-- [E007] Type Mismatch Error: tests/pos/i7807.scala:15:8 --------------------------------------------------------------
15 |   flip(m)
   |        ^
   |        Found:    (Test.m :
   |          (Test.n : (0 : Int) | (1 : Int)) match {
   |            case (0 : Int) => (1 : Int)
   |            case (1 : Int) => (0 : Int)
   |          }
   |        )
   |        Required: (0 : Int) | (1 : Int)

Should an issue be opened about this? Though it seems the current spec does not say this should work, I find it surprising that it does not.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I am not sure it should work. Generally, match types are on a thin line between expressiveness and soundness. So generally demanding they do more than they do would have to come with an algorithm that shows how to do it and an argument why this would not break soundness.