-
Notifications
You must be signed in to change notification settings - Fork 236
The unification algorithm
The algorithm is defined in the file typechecker/FStar.TypeChecker.Rel.fs
During type checking a guard containing all constraints is being built. When the guard is to be discharged, one calls discharge_guard. This method first tries to apply unification and if SMT is allowed, it then sends the updated obligation to SMT.
Before we try to apply unification, we translate the guard into a list of unification constraints (working list) in wl_of_guard. The unification problem might allow deferred problems or not (the working list defer_ok switch).
Then we can call the algorithm on the problem by recursing on the problems in the list.
Problems can be either computation constraints or typing constraints
In case deferring constraints is not allowed and the problem is not rigid-rigid or flex-flex, we try one of solve_flex_rigid_join and solve_rigid_flex_meet. Otherwise, we apply the main solving function solve_t'.
Unification applies different rules according to the two types we try to unify. In this section we describe the different possible cases.
Checked first.
In case both sides are syntactically identical (using BU.physical_equality), we remove this problem and continue
From some reason, we check it twice! Remove one case.
This cases are dealt with first.
We call solve_one_universe_eq
In these cases, we have a variable (or an application with a variable head - HO variable) on one side and a term on the other.
Flex-rigid cases are the most interesting ones. In FO, patterns and FCU, we just replace the variable with a version of the term on the other side.
In the other cases, a non-determinism exists in the problem since we might be able to unify the problem with two different substitutions. The imitate one tries to replace the variable with a term whose head is the same as the head of the other term (which is either a constant of a bvar). The project case tries to project one of the arguments into head position.
This is the standard case where we compare them syntactically. We apply solve_t_flex_rigid.
Covers when we have a variable on one side and a universe or an arrow type on the other. According to the comments:
this case is so common, that even though we could delay, it is almost always ok to solve it immediately as an equality besides, in the case of arrows, if we delay it, the arity of various terms built by the unifier goes awry so, don't delay!
These problems are treated as syntactical equality
If we can defer these problems, we do so. Otherwise,
Cases where we have variables on both sides. They have most general unifiers in patterns and FCU but might have inifinite minimal complete unifiers set otherwise.
Therefore, first-order, patterns and FCU should be applied eagerly, the rest should be deferred.
We call the flex_flex function