Istari

Typechecking

Typechecking for the Istari logic is undecidable, so typechecking is necessarily best effort. The typechecker should generally work well, provided the terms:

  1. use only constants whose types are known,

  2. are kept in beta-normal form,

  3. do not require establishing non-trivial facts (including equalities) to typecheck, and

  4. do not entail ambiguous typing constraints.

Ambiguous constraints

Proviso #4 requires some elaboration. Ambiguous typing constraints will be avoided if all type arguments are supplied. When type arguments are omitted, Istari will create evars for those arguments, and resolve them using higher-order unification. To make higher-order unification practical, Istari employs the relaxed pattern fragment. An evar is in the pattern fragment when it is applied to (or is substituted into by) distinct variables. For example, E x y is in the pattern fragment, but E x x, E x (f x) and E x E' are not. In the relaxed pattern fragment, evars with non-variable arguments/substitutends are permitted, but those arguments/substitutends are ignored. Thus E x (f x) and E x E' are permitted, but the solution for E will never use its second argument.

Non-pattern evars arise most frequently when one substitutes into an evar. For example, suppose f : forall (x : A) . E and f M is used where a B is expected. This creates a constraint equating [M / x] E with B, but the former is not in the pattern fragment. In such a situation, the typechecker may (depending on exactly what M is) ignore the dependency on M, or it may defer the entire constraint, in the hope that some other constraint will resolve E. In the latter case, if no other constraint resolves E, an ambiguous constraint is reported.

Additional discussion of unification can be found here.

Coping strategies

When typechecking fails, there are some strategies that can be employed.

The algorithm

A typecheckable proposition has one of the following forms:

The typechecker seeks to prove typecheckable propositions. In addition, the typechecker will attempt to discharge level constraints (i <l= j), and positivity requirements for inductive types (positive (fn t . A)).

The algorithm proceeds as follows:

Typing

For goals of the form M : A, put M in basic whnf, and put A in hard whnf. Then:

  1. If A is level and M is an evar, set the goal aside for the level solver.

  2. If M is unknown, defer.

  3. If M or A is marked manual, generate a subgoal and stop. (We say a term is marked manual when it has the form manual _ or manualf _.)

  4. If the goal matches a hypothesis, use it.

  5. If M is a variable, attempt to unify its type with A, unless its type is a universe. (This is not quite a special case of 8, since A might be intersect, etc.)

  6. If A is known, use any applicable intro or formation rule.

  7. If M is let, use the let rule. (We don’t treat this as a normal constant because we don’t want to require that the bound term’s type belongs to a universe.)

    If M is letnext, use the nondependent letnext rule. (The special typing aspects of letnext mean that we cannot handle it the same way as other open-scope elim forms.)

  8. If M is a path then:

    a. Infer the natural type for M, say B.

    b. If M’s natural type cannot be inferred because a prefix of its type is an evar, defer.

    c. If B is not of the form U i, attempt to unify A and B. (Special case of d, but avoids extra subgoals.)

    Note: This comports with the use of the “greedy algorithm” to resolve subtyping.

    d. Prove B <: A.

  9. Reject

Type formation

For goals of the form A : type, put A in basic whnf. Then:

  1. If A is unknown, defer.

  2. If A is marked manual, generate a subgoal and stop.

  3. If the goal matches a hypothesis, use it.

  4. If A is a variable and its sort is type or U i then accept.

  5. If A is known, use any applicable formation rule.

  6. Prove A : U i for fresh i.

Subtyping

For goals of the form A <: B, put A and B in hard whnf. Then:

  1. If A or B is marked manual, generate a subgoal and stop.

  2. If B is U i, then:

    a. Attempt to unify A with U j, for fresh j. If successful, prove j <l= i and i, j : level.

    b. Attempt to unify A with K j, for fresh j. If successful, prove 1 + j <l= i and i, j : level.

    c. Reject

  3. Unify A and B if possible. If successful, prove A : type.

    Note: This means subtyping is resolved using the “greedy algorithm” when possible. This usually performs well in practice, but occasionally it can have unpredictable results.

  4. If the goal matches a hypothesis, use it.

  5. Use any applicable subtyping rule.

  6. Prove A = B : type.

Type equivalence

For goals of the form A = B : type, put A and B in hard whnf. Then:

  1. If A or B is marked manual, generate a subgoal and stop.

  2. Unify A and B if possible. If successful, prove A : type.

  3. If the goal matches a hypothesis, use it.

  4. Use any applicable type equality rule.

  5. Prove A = B : U i for unknown i.

Equality at a universe

For goals of the form A = B : U i or A = B : K i, put A and B in hard whnf. Then:

  1. If A or B is marked manual, generate a subgoal and stop.

  2. Unify A and B if possible. If successful, prove A : U i or A : K i.

  3. If the goal matches a hypothesis, use it.

  4. Use any applicable type equality rule.

  5. Try compatibility.

  6. Reject.

Reduction strategies

Three strategies are used for normalization, depending on the context:

  1. Standard reduction (used by unification)

    • Utilizes user-defined reductions.
    • Never unfolds soft or firm constants.
  2. Hard reduction (used in some typechecking circumstances, and many tactics)

    • Utilizes user-defined reductions.
    • Always unfolds soft or firm constants.
  3. Basic reduction (used in some typchecking circumstances)

    • Never utilizes user-defined reductions.
    • Always unfolds soft constants.
    • Never unfolds firm constants.

    In other words, basic reduction unfolds soft head constants, but otherwise does only the minimum necessary to put a term into whnf. To do more might remove vital type annotations expressed using firm constants.

Typechecker interface

There are five main entry points to the typechecker:

When typechecking fails to discharge a goal, it attaches a short message (e.g., undischarged typing obligation). One can obtain further information on what went wrong by asking for detail (by calling Prover.detail : unit -> unit or just entering C-c C-d in the UI.)

For example, if typechecker is invoked on the goal true + 1 : nat, one gets back the subgoal:

[undischarged typing obligation]
|-
bool = nat : U E6

1 goal (depth 0)

Additional detail provides:

Type error: incompatible type paths
 first: bool
second: nat


with history:
[  0]  bool = nat : U E6
[  1]  bool = nat : type
[  2]  bool <: nat
[  3]  true : nat
[  4]  true + 1 : nat

First it explains where it got stuck (bool and nat don’t seem to be equal). Then it gives a trace of the typechecker’s efforts that led to that point. At the end of the trace (goal 4 in this case) is the initial goal.

One can get a detailed trace of everything the typechecker does by setting Typecheck.trace : bool ref to true.