diff options
Diffstat (limited to 'test-suite/bugs/closed/3045.v')
-rw-r--r-- | test-suite/bugs/closed/3045.v | 34 |
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 00000000..ef110ad0 --- /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 [ [] ? ]. |