Fixing the anomaly in bug #3045 (a filter was not type-safe in

2nd-order matching).

We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is
well-typed when taking the filtered context Gamma) in 2nd order
matching. Maybe this weakens the power of the 2nd order matching
algorithm, so it is not clear that it is the good fix.

Another fix could have been to ensure that taking the closure of
filter does not extend it beyond the original filter (hence keeping
the filter untyped if it was already untyped).

As for the bug #3045, it also revealed that some "destruct c as [[]]"
could be made stronger as decomposing the destruct in two parts
"destruct c as [x]; destruct x" workis while it currently fails if in
one part.

2 files changed, 39 insertions, 2 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6946279838..19e405b80d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -838,8 +838,11 @@ let apply_on_subterm env evdref f c t =
   applyrec (env,(0,c)) t
 
 let filter_possible_projections c ty ctxt args =
-  let fv1 = free_rels c in
-  let fv2 = collect_vars c in
+  (* Since args in the types will be replaced by holes, we count the
+     fv of args to have a well-typed filter; don't know how necessary
+     it is however to have a well-typed filter here *)
+  let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in
+  let fv2 = collect_vars (mkApp (c,args)) in
   let len = Array.length args in
   let tyvars = collect_vars ty in
   List.map_i (fun i (id,b,_) ->
diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v
new file mode 100644
index 0000000000..ef110ad0d0
--- /dev/null
+++ b/test-suite/bugs/closed/3045.v
@@ -0,0 +1,34 @@
+
+Set Asymmetric Patterns.
+Generalizable All Variables.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type;
+
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+  }.
+
+Arguments Compose {obj} [C s d d'] m1 m2 : rename.
+
+Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
+| ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'.
+
+Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d :=
+  match m in @ReifiedMorphism objC C s d return Morphism C s d with
+    | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
+                                                         (@ReifiedMorphismDenote _ _ _ _ m2)
+  end.
+
+Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d)
+: { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }.
+refine match m with
+         | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _
+       end; clear m.
+(* This fails with an error rather than an anomaly, but morally 
+   it should work, if destruct were able to do the good generalization
+   in advance, before doing the "intros []". *)
+Fail destruct (@ReifiedMorphismSimplifyWithProof T s1 d0 d0' m1) as [ [] ? ].