ConstraintSystem

The scope in which the goals are solved.

The type checker used to query type relations and resolve names.

The goals in the system.

A map from goal its outcome.

The fresh goals to solve.

The goals that are currently stale.

The root goals that could not be solved.

A map from open type or term variable to its assignment.

This map is monotonically extended during constraint solving to assign a type or term to each open variable in the constraint system. A system is complete if it can be used to derive a complete substitution map w.r.t. its open variables.

A map from name expression to its referred declaration.

This map is monotonically extended during constraint solving to assign a declaration to each unresolved name expression in the constraint system. A system is complete if it can be used to derive a complete name binding map w.r.t. its unresolved name expressions.

A map from call expression to its operands after desugaring and implicit resolution.

The penalties associated with the constraint system.

This value serves to prune explorations that cannot produce a better solution than one already computed.

Indicates whether this instance should log a trace.

The current indentation level for logging messages.

Creates an instance for solving the constraints in obligations, logging a trace of the deduction process if loggingIsEnabled is true.

Creates an instance copying the state of other.

Solves this instance, using checker to query type relations and resolve names and returning the best solution found.

Solves this instance and returns the best solution with a score inferior or equal to self.maxScore, or nil if no such solution can be found.

Eliminates g, storing the necessary assumptions about its open variables in self and returning a solution if there are no more goals to solve.

Returns the currently known cost of the solution being computed.

The cost of a solution increases monotonically when a constraint is eliminated.

Returns true iff the solving g failed and g isn’t subordinate.

Records the outcome o for the goal key.

Creates a solution from the current state.

Creates an ambiguous solution, reporting the ambiguity with d.

The return value is the intersection of the choices and diagnostics that are identical in each result along with an additional diagnostic describing the ambiguity.

Determines whether g.model conforms to g.concept and returns: .success if it conforms explicitly, .product if it may conform structurally,.failure if it doesn’t conform, or nil if neither of these outcomes can be be determined yet.

Returns a closure diagnosing a failure to solve goal.

Returns eiteher .success if g.left is unifiable with g.right or .failure otherwise.

Returns a closure diagnosing a failure to solve goal.

Returns .success if g.left is subtype of g.right, .failure if it isn’t, .product if g must be broken down to smaller goals, or nil if that can’t be determined yet.

If the constraint is strict, then g.left must be different than g.right.

Implements of solve(subtyping:) for two ArrowTypes.

Implements of solve(subtyping:) for two UnionTypes.

Returns the outcome of solving subtype <: suprtype as a simplification of goal.

Returns a closure diagnosing a failure to solve goal.

Returns either .success if instances of g.left can be passed to a parameter g.right, .failure if they can’t, or nil if neither of these outcomes can be determined yet.

Returns either .success if instances of goal.left can be passed to a parameter p, .failure if they can’t, or nil if neither of these outcomes can be determined yet.

Returns either .success if g.subject has a member g.memberName of type g.memberType, .failure if it doesn’t, .product if g must be broken down to smaller goals, or nil if if neither of these outcomes can be determined yet.

Returns either .success if g.subject is a tuple type whose g.elementIndex-th element has type g.elementType, .failure if it doesn’t, .product if g must be broken down to smaller goals, or nil if if neither of these outcomes can be determined yet.

Returns either .success if g.callee is a callable type with parameters g.parameters and return type g.output, .failure if it doesn’t, .product if g must be broken down to smaller goals, or nil if neither of these outcomes can be determined yet.

Returns a closure diagnosing a failure to solve g because of an invalid callee.

Returns how the arguments in goal match the parameters of callee.

Undocumented

Solves the remaining goals separately for each choice in g and returns the best solution.

Solves the remaining goals separately for each choice in g and returns the best solution.

Solves the remaining goals in self exploring each choice in g with a separate constraint systems configured with configureSubSystem returns the best solution of each exploration.

Returns an outcome indicating that a goal has been broken into given subordinates and forwards their diagnostics.

Schedules g to be solved in the future and returns its identity.

Inserts g into the fresh set and returns its identity.

Inserts batch into the fresh set.

Schedules g to be solved only once the solver has inferred more information about at least one of its type variables.

Returns true iff lhs and rhs can be unified, updating the substitution table.

Type unification consists of finding substitutions that makes lhs and rhs equal. Both types are visited in lockstep, updating self.subscritutions every time either side is a variable for which no substitution has been made yet.

Returns true iff lhs and rhs can be unified.

Returns true iff lhs and rhs can be unified.

Returns true iff lhs and rhs can be unified.

Returns true iff t and u are equal under some substitution of their variables.

Returns true iff the result of matches(_:_:) applied on all elements from ts and us pairwise is true.

Returns true iff t and u are equal under some substitution of their variables.

Returns true iff t and u are equal under some substitution of their variables.

Extends the type substution table to map tau to substitute.

Extends the term substution table to map tau to substitute.

Refresh stale constraints containing variables that have been assigned.

Logs a line of text in the standard output if self.loggingIsEnabled is true.

Logs outcome in the standard output if self.loggingIsEnabled is true.

Logs self‘s current state in the standard output if self.loggingIsEnabled is true.