@@ -1364,14 +1364,26 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
1364
1364
1365
1365
/** Returns true iff the result of evaluating either `op1` or `op2` is true and approximates resulting constraints.
1366
1366
*
1367
- * If we're _not_ in GADTFlexible mode, we try to keep the smaller of the two constraints.
1368
- * If we're _in_ GADTFlexible mode, we keep the smaller constraint if any, or no constraint at all.
1367
+ * If we're inferring GADT bounds or constraining a method based on its
1368
+ * expected type, we infer only the _necessary_ constraints, this means we
1369
+ * keep the smaller constraint if any, or no constraint at all. This is
1370
+ * necessary for GADT bounds inference to be sound. When constraining a
1371
+ * method, this avoid committing of constraints that would later prevent us
1372
+ * from typechecking method arguments, see or-inf.scala and and-inf.scala for
1373
+ * examples.
1369
1374
*
1375
+ * Otherwise, we infer _sufficient_ constraints: we try to keep the smaller of
1376
+ * the two constraints, but if never is smaller than the other, we just pick
1377
+ * the first one.
1378
+ *
1379
+ * @see [[necessaryEither ]] for the GADT / result type case
1370
1380
* @see [[sufficientEither ]] for the normal case
1371
- * @see [[necessaryEither ]] for the GADTFlexible case
1372
1381
*/
1373
1382
protected def either (op1 : => Boolean , op2 : => Boolean ): Boolean =
1374
- if (ctx.mode.is(Mode .GadtConstraintInference )) necessaryEither(op1, op2) else sufficientEither(op1, op2)
1383
+ if ctx.mode.is(Mode .GadtConstraintInference ) || ctx.mode.is(Mode .ConstrainResult ) then
1384
+ necessaryEither(op1, op2)
1385
+ else
1386
+ sufficientEither(op1, op2)
1375
1387
1376
1388
/** Returns true iff the result of evaluating either `op1` or `op2` is true,
1377
1389
* trying at the same time to keep the constraint as wide as possible.
@@ -1438,8 +1450,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
1438
1450
* T1 & T2 <:< T3
1439
1451
* T1 <:< T2 | T3
1440
1452
*
1441
- * Unlike [[sufficientEither ]], this method is used in GADTFlexible mode, when we are attempting to infer GADT
1442
- * constraints that necessarily follow from the subtyping relationship. For instance, if we have
1453
+ * Unlike [[sufficientEither ]], this method is used in GADTConstraintInference mode, when we are attempting
1454
+ * to infer GADT constraints that necessarily follow from the subtyping relationship. For instance, if we have
1443
1455
*
1444
1456
* enum Expr[T] {
1445
1457
* case IntExpr(i: Int) extends Expr[Int]
@@ -1466,48 +1478,49 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
1466
1478
*
1467
1479
* then the necessary constraint is { A = Int }, but correctly inferring that is, as far as we know, too expensive.
1468
1480
*
1481
+ * This method is also used in ConstrainResult mode
1482
+ * to avoid inference getting stuck due to lack of backtracking,
1483
+ * see or-inf.scala and and-inf.scala for examples.
1484
+ *
1469
1485
* Method name comes from the notion that we are keeping the constraint which is necessary to satisfy both
1470
1486
* subtyping relationships.
1471
1487
*/
1472
- private def necessaryEither (op1 : => Boolean , op2 : => Boolean ): Boolean = {
1488
+ private def necessaryEither (op1 : => Boolean , op2 : => Boolean ): Boolean =
1473
1489
val preConstraint = constraint
1474
-
1475
1490
val preGadt = ctx.gadt.fresh
1476
- // if GADTflexible mode is on, we expect to always have a ProperGadtConstraint
1477
- val pre = preGadt.asInstanceOf [ProperGadtConstraint ]
1478
- if (op1) {
1479
- val leftConstraint = constraint
1480
- val leftGadt = ctx.gadt.fresh
1491
+
1492
+ def allSubsumes (leftGadt : GadtConstraint , rightGadt : GadtConstraint , left : Constraint , right : Constraint ): Boolean =
1493
+ subsumes(left, right, preConstraint) && preGadt.match
1494
+ case preGadt : ProperGadtConstraint =>
1495
+ preGadt.subsumes(leftGadt, rightGadt, preGadt)
1496
+ case _ =>
1497
+ true
1498
+
1499
+ if op1 then
1500
+ val op1Constraint = constraint
1501
+ val op1Gadt = ctx.gadt.fresh
1481
1502
constraint = preConstraint
1482
1503
ctx.gadt.restore(preGadt)
1483
- if (op2)
1484
- if (pre.subsumes(leftGadt, ctx.gadt, preGadt) && subsumes(leftConstraint, constraint, preConstraint)) {
1485
- gadts.println(i " GADT CUT - prefer ${ctx.gadt} over $leftGadt" )
1486
- constr.println(i " CUT - prefer $constraint over $leftConstraint" )
1487
- true
1488
- }
1489
- else if (pre.subsumes(ctx.gadt, leftGadt, preGadt) && subsumes(constraint, leftConstraint, preConstraint)) {
1490
- gadts.println(i " GADT CUT - prefer $leftGadt over ${ctx.gadt}" )
1491
- constr.println(i " CUT - prefer $leftConstraint over $constraint" )
1492
- constraint = leftConstraint
1493
- ctx.gadt.restore(leftGadt)
1494
- true
1495
- }
1496
- else {
1504
+ if op2 then
1505
+ if allSubsumes(op1Gadt, ctx.gadt, op1Constraint, constraint) then
1506
+ gadts.println(i " GADT CUT - prefer ${ctx.gadt} over $op1Gadt" )
1507
+ constr.println(i " CUT - prefer $constraint over $op1Constraint" )
1508
+ else if allSubsumes(ctx.gadt, op1Gadt, constraint, op1Constraint) then
1509
+ gadts.println(i " GADT CUT - prefer $op1Gadt over ${ctx.gadt}" )
1510
+ constr.println(i " CUT - prefer $op1Constraint over $constraint" )
1511
+ constraint = op1Constraint
1512
+ ctx.gadt.restore(op1Gadt)
1513
+ else
1497
1514
gadts.println(i " GADT CUT - no constraint is preferable, reverting to $preGadt" )
1498
1515
constr.println(i " CUT - no constraint is preferable, reverting to $preConstraint" )
1499
1516
constraint = preConstraint
1500
1517
ctx.gadt.restore(preGadt)
1501
- true
1502
- }
1503
- else {
1504
- constraint = leftConstraint
1505
- ctx.gadt.restore(leftGadt)
1506
- true
1507
- }
1508
- }
1518
+ else
1519
+ constraint = op1Constraint
1520
+ ctx.gadt.restore(op1Gadt)
1521
+ true
1509
1522
else op2
1510
- }
1523
+ end necessaryEither
1511
1524
1512
1525
/** Does type `tp1` have a member with name `name` whose normalized type is a subtype of
1513
1526
* the normalized type of the refinement `tp2`?
0 commit comments