Repository: hylo-lang/hylo (swift)

Issue:
stale constraint
I got this, which looks like an internal error: “stale constraint 'Int ⤷ %350'” by running this (incorrect) val code with the tip of my test-generation branch:

```
//- compileAndRun expecting: success

fun factorial(_ n: Int) -> Int {
  if n < 2 { 1 } else { n * factorial(n - 1) }
}

fun assert(_ b: Bool) {
  if !b + 2 {
    let _ = fatal_error()
  }
}

public fun main() {
  let r = factorial(6)
  assert(r == 720)
}
```

Pull request description:

Patch:
diff --git a/Sources/FrontEnd/TypeChecking/ConstraintSystem.swift b/Sources/FrontEnd/TypeChecking/ConstraintSystem.swift
index f3507f593..de3530e2f 100644
--- a/Sources/FrontEnd/TypeChecking/ConstraintSystem.swift
+++ b/Sources/FrontEnd/TypeChecking/ConstraintSystem.swift
@@ -42,9 +42,6 @@ struct ConstraintSystem {
   /// already computed.
   private var penalties: Int = 0
 
-  /// The score of the best solution computed so far.
-  private var bestScore = Solution.Score.worst
-
   /// Indicates whether this instance should log a trace.
   private let isLoggingEnabled: Bool
 
@@ -66,19 +63,22 @@ struct ConstraintSystem {
 
   /// Solves this instance using `checker` to query type relations and resolve names, returning the
   /// best solution.
-  mutating func solution(_ checker: inout TypeChecker) -> Solution {
-    betterSolution(&checker)!
+  mutating func solution(querying checker: inout TypeChecker) -> Solution {
+    solution(notWorseThan: .worst, querying: &checker)!
   }
 
   /// Solves this instance using `checker` to query type relations and resolve names, returning the
-  /// best solution or `nil` if no solution with a score better than `self.bestScore` can be found.
-  private mutating func betterSolution(_ checker: inout TypeChecker) -> Solution? {
+  /// best solution with a score inferior or equal to `maxScore` or `nil` if no such solution with
+  /// can be found.
+  private mutating func solution(
+    notWorseThan maxScore: Solution.Score, querying checker: inout TypeChecker
+  ) -> Solution? {
     logState()
     log("steps:")
 
     while let g = fresh.popLast() {
       // Make sure the current solution is still worth exploring.
-      if score() > bestScore {
+      if score() > maxScore {
         log("- abort")
         return nil
       }
@@ -155,8 +155,7 @@ struct ConstraintSystem {
     assert(outcomes.enumerated().allSatisfy({ (i, o) in (o != nil) || stale.contains(i) }))
 
     for g in stale {
-      let c = goals[g]
-      setOutcome(.failure({ (d, _, _) in d.insert(.error(staleConstraint: c)) }), for: g)
+      setOutcome(.failure({ (_, _, _) in () }), for: g)
     }
 
     let m = typeAssumptions.optimized()
@@ -166,7 +165,8 @@ struct ConstraintSystem {
     }
 
     return Solution(
-      substitutions: m, bindings: bindingAssumptions, penalties: penalties, diagnostics: d)
+      substitutions: m, bindings: bindingAssumptions,
+      penalties: penalties, diagnostics: d, stale: stale.map({ goals[$0] }))
   }
 
   /// Creates an ambiguous solution.
@@ -445,7 +445,7 @@ struct ConstraintSystem {
 
     if candidates.elements.isEmpty {
       return .failure { (d, m, _) in
-        let t = m.reify(goal.memberType)
+        let t = m.reify(goal.subject)
         d.insert(.error(undefinedName: goal.memberName, in: t, at: goal.origin.site))
       }
     }
@@ -681,7 +681,7 @@ struct ConstraintSystem {
       // Don't bother if there's no chance to find a better solution.
       var underestimatedChoiceScore = score()
       underestimatedChoiceScore.penalties += choice.penalties
-      if underestimatedChoiceScore > bestScore {
+      if underestimatedChoiceScore > results.score {
         log("- skip: \"\(choice)\"")
         continue
       }
@@ -694,11 +694,13 @@ struct ConstraintSystem {
       var exploration = self
       let s = configureSubSystem(&exploration, choice)
       exploration.setOutcome(s.isEmpty ? .success : delegate(to: s), for: g)
-      guard let newSolution = exploration.betterSolution(&checker) else { continue }
+      guard let new = exploration.solution(notWorseThan: results.score, querying: &checker) else {
+        continue
+      }
 
       // Insert the new result.
       results.insert(
-        (choice, newSolution),
+        (choice, new),
         rankingSolutionWith: { (a, b) in rank(a, b, querying: &checker) })
     }
 
@@ -972,7 +974,7 @@ struct ConstraintSystem {
 
     // Solve the constraint system.
     var s = ConstraintSystem(constraints, bindings: [:], in: scope, loggingTrace: isLoggingEnabled)
-    return !s.solution(&checker).diagnostics.containsError
+    return !s.solution(querying: &checker).isSound
   }
 
   /// Logs a line of text in the standard output.
@@ -1073,7 +1075,7 @@ private struct Explorations<T: DisjunctiveConstraintProtocol> {
   private(set) var elements: [Element] = []
 
   /// The score of the solutions in this set.
-  private var score = Solution.Score.worst
+  private(set) var score = Solution.Score.worst
 
   /// Creates an empty set.
   init() {}
diff --git a/Sources/FrontEnd/TypeChecking/Solution.swift b/Sources/FrontEnd/TypeChecking/Solution.swift
index a086aac90..2a6354316 100644
--- a/Sources/FrontEnd/TypeChecking/Solution.swift
+++ b/Sources/FrontEnd/TypeChecking/Solution.swift
@@ -35,9 +35,12 @@ struct Solution {
   /// The diagnostics of the errors associated with the solution.
   private(set) var diagnostics: DiagnosticSet
 
+  /// The constraints that could not be solved.
+  private(set) var stale: [Constraint]
+
   /// Creates an empty solution.
   init() {
-    self.init(substitutions: [:], bindings: [:], penalties: 0, diagnostics: [])
+    self.init(substitutions: [:], bindings: [:], penalties: 0, diagnostics: [], stale: [])
   }
 
   /// Creates an instance with the given properties.
@@ -45,16 +48,25 @@ struct Solution {
     substitutions typeAssumptions: SubstitutionMap,
     bindings bindingAssumptions: [NameExpr.ID: DeclReference],
     penalties: Int,
-    diagnostics: DiagnosticSet
+    diagnostics: DiagnosticSet,
+    stale: [Constraint]
   ) {
     self.typeAssumptions = typeAssumptions
     self.bindingAssumptions = bindingAssumptions
     self.penalties = penalties
     self.diagnostics = diagnostics
+    self.stale = stale
+  }
+
+  /// `true` iff the solution has no error.
+  var isSound: Bool {
+    !diagnostics.containsError && stale.isEmpty
   }
 
   /// The score of the solution.
-  var score: Score { Score(errorCount: diagnostics.elements.count, penalties: penalties) }
+  var score: Score {
+    Score(errorCount: diagnostics.elements.count + stale.count, penalties: penalties)
+  }
 
   /// Incorporates `d` into `self`.
   mutating func incorporate(_ d: Diagnostic) {
diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker+ConstraintGeneration.swift b/Sources/FrontEnd/TypeChecking/TypeChecker+ConstraintGeneration.swift
index 567d24112..5c36a3345 100644
--- a/Sources/FrontEnd/TypeChecking/TypeChecker+ConstraintGeneration.swift
+++ b/Sources/FrontEnd/TypeChecking/TypeChecker+ConstraintGeneration.swift
@@ -621,27 +621,20 @@ extension TypeChecker {
         return .error
       }
 
-      // Infer the type of the callee.
-      let parameterType = ^TypeVariable()
-      state.facts.append(
-        ParameterConstraint(
-          rhsType, parameterType,
-          origin: ConstraintOrigin(.argument, at: ast.site(of: rhs))))
-
+      let operatorType = ^TypeVariable()
       let outputType = ^TypeVariable()
-      let calleeType = LambdaType(
-        receiverEffect: .let,
-        environment: ^TupleType(labelsAndTypes: [("self", ^RemoteType(.let, lhsType))]),
-        inputs: [CallableTypeParameter(type: parameterType)],
-        output: outputType)
-      state.facts.assign(^calleeType, to: callee.expr)
+      state.facts.assign(operatorType, to: callee.expr)
 
-      // Create a member constraint for the operator.
+      // The operator is a member function of the left operand.
       state.facts.append(
         MemberConstraint(
-          lhsType, hasMemberReferredToBy: callee.expr, ofType: ^calleeType,
-          in: ast,
+          lhsType, hasMemberReferredToBy: callee.expr, ofType: operatorType, in: ast,
           origin: ConstraintOrigin(.member, at: ast[callee.expr].site)))
+      state.facts.append(
+        FunctionCallConstraint(
+          operatorType, accepts: [.init(label: nil, type: rhsType, site: ast.site(of: rhs))],
+          returns: outputType,
+          origin: ConstraintOrigin(.callee, at: ast.site(of: subject))))
 
       return outputType
 
diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift b/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift
index 4cc350bf1..f232221a4 100644
--- a/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift
+++ b/Sources/FrontEnd/TypeChecking/TypeChecker+Diagnostics.swift
@@ -190,10 +190,6 @@ extension Diagnostic {
     .note("trait '\(x)' requires initializer with type '\(t)'", at: site)
   }
 
-  static func error(staleConstraint c: any Constraint) -> Diagnostic {
-    .error("stale constraint '\(c)'", at: c.origin.site)
-  }
-
   static func error(
     illegalUseOfStaticMember name: Name, onInstanceOf: AnyType, at site: SourceRange
   ) -> Diagnostic {
diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker.swift b/Sources/FrontEnd/TypeChecking/TypeChecker.swift
index 5e8329c69..a8d3f8cbb 100644
--- a/Sources/FrontEnd/TypeChecking/TypeChecker.swift
+++ b/Sources/FrontEnd/TypeChecking/TypeChecker.swift
@@ -1564,7 +1564,7 @@ public struct TypeChecker {
       bindings: facts.inferredBindings,
       in: useScope,
       loggingTrace: shouldLogTrace)
-    let solution = s.solution(&self)
+    let solution = s.solution(querying: &self)
 
     if shouldLogTrace {
       print(solution)
@@ -1587,12 +1587,11 @@ public struct TypeChecker {
     }
 
     // Run deferred queries.
-    let success = deferredQueries.reduce(
-      !solution.diagnostics.containsError, { (s, q) in q(&self, solution) && s })
+    let isSound = deferredQueries.reduce(solution.isSound, { (s, q) in q(&self, solution) && s })
 
     diagnostics.formUnion(solution.diagnostics)
-    assert(success || diagnostics.containsError)
-    return (succeeded: success, solution: solution)
+    assert(isSound || diagnostics.containsError, "inferrence failed without diagnostics")
+    return (succeeded: isSound, solution: solution)
   }
 
   // MARK: Name binding


Test patch:
diff --git a/Tests/ValTests/TestCases/TypeChecking/BindingTypeInferenceWithHints.val b/Tests/ValTests/TestCases/TypeChecking/BindingTypeInferenceWithHints.val
index 3a064ad8e..77be37ea0 100644
--- a/Tests/ValTests/TestCases/TypeChecking/BindingTypeInferenceWithHints.val
+++ b/Tests/ValTests/TestCases/TypeChecking/BindingTypeInferenceWithHints.val
@@ -1,4 +1,11 @@
 //- typeCheck expecting: success
 
-let x0: { Int, Double } = (2, 3)
-let x1: { _, Double } = (2, 3)
+fun check<T>(_ x: T) {}
+
+public fun main() {
+  let x0: {Int, Double} = (2, 3)
+  check<{Int, Double}>(x0)
+
+  let x1: {_, Double} = (2, 3)
+  check<{Int, Double}>(x1)
+}
diff --git a/Tests/ValTests/TestCases/TypeChecking/ConditionalStmt.val b/Tests/ValTests/TestCases/TypeChecking/ConditionalStmt.val
new file mode 100644
index 000000000..00bc993a6
--- /dev/null
+++ b/Tests/ValTests/TestCases/TypeChecking/ConditionalStmt.val
@@ -0,0 +1,10 @@
+//- typeCheck expecting: failure
+
+fun trap() {}
+
+fun assert(_ b: Bool) {
+  //! @+1 diagnostic type 'Bool' has no member 'infix+'
+  if !b + 2 {
+    trap()
+  }
+}