Dependent type inference for branches

[gancherj]

Hi all! I am trying to understand how F* manages type inference for unifying branches of a case split. In particular, how it manages to avoid variable escape for dependent types. Consider the following:

let foo (b : bool) =
  if b then
    let x : nat = 3 in
    let y : (a:nat{a == x + 1}) = 4 in
    y
  else
    let z : nat = 7 in
    let w : (a:nat{a == z + 1}) = 8 in
    w

emacs mode correctly reports foo to have type bool -> nat. And indeed, if I change the type annotation on w to be int instead of nat, foo is inferred to have type bool -> int. My question is: how does F* synthesize the common return type of the two branches to avoid x and z escaping their scopes, and unifying to the common refinement of nat?
Can I think of it as a unification problem, of the form (x |- a:nat{a == x+1}) <= (|- ?u) and (z |- a:nat{a == z + 1}) <= (|- ?u)?

[aseemr]

Hi @gancherj, you are right, there are two subtyping constraints as you have written.

When typechecking the match term here, F* creates a fresh unification variable b |- ?u:Type for the type of the match. The gamma for the unification variable ?u is just b, i.e. b is the only free variable that may occur in the solution of ?u.

For the then branch, F* creates a subtyping constraint a:nat{a == x + 1} <: ?u, and similarly a:nat{a == z + 1} <: ?u for the else branch. Since these are rigid-flex subtyping constraints, F* defers solving them until it has typechecked the whole term, this is so that it can collect other constraints on say ?u; in this case though these are the only two.

F* then collects all subtyping constraints for ?u, just these two here, and tries to solve them by combining the refinements. So, it tries to assign ?u = a:nat{a == x + 1 \/ a == z + 1} --- this fails since the only free variable that may occur in the solution of ?u is b, and this solution has x and z that are not allowed.

F* then tries a widening heuristic, and solves ?u = nat from the first constraint, dropping the refinement. With this solution, it then tries to check that the other subtyping constraints are also satisfied; in this case, yes. So F* succeeds with ?u = nat.

When w:int, then the logic to combine the refinements from the two subtyping constraints comes up with int as the result (nat is x:int{x >= 0}), and after that it works without any widening.

There is a third case here that I will just mention If we annotate the return type of foo itself, then F* will use bidirectional typechecking, where the match branches will be checked with the expected type as the annotated return type of foo (instead of a unification variable), and the subtyping constraints for the two branches will get solved separately, no need to join.

[gancherj]

I see! That makes sense. Thanks for the detailed answer!