_two_phase

Two Phase Type Checker

Below are attempts to understand the guards discharging process as well as its relationship with typechecking.

Summary

The relationship between discharging guards and type checking seems pretty complex. At different points in type checking, guards are generated. In some places, the type checking algorithm is asking to discharge guards and is waiting for results. Some of these requests target also SMT. Some others also loop between SMT and unification until a fix point is achieved.

Work should be done in understanding why some cases require SMT while others dont.

Discussions with people on the team hinted that the first phase will do unification only while the second phase will do SMT solving. From the description of the task on the roadmap, it seems that the first phase will deal with universes, types, implicit arguments and effect labels while the second will deal with WPs.

Clearly, from looking at the code, the two are mixed together. For example, inferring implicits applies both unification and SMT in a loop.

Conclusion

Unification is completely separated from SMT. A constraint is given to unification and the result to SMT and vice versa but there is no backtracking between SMT and unification. It means that the unification algorithm can be implemented as a separate entity. The benefits will be a dedicated unification algorithm for the F* language which is based on well-established papers and algorithms used in other dependent typed languages.

In order to efficiently separate the two phases, one needs first to understand if SMT is required to the constraints which are planned for the first phase. I.e. inferring implicit arguments really requires SMT?

Some subtype relations require SMT as well. Can they be dealt with by a stronger unification algorithm? Should they be deferred to the second phase?

Aseem's approach was to run it first in Lax mode in order for the SMT call to always succeed and then run it again with SMT turned on.

An attempt at approximating what discharging guards is doing

A more technical but partial description can be found here.

The type checking code generates and discharge guards using the Rel file. When trying to discharge guards, unification is always applied first in order to compute a list of unresolved constraints. If SMT is supported, unsolved constraints are then being forwarded to Z3.

There is a loop calling unification, then SMT, then unification, ....

Guards are conjunctions and implications of problems which are either typing problems or computation problems.

During unification, some problems are being deferred and when the non-deferred ones are all solved, unification is applied recursively. There is a mechanism checking if we have reached a fixed point when applying unification (using a counter which is incremented every time a substitution was applied, i.e. a problem was changed).

According to a remark, deferred can contain non-patterns and some subtype constraints containing variables.

Each problem is prioritized according to its rank since we always want to solve simple problems first (rigid-rigid, etc.).

There are two types of constraints - computation and typing.

There are 2 types of typing constraints - equality and subtyping.

Each guard can be defined to be trivial or non trivial, what does it mean?

The unification algorithms has options for solving patterns and non-patterns, equalities and subtyping relations.

A flex-flex subtype relation (even pattern) is always deferred if possible, if not, it is considered as equality and there is a loss of generality. (commented in code).

First or higher-order flex-rigid constraints where the rigid is a constant are always treated as equality. There is a remark that in case of arrows delaying destroys arity. This is also a loss of generality using the example from the above comment (not commented in code).

An attempt in understanding the relationship between type checking and discharging guards

Discharging guards is done using different methods during type checking. Some also expect SMT involvement if allowed.

discharge_guard (with SMT)

This method applies once unification and then SMT and is called when

• check_inductive_well_typeness
• tc_abs
• tc_eqn
• check_top_level_let_rec
• building a let rec environment

resolve_implicits

This method loop on unification, SMT, unification, .. but only on resolving implicits

• tc_eqn
• check_top_level_let
• check_top+level_let_rec
• build_let_rec_env

solve_deferred_constraints

Is applying only unification

• tc_abs
• check_application_args
• check_top_level_let
• check_top_level_let_rec
• tc_tot_or_gtot_term
• universe_of_aux

force_trivial_guard

Tries both solve_deferred_constraints and resolve_implicits from above and occurs in many places. It asserts that the guard is solvable.