unification unsoundly discards context variables in substitutions

[JasonGross]

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).
*)

Originally posted by @JasonGross in coq/ceps#59 (comment)

[herbelin]

You're right, only dependences in incompatible "neutral terms" could be discarded.