@@ -153,20 +153,39 @@ object Inferencing {
153153 def isSkolemFree (tp : Type )(implicit ctx : Context ): Boolean =
154154 ! tp.existsPart(_.isInstanceOf [SkolemType ])
155155
156- /** Infer constraints that should be in scope for a case body with given pattern and scrutinee types.
156+ /** Derive information about a pattern type by comparing it with some variant of the
157+ * static scrutinee type. We have the following situation in case of a (dynamic) pattern match:
157158 *
158- * If `termPattern`, infer constraints from knowing that there exists a value which of both scrutinee
159- * and pattern types (which is the case for normal pattern matching). If not `termPattern`, instead
160- * infer constraints from knowing that `tp <: pt`.
159+ * StaticScrutineeType PatternType
160+ * \ /
161+ * DynamicScrutineeType
161162 *
162- * If a pattern matches during normal pattern matching, we can be certain that there exists a value
163- * which is of both scrutinee and pattern types (the value we're matching on). If this value
164- * was in a variable, say `x`, then we could simply infer constraints from `x.type <: pt`. Since we might
165- * be matching on an expression as well, we take a skolem of the scrutinee, which is essentially an existential
166- * singleton type (see [[dotty.tools.dotc.core.Types.SkolemType ]]).
163+ * If `PatternType` is not a subtype of `StaticScrutineeType, there's no information to be gained.
164+ * Now let's say we can prove that `PatternType <: StaticScrutineeType`.
167165 *
168- * Note that we need to sometimes widen type parameters of the scrutinee type to avoid unsoundness -
169- * see i3989c.scala and related issue discussion on Github.
166+ * StaticScrutineeType
167+ * | \
168+ * | \
169+ * | \
170+ * | PatternType
171+ * | /
172+ * DynamicScrutineeType
173+ *
174+ * What can we say about the relationship of parameter types between `PatternType` and
175+ * `DynamicScrutineeType`?
176+ *
177+ * - If `DynamicScrutineeType` refines the type parameters of `StaticScrutineeType`
178+ * in the same way as `PatternType` ("invariant refinement"), the subtype test
179+ * `PatternType <:< StaticScrutineeType` tells us all we need to know.
180+ * - Otherwise, if variant refinement is a possibility we can only make predictions
181+ * about invariant parameters of `StaticScrutineeType`. Hence we do a subtype test
182+ * where `PatternType <: widenVariantParams(StaticScrutineeType)`, where `widenVariantParams`
183+ * replaces all type argument of variant parameters with empty bounds.
184+ *
185+ * Invariant refinement can be assumed if `PatternType`'s class(es) are final or
186+ * case classes (because of `RefChecks#checkCaseClassInheritanceInvariant`).
187+ *
188+ * @param termPattern are we dealing with a term-level or a type-level pattern?
170189 */
171190 def constrainPatternType (tp : Type , pt : Type , termPattern : Boolean )(implicit ctx : Context ): Boolean = {
172191 def refinementIsInvariant (tp : Type ): Boolean = tp match {
0 commit comments