diff options
| -rw-r--r-- | pretyping/evarconv.ml | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3045.v | 34 |
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 [ [] ? ]. |