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.

1 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v
new file mode 100644
index 000000000..ef110ad0d
--- /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 [ [] ? ].