Fix bug rocq-prover#4101, noccur_evar's expand_projection can legitimately fail

when called from w_unify, so we protect it.

Author: mattam82

pretyping/evarsolve.ml

@@ -192,7 +192,13 @@ let noccur_evar env evd evk c =
       (match pi2 (Environ.lookup_rel i env) with
        | None -> ()
        | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
-  | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c [])
+  | Proj (p,c) -> 
+    let c = 
+      try Retyping.expand_projection env evd p c []
+      with Retyping.RetypeError _ -> 
+	(* Can happen when called from w_unify which doesn't assign evars/metas 
+	   eagerly enough *) c
+    in occur_rec acc c
   | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
     occur_rec acc c
   in

test-suite/bugs/closed/4101.v

@@ -0,0 +1,19 @@
+(* File reduced by coq-bug-finder from original input, then from 10940 lines to 152 lines, then from 509 lines to 163 lines, then from 178 lines to 66 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 2 2015 18:53:10 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (e77f178e60918f14eacd1ec0364a491d4cfd0f3f) *)
+
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x),
+                      (forall x, f x = g x) -> f = g.
+Lemma sigT_obj_eq
+: forall (T : Type) (T0 : T -> Type)
+         (s s0 : forall s : sigT T0,
+                   sigT (fun _ : T0 (projT1 s) => unit) ->
+                   sigT (fun _ : T0 (projT1 s) => unit)),
+   s0 = s.
+Proof.
+  intros.
+  Set Debug Tactic Unification.
+  apply path_forall.