Fixing #2836 (materialize_evar might refine as a side effect the

current evar to project; this may happen if this evar is dependent and
is involved in evar-evar conversion problem eventually solved by
instantiating the current evar; could maybe be optimized when the evar
to materialize has invertible instance in which case
define_evar_from_virtual_equation applied on the current evar could be
shortcut, avoiding to create an evar).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 46 insertions, 0 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 036bed5252..a2c63982bc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -146,6 +146,11 @@ let noccur_evar evd evk c =
   in
   try occur_rec c; true with Occur -> false
 
+let normalize_evar evd ev =
+  match kind_of_term (whd_evar evd (mkEvar ev)) with
+  | Evar (evk,args) -> (evk,args)
+  | _ -> assert false
+
 (**********************)
 (* Creating new metas *)
 (**********************)
@@ -1591,6 +1596,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
 	  let ty = get_type_of env' !evdref t in
 	  let (evd,evar'',ev'') =
              materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+          (* materialize_evar may instantiate ev' by another evar; adjust it *)
+          let (evk',args' as ev') = normalize_evar evd ev' in
 	  let evd =
 	     (* Try to project (a restriction of) the left evar ... *)
 	    try
diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/shouldsucceed/2836.v
new file mode 100644
index 0000000000..a948b75e27
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2836.v
@@ -0,0 +1,39 @@
+(* Check that possible instantiation made during evar materialization
+   are taken into account and do not raise Not_found *)
+
+Set Implicit Arguments.
+
+Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := {
+  Object :> _ := obj;
+
+  Identity' : forall o, Morphism o o;
+  Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+}.
+
+Section SpecializedCategoryInterface.
+  Variable obj : Type.
+  Variable mor : obj -> obj -> Type.
+  Variable C : @SpecializedCategory obj mor.
+
+  Definition Morphism (s d : C) := mor s d.
+  Definition Identity (o : C) : Morphism o o := C.(Identity') o.
+  Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) :
+Morphism s d' := C.(Compose') s d d' m m0.
+End SpecializedCategoryInterface.
+
+Section ProductCategory.
+  Variable objC : Type.
+  Variable morC : objC -> objC -> Type.
+  Variable objD : Type.
+  Variable morD : objD -> objD -> Type.
+  Variable C : SpecializedCategory morC.
+  Variable D : SpecializedCategory morD.
+
+(* Should fail nicely *)
+Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d
+=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type).
+Fail refine {|
+      Identity' := (fun o => (Identity (fst o), Identity (snd o)));
+      Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd
+m2) (snd m1)))
+    |}.