NI: Support forking inference with heuristics

Mostly, it only affects FIR

It partially allows to consider several variance of constraints like
A<Int> & A<T> <: A<X_var> that are mostly brought by smart casts

^KT-49542 Fixed
^KT-50489 Relates

analysis/analysis-api-fir/src/org/jetbrains/kotlin/analysis/api/fir/diagnostics/KtFirDataClassConverters.kt

@@ -1524,6 +1524,13 @@ internal val KT_DIAGNOSTIC_CONVERTER = KtDiagnosticConverterBuilder.buildConvert
             token,
         )
     }
+    add(FirErrors.INFERENCE_UNSUCCESSFUL_FORK) { firDiagnostic ->
+        InferenceUnsuccessfulForkImpl(
+            firDiagnostic.a,
+            firDiagnostic as KtPsiDiagnostic,
+            token,
+        )
+    }
     add(FirErrors.OVERLOAD_RESOLUTION_AMBIGUITY) { firDiagnostic ->
         OverloadResolutionAmbiguityImpl(
             firDiagnostic.a.map { firBasedSymbol ->

analysis/analysis-api-fir/src/org/jetbrains/kotlin/analysis/api/fir/diagnostics/KtFirDiagnostics.kt

@@ -1095,6 +1095,11 @@ sealed class KtFirDiagnostic<PSI : PsiElement> : KtDiagnosticWithPsi<PSI> {
         override val diagnosticClass get() = RedundantSpreadOperatorInNamedFormInFunction::class
     }
 
+    abstract class InferenceUnsuccessfulFork : KtFirDiagnostic<PsiElement>() {
+        override val diagnosticClass get() = InferenceUnsuccessfulFork::class
+        abstract val message: String
+    }
+
     abstract class OverloadResolutionAmbiguity : KtFirDiagnostic<PsiElement>() {
         override val diagnosticClass get() = OverloadResolutionAmbiguity::class
         abstract val candidates: List<KtSymbol>

analysis/analysis-api-fir/src/org/jetbrains/kotlin/analysis/api/fir/diagnostics/KtFirDiagnosticsImpl.kt

@@ -1312,6 +1312,12 @@ internal class RedundantSpreadOperatorInNamedFormInFunctionImpl(
     override val token: ValidityToken,
 ) : KtFirDiagnostic.RedundantSpreadOperatorInNamedFormInFunction(), KtAbstractFirDiagnostic<KtExpression>
 
+internal class InferenceUnsuccessfulForkImpl(
+    override val message: String,
+    override val firDiagnostic: KtPsiDiagnostic,
+    override val token: ValidityToken,
+) : KtFirDiagnostic.InferenceUnsuccessfulFork(), KtAbstractFirDiagnostic<PsiElement>
+
 internal class OverloadResolutionAmbiguityImpl(
     override val candidates: List<KtSymbol>,
     override val firDiagnostic: KtPsiDiagnostic,

analysis/low-level-api-fir/tests/org/jetbrains/kotlin/analysis/low/level/api/fir/diagnostic/compiler/based/DiagnosisCompilerTestFE10TestdataTestGenerated.java

@@ -13803,6 +13803,12 @@ public class DiagnosisCompilerTestFE10TestdataTestGenerated extends AbstractDiag
                 runTest("compiler/testData/diagnostics/tests/inference/selectOfLambdaWithExtensionEnabled.kt");
             }
 
+            @Test
+            @TestMetadata("smartCastFork.kt")
+            public void testSmartCastFork() throws Exception {
+                runTest("compiler/testData/diagnostics/tests/inference/smartCastFork.kt");
+            }
+
             @Test
             @TestMetadata("specialCallsWithCallableReferences.kt")
             public void testSpecialCallsWithCallableReferences() throws Exception {
@@ -36583,6 +36589,12 @@ public class DiagnosisCompilerTestFE10TestdataTestGenerated extends AbstractDiag
                 runTest("compiler/testData/diagnostics/testsWithStdLib/inference/kt4975.kt");
             }
 
+            @Test
+            @TestMetadata("plusAssignOnArrayList.kt")
+            public void testPlusAssignOnArrayList() throws Exception {
+                runTest("compiler/testData/diagnostics/testsWithStdLib/inference/plusAssignOnArrayList.kt");
+            }
+
             @Test
             @TestMetadata("recursiveFlexibleAssertions.kt")
             public void testRecursiveFlexibleAssertions() throws Exception {

compiler/fir/analysis-tests/tests-gen/org/jetbrains/kotlin/test/runners/FirOldFrontendDiagnosticsTestGenerated.java

@@ -13803,6 +13803,12 @@ public class FirOldFrontendDiagnosticsTestGenerated extends AbstractFirDiagnosti
                 runTest("compiler/testData/diagnostics/tests/inference/selectOfLambdaWithExtensionEnabled.kt");
             }
 
+            @Test
+            @TestMetadata("smartCastFork.kt")
+            public void testSmartCastFork() throws Exception {
+                runTest("compiler/testData/diagnostics/tests/inference/smartCastFork.kt");
+            }
+
             @Test
             @TestMetadata("specialCallsWithCallableReferences.kt")
             public void testSpecialCallsWithCallableReferences() throws Exception {
@@ -36583,6 +36589,12 @@ public class FirOldFrontendDiagnosticsTestGenerated extends AbstractFirDiagnosti
                 runTest("compiler/testData/diagnostics/testsWithStdLib/inference/kt4975.kt");
             }
 
+            @Test
+            @TestMetadata("plusAssignOnArrayList.kt")
+            public void testPlusAssignOnArrayList() throws Exception {
+                runTest("compiler/testData/diagnostics/testsWithStdLib/inference/plusAssignOnArrayList.kt");
+            }
+
             @Test
             @TestMetadata("recursiveFlexibleAssertions.kt")
             public void testRecursiveFlexibleAssertions() throws Exception {

compiler/fir/analysis-tests/tests-gen/org/jetbrains/kotlin/test/runners/FirOldFrontendDiagnosticsWithLightTreeTestGenerated.java

@@ -13803,6 +13803,12 @@ public class FirOldFrontendDiagnosticsWithLightTreeTestGenerated extends Abstrac
                 runTest("compiler/testData/diagnostics/tests/inference/selectOfLambdaWithExtensionEnabled.kt");
             }
 
+            @Test
+            @TestMetadata("smartCastFork.kt")
+            public void testSmartCastFork() throws Exception {
+                runTest("compiler/testData/diagnostics/tests/inference/smartCastFork.kt");
+            }
+
             @Test
             @TestMetadata("specialCallsWithCallableReferences.kt")
             public void testSpecialCallsWithCallableReferences() throws Exception {
@@ -36583,6 +36589,12 @@ public class FirOldFrontendDiagnosticsWithLightTreeTestGenerated extends Abstrac
                 runTest("compiler/testData/diagnostics/testsWithStdLib/inference/kt4975.kt");
             }
 
+            @Test
+            @TestMetadata("plusAssignOnArrayList.kt")
+            public void testPlusAssignOnArrayList() throws Exception {
+                runTest("compiler/testData/diagnostics/testsWithStdLib/inference/plusAssignOnArrayList.kt");
+            }
+
             @Test
             @TestMetadata("recursiveFlexibleAssertions.kt")
             public void testRecursiveFlexibleAssertions() throws Exception {

compiler/fir/checkers/checkers-component-generator/src/org/jetbrains/kotlin/fir/checkers/generator/diagnostics/FirDiagnosticsList.kt

@@ -503,6 +503,10 @@ object DIAGNOSTICS_LIST : DiagnosticList("FirErrors") {
         val ASSIGNING_SINGLE_ELEMENT_TO_VARARG_IN_NAMED_FORM_ANNOTATION by deprecationError<KtExpression>(LanguageFeature.ProhibitAssigningSingleElementsToVarargsInNamedForm)
         val REDUNDANT_SPREAD_OPERATOR_IN_NAMED_FORM_IN_ANNOTATION by warning<KtExpression>()
         val REDUNDANT_SPREAD_OPERATOR_IN_NAMED_FORM_IN_FUNCTION by warning<KtExpression>()
+
+        val INFERENCE_UNSUCCESSFUL_FORK by error<PsiElement> {
+            parameter<String>("message")
+        }
     }
 
     val AMBIGUITY by object : DiagnosticGroup("Ambiguity") {

compiler/fir/checkers/gen/org/jetbrains/kotlin/fir/analysis/diagnostics/FirErrors.kt

@@ -341,6 +341,7 @@ object FirErrors {
     val ASSIGNING_SINGLE_ELEMENT_TO_VARARG_IN_NAMED_FORM_ANNOTATION by deprecationError0<KtExpression>(ProhibitAssigningSingleElementsToVarargsInNamedForm)
     val REDUNDANT_SPREAD_OPERATOR_IN_NAMED_FORM_IN_ANNOTATION by warning0<KtExpression>()
     val REDUNDANT_SPREAD_OPERATOR_IN_NAMED_FORM_IN_FUNCTION by warning0<KtExpression>()
+    val INFERENCE_UNSUCCESSFUL_FORK by error1<PsiElement, String>()
 
     // Ambiguity
     val OVERLOAD_RESOLUTION_AMBIGUITY by error1<PsiElement, Collection<FirBasedSymbol<*>>>(SourceElementPositioningStrategies.REFERENCE_BY_QUALIFIED)

compiler/fir/checkers/src/org/jetbrains/kotlin/fir/analysis/diagnostics/FirErrorsDefaultMessages.kt

@@ -250,6 +250,7 @@ import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors.INCONSISTENT_TYPE
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors.INCORRECT_CHARACTER_LITERAL
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors.INC_DEC_SHOULD_NOT_RETURN_UNIT
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors.INFERENCE_ERROR
+import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors.INFERENCE_UNSUCCESSFUL_FORK
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors.INFIX_MODIFIER_REQUIRED
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors.INITIALIZATION_BEFORE_DECLARATION
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors.INITIALIZER_REQUIRED_FOR_DESTRUCTURING_DECLARATION
@@ -928,6 +929,7 @@ object FirErrorsDefaultMessages : BaseDiagnosticRendererFactory() {
         )
         map.put(REDUNDANT_SPREAD_OPERATOR_IN_NAMED_FORM_IN_ANNOTATION, "Redundant spread (*) operator")
         map.put(REDUNDANT_SPREAD_OPERATOR_IN_NAMED_FORM_IN_FUNCTION, "Redundant spread (*) operator")
+        map.put(INFERENCE_UNSUCCESSFUL_FORK, "Unsuccessful inference fork at position: {0}", TO_STRING)
 
         map.put(TYPE_MISMATCH, "Type mismatch: inferred type is {1} but {0} was expected", TO_STRING, TO_STRING, NOT_RENDERED)
         map.put(THROWABLE_TYPE_MISMATCH, "Throwable type mismatch: actual type is {0}", TO_STRING, NOT_RENDERED)

compiler/fir/checkers/src/org/jetbrains/kotlin/fir/analysis/diagnostics/coneDiagnosticToFirDiagnostic.kt

@@ -370,6 +370,12 @@ private fun ConstraintSystemError.toDiagnostic(
                 typeVariableName,
             )
         }
+        is NoSuccessfulFork -> {
+            FirErrors.INFERENCE_UNSUCCESSFUL_FORK.createOn(
+                source,
+                position.initialConstraint.asStringWithoutPosition(),
+            )
+        }
         else -> null
     }
 }

compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/calls/CallKind.kt

@@ -19,6 +19,7 @@ sealed class CallKind(vararg resolutionSequence: ResolutionStage) {
         CheckDslScopeViolation,
         CheckLowPriorityInOverloadResolution,
         PostponedVariablesInitializerResolutionStage,
+        ConstraintSystemForks
     )
 
     object SyntheticSelect : CallKind(
@@ -27,7 +28,8 @@ sealed class CallKind(vararg resolutionSequence: ResolutionStage) {
         CreateFreshTypeVariableSubstitutorStage,
         CollectTypeVariableUsagesInfo,
         CheckArguments,
-        EagerResolveOfCallableReferences
+        EagerResolveOfCallableReferences,
+        ConstraintSystemForks,
     )
 
     object Function : CallKind(
@@ -47,6 +49,7 @@ sealed class CallKind(vararg resolutionSequence: ResolutionStage) {
         EagerResolveOfCallableReferences,
         CheckLowPriorityInOverloadResolution,
         PostponedVariablesInitializerResolutionStage,
+        ConstraintSystemForks,
     )
 
     object DelegatingConstructorCall : CallKind(
@@ -62,6 +65,7 @@ sealed class CallKind(vararg resolutionSequence: ResolutionStage) {
         CheckDslScopeViolation,
         CheckArguments,
         EagerResolveOfCallableReferences,
+        ConstraintSystemForks,
     )
 
     object CallableReference : CallKind(
@@ -84,7 +88,8 @@ sealed class CallKind(vararg resolutionSequence: ResolutionStage) {
         CreateFreshTypeVariableSubstitutorStage,
         CollectTypeVariableUsagesInfo,
         CheckArguments,
-        EagerResolveOfCallableReferences
+        EagerResolveOfCallableReferences,
+        ConstraintSystemForks,
     )
 
     internal class CustomForIde(vararg resolutionSequence: ResolutionStage) : CallKind(*resolutionSequence)

compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/calls/ResolutionStages.kt

@@ -7,14 +7,19 @@ package org.jetbrains.kotlin.fir.resolve.calls
 
 import org.jetbrains.kotlin.config.LanguageFeature
 import org.jetbrains.kotlin.descriptors.Modality
-import org.jetbrains.kotlin.fir.*
+import org.jetbrains.kotlin.fir.FirVisibilityChecker
 import org.jetbrains.kotlin.fir.declarations.*
 import org.jetbrains.kotlin.fir.declarations.utils.*
 import org.jetbrains.kotlin.fir.expressions.*
+import org.jetbrains.kotlin.fir.languageVersionSettings
+import org.jetbrains.kotlin.fir.matchingParameterFunctionType
 import org.jetbrains.kotlin.fir.references.FirSuperReference
 import org.jetbrains.kotlin.fir.resolve.directExpansionType
 import org.jetbrains.kotlin.fir.resolve.fullyExpandedType
-import org.jetbrains.kotlin.fir.resolve.inference.*
+import org.jetbrains.kotlin.fir.resolve.inference.ConeTypeParameterBasedTypeVariable
+import org.jetbrains.kotlin.fir.resolve.inference.ResolvedCallableReferenceAtom
+import org.jetbrains.kotlin.fir.resolve.inference.csBuilder
+import org.jetbrains.kotlin.fir.resolve.inference.hasBuilderInferenceAnnotation
 import org.jetbrains.kotlin.fir.resolve.toSymbol
 import org.jetbrains.kotlin.fir.scopes.FirTypeScope
 import org.jetbrains.kotlin.fir.scopes.FirUnstableSmartcastTypeScope
@@ -25,6 +30,7 @@ import org.jetbrains.kotlin.fir.symbols.SyntheticSymbol
 import org.jetbrains.kotlin.fir.symbols.ensureResolved
 import org.jetbrains.kotlin.fir.symbols.impl.*
 import org.jetbrains.kotlin.fir.types.*
+import org.jetbrains.kotlin.fir.visibilityChecker
 import org.jetbrains.kotlin.name.ClassId
 import org.jetbrains.kotlin.name.FqName
 import org.jetbrains.kotlin.name.Name
@@ -527,3 +533,15 @@ internal object CheckDeprecatedSinceKotlin : ResolutionStage() {
         }
     }
 }
+
+internal object ConstraintSystemForks : ResolutionStage() {
+    override suspend fun check(candidate: Candidate, callInfo: CallInfo, sink: CheckerSink, context: ResolutionContext) {
+        if (candidate.system.hasContradiction) return
+
+        candidate.system.processForkConstraints()
+
+        if (candidate.system.hasContradiction) {
+            sink.yieldDiagnostic(candidate.system.errors.firstOrNull()?.let(::InferenceError) ?: InapplicableCandidate)
+        }
+    }
+}

compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/inference/ConeConstraintSystemUtilContext.kt

@@ -125,4 +125,7 @@ object ConeConstraintSystemUtilContext : ConstraintSystemUtilContext {
 
     override val isForcedConsiderExtensionReceiverFromConstrainsInLambda: Boolean
         get() = true
+
+    override val isForcedAllowForkingInferenceSystem: Boolean
+        get() = true
 }

compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/inference/ConstraintSystemCompleter.kt

@@ -50,6 +50,8 @@ class ConstraintSystemCompleter(private val components: BodyResolveComponents, p
     ) = with(c) {
         val topLevelTypeVariables = candidateReturnType.extractTypeVariables()
 
+        c.processForkConstraints()
+
         completion@ while (true) {
             val postponedArguments = getOrderedNotAnalyzedPostponedArguments(topLevelAtoms) // TODO: This is very slow
 

compiler/resolution.common/src/org/jetbrains/kotlin/resolve/calls/inference/NewConstraintSystem.kt

@@ -7,8 +7,10 @@ package org.jetbrains.kotlin.resolve.calls.inference
 
 import org.jetbrains.kotlin.resolve.calls.components.PostponedArgumentsAnalyzerContext
 import org.jetbrains.kotlin.resolve.calls.inference.components.ConstraintSystemCompletionContext
+import org.jetbrains.kotlin.resolve.calls.inference.model.Constraint
 import org.jetbrains.kotlin.resolve.calls.inference.model.ConstraintStorage
 import org.jetbrains.kotlin.resolve.calls.inference.model.ConstraintSystemError
+import org.jetbrains.kotlin.types.model.TypeVariableMarker
 
 interface NewConstraintSystem {
     val hasContradiction: Boolean
@@ -21,4 +23,8 @@ interface NewConstraintSystem {
 
     fun asConstraintSystemCompleterContext(): ConstraintSystemCompletionContext
     fun asPostponedArgumentsAnalyzerContext(): PostponedArgumentsAnalyzerContext
+    fun processForkConstraints()
 }
+
+typealias ForkPointData = List<ConstraintsFromSingleFork>
+typealias ConstraintsFromSingleFork = Set<Pair<TypeVariableMarker, Constraint>>

compiler/resolution.common/src/org/jetbrains/kotlin/resolve/calls/inference/components/ConstraintInjector.kt

@@ -8,6 +8,8 @@ package org.jetbrains.kotlin.resolve.calls.inference.components
 import org.jetbrains.kotlin.config.LanguageFeature
 import org.jetbrains.kotlin.config.LanguageVersionSettings
 import org.jetbrains.kotlin.resolve.calls.inference.ConstraintSystemOperation
+import org.jetbrains.kotlin.resolve.calls.inference.ConstraintsFromSingleFork
+import org.jetbrains.kotlin.resolve.calls.inference.ForkPointData
 import org.jetbrains.kotlin.resolve.calls.inference.model.*
 import org.jetbrains.kotlin.resolve.calls.inference.model.ConstraintKind.*
 import org.jetbrains.kotlin.types.AbstractTypeApproximator
@@ -16,6 +18,8 @@ import org.jetbrains.kotlin.types.TypeApproximatorConfiguration
 import org.jetbrains.kotlin.types.TypeCheckerState
 import org.jetbrains.kotlin.types.model.*
 import org.jetbrains.kotlin.utils.SmartList
+import org.jetbrains.kotlin.utils.addIfNotNull
+import org.jetbrains.kotlin.utils.addToStdlib.popLast
 import kotlin.math.max
 
 class ConstraintInjector(
@@ -31,6 +35,8 @@ class ConstraintInjector(
         var maxTypeDepthFromInitialConstraints: Int
         val notFixedTypeVariables: MutableMap<TypeConstructorMarker, MutableVariableWithConstraints>
         val fixedTypeVariables: MutableMap<TypeConstructorMarker, KotlinTypeMarker>
+        val constraintsFromAllForkPoints: MutableList<Pair<IncorporationConstraintPosition, ForkPointData>>
+        val atCompletionState: Boolean
 
         fun addInitialConstraint(initialConstraint: InitialConstraint)
         fun addError(error: ConstraintSystemError)
@@ -39,6 +45,8 @@ class ConstraintInjector(
             position: IncorporationConstraintPosition,
             constraints: MutableList<Pair<TypeVariableMarker, Constraint>>
         )
+
+        fun processForkConstraints()
     }
 
     fun addInitialSubtypeConstraint(c: Context, lowerType: KotlinTypeMarker, upperType: KotlinTypeMarker, position: ConstraintPosition) {
@@ -133,10 +141,41 @@ class ConstraintInjector(
         processConstraints(c, typeCheckerState, skipProperEqualityConstraints = false)
     }
 
+    fun processForkConstraints(
+        c: Context,
+        constraintSet: Collection<Pair<TypeVariableMarker, Constraint>>,
+        position: IncorporationConstraintPosition
+    ) {
+        processGivenConstraints(
+            c,
+            TypeCheckerStateForConstraintInjector(c, position),
+            constraintSet,
+        )
+    }
+
     private fun processConstraints(
         c: Context,
         typeCheckerState: TypeCheckerStateForConstraintInjector,
         skipProperEqualityConstraints: Boolean = true
+    ): MutableList<Pair<TypeVariableMarker, Constraint>>? {
+        return processConstraintsIgnoringForksData(typeCheckerState, c, skipProperEqualityConstraints).also {
+            typeCheckerState.extractForkPointsData()?.let { allForkPointsData ->
+                allForkPointsData.mapTo(c.constraintsFromAllForkPoints) { forkPointData ->
+                    typeCheckerState.position to forkPointData
+                }
+
+                // During completion, we start processing fork constrains immediately
+                if (c.atCompletionState) {
+                    c.processForkConstraints()
+                }
+            }
+        }
+    }
+
+    private fun processConstraintsIgnoringForksData(
+        typeCheckerState: TypeCheckerStateForConstraintInjector,
+        c: Context,
+        skipProperEqualityConstraints: Boolean
     ): MutableList<Pair<TypeVariableMarker, Constraint>>? {
         val properConstraintsProcessingEnabled =
             languageVersionSettings.supportsFeature(LanguageFeature.ProperTypeInferenceConstraintsProcessing)
@@ -165,7 +204,7 @@ class ConstraintInjector(
     private fun processGivenConstraints(
         c: Context,
         typeCheckerState: TypeCheckerStateForConstraintInjector,
-        constraintsToProcess: MutableList<Pair<TypeVariableMarker, Constraint>>
+        constraintsToProcess: Collection<Pair<TypeVariableMarker, Constraint>>
     ) {
         for ((typeVariable, constraint) in constraintsToProcess) {
             if (c.shouldWeSkipConstraint(typeVariable, constraint)) continue
@@ -235,22 +274,94 @@ class ConstraintInjector(
         // We use `var` intentionally to avoid extra allocations as this property is quite "hot"
         private var possibleNewConstraints: MutableList<Pair<TypeVariableMarker, Constraint>>? = null
 
+        private var forkPointsData: MutableList<ForkPointData>? = null
+        private var stackForConstraintsSetsFromCurrentForkPoint: Stack<MutableList<ConstraintsFromSingleFork>>? = null
+        private var stackForCurrentConstraintSetFromSingleFork: Stack<MutableList<Pair<TypeVariableMarker, Constraint>>>? = null
+
         override val isInferenceCompatibilityEnabled = languageVersionSettings.supportsFeature(LanguageFeature.InferenceCompatibility)
 
+        private val allowForking: Boolean
+            get() = constraintIncorporator.utilContext.isForcedAllowForkingInferenceSystem
+
         private var baseLowerType = position.initialConstraint.a
         private var baseUpperType = position.initialConstraint.b
 
         private var isIncorporatingConstraintFromDeclaredUpperBound = false
 
         fun extractAllConstraints() = possibleNewConstraints.also { possibleNewConstraints = null }
+        fun extractForkPointsData() = forkPointsData.also { forkPointsData = null }
 
         fun addPossibleNewConstraint(variable: TypeVariableMarker, constraint: Constraint) {
+            val constraintsSetsFromCurrentFork = stackForConstraintsSetsFromCurrentForkPoint?.lastOrNull()
+            if (constraintsSetsFromCurrentFork != null) {
+                val currentConstraintSetForFork = stackForCurrentConstraintSetFromSingleFork?.lastOrNull()
+                require(currentConstraintSetForFork != null) { "Constraint has been added not under fork {...} call " }
+                currentConstraintSetForFork.add(variable to constraint)
+                return
+            }
+
             if (possibleNewConstraints == null) {
                 possibleNewConstraints = SmartList()
             }
             possibleNewConstraints!!.add(variable to constraint)
         }
 
+        override fun runForkingPoint(block: ForkPointContext.() -> Unit): Boolean {
+            if (!allowForking) {
+                return super.runForkingPoint(block)
+            }
+
+            if (stackForConstraintsSetsFromCurrentForkPoint == null) {
+                stackForConstraintsSetsFromCurrentForkPoint = SmartList()
+            }
+
+            stackForConstraintsSetsFromCurrentForkPoint!!.add(SmartList())
+            val isThereSuccessfulFork = with(MyForkCreationContext()) {
+                block()
+                anyForkSuccessful
+            }
+
+            val constraintSets = stackForConstraintsSetsFromCurrentForkPoint?.popLast()
+            if (constraintSets == null || constraintSets.isEmpty()) return isThereSuccessfulFork
+
+            if (constraintSets.size > 1) {
+                if (forkPointsData == null) {
+                    forkPointsData = SmartList()
+                }
+                forkPointsData!!.addIfNotNull(
+                    constraintSets
+                )
+                return true
+            } else if (constraintSets.size == 1) {
+                processForkConstraints(
+                    c,
+                    constraintSets.single(),
+                    position,
+                )
+            }
+
+            return isThereSuccessfulFork
+        }
+
+        private inner class MyForkCreationContext : ForkPointContext {
+            var anyForkSuccessful = false
+
+            override fun fork(block: () -> Boolean) {
+                if (stackForCurrentConstraintSetFromSingleFork == null) {
+                    stackForCurrentConstraintSetFromSingleFork = SmartList()
+                }
+
+                stackForCurrentConstraintSetFromSingleFork!!.add(SmartList())
+
+                block().also { anyForkSuccessful = anyForkSuccessful || it }
+
+                stackForConstraintsSetsFromCurrentForkPoint!!.last()
+                    .addIfNotNull(
+                        stackForCurrentConstraintSetFromSingleFork?.popLast()?.takeIf { it.isNotEmpty() }?.toSet()
+                    )
+            }
+        }
+
         fun hasConstraintsToProcess() = possibleNewConstraints != null
 
         fun setConstrainingTypesToPrintDebugInfo(lowerType: KotlinTypeMarker, upperType: KotlinTypeMarker) {
@@ -445,3 +556,5 @@ data class ConstraintContext(
     val inputTypePositionBeforeIncorporation: OnlyInputTypeConstraintPosition? = null,
     val isNullabilityConstraint: Boolean
 )
+
+private typealias Stack<E> = MutableList<E>

compiler/resolution.common/src/org/jetbrains/kotlin/resolve/calls/inference/components/ConstraintSystemCompletionContext.kt

@@ -33,4 +33,5 @@ interface ConstraintSystemCompletionContext : VariableFixationFinder.Context, Re
     fun fixVariable(variable: TypeVariableMarker, resultType: KotlinTypeMarker, position: FixVariableConstraintPosition<*>)
 
     fun couldBeResolvedWithUnrestrictedBuilderInference(): Boolean
+    fun processForkConstraints()
 }

compiler/resolution.common/src/org/jetbrains/kotlin/resolve/calls/inference/components/ConstraintSystemUtilContext.kt

@@ -39,4 +39,6 @@ interface ConstraintSystemUtilContext {
     ): TypeVariableMarker
 
     val isForcedConsiderExtensionReceiverFromConstrainsInLambda get() = false
+
+    val isForcedAllowForkingInferenceSystem get() = false
 }

compiler/resolution.common/src/org/jetbrains/kotlin/resolve/calls/inference/model/ConstraintPositionAndErrors.kt

@@ -133,6 +133,8 @@ class ConstrainingTypeIsError(
     val position: IncorporationConstraintPosition
 ) : ConstraintSystemError(INAPPLICABLE)
 
+class NoSuccessfulFork(val position: IncorporationConstraintPosition) : ConstraintSystemError(INAPPLICABLE)
+
 class OnlyInputTypesDiagnostic(val typeVariable: TypeVariableMarker) : ConstraintSystemError(INAPPLICABLE)
 
 object LowerPriorityToPreserveCompatibility : ConstraintSystemError(RESOLVED_NEED_PRESERVE_COMPATIBILITY)

compiler/resolution.common/src/org/jetbrains/kotlin/resolve/calls/inference/model/ConstraintStorage.kt

@@ -5,8 +5,12 @@
 
 package org.jetbrains.kotlin.resolve.calls.inference.model
 
+import org.jetbrains.kotlin.resolve.calls.inference.ForkPointData
 import org.jetbrains.kotlin.types.AbstractTypeChecker
-import org.jetbrains.kotlin.types.model.*
+import org.jetbrains.kotlin.types.model.KotlinTypeMarker
+import org.jetbrains.kotlin.types.model.TypeCheckerProviderContext
+import org.jetbrains.kotlin.types.model.TypeConstructorMarker
+import org.jetbrains.kotlin.types.model.TypeVariableMarker
 
 /**
  * Every type variable can be in the following states:
@@ -42,6 +46,7 @@ interface ConstraintStorage {
     val postponedTypeVariables: List<TypeVariableMarker>
     val builtFunctionalTypesForPostponedArgumentsByTopLevelTypeVariables: Map<Pair<TypeConstructorMarker, List<Pair<TypeConstructorMarker, Int>>>, KotlinTypeMarker>
     val builtFunctionalTypesForPostponedArgumentsByExpectedTypeVariables: Map<TypeConstructorMarker, KotlinTypeMarker>
+    val constraintsFromAllForkPoints: List<Pair<IncorporationConstraintPosition, ForkPointData>>
 
     object Empty : ConstraintStorage {
         override val allTypeVariables: Map<TypeConstructorMarker, TypeVariableMarker> get() = emptyMap()
@@ -55,6 +60,7 @@ interface ConstraintStorage {
         override val postponedTypeVariables: List<TypeVariableMarker> get() = emptyList()
         override val builtFunctionalTypesForPostponedArgumentsByTopLevelTypeVariables: Map<Pair<TypeConstructorMarker, List<Pair<TypeConstructorMarker, Int>>>, KotlinTypeMarker> = emptyMap()
         override val builtFunctionalTypesForPostponedArgumentsByExpectedTypeVariables: Map<TypeConstructorMarker, KotlinTypeMarker> = emptyMap()
+        override val constraintsFromAllForkPoints: List<Pair<IncorporationConstraintPosition, ForkPointData>> = emptyList()
     }
 }
 
@@ -113,14 +119,16 @@ class InitialConstraint(
     val constraintKind: ConstraintKind, // see [checkConstraint]
     val position: ConstraintPosition
 ) {
-    override fun toString(): String {
+    override fun toString(): String = "${asStringWithoutPosition()} from $position"
+
+    fun asStringWithoutPosition(): String {
         val sign =
             when (constraintKind) {
                 ConstraintKind.EQUALITY -> "=="
                 ConstraintKind.LOWER -> ":>"
                 ConstraintKind.UPPER -> "<:"
             }
-        return "$a $sign $b from $position"
+        return "$a $sign $b"
     }
 }
 

compiler/resolution.common/src/org/jetbrains/kotlin/resolve/calls/inference/model/MutableConstraintStorage.kt

@@ -5,6 +5,7 @@
 
 package org.jetbrains.kotlin.resolve.calls.inference.model
 
+import org.jetbrains.kotlin.resolve.calls.inference.ForkPointData
 import org.jetbrains.kotlin.resolve.calls.inference.components.ConstraintSystemUtilContext
 import org.jetbrains.kotlin.resolve.calls.tower.isSuccess
 import org.jetbrains.kotlin.types.model.*
@@ -238,4 +239,6 @@ internal class MutableConstraintStorage : ConstraintStorage {
         LinkedHashMap()
     override val builtFunctionalTypesForPostponedArgumentsByExpectedTypeVariables: MutableMap<TypeConstructorMarker, KotlinTypeMarker> =
         LinkedHashMap()
+
+    override val constraintsFromAllForkPoints: MutableList<Pair<IncorporationConstraintPosition, ForkPointData>> = SmartList()
 }

compiler/resolution.common/src/org/jetbrains/kotlin/resolve/calls/inference/model/NewConstraintSystemImpl.kt

@@ -40,6 +40,8 @@ class NewConstraintSystemImpl(
 
     private var couldBeResolvedWithUnrestrictedBuilderInference: Boolean = false
 
+    override var atCompletionState: Boolean = false
+
     private enum class State {
         BUILDING,
         TRANSACTION,
@@ -100,7 +102,11 @@ class NewConstraintSystemImpl(
         storage.missedConstraints.add(position to constraints)
     }
 
-    override fun asConstraintSystemCompleterContext() = apply { checkState(State.BUILDING) }
+    override fun asConstraintSystemCompleterContext() = apply {
+        checkState(State.BUILDING)
+
+        this.atCompletionState = true
+    }
 
     override fun asPostponedArgumentsAnalyzerContext() = apply { checkState(State.BUILDING) }
 
@@ -203,6 +209,7 @@ class NewConstraintSystemImpl(
         val beforeTypeVariablesTransactionSize = typeVariablesTransaction.size
         val beforeMissedConstraintsCount = storage.missedConstraints.size
         val beforeConstraintCountByVariables = storage.notFixedTypeVariables.mapValues { it.value.rawConstraintsCount }
+        val beforeConstraintsFromAllForks = storage.constraintsFromAllForkPoints.size
 
         state = State.TRANSACTION
         // typeVariablesTransaction is clear
@@ -218,6 +225,7 @@ class NewConstraintSystemImpl(
         storage.maxTypeDepthFromInitialConstraints = beforeMaxTypeDepthFromInitialConstraints
         storage.errors.trimToSize(beforeErrorsCount)
         storage.missedConstraints.trimToSize(beforeMissedConstraintsCount)
+        storage.constraintsFromAllForkPoints.trimToSize(beforeConstraintsFromAllForks)
 
         val addedInitialConstraints = storage.initialConstraints.subList(beforeInitialConstraintCount, storage.initialConstraints.size)
 
@@ -337,6 +345,54 @@ class NewConstraintSystemImpl(
             return storage.postponedTypeVariables
         }
 
+    override val constraintsFromAllForkPoints: MutableList<Pair<IncorporationConstraintPosition, ForkPointData>>
+        get() {
+            checkState(State.BUILDING, State.COMPLETION, State.TRANSACTION)
+            return storage.constraintsFromAllForkPoints
+        }
+
+    override fun processForkConstraints() {
+        if (constraintsFromAllForkPoints.isEmpty()) return
+        val allForkPointsData = constraintsFromAllForkPoints.toList()
+        constraintsFromAllForkPoints.clear()
+
+        // There may be multiple fork points:
+        // - One from subtyping A<Int> & A<T> <: A<Xv>
+        // - Another one from B<String> & B<F> <: B<Yv>
+        // Each of them defines two sets of constraints, e.g. for the first for point:
+        // 1. {Xv=Int} – is a one-element set (but potentially there might be more constraints in the set)
+        // 2. {Xv=T} – second constraints set
+        for ((position, forkPointData) in allForkPointsData) {
+            if (!processForkPointData(forkPointData, position)) {
+                addError(NoSuccessfulFork(position))
+            }
+        }
+    }
+
+    /**
+     * @return true if there is a successful constraints set for the fork
+     */
+    private fun processForkPointData(
+        forkPointData: ForkPointData,
+        position: IncorporationConstraintPosition
+    ): Boolean {
+        return forkPointData.any { constraintSetForSingleFork ->
+            runTransaction {
+                constraintInjector.processForkConstraints(
+                    this@NewConstraintSystemImpl.apply { checkState(State.BUILDING, State.COMPLETION, State.TRANSACTION) },
+                    constraintSetForSingleFork,
+                    position,
+                )
+
+                if (constraintsFromAllForkPoints.isNotEmpty()) {
+                    processForkConstraints()
+                }
+
+                !hasContradiction
+            }
+        }
+    }
+
     // ConstraintInjector.Context, KotlinConstraintSystemCompleter.Context
     override fun addError(error: ConstraintSystemError) {
         checkState(State.BUILDING, State.COMPLETION, State.TRANSACTION)

compiler/testData/diagnostics/tests/inference/smartCastFork.fir.kt

@@ -0,0 +1,25 @@
+// SKIP_TXT
+// !DIAGNOSTICS: -UNUSED_VARIABLE
+
+interface A<E> {
+    fun foo(): E
+}
+
+interface B : A<Int>
+interface C : A<Long>
+
+fun <T> bar(a: A<T>, w: T) {
+    baz(a, w) // OK in FE1.0
+
+    if (a is B) {
+        baz(a, 1) // OK in FE1.0
+        baz(a, w) // Type mismatch: Required Int, but found E
+        <!INFERENCE_UNSUCCESSFUL_FORK("it(B & A<T>) <: A<TypeVariable(F)>")!>baz<!>(a, "")
+    }
+
+    if (a is B || a is C) {
+        baz(a, w) // OK in FE 1.0 (Smart cast doesn't work), fail at FIR: it infers F to `LBU(Int, Long)` and then `w` is considered inapplicable
+    }
+}
+
+fun <F> baz(a: A<F>, f: F) {}

compiler/testData/diagnostics/tests/inference/smartCastFork.kt

@@ -0,0 +1,25 @@
+// SKIP_TXT
+// !DIAGNOSTICS: -UNUSED_VARIABLE
+
+interface A<E> {
+    fun foo(): E
+}
+
+interface B : A<Int>
+interface C : A<Long>
+
+fun <T> bar(a: A<T>, w: T) {
+    baz(a, w) // OK in FE1.0
+
+    if (a is B) {
+        baz(<!DEBUG_INFO_SMARTCAST!>a<!>, 1) // OK in FE1.0
+        baz(<!DEBUG_INFO_SMARTCAST!>a<!>, <!TYPE_MISMATCH!>w<!>) // Type mismatch: Required Int, but found E
+        baz(<!DEBUG_INFO_SMARTCAST!>a<!>, <!TYPE_MISMATCH!>""<!>)
+    }
+
+    if (a is B || a is C) {
+        baz(a, w) // OK in FE 1.0 (Smart cast doesn't work), fail at FIR: it infers F to `LBU(Int, Long)` and then `w` is considered inapplicable
+    }
+}
+
+fun <F> baz(a: A<F>, f: F) {}

compiler/testData/diagnostics/testsWithStdLib/inference/plusAssignOnArrayList.kt

@@ -0,0 +1,9 @@
+// FIR_IDENTICAL
+// SKIP_TXT
+import java.util.*
+
+val a = ArrayList<String>()
+
+fun foo(l: List<String>) {
+    a.plusAssign(l)
+}

compiler/tests-common-new/tests-gen/org/jetbrains/kotlin/test/runners/DiagnosticTestGenerated.java

@@ -13809,6 +13809,12 @@ public class DiagnosticTestGenerated extends AbstractDiagnosticTest {
                 runTest("compiler/testData/diagnostics/tests/inference/selectOfLambdaWithExtensionEnabled.kt");
             }
 
+            @Test
+            @TestMetadata("smartCastFork.kt")
+            public void testSmartCastFork() throws Exception {
+                runTest("compiler/testData/diagnostics/tests/inference/smartCastFork.kt");
+            }
+
             @Test
             @TestMetadata("specialCallsWithCallableReferences.kt")
             public void testSpecialCallsWithCallableReferences() throws Exception {
@@ -36673,6 +36679,12 @@ public class DiagnosticTestGenerated extends AbstractDiagnosticTest {
                 runTest("compiler/testData/diagnostics/testsWithStdLib/inference/kt4975.kt");
             }
 
+            @Test
+            @TestMetadata("plusAssignOnArrayList.kt")
+            public void testPlusAssignOnArrayList() throws Exception {
+                runTest("compiler/testData/diagnostics/testsWithStdLib/inference/plusAssignOnArrayList.kt");
+            }
+
             @Test
             @TestMetadata("recursiveFlexibleAssertions.kt")
             public void testRecursiveFlexibleAssertions() throws Exception {

core/compiler.common/src/org/jetbrains/kotlin/types/AbstractTypeChecker.kt

@@ -62,6 +62,34 @@ open class TypeCheckerState(
         isFromNullabilityConstraint: Boolean = false
     ): Boolean? = null
 
+    // Handling cases like A<Int> & A<T> <: A<F_var>
+    // There are two possible solutions for F_var (Int and T) and both of them may work well or not with other constrains
+    // Effectively, we need to fork constraint system to two copies: one with F_var=Int and the other with F_var=T
+    // and then maintain them both until we find some contradiction with one of the versions.
+    //
+    // But that might lead to the exponential size of CS, thus we use the following heuristics:
+    // we accumulate forks data until the last stage of the candidate resolution and then try to apply back then
+    // until some of the constrains set has no contradiction.
+    //
+    // `atForkPoint` works trivially in non-inference context and for FE1.0: it just run basic subtyping mechanism for each subTypeArguments
+    // component until the first success
+    open fun runForkingPoint(block: ForkPointContext.() -> Unit): Boolean = with(ForkPointContext.Default()) {
+        block()
+        result
+    }
+
+    interface ForkPointContext {
+        fun fork(block: () -> Boolean)
+
+        class Default : ForkPointContext {
+            var result: Boolean = false
+            override fun fork(block: () -> Boolean) {
+                if (result) return
+                result = block()
+            }
+        }
+    }
+
     enum class LowerCapturedTypePolicy {
         CHECK_ONLY_LOWER,
         CHECK_SUBTYPE_AND_LOWER,
@@ -362,8 +390,11 @@ object AbstractTypeChecker {
 
                 if (!anyNonOutParameter && state.isSubtypeForSameConstructor(newArguments, superType)) return true
 
-                // TODO: rethink this; now components order in intersection type affects semantic due to run subtyping (which can add constraints) only until the first successful candidate
-                return supertypesWithSameConstructor.any { state.isSubtypeForSameConstructor(it.asArgumentList(), superType) }
+                return state.runForkingPoint {
+                    for (subTypeArguments in supertypesWithSameConstructor) {
+                        fork { state.isSubtypeForSameConstructor(subTypeArguments.asArgumentList(), superType) }
+                    }
+                }
             }
         }
     }

core/util.runtime/src/org/jetbrains/kotlin/utils/addToStdlib.kt

@@ -235,3 +235,5 @@ inline fun <T, U, K, V> List<T>.flatGroupBy(
     }
     return result
 }
+
+fun <E> MutableList<E>.popLast(): E = removeAt(lastIndex)