@@ -153,20 +153,39 @@ object Inferencing {
153
153
def isSkolemFree (tp : Type )(implicit ctx : Context ): Boolean =
154
154
! tp.existsPart(_.isInstanceOf [SkolemType ])
155
155
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:
157
158
*
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
161
162
*
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`.
167
165
*
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?
170
189
*/
171
190
def constrainPatternType (tp : Type , pt : Type , termPattern : Boolean )(implicit ctx : Context ): Boolean = {
172
191
def refinementIsInvariant (tp : Type ): Boolean = tp match {
0 commit comments