feat: introduce bag-of-constraints solver

[mlutze]

[magnus-madsen]

The diff is very large, it is just because of a missing merge/rebase? I feel like I still dont understand git.

[mlutze]

The diff is very large, it is just because of a missing merge/rebase? I feel like I still dont understand git.

Yeah, the git ghost is about. I'll fix it sometime.

[magnus-madsen]

Can you write me a short description of how to best review this?

[mlutze]

Can you write me a short description of how to best review this?

No, but I can write a long one.

Before this PR

Unification of types is handled in two different places:

• ConstraintSolver is called by Typer
• Unification is called everywhere else: Monomorph, HoleCompletion, EffectVerifier, Instances, Stratifier, as well as ConstraintSolver itself.
• Unification is just a wrapper around OldStarUnification

This PR

This PR does 2 things:

• introduces ConstraintSolver2, a bag-of-constraints, phase-based parser
• changes Unification to call ConstraintSolver2 instead of OldStarUnification

Other changes are administrative:

• Copy of RecordConstraintSolver using ConstraintSolver2 interface
• ditto SchemaConstraintSolver
• ditto TypeReduction
• Cutting off RecordUnification and SchemaUnification from the new Unification

ConstraintSolver2

This solver applies the unification rules as phases. The high-level algorithm is:

while progress:
    for each phase:
        for each constraint:
            apply the phase's rule to the constraint

Each phase is represented by a function taking a type constraint and returning one of the following:

• a type constraint
• a set of type constraints
• a set of type constraints and a substitution tree

These phases are applied to a collection of constraints through an abstraction Soup, which allows a pipeline-like syntax for applying rules, while hiding management of substitutions.

The substitution tree is not used in this PR, as it is intended for Purification constraints, which do not arise from calling Unification functions. You can think of the substitution tree as a simple substitution for now.

After this PR

At least three PRs will follow.

1. A PR to remove code made redundant by this PR. This includes:

• RecordUnification
• SchemaUnification
• EqualityEnvironment
• AssocTypeSubstitution
• OldStarUnification
• possibly more

2. A PR to replace ConstraintSolver with ConstraintSolver2. This will likely reveal some bugs.
3. A PR to remove code made redundant by PR 2. (By overwriting it with ContraintSolver2's helpers. This includes:

• TypeReduction
• RecordConstraintSolver
• SchemaConstraintSolver
• probably more

[magnus-madsen]

In the final version, how will Monomorpher conduct unification?

Will it use constraints? One constraint? Or will it just call deeper into the solver (i.e. some specific unification procedure?)

[mlutze]

In the final version, how will Monomorpher conduct unification?

Will it use constraints? One constraint? Or will it just call deeper into the solver (i.e. some specific unification procedure?)

It will use one constraint. That behavior is introduced by this PR, through an interface.

[magnus-madsen]

I still need to look at ConstraintSolver2

[magnus-madsen]

Adding some source comments for some of my comments might be useful.

[mlutze]

Adding some source comments for some of my comments might be useful.

I do not know what this means.

[magnus-madsen]

I will review this soon again, but I need Jonathans PR to land first. So you should also harass him :)

[magnus-madsen]

@mlutze There are no conflicts. Does this mean I can merge this or do you want to experiment?

[mlutze]

@mlutze There are no conflicts. Does this mean I can merge this or do you want to experiment?

Let's at least wait for one tick on the arewefast graph :)

[JonathanStarup]

Will this PR not use SetUnification.unifyAll? or is that later?

[mlutze]

Will this PR not use SetUnification.unifyAll? or is that later?

Later. This one only deals with one constraint at a time anyway.

[magnus-madsen]

@mlutze You can merge this tomorrow.