1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
|
package dotty.tools
package dotc
package core
import Types._, Contexts._, Symbols._
import Decorators._
import config.Config
import config.Printers._
/** Methods for adding constraints and solving them.
*
* Constraints are required to be in normalized form. This means
* (1) if P <: Q in C then also Q >: P in C
* (2) if P r Q in C and Q r R in C then also P r R in C, where r is <: or :>
*
* "P <: Q in C" means here: There is a constraint P <: H[Q],
* where H is the multi-hole context given by:
*
* H = []
* H & T
* T & H
* H | H
*
* (the idea is that a parameter Q in a H context is guaranteed to be a supertype of P).
*
* "P >: Q in C" means: There is a constraint P >: L[Q],
* where L is the multi-hole context given by:
*
* L = []
* L | T
* T | L
* L & L
*/
trait ConstraintHandling {
implicit val ctx: Context
def isSubType(tp1: Type, tp2: Type): Boolean
def deSkolemize(tp: Type, toSuper: Boolean): Type
val state: TyperState
import state.constraint
/** If the constraint is frozen we cannot add new bounds to the constraint. */
protected var frozenConstraint = false
/** If the constraint is ignored, subtype checks only take into account
* declared bounds of PolyParams. Used when forming unions and intersectons
* of constraint bounds
*/
private var ignoreConstraint = false
private def ignoringConstraint[T](op: => T): T = {
val savedIgnore = ignoreConstraint
val savedFrozen = frozenConstraint
ignoreConstraint = true
frozenConstraint = true
try op
finally {
ignoreConstraint = savedIgnore
frozenConstraint = savedFrozen
}
}
protected def isSubTypeWhenFrozen(tp1: Type, tp2: Type): Boolean = {
val saved = frozenConstraint
frozenConstraint = true
try isSubType(tp1, tp2)
finally frozenConstraint = saved
}
/** The current bounds of type parameter `param` */
final def bounds(param: PolyParam): TypeBounds = constraint at param match {
case bounds: TypeBounds if !ignoreConstraint => bounds
case _ => param.binder.paramBounds(param.paramNum)
}
/** Compare a solution of the constraint instead of the constrained parameters.
* The solution maps every parameter to its lower bound.
*/
protected var solvedConstraint = false
/** The parameters currently being constrained by addConstraint */
private var pendingParams: Set[PolyParam] = Set()
/** Make p2 = p1, transfer all bounds of p2 to p1 */
private def unify(p1: PolyParam, p2: PolyParam): Boolean = {
constr.println(s"unifying $p1 $p2")
val constraint1 = constraint.unify(p1, p2)
val bounds = constraint1.bounds(p1)
isSubType(bounds.lo, bounds.hi) && { constraint = constraint1; true }
}
/** If current constraint set is not frozen, add the constraint
*
* param >: bound if fromBelow is true
* param <: bound otherwise
*
* to the bounds of `param`. If `bound` is itself a constrained parameter, also
* add the dual constraint to `bound`.
* @pre `param` is in the constraint's domain
* @return Whether the augmented constraint is still satisfiable.
*/
def addConstraint(param: PolyParam, bound0: Type, fromBelow: Boolean): Boolean = {
/** Add bidirectional constraint. If new constraint implies 'A <: B' we also
* make sure 'B >: A' gets added and vice versa. Furthermore, if the constraint
* implies 'A <: B <: A', A and B get unified.
*/
def addc(param: PolyParam, bound: Type, fromBelow: Boolean): Boolean =
constraint.bounds(param) match {
case TypeBounds(plo: PolyParam, phi) if (plo eq phi) && constraint.contains(plo) =>
addc(plo, bound, fromBelow)
case pbounds0 =>
bound match {
case bound: PolyParam if constraint contains bound =>
val bbounds0 @ TypeBounds(lo, hi) = constraint.bounds(bound)
if (lo eq hi)
addc(param, lo, fromBelow)
else if (param == bound)
true
else if (fromBelow && param.occursIn(lo, fromBelow = true))
unify(param, bound)
else if (!fromBelow && param.occursIn(hi, fromBelow = false))
unify(bound, param)
else {
val pbounds = prepare(param, bound, fromBelow)
val bbounds = prepare(bound, param, !fromBelow)
pbounds.exists && bbounds.exists && {
install(param, pbounds.bounds, pbounds0)
install(bound, bbounds.bounds, bbounds0)
true
}
}
case bound: AndOrType if fromBelow != bound.isAnd =>
addc(param, bound.tp1, fromBelow) &&
addc(param, bound.tp2, fromBelow)
case bound: WildcardType =>
true
case bound => // !!! remove to keep the originals
val pbounds = prepare(param, bound, fromBelow)
pbounds.exists && {
install(param, pbounds.bounds, pbounds0)
true
}
}
}
/** Install bounds for param */
def install(param: PolyParam, newBounds: TypeBounds, oldBounds: TypeBounds): Unit = {
val curBounds = constraint.bounds(param)
constraint = constraint.updated(param, newBounds)
if (curBounds ne oldBounds) {
// In this case the bounds were updated previously by a recursive isSubType in
// the satisfiability check of prepare. Reapply the previously added bounds, but
// go through a full addConstraint in order to eliminate any cyclic dependencies
// via unification.
if (!ignoringConstraint(isSubType(curBounds.lo, newBounds.lo)))
addConstraint(param, curBounds.lo, fromBelow)
if (!ignoringConstraint(isSubType(newBounds.hi, curBounds.hi)))
addConstraint(param, curBounds.hi, !fromBelow)
}
}
/** Compute new bounds for `param` and check whether they are
* satisfiable. The check might in turn trigger other additions to the constraint.
* @return The new bounds for `param` (which are not installed yet), or
* NoType, if the new constraint would not be satisfiable.
*/
def prepare(param: PolyParam, bound: Type, fromBelow: Boolean): Type = {
constr.println(s"prepare ${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show}")
val oldBounds = constraint.bounds(param)
val newBounds = ignoringConstraint {
if (fromBelow) oldBounds.derivedTypeBounds(oldBounds.lo | bound, oldBounds.hi)
else oldBounds.derivedTypeBounds(oldBounds.lo, oldBounds.hi & bound)
}
val ok =
(param == bound) ||
(oldBounds eq newBounds) ||
{
if (pendingParams contains param) {
// Why the pendingParams test? It is possible that recursive subtype invocations
// come back with another constraint for `param`. An example came up when compiling
// ElimRepeated where we got the constraint
//
// Coll <: IterableLike[Tree, Coll]
//
// and added
//
// List[Tree] <: Coll
//
// The recursive bounds test is then
//
// List[Tree] <: IterableLike[Tree, Coll]
//
// and because of the F-bounded polymorphism in the supertype of List,
// i.e. List[T] <: IterableLike[T, List[T]], this leads again to
//
// List[Tree] <: Coll
//
// If a parameter is already pending, we avoid revisiting it here.
// Instead we combine the bounds computed here with the originally
// computed bounds when installing the original type.
constr.println(i"deferred bounds: $param $newBounds")
true
} else {
pendingParams += param
try isSubType(newBounds.lo, newBounds.hi)
finally pendingParams -= param
}
}
if (ok) newBounds else NoType
}
val bound = deSkolemize(bound0, toSuper = fromBelow).dealias.stripTypeVar
def description = s"${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show} to ${constraint.show}"
constr.println(s"adding $description")
val res = addc(param, bound, fromBelow)
constr.println(s"added $description")
if (Config.checkConstraintsNonCyclicTrans) constraint.checkNonCyclicTrans()
res
}
final def isConstrained(param: PolyParam): Boolean =
!frozenConstraint && !solvedConstraint && (constraint contains param)
/** Test whether the lower bounds of all parameters in this
* constraint are a solution to the constraint.
*/
final def isSatisfiable: Boolean = {
val saved = solvedConstraint
solvedConstraint = true
try
constraint.forallParams { param =>
val TypeBounds(lo, hi) = constraint.at(param)
isSubType(lo, hi) || {
ctx.log(i"sub fail $lo <:< $hi")
ctx.log(i"approximated = ${approxParams(lo)} <:< ${approxParams(hi)}")
false
}
}
finally solvedConstraint = saved
}
/** Solve constraint set for given type parameter `param`.
* If `fromBelow` is true the parameter is approximated by its lower bound,
* otherwise it is approximated by its upper bound. However, any occurrences
* of the parameter in a refinement somewhere in the bound are removed.
* (Such occurrences can arise for F-bounded types).
* The constraint is left unchanged.
* @return the instantiating type
* @pre `param` is in the constraint's domain.
*/
final def approximation(param: PolyParam, fromBelow: Boolean): Type = {
val avoidParam = new TypeMap {
override def stopAtStatic = true
def apply(tp: Type) = mapOver {
tp match {
case tp: RefinedType if param occursIn tp.refinedInfo => tp.parent
case _ => tp
}
}
}
val bounds = constraint.bounds(param)
val bound = if (fromBelow) bounds.lo else bounds.hi
val inst = avoidParam(bound)
typr.println(s"approx ${param.show}, from below = $fromBelow, bound = ${bound.show}, inst = ${inst.show}")
inst
}
/** Map that approximates each param in constraint by its lower bound.
* Currently only used for diagnostics.
*/
final def approxParams = new TypeMap { // !!! Dotty problem: Turn this def into a val => -Ycheck:mix fails
def apply(tp: Type): Type = tp.stripTypeVar match {
case tp: PolyParam if constraint contains tp =>
this(constraint.bounds(tp).lo)
case tp =>
mapOver(tp)
}
}
}
|
