Merge PR#567: Fix bug #5377: @? patterns broken.

2 files changed, 113 insertions, 19 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 886a982634..3c47cfdc4b 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -80,31 +80,71 @@ let add_binders na1 na2 binding_vars (names, terms as subst) =
 
 let rec build_lambda vars ctx m = match vars with
 | [] ->
-  let len = List.length ctx in
-  lift (-1 * len) m
+  if Vars.closed0 m then m else raise PatternMatchingFailure
 | n :: vars ->
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
   let len = List.length ctx in
-  let init i =
-    if i < pred n then mkRel (i + 2)
-    else if Int.equal i (pred n) then mkRel 1
-    else mkRel (i + 1)
-  in
-  let m = substl (List.init len init) m in
   let pre, suf = List.chop (pred n) ctx in
-  match suf with
+  let (na, t, suf) = match suf with
   | [] -> assert false
-  | (_, na, t) :: suf ->
-    let map i = if i > n then pred i else i in
-    let vars = List.map map vars in
-    (** Check that the abstraction is legal *)
-    let frels = free_rels t in
-    let brels = List.fold_right Int.Set.add vars Int.Set.empty in
-    let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in
-    (** Create the abstraction *)
-    let m = mkLambda (na, t, m) in
-    build_lambda vars (pre @ suf) m
+  | (_, na, t) :: suf -> (na, t, suf)
+  in
+  (** Check that the abstraction is legal by generating a transitive closure of
+      its dependencies. *)
+  let is_nondep t clear = match clear with
+  | [] -> true
+  | _ ->
+    let rels = free_rels t in
+    let check i b = b || not (Int.Set.mem i rels) in
+    List.for_all_i check 1 clear
+  in
+  let fold (_, _, t) clear = is_nondep t clear :: clear in
+  (** Produce a list of booleans: true iff we keep the hypothesis *)
+  let clear = List.fold_right fold pre [false] in
+  let clear = List.drop_last clear in
+  (** If the conclusion depends on a variable we cleared, failure *)
+  let () = if not (is_nondep m clear) then raise PatternMatchingFailure in
+  (** Create the abstracted term *)
+  let fold (k, accu) keep =
+    if keep then
+      let k = succ k in
+      (k, Some k :: accu)
+    else (k, None :: accu)
+  in
+  let keep, shift = List.fold_left fold (0, []) clear in
+  let shift = List.rev shift in
+  let map = function
+  | None -> mkProp (** dummy term *)
+  | Some i -> mkRel (i + 1)
+  in
+  (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *)
+  let subst =
+    List.map map shift @
+    mkRel 1 ::
+    List.mapi (fun i _ -> mkRel (i + keep + 2)) suf
+  in
+  let map i (id, na, c) =
+    let i = succ i in
+    let subst = List.skipn i subst in
+    let subst = List.map (fun c -> Vars.lift (- i) c) subst in
+    (id, na, substl subst c)
+  in
+  let pre = List.mapi map pre in
+  let pre = List.filter_with clear pre in
+  let m = substl subst m in
+  let map i =
+    if i > n then i - n + keep
+    else match List.nth shift (i - 1) with
+    | None ->
+      (** We cleared a variable that we wanted to abstract! *)
+      raise PatternMatchingFailure
+    | Some k -> k
+  in
+  let vars = List.map map vars in
+  (** Create the abstraction *)
+  let m = mkLambda (na, Vars.lift keep t, m) in
+  build_lambda vars (pre @ suf) m
 
 let rec extract_bound_aux k accu frels ctx = match ctx with
 | [] -> accu
diff --git a/test-suite/bugs/closed/5377.v b/test-suite/bugs/closed/5377.v
new file mode 100644
index 0000000000..130d9f9abf
--- /dev/null
+++ b/test-suite/bugs/closed/5377.v
@@ -0,0 +1,54 @@
+Goal ((forall (t : Type) (x y : t),
+          True ->
+          x = y)) -> False.
+Proof.
+  intro HG.
+  let P := lazymatch goal with
+  | [ H : forall t x y, True -> @?P t x y
+                        |- _ ]
+    => P
+  end in
+  pose (f := P).
+  unify f (fun (t : Type) (x y : t) => x = y).
+Abort.
+
+Goal True.
+Proof.
+let c := lazymatch constr:(fun (T : nat -> Type) (y : nat) (_ : T y) => y) with
+         | fun _ y _ => @?C y => C
+         end in
+pose (f := c).
+unify f (fun n : nat => n).
+Abort.
+
+Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
+Proof.
+intro.
+let P := lazymatch goal with
+| [ H : forall y, @?P y -> @?P y \/ _ |- _ ]
+  => P
+end in
+pose (f := P).
+unify f (fun x : nat => x = x).
+Abort.
+
+Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
+Proof.
+intro.
+lazymatch goal with
+| [ H : forall y, @?P y -> @?Q y \/ _ |- _ ]
+  => idtac
+end.
+Abort.
+
+Axiom eq : forall {T} (_ : T), Prop.
+
+Goal forall _ : (forall t (_ : eq t) (x : t), eq x), Prop.
+Proof.
+intro.
+let P := lazymatch goal with
+| [ H : forall t _ x, @?P t x |- _ ]
+  => P
+end in
+pose (f := P).
+Abort.