Skip to content

Commit 7d5046f

Browse files
committed
add tons of documentation
1 parent 898c47d commit 7d5046f

File tree

3 files changed

+51
-16
lines changed

3 files changed

+51
-16
lines changed

compiler/src/dotty/tools/dotc/core/GadtConstraint.scala

Lines changed: 18 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ sealed abstract class GadtConstraint extends Showable {
2525
/** Immediate bounds of a path-dependent type.
2626
* This variant of bounds will ONLY try to retrieve path-dependent GADT bounds. */
2727
def bounds(path: PathType, sym: Symbol)(using Context): TypeBounds | Null
28+
29+
/** Immediate bounds of path-dependent type tp. */
2830
def bounds(tp: TypeRef)(using Context): TypeBounds | Null
2931

3032
/** Full bounds of `sym`, including TypeRefs to other lower/upper symbols.
@@ -34,7 +36,10 @@ sealed abstract class GadtConstraint extends Showable {
3436
*/
3537
def fullBounds(sym: Symbol)(using Context): TypeBounds | Null
3638

39+
/** Full bounds of path dependent type path.sym. */
3740
def fullBounds(path: PathType, sym: Symbol)(using Context): TypeBounds | Null
41+
42+
/** Full bounds of path-dependent type tp. */
3843
def fullBounds(tp: TypeRef)(using Context): TypeBounds | Null
3944

4045
/** Is `sym1` ordered to be less than `sym2`? */
@@ -65,7 +70,10 @@ sealed abstract class GadtConstraint extends Showable {
6570
/** Check whether two paths are equivalent via path aliasing. */
6671
def isAliasingPath(p: PathType, q: PathType): Boolean
6772

68-
/** Scrutinee path of the current pattern matching. */
73+
/** Scrutinee path of the current pattern matching that is being typed.
74+
*
75+
* See `constrainTypeMembers` in `PatternTypeConstrainer`.
76+
*/
6977
def scrutineePath: TermRef | Null
7078

7179
/** Reset scrutinee path to null. */
@@ -74,10 +82,16 @@ sealed abstract class GadtConstraint extends Showable {
7482
/** Set the scrutinee path. */
7583
def withScrutineePath[T](path: TermRef | Null)(op: => T): T
7684

77-
/** Supply the real pattern path. */
85+
/** Supply the real pattern path.
86+
*
87+
* See `constrainTypeMembers` in `PatternTypeConstrainer`.
88+
*/
7889
def supplyPatternPath(path: TermRef)(using Context): Unit
7990

80-
/** Create a skolem type for pattern. */
91+
/** Create a skolem type for pattern and save it in the constraint handler.
92+
*
93+
* See `constrainTypeMembers` in `PatternTypeConstrainer`.
94+
*/
8195
def createPatternSkolem(pat: Type): SkolemType
8296

8397
/** Is the symbol registered in the constraint?
@@ -95,6 +109,7 @@ sealed abstract class GadtConstraint extends Showable {
95109
/** Checks whether a given path-dependent type is constrainable. */
96110
def isConstrainablePDT(path: PathType, sym: Symbol)(using Context): Boolean
97111

112+
/** Get all type members registered in the constraint handler for this path. */
98113
def registeredTypeMembers(path: PathType): List[Symbol]
99114

100115
/** GADT constraint narrows bounds of at least one variable */

compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -201,6 +201,7 @@ trait PatternTypeConstrainer { self: TypeComparer =>
201201
*
202202
* To inference SR constraints for the type members from the scrutinee `p` and the pattern `q`,
203203
* we first find all the abstract type members of `p`: A₁, A₂, ⋯, Aₖ.
204+
* If these path-dependent types are not registered in the handler, we will register them.
204205
*
205206
* Then, for each Aᵢ, if `q` also has a type member labaled `Aᵢ`, we inference SR constraints by calling
206207
* TypeComparer on the relation `p.Aᵢ <:< q.Aᵢ`.
@@ -209,12 +210,12 @@ trait PatternTypeConstrainer { self: TypeComparer =>
209210
* Specially, if for some `Aᵢ`, `p.Aᵢ` is abstract while `q.Aᵢ` is not, we will extract constraints
210211
* for both directions of the subtype relations (i.e. both `p.Aᵢ <:< q.Aᵢ` and `q.Aᵢ <:< p.Aᵢ`).
211212
*
212-
* How we find out and handle the path (`TermRef`) of the scrutinee and pattern.
213+
* How we find out and handle the path (`TermRef`) of the scrutinee and pattern:
213214
*
214-
* - The path of scrutinee is not directly available in `constrainPatternType`, since the scrutinee type
215-
* passed to this function is widened.
216-
* To make the path available during GADT reasoning, we save the scrutinee path in `Typer.typedCase`. The scrutinee path will be saved in `ctx.gadt.scrutineePath`.
217-
* Note that we have to clear the saved scrutinee path after using by calling `ctx.gadt.resetScrutineePath()`.
215+
* - The path of scrutinee is not directly available in `constrainPatternType`, since the scrutinee type passed to this function is widened.
216+
* To have access to the scrutinee path here, we save the scrutinee path in `Typer.typedCase` with `GadtConstraint.withScrutineePath`,
217+
* and the scrutinee path will be accessible as `ctx.gadt.scrutineePath`.
218+
* Note that we have to reset the saved scrutinee path to `null` after using by calling `ctx.gadt.resetScrutineePath()`.
218219
* This is because `constrainPatternType` may be called multiple times for one nested pattern. For example:
219220
*
220221
* e match
@@ -230,7 +231,7 @@ trait PatternTypeConstrainer { self: TypeComparer =>
230231
import NameKinds.DepParamName
231232
val realScrutineePath = ctx.gadt.scrutineePath
232233

233-
/* We reset scrutinee path so that the path will only be used at top level. */
234+
// We reset scrutinee path so that the path will only be used at top level.
234235
ctx.gadt.resetScrutineePath()
235236

236237
val saved = state.nn.constraint
@@ -242,8 +243,9 @@ trait PatternTypeConstrainer { self: TypeComparer =>
242243
val patternPath: SkolemType = ctx.gadt.createPatternSkolem(pat)
243244

244245
val registerScrutinee = ctx.gadt.contains(scrutineePath) || ctx.gadt.addToConstraint(scrutineePath)
245-
val registerPattern = ctx.gadt.addToConstraint(patternPath) // Pattern path is a freshly-created skolem,
246-
// so it will always be un-registered at this point
246+
// Pattern path is a freshly-created skolem,
247+
// so it will always be un-registered at this point
248+
val registerPattern = ctx.gadt.addToConstraint(patternPath)
247249

248250
/** Reconstruct subtype constraints for a path `p`, given that `p` and `q`
249251
are cohabitated.
@@ -260,7 +262,7 @@ trait PatternTypeConstrainer { self: TypeComparer =>
260262
261263
(3) q.T is unregistered. We will do SR on p.T <:< q.T and q.T <:< p.T.
262264
*/
263-
def reconstructSubTypeFor(p: PathType, q: PathType) =
265+
def reconstructSubType(p: PathType, q: PathType) =
264266
def processMember(sym: Symbol): Boolean =
265267
q.member(sym.name).isInstanceOf[NoDenotation.type] || {
266268
val pType = TypeRef(p, sym)
@@ -281,8 +283,8 @@ trait PatternTypeConstrainer { self: TypeComparer =>
281283
def constrainPattern: Boolean = {
282284
ctx.gadt.recordPathAliasing(scrutineePath, patternPath)
283285

284-
(!registerPattern || reconstructSubTypeFor(patternPath, scrutineePath))
285-
&& (!registerScrutinee || reconstructSubTypeFor(scrutineePath, patternPath))
286+
(!registerPattern || reconstructSubType(patternPath, scrutineePath))
287+
&& (!registerScrutinee || reconstructSubType(scrutineePath, patternPath))
286288
}
287289

288290
/** Reconstruct subtype when the pattern is an alias to another path.
@@ -299,8 +301,8 @@ trait PatternTypeConstrainer { self: TypeComparer =>
299301
val registerPtPath = ctx.gadt.contains(ptPath) || ctx.gadt.addToConstraint(ptPath)
300302

301303
val result =
302-
(!registerPtPath || reconstructSubTypeFor(ptPath, scrutineePath))
303-
&& (!registerScrutinee || reconstructSubTypeFor(scrutineePath, ptPath))
304+
(!registerPtPath || reconstructSubType(ptPath, scrutineePath))
305+
&& (!registerScrutinee || reconstructSubType(scrutineePath, ptPath))
304306

305307
ctx.gadt.recordPathAliasing(scrutineePath, ptPath)
306308

compiler/src/dotty/tools/dotc/typer/Typer.scala

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1755,18 +1755,36 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
17551755
case p: TermRef =>
17561756
tree.pat match {
17571757
case _: (Trees.Typed[_] | Trees.Ident[_] | Trees.Apply[_] | Trees.Bind[_]) =>
1758+
// We only record scrutinee path in the above cases, b/c recording
1759+
// it in all cases may lead to unsoundness.
1760+
//
1761+
// For example:
1762+
//
1763+
// def foo(e: (Expr, Expr)) = e match
1764+
// case (e1: Expr, e2: Expr) =>
1765+
//
1766+
// Here the pattern is a tuple. `constrainPatternType` will be called
1767+
// on the two elements of the tuple directly, without constraining
1768+
// `e` and the whole tuple first.
1769+
// Therefore, recording the scrutinee path in this case can give
1770+
// us constraints like `e1.type == e.type`, which is not true.
17581771
p
17591772
case _ =>
17601773
null
17611774
}
17621775
case _ => null
17631776
}
17641777

1778+
// Save the scrutinee path and then type the pattern.
1779+
// The scrutinee path will be used in SR reasoning for path-dependent types.
1780+
// See `constrainTypeMembers` in `PatternTypeConstrainer`.
17651781
val pat1 = gadtCtx.gadt.withScrutineePath(scrutineePath) {
17661782
typedPattern(tree.pat, wideSelType)(using gadtCtx)
17671783
}
17681784

17691785
if scrutineePath.ne(null) && pat1.symbol.isPatternBound then
1786+
// Subtitute the place holder with real pattern path in GADT constraints.
1787+
// See `constrainTypeMembers` in `PatternTypeConstrainer`.
17701788
gadtCtx.gadt.supplyPatternPath(pat1.symbol.termRef)
17711789

17721790
caseRest(pat1)(

0 commit comments

Comments
 (0)