diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 548c406d4aa6..877630d4913e 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -1234,7 +1234,55 @@ class Typer extends Namer if (tree.isInline) checkInInlineContext("inline match", tree.posd) val sel1 = typedExpr(tree.selector) val selType = fullyDefinedType(sel1.tpe, "pattern selector", tree.span).widen - val result = typedMatchFinish(tree, sel1, selType, tree.cases, pt) + + /** Extractor for match types hidden behind an AppliedType/MatchAlias */ + object MatchTypeInDisguise { + def unapply(tp: AppliedType): Option[MatchType] = tp match { + case AppliedType(tycon: TypeRef, args) => + tycon.info match { + case MatchAlias(alias) => + alias.applyIfParameterized(args) match { + case mt: MatchType => Some(mt) + case _ => None + } + case _ => None + } + case _ => None + } + } + + /** Does `tree` has the same shape as the given match type? + * We only support typed patterns with empty guards, but + * that could potentially be extended in the future. + */ + def isMatchTypeShaped(mt: MatchType): Boolean = + mt.cases.size == tree.cases.size + && sel1.tpe.frozen_<:<(mt.scrutinee) + && tree.cases.forall(_.guard.isEmpty) + && tree.cases + .map(cas => untpd.unbind(untpd.unsplice(cas.pat))) + .zip(mt.cases) + .forall { + case (pat: Typed, pt) => + // To check that pattern types correspond we need to type + // check `pat` here and throw away the result. + val gadtCtx: Context = ctx.fresh.setFreshGADTBounds + val pat1 = typedPattern(pat, selType)(using gadtCtx) + val Typed(_, tpt) = tpd.unbind(tpd.unsplice(pat1)) + instantiateMatchTypeProto(pat1, pt) match { + case defn.MatchCase(patternTp, _) => tpt.tpe frozen_=:= patternTp + case _ => false + } + case _ => false + } + + val result = pt match { + case MatchTypeInDisguise(mt) if isMatchTypeShaped(mt) => + typedDependentMatchFinish(tree, sel1, selType, tree.cases, mt) + case _ => + typedMatchFinish(tree, sel1, selType, tree.cases, pt) + } + result match { case Match(sel, CaseDef(pat, _, _) :: _) => tree.selector.removeAttachment(desugar.CheckIrrefutable) match { @@ -1250,6 +1298,21 @@ class Typer extends Namer result } + /** Special typing of Match tree when the expected type is a MatchType, + * and the patterns of the Match tree and the MatchType correspond. + */ + def typedDependentMatchFinish(tree: untpd.Match, sel: Tree, wideSelType: Type, cases: List[untpd.CaseDef], pt: MatchType)(using Context): Tree = { + var caseCtx = ctx + val cases1 = tree.cases.zip(pt.cases) + .map { case (cas, tpe) => + val case1 = typedCase(cas, sel, wideSelType, tpe)(using caseCtx) + caseCtx = Nullables.afterPatternContext(sel, case1.pat) + case1 + } + .asInstanceOf[List[CaseDef]] + assignType(cpy.Match(tree)(sel, cases1), sel, cases1).cast(pt) + } + // Overridden in InlineTyper for inline matches def typedMatchFinish(tree: untpd.Match, sel: Tree, wideSelType: Type, cases: List[untpd.CaseDef], pt: Type)(using Context): Tree = { val cases1 = harmonic(harmonize, pt)(typedCases(cases, sel, wideSelType, pt.dropIfProto)) @@ -1290,17 +1353,33 @@ class Typer extends Namer } } + /** If the prototype `pt` is the type lambda (when doing a dependent + * typing of a match), instantiate that type lambda with the pattern + * variables found in the pattern `pat`. + */ + def instantiateMatchTypeProto(pat: Tree, pt: Type)(implicit ctx: Context) = pt match { + case caseTp: HKTypeLambda => + val bindingsSyms = tpd.patVars(pat).reverse + val bindingsTps = bindingsSyms.collect { case sym if sym.isType => sym.typeRef } + caseTp.appliedTo(bindingsTps) + case pt => pt + } + /** Type a case. */ def typedCase(tree: untpd.CaseDef, sel: Tree, wideSelType: Type, pt: Type)(using Context): CaseDef = { val originalCtx = ctx val gadtCtx: Context = ctx.fresh.setFreshGADTBounds def caseRest(pat: Tree)(using Context) = { + val pt1 = instantiateMatchTypeProto(pat, pt) match { + case defn.MatchCase(_, bodyPt) => bodyPt + case pt => pt + } val pat1 = indexPattern(tree).transform(pat) val guard1 = typedExpr(tree.guard, defn.BooleanType) - var body1 = ensureNoLocalRefs(typedExpr(tree.body, pt), pt, ctx.scope.toList) - if (pt.isValueType) // insert a cast if body does not conform to expected type if we disregard gadt bounds - body1 = body1.ensureConforms(pt)(originalCtx) + var body1 = ensureNoLocalRefs(typedExpr(tree.body, pt1), pt1, ctx.scope.toList) + if (pt1.isValueType) // insert a cast if body does not conform to expected type if we disregard gadt bounds + body1 = body1.ensureConforms(pt1)(originalCtx) assignType(cpy.CaseDef(tree)(pat1, guard1, body1), pat1, body1) } diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist index 950d1ce60d0f..a4cdd5a650de 100644 --- a/compiler/test/dotc/pos-test-pickling.blacklist +++ b/compiler/test/dotc/pos-test-pickling.blacklist @@ -26,6 +26,7 @@ matchtype.scala i7087.scala i7868.scala i7872.scala +6709.scala # Opaque type i5720.scala diff --git a/docs/docs/reference/new-types/match-types.md b/docs/docs/reference/new-types/match-types.md index 0f3ea15427b4..0ca610f62e05 100644 --- a/docs/docs/reference/new-types/match-types.md +++ b/docs/docs/reference/new-types/match-types.md @@ -3,7 +3,7 @@ layout: doc-page title: "Match Types" --- -A match type reduces to one of a number of right hand sides, depending on a scrutinee type. Example: +A match type reduces to one of its right-hand sides, depending on a scrutinee type. Example: ```scala type Elem[X] = X match { @@ -12,23 +12,29 @@ type Elem[X] = X match { case Iterable[t] => t } ``` -This defines a type that, depending on the scrutinee type `X`, can reduce to one of its right hand sides. For instance, + +This defines a type that reduces as follows: + ```scala Elem[String] =:= Char Elem[Array[Int]] =:= Int Elem[List[Float]] =:= Float Elem[Nil.type] =:= Nothing ``` + Here `=:=` is understood to mean that left and right hand sides are mutually subtypes of each other. In general, a match type is of the form + ```scala S match { P1 => T1 ... Pn => Tn } ``` + where `S`, `T1`, ..., `Tn` are types and `P1`, ..., `Pn` are type patterns. Type variables in patterns start as usual with a lower case letter. Match types can form part of recursive type definitions. Example: + ```scala type LeafElem[X] = X match { case String => Char @@ -37,15 +43,38 @@ type LeafElem[X] = X match { case AnyVal => X } ``` + Recursive match type definitions can also be given an upper bound, like this: + ```scala type Concat[Xs <: Tuple, +Ys <: Tuple] <: Tuple = Xs match { case Unit => Ys case x *: xs => x *: Concat[xs, Ys] } ``` + In this definition, every instance of `Concat[A, B]`, whether reducible or not, is known to be a subtype of `Tuple`. This is necessary to make the recursive invocation `x *: Concat[xs, Ys]` type check, since `*:` demands a `Tuple` as its right operand. +## Dependent typing + +Match types can be used to define dependently type methods. For instance, here is value level counterpart to the`LeafElem` defined above (note the use of the match type as return type): + +```scala +def leafElem[X](x: X): LeafElem[X] = x match { + case x: String => x.charAt(0) + case x: Array[t] => leafElem(x(9)) + case x: Iterable[t] => leafElem(x.next()) + case x: AnyVal => x +} +``` + +This special mode of typing for match expressions is only used when the following conditions are met: + +1. The match expression patterns do not have guards +2. The match expression scrutinee's type is a subtype of the match type scrutinee's type +3. The match expression and the match type have the same number of cases +4. The match expression patterns are all [Typed Patterns](https://scala-lang.org/files/archive/spec/2.13/08-pattern-matching.html#typed-patterns), and these types are `=:=` to their corresponding type patterns in the match type + ## Representation of Match Types The internal representation of a match type @@ -56,6 +85,7 @@ is `Match(S, C1, ..., Cn) <: B` where each case `Ci` is of the form ``` [Xs] =>> P => T ``` + Here, `[Xs]` is a type parameter clause of the variables bound in pattern `Pi`. If there are no bound type variables in a case, the type parameter clause is omitted and only the function type `P => T` is kept. So each case is either a unary function type or a type lambda over a unary function type. `B` is the declared upper bound of the match type, or `Any` if no such bound is given. @@ -63,135 +93,71 @@ We will leave it out in places where it does not matter for the discussion. Scru ## Match type reduction -We define match type reduction in terms of an auxiliary relation, `can-reduce`: +Match type reduction follows the semantics of match expression, that is, a match type of the form `S match { P1 => T1 ... Pn => Tn }` reduces to `Ti` if and only if `s: S match { _: P1 => T1 ... _: Pn => Tn }` evaluates to a value of type `Ti` for all `s: S`. -``` -Match(S, C1, ..., Cn) can-reduce i, T' -``` -if `Ci = [Xs] =>> P => T` and there are minimal instantiations `Is` of the type variables `Xs` such that -``` -S <: [Xs := Is] P -T' = [Xs := Is] T -``` -An instantiation `Is` is _minimal_ for `Xs` if all type variables in `Xs` that appear -covariantly and nonvariantly in `Is` are as small as possible and all type variables in `Xs` that appear contravariantly in `Is` are as large as possible. Here, "small" and "large" are understood with respect to `<:`. +The compiler implements the following reduction algorithm: -For simplicity, we have omitted constraint handling so far. The full formulation of subtyping tests describes them as a function from a constraint and a pair of types to -either _success_ and a new constraint or _failure_. In the context of reduction, the subtyping test `S <: [Xs := Is] P` is understood to leave the bounds of all variables -in the input constraint unchanged, i.e. existing variables in the constraint cannot be instantiated by matching the scrutinee against the patterns. +- If the scrutinee type `S` is an empty set of values (such as `Nothing` or `String & Int`), do not reduce. +- Sequentially consider each pattern `Pi` + - If `S <: Pi` reduce to `Ti`. + - Otherwise, try constructing a proof that `S` and `Pi` are disjoint, or, in other words, that no value `s` of type `S` is also of type `Pi`. + - If such proof is found, proceed to the next case (`Pi+1`), otherwise, do not reduce. -Using `can-reduce`, we can now define match type reduction proper in the `reduces-to` relation: -``` -Match(S, C1, ..., Cn) reduces-to T -``` -if -``` -Match(S, C1, ..., Cn) can-reduce i, T -``` -and, for `j` in `1..i-1`: `Cj` is disjoint from `Ci`, or else `S` cannot possibly match `Cj`. -See the section on [overlapping patterns](#overlapping-patterns) for an elaboration of "disjoint" and "cannot possibly match". +Disjointness proofs rely on the following properties of Scala types: + +1. Single inheritance of classes +2. Final classes cannot be extended +3. Constant types with distinct values are nonintersecting + +Type parameters in patterns are minimally instantiated when computing `S <: Pi`. An instantiation `Is` is _minimal_ for `Xs` if all type variables in `Xs` that appear covariantly and nonvariantly in `Is` are as small as possible and all type variables in `Xs` that appear contravariantly in `Is` are as large as possible. Here, "small" and "large" are understood with respect to `<:`. + +For simplicity, we have omitted constraint handling so far. The full formulation of subtyping tests describes them as a function from a constraint and a pair of types to either _success_ and a new constraint or _failure_. In the context of reduction, the subtyping test `S <: [Xs := Is] P` is understood to leave the bounds of all variables in the input constraint unchanged, i.e. existing variables in the constraint cannot be instantiated by matching the scrutinee against the patterns. ## Subtyping Rules for Match Types The following rules apply to match types. For simplicity, we omit environments and constraints. The first rule is a structural comparison between two match types: + ``` -Match(S, C1, ..., Cm) <: Match(T, D1, ..., Dn) +S match { P1 => T1 ... Pm => Tm } <: T match { Q1 => U1 ... Qn => Un } ``` + if + ``` -S <: T, m >= n, Ci <: Di for i in 1..n +S =:= T, m >= n, Pi =:= Qi and Ti <: Ui for i in 1..n ``` -I.e. scrutinees and corresponding cases must be subtypes, no case re-ordering is allowed, but the subtype can have more cases than the supertype. + +I.e. scrutinees and patterns must be equal and the corresponding bodies must be subtypes. No case re-ordering is allowed, but the subtype can have more cases than the supertype. The second rule states that a match type and its redux are mutual subtypes + ``` - Match(S, Cs) <: T - T <: Match(S, Cs) +S match { P1 => T1 ... Pn => Tn } <: U +U <: S match { P1 => T1 ... Pn => Tn } ``` + if -``` - Match(S, Cs) reduces-to T -``` -The third rule states that a match type conforms to its upper bound ``` - (Match(S, Cs) <: B) <: B +S match { P1 => T1 ... Pn => Tn } reduces-to U ``` -## Variance Laws for Match Types - -Within a match type `Match(S, Cs) <: B`, all occurrences of type variables count as covariant. By the nature of the cases `Ci` this means that occurrences in pattern position are contravarant (since patterns are represented as function type arguments). - - +The third rule states that a match type conforms to its upper bound: -## Typing Rules for Match Expressions (Work in Progress) - - - -Typing rules for match expressions are tricky. First, they need some new form of GADT matching for value parameters. -Second, they have to account for the difference between sequential match on the term level and parallel match on the type level. As a running example consider: -```scala -type M[X] = X match { - case A => 1 - case B => 2 -} ``` -We would like to be able to typecheck -```scala -def m[X](x: X): M[X] = x match { - case _: A => 1 // type error - case _: B => 2 // type error -} -``` -Unfortunately, this goes nowhere. Let's try the first case. We have: `x.type <: A` and `x.type <: X`. This tells -us nothing useful about `X`, so we cannot reduce `M` in order to show that the right hand side of the case is valid. - -The following variant is more promising but does not compile either: -```scala -def m(x: Any): M[x.type] = x match { - case _: A => 1 - case _: B => 2 -} +(S match { P1 => T1 ... Pn => Tn } <: B) <: B ``` -To make this work, we would need a new form of GADT checking: If the scrutinee is a term variable `s`, we can make use of -the fact that `s.type` must conform to the pattern's type and derive a GADT constraint from that. For the first case above, -this would be the constraint `x.type <: A`. The new aspect here is that we need GADT constraints over singleton types where -before we just had constraints over type parameters. - -Assuming this extension, we can then try to typecheck as usual. E.g. to typecheck the first case `case _: A => 1` of the definition of `m` above, GADT matching will produce the constraint `x.type <: A`. Therefore, `M[x.type]` reduces to the singleton type `1`. The right hand side `1` of the case conforms to this type, so the case typechecks. - -Typechecking the second case hits a snag, though. In general, the assumption `x.type <: B` is not enough to prove that -`M[x.type]` reduces to `2`. However we can reduce `M[x.type]` to `2` if the types `A` and `B` do not overlap. -So correspondence of match terms to match types is feasible only in the case of non-overlapping patterns (see next section about [overlapping patterns](#overlapping-patterns)) - -For simplicity, we have disregarded the `null` value in this discussion. `null` does not cause a fundamental problem but complicates things somewhat because some forms of patterns do not match `null`. - -## Overlapping Patterns -A complete defininition of when two patterns or types overlap still needs to be worked out. Some examples we want to cover are: +## Termination - - Two classes overlap only if one is a subtype of the other - - A final class `C` overlaps with a trait `T` only if `C` extends `T` directly or indirectly. - - A class overlaps with a sealed trait `T` only if it overlaps with one of the known subclasses of `T`. - - An abstract type or type parameter `A` overlaps with a type `B` only if `A`'s upper bound overlaps with `B`. - - A union type `A1 | ... | An` overlaps with `B` only if at least one of `Ai` for `i` in `1..n` overlaps with `B`. - - An intersection type `A1 & ... & An` overlaps with `B` only if all of `Ai` for `i` in `1..n` overlap with `B`. - - If `C[X1, ..., Xn]` is a case class, then the instance type `C[A1, ..., An]` overlaps with the instance type `C[B1, ..., Bn]` only if for every index `i` in `1..n`, - if `Xi` is the type of a parameter of the class, then `Ai` overlaps with `Bi`. +Match type definitions can be recursive, which means that it's possible to run +into an infinite loop while reducing match types. - The last rule in particular is needed to detect non-overlaps for cases where the scrutinee and the patterns are tuples. I.e. `(Int, String)` does not overlap `(Int, Int)` since -`String` does not overlap `Int`. - -## Handling Termination - -Match type definitions can be recursive, which raises the question whether and how to check -that reduction terminates. This is currently an open question. We should investigate whether -there are workable ways to enforce that recursion is primitive. - -Note that, since reduction is linked to subtyping, we already have a cycle dectection mechanism in place. +Since reduction is linked to subtyping, we already have a cycle detection mechanism in place. So the following will already give a reasonable error message: + ```scala type L[X] = X match { case Int => L[X] @@ -199,39 +165,25 @@ type L[X] = X match { def g[X]: L[X] = ??? ``` -``` - | val x: Int = g[Int] - | ^^^^^^ - | found: Test.L[Int] - | required: Int -``` - -The subtype cycle test can be circumvented by producing larger types in each recursive invocation, as in the following definitions: ```scala -type LL[X] = X match { - case Int => LL[LL[X]] -} -def gg[X]: LL[X] = ??? -``` -In this case subtyping enters into an infinite recursion. This is not as bad as it looks, however, because -`dotc` turns selected stack overflows into type errors. If there is a stackoverflow during subtyping, -the exception will be caught and turned into a compile-time error that indicates -a trace of the subtype tests that caused the overflow without showing a full stacktrace. -Concretely: -``` - | val xx: Int = gg[Int] - | ^ + | val x: Int = g[Int] + | ^ |Recursion limit exceeded. |Maybe there is an illegal cyclic reference? |If that's not the case, you could also try to increase the stacksize using the -Xss JVM option. |A recurring operation is (inner to outer): | - | subtype Test.LL[Int] <:< Int - | subtype Test.LL[Int] <:< Int - | ... - | subtype Test.LL[Int] <:< Int + | subtype LazyRef(Test.L[Int]) <:< Int ``` -(The actual error message shows some additional lines in the stacktrace). + +Internally, `dotc` detects these cycles by turning selected stackoverflows +into type errors. If there is a stackoverflow during subtyping, the exception +will be caught and turned into a compile-time error that indicates a trace of +the subtype tests that caused the overflow without showing a full stacktrace. + +## Variance Laws for Match Types + +Within a match type `Match(S, Cs) <: B`, all occurrences of type variables count as covariant. By the nature of the cases `Ci` this means that occurrences in pattern position are contravarant (since patterns are represented as function type arguments). ## Related Work @@ -239,8 +191,6 @@ Match types have similarities with [closed type families](https://wiki.haskell.o - Subtyping instead of type equalities. - Match type reduction does not tighten the underlying constraint, whereas type family reduction does unify. This difference in approach mirrors the difference between local type inference in Scala and global type inference in Haskell. - - No a-priori requirement that cases are non-overlapping. Uses parallel reduction - instead of always chosing a unique branch. Match types are also similar to Typescript's [conditional types](https://github.com/Microsoft/TypeScript/pull/21316). The main differences here are: @@ -248,5 +198,4 @@ Match types are also similar to Typescript's [conditional types](https://github. match types also work for type parameters and abstract types. - Match types can bind variables in type patterns. - Match types support direct recursion. - -Conditional types in Typescript distribute through union types. We should evaluate whether match types should support this as well. + - Conditional types distribute through union types. diff --git a/tests/neg/6709.scala b/tests/neg/6709.scala new file mode 100644 index 000000000000..3ee522386bd6 --- /dev/null +++ b/tests/neg/6709.scala @@ -0,0 +1,58 @@ +object Test { + type M[X] = X match { + case Int => String + case Double => Int + } + + def m_OK[X](x: X): M[X] = x match { + case _: Int => "" + case _: Double => 1 + } + + def m_error0[X](x: X): M[X] = x match { + case Some(i: Int) => "" // error + case _: Double => 1 // error + } + + def m_error1[X](x: X): M[X] = x match { + case s: String => "" // error + case _: Double => 1 // error + } + + def m_error2[X](x: X): M[X] = x match { + case _: Double => 1 // error + case _: Int => "" // error + } + + def m_error3[X](x: X): M[X] = x match { + case _: Int => "" // error + } + + def m_error4[X](x: X): M[X] = x match { + case _: Int => "" // error + case _: Double => 1 // error + case _: String => true // error + } + + def m_error5[X](x: X): M[X] = x match { + case _: Int if true => "" // error + case _: Double => 1 // error + } + + case class Blah[A, B](a: A, b: B) + + type LeafElem[X] = X match { + case Array[t] => t + case Blah[a, b] => a + } + + def leafElem_ok[X](x: X): LeafElem[X] = x match { + case y: Array[t] => y.apply(0) + case y: Blah[a, b] => y.a + } + + def leafElem_error[X](x: X): LeafElem[X] = x match { + case y: Array[t] => 0 // error + case y: Blah[a, b] => y.b // error + } +} diff --git a/tests/pos/6709.scala b/tests/pos/6709.scala new file mode 100644 index 000000000000..1833459efff5 --- /dev/null +++ b/tests/pos/6709.scala @@ -0,0 +1,71 @@ +object Foo { + type LeafElem[X] = X match { + case String => Char + case Array[t] => LeafElem[t] + case Iterable[t] => LeafElem[t] + case AnyVal => X + } + + def leafElem[X](x: X): LeafElem[X] = + x match { + case x: String => x.charAt(0) + case x: Array[t] => leafElem(x(0)) + case x: Iterable[t] => leafElem(x.head) + case _: AnyVal => x + } + + def leafElem2[X](x: X): LeafElem[X] = + x match { + case _: String => leafElem[X](x) + case w: Array[t] => leafElem[X](x) + } +} + +object Bar { + import compiletime.S + + type Plus[A <: Int, B <: Int] <: Int = + A match { + case 0 => B + case S[p] => S[Plus[p, B]] + } + + def plus[A <: Int, B <: Int](a: A, b: B): Plus[A, B] = + a match { + case _: 0 => b + case a: S[p] => succ(plus(pred(a), b)) + } + + def pred[X <: Int](x: S[X]): X = (x - 1).asInstanceOf + def succ[X <: Int](x: X): S[X] = (x + 1).asInstanceOf + + val nine: 9 = plus[4, 5](4, 5) +} + +object Main { + enum BinNat { + case Zero + // 2n + 1 + case Odd[N <: BinNat](n: N) + // 2(n + 1) + case Even[N <: BinNat](n: N) + } + + import BinNat._ + + type Inc[N <: BinNat] <: BinNat = + N match { + case Zero.type => Odd[Zero.type] + case Odd[n] => Even[n] + case Even[n] => Odd[Inc[n]] + } + + def inc[N <: BinNat](b: N): Inc[N] = + b match { + case _: Zero.type => new Odd(Zero) + case o: Odd[n] => new Even(o.n) + case e: Even[n] => + // 2(n + 1) + 1 = 2(inc(n)) + 1 + new Odd(inc(e.n)) + } +}