@@ -1364,14 +1364,26 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
13641364
13651365 /** Returns true iff the result of evaluating either `op1` or `op2` is true and approximates resulting constraints.
13661366 *
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.
13691374 *
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
13701380 * @see [[sufficientEither ]] for the normal case
1371- * @see [[necessaryEither ]] for the GADTFlexible case
13721381 */
13731382 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)
13751387
13761388 /** Returns true iff the result of evaluating either `op1` or `op2` is true,
13771389 * 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
14381450 * T1 & T2 <:< T3
14391451 * T1 <:< T2 | T3
14401452 *
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
14431455 *
14441456 * enum Expr[T] {
14451457 * case IntExpr(i: Int) extends Expr[Int]
@@ -1466,48 +1478,49 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
14661478 *
14671479 * then the necessary constraint is { A = Int }, but correctly inferring that is, as far as we know, too expensive.
14681480 *
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+ *
14691485 * Method name comes from the notion that we are keeping the constraint which is necessary to satisfy both
14701486 * subtyping relationships.
14711487 */
1472- private def necessaryEither (op1 : => Boolean , op2 : => Boolean ): Boolean = {
1488+ private def necessaryEither (op1 : => Boolean , op2 : => Boolean ): Boolean =
14731489 val preConstraint = constraint
1474-
14751490 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
14811502 constraint = preConstraint
14821503 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
14971514 gadts.println(i " GADT CUT - no constraint is preferable, reverting to $preGadt" )
14981515 constr.println(i " CUT - no constraint is preferable, reverting to $preConstraint" )
14991516 constraint = preConstraint
15001517 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
15091522 else op2
1510- }
1523+ end necessaryEither
15111524
15121525 /** Does type `tp1` have a member with name `name` whose normalized type is a subtype of
15131526 * the normalized type of the refinement `tp2`?
0 commit comments