Exponential time resolution in Adalog
=====================================

## Problem

When we started Libadalang, we decided to use a constraints solver to resolve
overload in Ada name resolution.

The way resolution works, is that we traverse expression trees, and create sets
of constraints on references and types. Expressions which involve resolving
overloads, such as subprogram calls, will create disjunctions in the set of
constraints.

### Examples

#### Simple example

Here is an example of a simple statement, whose resolution does not create any
disjunctions, because no overloading is involved

procedure Test is
   function Add (L, R : Integer) return Integer is (L + R);

   A : Integer;
begin
   A := Add (2, Add (3, 5));
   pragma Test_Statement;
end Test;

Adalog produces the following equation for it

<All>:
|  Member <Id "A" 6:4-6:5>.F_R_Ref_Var {<ObjectDecl ["A"] 4:4-4:16>}
|  Bind <Id "A" 6:4-6:5>.F_R_Ref_Var <=> <Id "A" 6:4-6:5>.F_Type_Var (convert: BasicDecl.p_expr_type)
|  Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:14-6:15>.F_Type_Var
|  Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:22-6:23>.F_Type_Var
|  Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:25-6:26>.F_Type_Var
|  Unify <Id "Add" 6:17-6:20>.F_R_Ref_Var <= <ExprFunction ["Add"] 2:4-2:60>
|  Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
|  Unify <Int 6:22-6:23>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
|  Unify <Int 6:25-6:26>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
|  Bind <Id "Add" 6:17-6:20>.F_R_Ref_Var <=> <Id "Add" 6:17-6:20>.F_R_Ref_Var
|  Member <Id "Add" 6:17-6:20>.F_R_Ref_Var {<ExprFunction ["Add"] 2:4-2:60>}
|  Bind <Id "Add" 6:17-6:20>.F_R_Ref_Var <=> <Id "Add" 6:17-6:20>.F_Type_Var (convert: BasicDecl.p_expr_type)
|  Unify <Id "Add" 6:9-6:12>.F_R_Ref_Var <= <ExprFunction ["Add"] 2:4-2:60>
|  Unify <CallExpr 6:9-6:28>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
|  Unify <Int 6:14-6:15>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
|  Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
|  Bind <Id "Add" 6:9-6:12>.F_R_Ref_Var <=> <Id "Add" 6:9-6:12>.F_R_Ref_Var
|  Member <Id "Add" 6:9-6:12>.F_R_Ref_Var {<ExprFunction ["Add"] 2:4-2:60>}
|  Bind <Id "Add" 6:9-6:12>.F_R_Ref_Var <=> <Id "Add" 6:9-6:12>.F_Type_Var (convert: BasicDecl.p_expr_type)
|  Bind <CallExpr 6:9-6:28>.F_Type_Var <=> <Id "A" 6:4-6:5>.F_Type_Var (equals: BaseTypeDecl.p_matching_assign_type)

What we can see in the above constraint set, is that there is no disjunction:
The top level All constraint is a conjunction, ensuring all conditions are met.
The worst execution time is linear.

**Beware**, note that the Member constraint can be a disjunction if there is
more than one element in the set, which is not the case here.

#### Disjunction example

Here is however a program that creates a disjunction

procedure Test1 is
   type Int is range 0 .. 10;
   type Int2 is range 0 .. 10;

   function B (P : Int2) return Int;
   function B (P : Int) return Int;
   function B (P : Int) return Int2;

   A : Int;
begin
   A := B (9);
   pragma Test_Block;
end Test1;

And the corresponding equation

<All>:
|  Member <Id "A" 11:4-11:5>.F_R_Ref_Var {<ObjectDecl ["A"] 9:4-9:12>}
|  Bind <Id "A" 11:4-11:5>.F_R_Ref_Var <=> <Id "A" 11:4-11:5>.F_Type_Var (convert: BasicDecl.p_expr_type)
|  Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 11:12-11:13>.F_Type_Var
|  <Any>:
|  |  <All>:
|  |  |  Unify <Id "B" 11:9-11:10>.F_R_Ref_Var <= <SubpDecl ["B"] 7:4-7:37>
|  |  |  Unify <CallExpr 11:9-11:14>.F_Type_Var <= <TypeDecl ["Int2"] 3:4-3:31> (equals: BaseTypeDecl.p_matching_type)
|  |  |  Unify <Int 11:12-11:13>.F_Type_Var <= <TypeDecl ["Int"] 2:4-2:30> (equals: BaseTypeDecl.p_matching_formal_type)
|  |  <All>:
|  |  |  Unify <Id "B" 11:9-11:10>.F_R_Ref_Var <= <SubpDecl ["B"] 6:4-6:36>
|  |  |  Unify <CallExpr 11:9-11:14>.F_Type_Var <= <TypeDecl ["Int"] 2:4-2:30> (equals: BaseTypeDecl.p_matching_type)
|  |  |  Unify <Int 11:12-11:13>.F_Type_Var <= <TypeDecl ["Int"] 2:4-2:30> (equals: BaseTypeDecl.p_matching_formal_type)
|  |  <All>:
|  |  |  Unify <Id "B" 11:9-11:10>.F_R_Ref_Var <= <SubpDecl ["B"] 5:4-5:37>
|  |  |  Unify <CallExpr 11:9-11:14>.F_Type_Var <= <TypeDecl ["Int"] 2:4-2:30> (equals: BaseTypeDecl.p_matching_type)
|  |  |  Unify <Int 11:12-11:13>.F_Type_Var <= <TypeDecl ["Int2"] 3:4-3:31> (equals: BaseTypeDecl.p_matching_formal_type)
|  Bind <Id "B" 11:9-11:10>.F_R_Ref_Var <=> <Id "B" 11:9-11:10>.F_R_Ref_Var
|  Member <Id "B" 11:9-11:10>.F_R_Ref_Var {<SubpDecl ["B"] 7:4-7:37>, <SubpDecl ["B"] 6:4-6:36>, <SubpDecl ["B"] 5:4-5:37>}
|  Bind <Id "B" 11:9-11:10>.F_R_Ref_Var <=> <Id "B" 11:9-11:10>.F_Type_Var (convert: BasicDecl.p_expr_type)
|  Bind <CallExpr 11:9-11:14>.F_Type_Var <=> <Id "A" 11:4-11:5>.F_Type_Var (equals: BaseTypeDecl.p_matching_assign_type)

Here we can see a disjunction, in the form of the `Any` and
`Member`constraints.

Disjunctions are at the heart of the problem of exponential complexity.

## Why disjunctions are a problem

Due to the way Adalog works, it will potentially explore the whole solution
tree before finding a solution. For disjunctions, it means that Adalog will
explore the [Cartesian product](https://en.wikipedia.org/wiki/Cartesian_product)
of all possible alternatives in all disjunctions.

The resulting runtime is exponential in the worst case. We also found real
world cases where solving becomes exponential.

## Exponential example

The following (simplified) example, is a case where Libadalang has an
exponential complexity. For each add in the ladder of add calls, the number of
explored solutions is ~doubled.

procedure ExponentialResolution is
   function Add (L : Integer; R : Integer) return Integer;
   function Add (L : Integer; R : String) return String;
   function Add (L : String; R : Integer) return String;
   function Add (L : Float; R : String) return String;
   function Add (L : Float; R : Float) return String;
   function Add (L, R: Character) return String;
   function Add (L, R: Integer) return String;
   function Add (L, R: Integer) return Float;
   function Add (L : String; R : Float) return String;
   function Add (L : Integer; R : Integer) return String;

   A : Integer;
begin
   A := Add
     (1, Add
      (2, Add (3, Add (4, Add (5, Add (6, Add (7, Add (8, Add (9, 10)))))))));
   pragma Test_Statement;
end ExponentialResolution;

What happens is that the correct overload is the last to be tried, for every
add call. The solver will explore every combination of add overloads before
finding the good one.

This is also linked to the fact that we use literals in the example. The same
behavior doesn't exhibit if you use a variable with a fixed type.

## How to solve the problem

### Intuitively

Intuitively, in the example above, there is no reason the solver has to be so
dumb. The way we would figure out the proper overloads by hand, is to start at
the leaves of the expression (here `Add (9, 10)`), find its type or set of
types, and propagate it downwards.

In this case, there is only one valid overload for this one, that can be
propagated down every call.

Conversely, we could start from the root (here the assignment), which imposes a
pretty strict constraint on the equation (type has to be integer). Again, it
would set the only possible overload of the toplevel Add call, since only one
Add function returns an Integer.

This example has been engineered to both be trivial intuitively and a worst
case scenario for the solver.

> #### A note about failure
>
> In the example above, and in most cases (not all), constraints order could be
> rearranged so that the solution is found much faster.
>
> **However**, if the expression is invalid (eg. the equation has no solution),
> the solver has no other choice than to explore the whole solution space !
>
> For this reason, reordering tricks, in Langkit or in Libadalang, might not be
> sufficient long term.
>
> They could however be a short-term solution, with a guard that stops resolution
> when it takes too long.

### Formally

Equations are constructed top-down by the solver, which means that constraints
about the leaves will be accumulated at the top of the equation, then by
descending order.

We propose propagating constraints prior to solving, to weed out disjunctions
that are never possible.

Propagating constraints would work by keeping a set of "always True" facts
about each logic variable, at different points in the equation, and use this
set to weed out constraints that we know to be False.

### An example

Taking a much simplified example for the case shown above:

procedure ExponentialResolution is
   function Add (L : Integer; R : Integer) return Integer;
   function Add (L : Integer; R : String) return String;
   A : Integer;
begin
   A := Add (2, Add (2, 2));
end ExponentialResolution;

We get the following equation

~~~
<All>:
| Member <Id "A" 6:4-6:5>.F_R_Ref_Var {<ObjectDecl ["A"] 4:4-4:16>}
| Bind <Id "A" 6:4-6:5>.F_R_Ref_Var <=> <Id "A" 6:4-6:5>.F_Type_Var (convert: BasicDecl.p_expr_type)
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:14-6:15>.F_Type_Var
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:22-6:23>.F_Type_Var
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:25-6:26>.F_Type_Var
| <Any>:
| | <All>:
| | | Unify <Id "Add" 6:17-6:20>.F_R_Ref_Var <= <SubpDecl ["Add"] 3:4-3:57>
| | | Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["String"] 104:3-104:57> (equals: BaseTypeDecl.p_matching_type)
| | | Unify <Int 6:22-6:23>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| | | Unify <Int 6:25-6:26>.F_Type_Var <= <TypeDecl ["String"] 104:3-104:57> (equals: BaseTypeDecl.p_matching_formal_type)
| | <All>:
| | | Unify <Id "Add" 6:17-6:20>.F_R_Ref_Var <= <SubpDecl ["Add"] 2:4-2:59>
| | | Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
| | | Unify <Int 6:22-6:23>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| | | Unify <Int 6:25-6:26>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Bind <Id "Add" 6:17-6:20>.F_R_Ref_Var <=> <Id "Add" 6:17-6:20>.F_R_Ref_Var
| Member <Id "Add" 6:17-6:20>.F_R_Ref_Var {<SubpDecl ["Add"] 3:4-3:57>, <SubpDecl ["Add"] 2:4-2:59>}
| Bind <Id "Add" 6:17-6:20>.F_R_Ref_Var <=> <Id "Add" 6:17-6:20>.F_Type_Var (convert: BasicDecl.p_expr_type)
| <Any>:
| | <All>:
| | | Unify <Id "Add" 6:9-6:12>.F_R_Ref_Var <= <SubpDecl ["Add"] 3:4-3:57>
| | | Unify <CallExpr 6:9-6:28>.F_Type_Var <= <TypeDecl ["String"] 104:3-104:57> (equals: BaseTypeDecl.p_matching_type)
| | | Unify <Int 6:14-6:15>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| | | Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["String"] 104:3-104:57> (equals: BaseTypeDecl.p_matching_formal_type)
| | <All>:
| | | Unify <Id "Add" 6:9-6:12>.F_R_Ref_Var <= <SubpDecl ["Add"] 2:4-2:59>
| | | Unify <CallExpr 6:9-6:28>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
| | | Unify <Int 6:14-6:15>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| | | Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Bind <Id "Add" 6:9-6:12>.F_R_Ref_Var <=> <Id "Add" 6:9-6:12>.F_R_Ref_Var
| Member <Id "Add" 6:9-6:12>.F_R_Ref_Var {<SubpDecl ["Add"] 3:4-3:57>, <SubpDecl ["Add"] 2:4-2:59>}
| Bind <Id "Add" 6:9-6:12>.F_R_Ref_Var <=> <Id "Add" 6:9-6:12>.F_Type_Var (convert: BasicDecl.p_expr_type)
| Bind <CallExpr 6:9-6:28>.F_Type_Var <=> <Id "A" 6:4-6:5>.F_Type_Var (equals: BaseTypeDecl.p_matching_assign_type)
~~~

Here, we see that constraints for the leaves of the expression (the integer
literals) accumulated at the top of the expression.

We'll build the following constraint set:

~~~
Constraint set in toplevel All:
Int 6:14: Is_Int
Int 6:22: Is_Int
Int 6:25: Is_Int
~~~

If we carry this information in the subsequent child constraints, when we
arrive on the constraint

~~~
Unify <Int 6:25-6:26>.F_Type_Var <= <TypeDecl ["String"] 104:3-104:57> (equals: BaseTypeDecl.p_matching_formal_type)
~~~

We can query the constraints on the Int literal's type var, and see that this
can never be true, and transform this constraint into a False rel. This will in
turn allow us to:

1. Fold the whole `All` block into a False rel.
2. Inline the `Any` block into its parent, since it has only one disjunction
now.

This will yield the following equation:

~~~
<All>:
| Member <Id "A" 6:4-6:5>.F_R_Ref_Var {<ObjectDecl ["A"] 4:4-4:16>}
| Bind <Id "A" 6:4-6:5>.F_R_Ref_Var <=> <Id "A" 6:4-6:5>.F_Type_Var (convert: BasicDecl.p_expr_type)
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:14-6:15>.F_Type_Var
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:22-6:23>.F_Type_Var
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:25-6:26>.F_Type_Var
| Unify <Id "Add" 6:17-6:20>.F_R_Ref_Var <= <SubpDecl ["Add"] 2:4-2:59>
| Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
| Unify <Int 6:22-6:23>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Unify <Int 6:25-6:26>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Bind <Id "Add" 6:17-6:20>.F_R_Ref_Var <=> <Id "Add" 6:17-6:20>.F_R_Ref_Var
| Member <Id "Add" 6:17-6:20>.F_R_Ref_Var {<SubpDecl ["Add"] 3:4-3:57>, <SubpDecl ["Add"] 2:4-2:59>}
| Bind <Id "Add" 6:17-6:20>.F_R_Ref_Var <=> <Id "Add" 6:17-6:20>.F_Type_Var (convert: BasicDecl.p_expr_type)
| <Any>:
| | <All>:
| | | Unify <Id "Add" 6:9-6:12>.F_R_Ref_Var <= <SubpDecl ["Add"] 3:4-3:57>
| | | Unify <CallExpr 6:9-6:28>.F_Type_Var <= <TypeDecl ["String"] 104:3-104:57> (equals: BaseTypeDecl.p_matching_type)
| | | Unify <Int 6:14-6:15>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| | | Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["String"] 104:3-104:57> (equals: BaseTypeDecl.p_matching_formal_type)
| | <All>:
| | | Unify <Id "Add" 6:9-6:12>.F_R_Ref_Var <= <SubpDecl ["Add"] 2:4-2:59>
| | | Unify <CallExpr 6:9-6:28>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
| | | Unify <Int 6:14-6:15>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| | | Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Bind <Id "Add" 6:9-6:12>.F_R_Ref_Var <=> <Id "Add" 6:9-6:12>.F_R_Ref_Var
| Member <Id "Add" 6:9-6:12>.F_R_Ref_Var {<SubpDecl ["Add"] 3:4-3:57>, <SubpDecl ["Add"] 2:4-2:59>}
| Bind <Id "Add" 6:9-6:12>.F_R_Ref_Var <=> <Id "Add" 6:9-6:12>.F_Type_Var (convert: BasicDecl.p_expr_type)
| Bind <CallExpr 6:9-6:28>.F_Type_Var <=> <Id "A" 6:4-6:5>.F_Type_Var (equals: BaseTypeDecl.p_matching_assign_type)
~~~

In the original constraint set we computed, we did not have enough information
to filter any of the second's disjunction branches. We cannot filter the first
one (which is the one we want to filter), because the filtering depends on the
type of the first call expression.

However, we now have a unique constraint for the type of this call expr, since
we inlined one of the first disjunction's branches:

~~~
Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
~~~

So, if we:

1. Also keep track of Unifys instead of just predicates, constructing a set of
possible values
2. Recompute the set of constraints with the relations we just inlined

We can get the following set of constraints:

~~~
Constraint set in toplevel All:
Int 6:14.type: Is_Int
Int 6:22.type: Is_Int, {TypeDecl Integer}
Int 6:25.type: Is_Int, {TypeDecl Integer}
Id Add 6:17.ref: {SubpDecl Add 2:4}
CallExpr 6:17.type: {TypeDecl Integer}
~~~

Which will allow us to filter out the first branch of the second disjunction,
since it's trying to unify the type of the callexpr at line 6 with String, and
we know from the constraint set that it can only be an Integer.

After propagating the False rel, we'll have the following relation:

~~~
<All>:
| Member <Id "A" 6:4-6:5>.F_R_Ref_Var {<ObjectDecl ["A"] 4:4-4:16>}
| Bind <Id "A" 6:4-6:5>.F_R_Ref_Var <=> <Id "A" 6:4-6:5>.F_Type_Var (convert: BasicDecl.p_expr_type)
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:14-6:15>.F_Type_Var
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:22-6:23>.F_Type_Var
| Predicate Base_Type_Decl.P_Is_Int_Type_Or_Null on <Int 6:25-6:26>.F_Type_Var
| Unify <Id "Add" 6:17-6:20>.F_R_Ref_Var <= <SubpDecl ["Add"] 2:4-2:59>
| Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
| Unify <Int 6:22-6:23>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Unify <Int 6:25-6:26>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Bind <Id "Add" 6:17-6:20>.F_R_Ref_Var <=> <Id "Add" 6:17-6:20>.F_R_Ref_Var
| Member <Id "Add" 6:17-6:20>.F_R_Ref_Var {<SubpDecl ["Add"] 3:4-3:57>, <SubpDecl ["Add"] 2:4-2:59>}
| Bind <Id "Add" 6:17-6:20>.F_R_Ref_Var <=> <Id "Add" 6:17-6:20>.F_Type_Var (convert: BasicDecl.p_expr_type)
| Unify <Id "Add" 6:9-6:12>.F_R_Ref_Var <= <SubpDecl ["Add"] 2:4-2:59>
| Unify <CallExpr 6:9-6:28>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_type)
| Unify <Int 6:14-6:15>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Unify <CallExpr 6:17-6:27>.F_Type_Var <= <TypeDecl ["Integer"] 4:3-4:54> (equals: BaseTypeDecl.p_matching_formal_type)
| Bind <Id "Add" 6:9-6:12>.F_R_Ref_Var <=> <Id "Add" 6:9-6:12>.F_R_Ref_Var
| Member <Id "Add" 6:9-6:12>.F_R_Ref_Var {<SubpDecl ["Add"] 3:4-3:57>, <SubpDecl ["Add"] 2:4-2:59>}
| Bind <Id "Add" 6:9-6:12>.F_R_Ref_Var <=> <Id "Add" 6:9-6:12>.F_Type_Var (convert: BasicDecl.p_expr_type)
| Bind <CallExpr 6:9-6:28>.F_Type_Var <=> <Id "A" 6:4-6:5>.F_Type_Var (equals: BaseTypeDecl.p_matching_assign_type)
~~~

In this case, the solution space is of size 1, so the solver just has to affect values to variables.

#### High-level algorithm

At a high level, the constraint propagation would be a top-down visitor for the
constraint system.

The visitor would have a state, that would be passed down the visitor. Visiting
a node would return a new state object, that is the set of constraints that
have been inferred visiting the node.

type State is
    vars_to_values: Map[LogicVar, Vector[NodeVal]]

type NodeVal is
    node    : Node
    eq_prop : PropertyRef

Since the State type is basically a set of possible values for each encountered
logic variable, it would have union and intersection operations.

function intersection(state_1, state_2: State) is
    State(map(x, y -> intersection(x, y),
              zip(state_1.vars_to_values, state_2.vars_to_values)))

function union(state_1, state_2: State) is
    State(map(x, y -> union(x, y),
              zip(state_1.vars_to_values, state_2.vars_to_values)))

The intersection operation between two set of NodeVals is a bit special because

function intersection(v1, v2: Vector[Node]) is