Unification structure

[herbelin]

This CEP is about organizing knowledge about the (evarconv) unification algorithm of Coq in the hope to draw directions for the future.

It is a rather extensive first draft but at the same time a rather naive one. A lot should be done to make it even more comprehensive, collecting experiences and contributions of everyone.

Rendered here

[JasonGross]

This optimization seems unsound?
Consider x : nat |- ?e : nat and the pair of unification problems |- ?e@{x:=O} == ?e@{x:=S O} and x : nat |- ?e@{x:=x} == match x with O => O | S _ => O end. The only valid solution of this is ?e := match x with O => O | S _ => O end, which refers to x.
And in fact Coq fails to solve such a problem:

Check let e := (fun x => ?[e]) in
      eq_refl : (e O, e) = (e (S O), fun x => match x with O => O | S _ => O end).
(* Error:
In environment
e := fun _ : nat => ?e : nat -> nat
The term "eq_refl" has type "(e 0, e) = (e 0, e)" while it is expected to have type
 "(e 0, e) = (e 1, fun x : nat => match x with
                                  | 0 | _ => 0
                                  end)" (cannot instantiate "?e" because "x" is not in its scope).
*)

[JasonGross]

Reported as coq/coq#15110

[herbelin]

You're right, this should be distinct neutral, i.e. blocking on a variable, head normal forms. Current code is indeed wrong and should be modified.

[JasonGross]

I'm not sure I understand this one. Is conversion run again after unification completes? How do you get convertibility constraints? Also, this seems overly optimistic, consider x : nat |- ?e : nat and |- ?f : nat and the pair of unification problems |- ?e@{x:=O} == ?e@{x:=S O} and x : nat |- ?e@{x:=x} == match x with O => O | S _ => ?f end. We must instantiate ?e with match x with O => O | S _ => ?f end, and only after this substitution do we get |- O == ?f out of the first unification problem, which it seems would have been dropped according to this rule.

It seems that Coq can solve this problem, though?

Check let e := (fun x => ?[e]) in
      let f := ?[f] in
      eq_refl : (e, e O) = (fun x => match x with O => O | S _ => f end, e (S O)).

[herbelin]

It seems I meant "If both instances are pointwise existential-variable-free compatible terms". So, with your previous remark, it should be "If both instances are pointwise existential-variable-free compatible neutral terms".

Your example works because e := fun x => match x with O => O is solved first. If you invert the order of unification problems:

Check let e := (fun x => ?[e]) in
      let f := ?[f] in
      eq_refl : (e O, e) = (e (S O), fun x => match x with O => O | S _ => f end).

it fails.

[JasonGross]

What does "non-erasable position" mean? What does "restricted" mean?

[JasonGross]

If I'm understanding correctly, this again seems incorrect for the same reason as above. We might have consider x : nat |- ?e : bool and x : nat |- ?e' : bool and the triple of unification problems x, y : nat |- ?e@{x:=S x} == ?e'@{x:=S y} and x : nat |- ?e@{x:=x} == match x with O => true | S _ => false end and x : nat |- ?e@{x:=x} == match x with O => true | S _ => false end. We must instantiate ?e and e' both with match x with O => true | S _ => false end.

Check let e := (fun x => ?[e]) in
      let e' := (fun x => ?[e']) in
      fun x y => eq_refl
                 : (e (S x), e, e') =
                   (e' (S y), (fun x => match x with O => true | S _ => false end),
                    (fun x => match x with O => true | S _ => false end)).
(* Error:
In environment
e := fun x : nat => match x with
                    | 0 => true
                    | S _ => false
                    end : nat -> bool
e' := fun _ : nat => false : nat -> bool
x : nat
y : nat
The term "eq_refl" has type "(e (S x), e, e') = (e (S x), e, e')" while it is expected to have type
 "(e (S x), e, e') =
  (e' (S y), fun x : nat => match x with
                            | 0 => true
                            | S _ => false
                            end, fun x : nat => match x with
                                                | 0 => true
                                                | S _ => false
                                                end)" (cannot unify "e'" and
"fun x : nat => match x with
                | 0 => true
                | S _ => false
                end").
*)

[JasonGross]

Note that this can cause the pattern solution to be incorrect if there are other variables in the context which are assigned to terms which are headed by a constructor, because we may choose whether or not to match on them. (Consider x, y : bool |- ?e and x : bool |- ?e@{x:=x,y:=true} == x, we can solve this with either x or with if y then x else _, and the latter may be manded by a future unification problem.)

[herbelin]

This should be formulated clearly. It is among the variables, so the presence of true makes that it is not a pattern (see the Option.List.map in Evarsolve.is_unification_pattern_evar; the restriction to actual dependencies in get_actual_deps comes after).

[JasonGross]

This is only guaranteed to generate a good solution either (a) in the presence of eta conversion for the record type, or (b) when no subterm of the constructor tree, other than the leaves, occurs in the RHS. e.g., x, y, z |- ?e@{x:=(x,(y,z))} == (y,z) can be solved with either snd x or (fst (snd x), snd (snd x)).

[herbelin]

Right.

[JasonGross]

I think this should be subsumed by introducing constructors of types with eta. That is, if we have ?P t =?= u, we can always instantiate ?P with fun x => ?Q, turning the application into a substitution. And if we have fst ?x =?= u (or match ?x with pair x y => Q end =?= u) and primitive projections / eta are turned on, it should always be safe to instantiate ?x with (?a, ?b) (though we probably want to run canonical structures first, and we maybe want to make sure that u doesn't reduce to something that structurally matches such a projection/match, because otherwise we may forget information that we want to remember for first-order heuristics)

[JasonGross]

Oh, I see this is mentioned below

[JasonGross]

What does this mean? Or what's an example?

[JasonGross]

What's the difference between downwards and upwards here? (Or what's an example?)

[herbelin]

By downwards I mean the largest well-formed context which exclude the forbidden variables. By upwards, I mean the smallest well-formed context which include the allowed variables.

[JasonGross]

Hmmm, it seems that upwards is more powerful unless we have reduced enough that no further occurrences of forbidden variables can be erased by reduction. Consider T : Type, f : T -> Type, x : T |- ?e : Type, and the pair of problems A, B : Type, f : bool -> Type, x : bool |- ?e@{T:=(fun _ => bool) A,f:=f,x:=x} == ?e@{T:=(fun _ => bool) B,f:=f,x:=x} and f : bool -> Type, x : bool |- ?e@{T:=bool,f:=f,x:=x} == f x. IIUC, upwards closure would keep T, while downwards would remove it? (Do you have an example not involving reduction where they differ where upwards closure does better than downwards closure?)

[JasonGross]

But maybe this is what you meant by "erasable"?

[herbelin]

Thanks a lot for the review! I'll answer the remaining questions when I'll have more time.

[herbelin]

You're right, this should be distinct neutral, i.e. blocking on a variable, head normal forms. Current code is indeed wrong and should be modified.

[herbelin]

It seems I meant "If both instances are pointwise existential-variable-free compatible terms". So, with your previous remark, it should be "If both instances are pointwise existential-variable-free compatible neutral terms".

Your example works because e := fun x => match x with O => O is solved first. If you invert the order of unification problems:

Check let e := (fun x => ?[e]) in
      let f := ?[f] in
      eq_refl : (e O, e) = (e (S O), fun x => match x with O => O | S _ => f end).

it fails.

[herbelin]

This should be formulated clearly. It is among the variables, so the presence of true makes that it is not a pattern (see the Option.List.map in Evarsolve.is_unification_pattern_evar; the restriction to actual dependencies in get_actual_deps comes after).

[herbelin]

Right.

[herbelin]

By downwards I mean the largest well-formed context which exclude the forbidden variables. By upwards, I mean the smallest well-formed context which include the allowed variables.

[JasonGross]

Is this a performance optimization?