Merge pull request hylo-lang#190 from val-lang/refreshing

Refine the algorithm for refreshing stale constraints

Sources/Core/Constraints/ConformanceConstraint.swift

@@ -26,10 +26,6 @@ public struct ConformanceConstraint: Constraint, Hashable {
     modify(&subject, with: transform)
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    subject == variable
-  }
-
 }
 
 extension ConformanceConstraint: CustomStringConvertible {

Sources/Core/Constraints/Constraint.swift

@@ -13,9 +13,6 @@ public protocol Constraint {
   /// Applies `transform` on constituent types of `self`.
   mutating func modifyTypes(_ transform: (AnyType) -> AnyType)
 
-  /// Returns whether the constraint depends on the specified variable.
-  func depends(on variable: TypeVariable) -> Bool
-
   /// Hashes the salient features of `self` by feeding them into `hasher`.
   func hash(into hasher: inout Hasher)
 

Sources/Core/Constraints/DisjunctionConstraint.swift

@@ -50,15 +50,6 @@ public struct DisjunctionConstraint: Constraint, Hashable {
     }
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    for m in choices {
-      for c in m.constraints {
-        if c.depends(on: variable) { return true }
-      }
-    }
-    return false
-  }
-
 }
 
 extension DisjunctionConstraint: CustomStringConvertible {

Sources/Core/Constraints/EqualityConstraint.swift

@@ -32,10 +32,6 @@ public struct EqualityConstraint: Constraint, Hashable {
     modify(&right, with: transform)
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    (left == variable) || (right == variable)
-  }
-
 }
 
 extension EqualityConstraint: CustomStringConvertible {

Sources/Core/Constraints/FunctionCallConstraint.swift

@@ -37,12 +37,6 @@ public struct FunctionCallConstraint: Constraint, Hashable {
     }
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    calleeType == variable
-      || returnType == variable
-      || parameters.contains(where: { (p) in p.type == variable })
-  }
-
 }
 
 extension FunctionCallConstraint: CustomStringConvertible {

Sources/Core/Constraints/LiteralConstraint.swift

@@ -35,10 +35,6 @@ public struct LiteralConstraint: Constraint, Hashable {
     modify(&defaultSubject, with: transform)
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    subject == variable
-  }
-
 }
 
 extension LiteralConstraint: CustomStringConvertible {

Sources/Core/Constraints/MemberConstraint.swift

@@ -38,10 +38,6 @@ public struct MemberConstraint: Constraint, Hashable {
     modify(&memberType, with: transform)
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    (subject == variable) || (memberType == variable)
-  }
-
 }
 
 extension MemberConstraint: CustomStringConvertible {

Sources/Core/Constraints/OverloadConstraint.swift

@@ -82,10 +82,6 @@ public struct OverloadConstraint: Constraint, Hashable {
     }
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    overloadedExprType == variable
-  }
-
 }
 
 extension OverloadConstraint: CustomStringConvertible {

Sources/Core/Constraints/ParameterConstraint.swift

@@ -27,10 +27,6 @@ public struct ParameterConstraint: Constraint, Hashable {
     modify(&right, with: transform)
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    (left == variable) || (right == variable)
-  }
-
 }
 
 extension ParameterConstraint: CustomStringConvertible {

Sources/Core/Constraints/PredicateConstraint.swift

@@ -14,8 +14,6 @@ public struct PredicateConstraint: Constraint, Hashable {
 
   public mutating func modifyTypes(_ transform: (AnyType) -> AnyType) {}
 
-  public func depends(on variable: TypeVariable) -> Bool { false }
-
 }
 
 extension PredicateConstraint: CustomStringConvertible {

Sources/Core/Constraints/SubtypingConstraint.swift

@@ -26,10 +26,6 @@ public struct SubtypingConstraint: Constraint, Hashable {
     modify(&right, with: transform)
   }
 
-  public func depends(on variable: TypeVariable) -> Bool {
-    (left == variable) || (right == variable)
-  }
-
 }
 
 extension SubtypingConstraint: CustomStringConvertible {

Sources/FrontEnd/TypeChecking/ConstraintSolver.swift

@@ -190,14 +190,10 @@ struct ConstraintSolver {
 
     switch (goal.left.base, goal.right.base) {
     case (let tau as TypeVariable, _):
-      log("- assume \"\(tau) = \(goal.right)\"")
-      typeAssumptions.assign(goal.right, to: tau)
-      refresh(constraintsDependingOn: tau)
+      assume(tau, equals: goal.right)
 
     case (_, let tau as TypeVariable):
-      log("- assume \"\(tau) = \(goal.left)\"")
-      typeAssumptions.assign(goal.left, to: tau)
-      refresh(constraintsDependingOn: tau)
+      assume(tau, equals: goal.left)
 
     case (let l as TupleType, let r as TupleType):
       // Make sure `L` and `R` are structurally compatible.
@@ -590,10 +586,10 @@ struct ConstraintSolver {
     }
 
     // Slow path: inspect how the solution compares with the ones we have.
-    let lhs = newSolution.reify(comparator, withVariables: .substituteByError)
+    let lhs = newSolution.typeAssumptions.reify(comparator, withVariables: .substituteByError)
     var i = 0
     while i < solutions.count {
-      let rhs = solutions[i].reify(comparator, withVariables: .substituteByError)
+      let rhs = solutions[i].typeAssumptions.reify(comparator, withVariables: .substituteByError)
       if checker.areEquivalent(lhs, rhs) {
         // Check if the new solution binds name expressions to more specialized declarations.
         switch checker.compareSolutionBindings(newSolution, solutions[0], scope: scope) {
@@ -645,12 +641,24 @@ struct ConstraintSolver {
     stale.append(constraint)
   }
 
-  /// Moves the stale constraints depending on the specified variables back to the fresh set.
-  private mutating func refresh(constraintsDependingOn variable: TypeVariable) {
+  /// Extends the type substution table to map `tau` to `substitute`.
+  private mutating func assume(_ tau: TypeVariable, equals substitute: AnyType) {
+    log("- assume \"\(tau) = \(substitute)\"")
+    typeAssumptions.assign(substitute, to: tau)
+
+    // Refresh stale constraints.
     for i in (0 ..< stale.count).reversed() {
-      if stale[i].depends(on: variable) {
+      var changed = false
+      let updated = stale[i].modifyingTypes({ (type) in
+        let u = typeAssumptions.reify(type, withVariables: .keep)
+        changed = changed || (type != u)
+        return u
+      })
+
+      if changed {
         log("- refresh \(stale[i])")
-        fresh.append(stale.remove(at: i))
+        stale.remove(at: i)
+        fresh.append(updated)
       }
     }
   }
@@ -670,7 +678,7 @@ struct ConstraintSolver {
   private func finalize() -> Solution {
     assert(fresh.isEmpty)
     return Solution(
-      typeAssumptions: typeAssumptions.asDictionary(),
+      typeAssumptions: typeAssumptions.optimized(),
       bindingAssumptions: bindingAssumptions,
       penalties: penalties,
       diagnostics: diagnostics + stale.map(Diagnostic.diagnose(staleConstraint:)))

Sources/FrontEnd/TypeChecking/Solution.swift

@@ -3,17 +3,6 @@ import Core
 /// A solution returned by a constraint solver.
 struct Solution {
 
-  /// A policy for substituting type variales during reification.
-  enum SubstitutionPolicy {
-
-    /// Substitute free variables by error types.
-    case substituteByError
-
-    /// Do not substitute free variables.
-    case keep
-
-  }
-
   /// The score of a solution.
   struct Score: Comparable {
 
@@ -35,7 +24,7 @@ struct Solution {
   }
 
   /// The type assumptions made by the solver.
-  let typeAssumptions: [TypeVariable: AnyType]
+  let typeAssumptions: SubstitutionMap
 
   /// The name binding assumptions made by the solver.
   let bindingAssumptions: [NodeID<NameExpr>: DeclRef]
@@ -53,7 +42,7 @@ struct Solution {
 
   /// Creates an instance with the given properties.
   init(
-    typeAssumptions: [TypeVariable: AnyType],
+    typeAssumptions: SubstitutionMap,
     bindingAssumptions: [NodeID<NameExpr>: DeclRef],
     penalties: Int,
     diagnostics: [Diagnostic]
@@ -67,31 +56,6 @@ struct Solution {
   /// The score of the solution.
   var score: Score { Score(errorCount: diagnostics.count, penalties: penalties) }
 
-  /// Subtitutes each type variable occuring in `type` by its corresponding substitution in `self`,
-  /// apply `substitutionPolicy` to deal with free variables.
-  func reify(_ type: AnyType, withVariables substitutionPolicy: SubstitutionPolicy) -> AnyType {
-    func _impl(type: AnyType) -> TypeTransformAction {
-      if let v = TypeVariable(type) {
-        // Substitute variables.
-        if let t = typeAssumptions[v] {
-          return .stepInto(t)
-        } else {
-          switch substitutionPolicy {
-          case .substituteByError:
-            return .stepInto(.error)
-          case .keep:
-            return .stepOver(type)
-          }
-        }
-      } else {
-        // Recursively visit other types.
-        return .stepInto(type)
-      }
-    }
-
-    return type.transform(_impl(type:))
-  }
-
   /// Adds `d` to the list of diagnostics associated with this solution.
   mutating func addDiagnostic(_ d: Diagnostic) {
     diagnostics.append(d)

Sources/FrontEnd/TypeChecking/SubstitutionMap.swift

@@ -3,12 +3,39 @@ import Core
 /// A substitution table mapping type variables to assumptions during type inference
 struct SubstitutionMap {
 
+  /// A policy for substituting type variales during reification.
+  enum SubstitutionPolicy {
+
+    /// Substitute free variables by error types.
+    case substituteByError
+
+    /// Do not substitute free variables.
+    case keep
+
+  }
+
   /// The internal storage of the map.
   private var storage: [TypeVariable: AnyType] = [:]
 
   /// Creates an empty substitution map.
   init() {}
 
+  /// Returns a copy of this instance with its internal representation optimized.
+  func optimized() -> Self {
+    var result = SubstitutionMap()
+    result.storage = storage.mapValues({ self[$0] })
+    return result
+  }
+
+  /// Returns the substitution for `variable`, if any.
+  subscript(variable: TypeVariable) -> AnyType? {
+    if let t = storage[variable] {
+      return self[t]
+    } else {
+      return nil
+    }
+  }
+
   /// Returns the substitution for `type` if it is a variable to which a type is assigned in this
   /// map. Otherwise, returns `type`.
   subscript(type: AnyType) -> AnyType {
@@ -23,7 +50,7 @@ struct SubstitutionMap {
     return walked
   }
 
-  /// Assigns `substition` to `variable`.
+  /// Assigns `substitution` to `variable`.
   mutating func assign(_ substitution: AnyType, to variable: TypeVariable) {
     var walked = variable
     while let a = storage[walked] {
@@ -36,29 +63,57 @@ struct SubstitutionMap {
     storage[walked] = substitution
   }
 
-  /// Returns a dictionary representing the same mapping as `self`.
-  func asDictionary() -> [TypeVariable: AnyType] {
-    Dictionary(uniqueKeysWithValues: storage.lazy.map { (k, v) in (k, self[v]) })
+  /// Subtitutes each type variable occuring in `type` by its corresponding substitution in `self`,
+  /// apply `substitutionPolicy` to deal with free variables.
+  func reify(_ type: AnyType, withVariables substitutionPolicy: SubstitutionPolicy) -> AnyType {
+    func _impl(type: AnyType) -> TypeTransformAction {
+      if type.base is TypeVariable {
+        // Walk `type`.
+        let walked = self[type]
+
+        // Substitute `walked` for `type`.
+        if walked.base is TypeVariable {
+          switch substitutionPolicy {
+          case .substituteByError:
+            return .stepInto(.error)
+          case .keep:
+            return .stepOver(type)
+          }
+        } else {
+          return .stepInto(walked)
+        }
+      } else if !type[.hasVariable] {
+        // Nothing to do if the type doesn't contain any variable.
+        return .stepOver(type)
+      } else {
+        // Recursively visit other types.
+        return .stepInto(type)
+      }
+    }
+
+    return type.transform(_impl(type:))
   }
 
 }
 
-extension SubstitutionMap: CustomStringConvertible {
+extension SubstitutionMap: ExpressibleByDictionaryLiteral {
 
-  var description: String {
-    let elements = storage.map({ (key, value) in "\(key): \(value)" }).joined(separator: ", ")
-    return "[\(elements)]"
+  init(dictionaryLiteral elements: (TypeVariable, AnyType)...) {
+    for (k, v) in elements {
+      self.assign(v, to: k)
+    }
   }
 
 }
 
+extension SubstitutionMap: CustomStringConvertible {
+
+  var description: String { String(describing: storage) }
+
+}
+
 extension SubstitutionMap: CustomReflectable {
 
-  var customMirror: Mirror {
-    Mirror(
-      self,
-      children: storage.map({ (key, value) in (label: "\(key)", value: value) }),
-      displayStyle: .collection)
-  }
+  var customMirror: Mirror { storage.customMirror }
 
 }