Tweak widenAbstractOKFor docs & doc poisoned

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

@@ -63,6 +63,13 @@ trait ConstraintHandling {
    *  toplevel; it is turned on again when we add parts of the scrutinee to the constraint.
    */
   protected var canWidenAbstract: Boolean = true
+
+  /**
+   * Used for match type reduction.
+   * When an abstract type may not be widened, according to `widenAbstractOKFor`,
+   * we record it in this set, so that we can ultimately fail the reduction, but
+   * with all the information that comes out from continuing to widen the abstract type.
+   */
   protected var poisoned: Set[TypeParamRef] = Set.empty
 
   protected var myNecessaryConstraintsOnly = false

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

@@ -867,10 +867,14 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     }
 
     /** Can we widen an abstract type when comparing with `tp`?
-     *  This is NOT the case if one of the following is true:
-     *    - canWidenAbstract is false,
-     *    - or `tp` contains a non-wildcard type parameter of the matched-against
-     *      case lambda that appears in co- or contra-variant position
+    *   This is the case with the following cases:
+    *    - if `canWidenAbstract` is true.
+     *
+     *  Secondly, if `tp` is a type parameter, we can widen if:
+     *    - if `tp` is not a type parameter of the matched-against case lambda
+     *    - if `tp` is an invariant or wildcard type parameter
+     *    - finally, allow widening, but record the type parameter in `poisoned`,
+     *      so that can be accounted for during the reduction step
      */
     def widenAbstractOKFor(tp: Type): Boolean =
       val acc = new TypeAccumulator[Boolean]:
@@ -3114,6 +3118,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
   }
 
   def matchCases(scrut: Type, cases: List[Type])(using Context): Type = {
+    // a reference for the type parameters poisoned during matching
+    // for use during the reduction step
     var poisoned: Set[TypeParamRef] = Set.empty
 
     def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]:

docs/_docs/reference/new-types/match-types.md

@@ -140,6 +140,8 @@ An instantiation `Is` is _minimal_ for `Xs` if all type variables in `Xs` that
 appear covariantly and nonvariantly in `Is` are as small as possible and all
 type variables in `Xs` that appear contravariantly in `Is` are as large as
 possible.  Here, "small" and "large" are understood with respect to  `<:`.
+But, type parameter will not be "large" if a pattern containing it is matched
+against lambda case in co- or contra-variant position.
 
 For simplicity, we have omitted constraint handling so far. The full formulation
 of subtyping tests describes them as a function from a constraint and a pair of