Fixing bug #2817 (occur check was not done up to instantiation of

known instances in unification.ml). This refines the fix to bug #1918.

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

4 files changed, 28 insertions, 4 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index ab676f0e9..d7fb3f63b 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -265,6 +265,7 @@ let destMeta c = match kind_of_term c with
   | _ -> invalid_arg "destMeta"
 
 let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false
+let isMetaOf mv c = match kind_of_term c with Meta mv' -> mv = mv' | _ -> false
 
 (* Destructs a variable *)
 let destVar c = match kind_of_term c with
diff --git a/kernel/term.mli b/kernel/term.mli
index e83be6d63..d826fb605 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -235,6 +235,7 @@ val isVarId : identifier -> constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
+val isMetaOf : metavariable -> constr -> bool
 val isEvar_or_Meta : constr -> bool
 val isSort : constr -> bool
 val isCast : constr -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d2f8ec232..4bf0928dc 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -39,6 +39,15 @@ let occur_meta_or_undefined_evar evd c =
     | _ -> iter_constr occrec c
   in try occrec c; false with Occur | Not_found -> true
 
+let occur_meta_evd sigma mv c =
+  let rec occrec c =
+    (* Note: evars are not instantiated by terms with metas *)
+    let c = whd_evar sigma (whd_meta sigma c) in
+    match kind_of_term c with
+    | Meta mv' when mv = mv' -> raise Occur
+    | _ -> iter_constr occrec c
+  in try occrec c; false with Occur -> true
+
 (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
    gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
 
@@ -388,7 +397,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
                check_compatibility curenv substn tyM tyN);
 	    if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst
 	    else sigma,(k2,cM,stM)::metasubst,evarsubst
-	| Meta k, _ when not (dependent cM cN) ->
+	| Meta k, _ ->
             if wt && flags.check_applied_meta_types then
               (let tyM = Typing.meta_type sigma k in
                let tyN = get_type_of curenv sigma cN in
@@ -401,7 +410,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	      (k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst,
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cN)
-	| _, Meta k when not (dependent cN cM) ->
+	| _, Meta k ->
             if wt && flags.check_applied_meta_types then
               (let tyM = get_type_of curenv sigma cM in
                let tyN = Typing.meta_type sigma k in
@@ -903,8 +912,13 @@ let w_merge env with_types flags (evd,metas,evars) =
 	    in
               w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns
     	  else
-	    let evd' = meta_assign mv (c,(status,TypeProcessed)) evd in
-	      w_merge_rec evd' (metas''@metas) evars'' eqns
+            let evd' =
+              if occur_meta_evd evd mv c then
+                if isMetaOf mv (whd_betadeltaiota env evd c) then evd
+                else error_cannot_unify env evd (mkMeta mv,c)
+              else
+	        meta_assign mv (c,(status,TypeProcessed)) evd in
+	    w_merge_rec evd' (metas''@metas) evars'' eqns
     | [] ->
 	(* Process type eqns *)
 	let rec process_eqns failures = function
diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v
new file mode 100644
index 000000000..25ac15574
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2817.v
@@ -0,0 +1,8 @@
+(** Occur-check for Meta (up to application of already known instances) *)
+
+Goal forall (f: nat -> nat -> Prop) (x:bool)
+  (H: forall  (u: nat), f u u -> True)
+  (H0: forall x0, f (if x then x0 else x0) x0),
+False.
+
+intros; apply H in H0. (* crashes *)