- Fixes for canonical structure resolution (check that the initial term indeed unifies

with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.

10 files changed, 58 insertions, 35 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 63b54581a..e24c18ae2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -127,7 +127,7 @@ let check_conv_record (t1,sk1) (t2,sk2) =
     with Not_found ->
       lookup_canonical_conversion (proji,Default_cs),[]
   in
-  let { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
+  let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
         o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
   let params1, c1, extra_args1 =
     match arg with
@@ -145,8 +145,10 @@ let check_conv_record (t1,sk1) (t2,sk2) =
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
   let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
   let c' = subst_univs_level_constr subst c in
+  let t' = subst_univs_level_constr subst t' in
   let bs' = List.map (subst_univs_level_constr subst) bs in
-    ctx',c',bs',(Stack.append_app_list params Stack.empty,params1),(Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
+    ctx',t',c',bs',(Stack.append_app_list params Stack.empty,params1),
+    (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
     (n,Stack.zip(t2,sk2))
 
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
@@ -666,21 +668,26 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
       end
 
-and conv_record trs env evd (ctx,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+and conv_record trs env evd (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
   if Reductionops.Stack.compare_shape ts ts1 then
-    let (evd',ks,_) =
+    let (evd',ks,_,test) =
       List.fold_left
-	(fun (i,ks,m) b ->
-	  if Int.equal m n then (i,t2::ks, m-1) else
+	(fun (i,ks,m,test) b ->
+	  if Int.equal m n then 
+	    let ty = Retyping.get_type_of env i t2 in
+	    let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
+	      (i,t2::ks, m-1, test)
+	  else
 	    let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
             let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
-	    (i', ev :: ks, m - 1))
-	(evd,[],List.length bs - 1) bs
+	    (i', ev :: ks, m - 1,test))
+	(evd,[],List.length bs - 1,fun i -> Success i) bs
     in
     let app = mkApp (c, Array.rev_of_list ks) in
     ise_and evd'
-      [(fun i ->
+      [test;
+       (fun i ->
 	exact_ise_stack2 env i
           (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x))
           params1 params);
@@ -689,7 +696,8 @@ and conv_record trs env evd (ctx,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t
            (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u))
            us2 us);
        (fun i -> evar_conv_x trs env i CONV c1 app);
-       (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1)]
+       (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1);
+       (fun i -> evar_conv_x trs env i CONV (substl ks t) t2)]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index c99929b5e..aa45b5ef1 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -43,7 +43,7 @@ val check_problems_are_solved : env -> evar_map -> unit
 (** Check if a canonical structure is applicable *)
 
 val check_conv_record : constr * types Stack.t -> constr * types Stack.t ->
-  Univ.universe_context_set * constr * constr list * (constr Stack.t * constr Stack.t) *
+  Univ.universe_context_set * constr * constr * constr list * (constr Stack.t * constr Stack.t) *
     (constr Stack.t * types Stack.t) *
     (constr Stack.t * types Stack.t) * constr *
     (int * constr)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 306116d76..761f11c11 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -30,8 +30,8 @@ let refresh_universes dir evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh t = match kind_of_term t with
-    | Sort (Type u as s) when Univ.universe_level u = None ||
-			   Evd.is_sort_variable evd s = None ->
+    | Sort (Type u as s) when Univ.universe_level u = None
+			 (* || Evd.is_sort_variable evd s = None *) ->
       (modified := true;
        (* s' will appear in the term, it can't be algebraic *)
        let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d18568500..166bab4b8 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -390,19 +390,20 @@ let process_universe_constraints univs vars alg local cstrs =
 		  instantiate_variable l' (Univ.Universe.make r') vars
 		else if rloc then 
 		  instantiate_variable r' (Univ.Universe.make l') vars
-		else 
-		  (* Two rigid/global levels, one of them being Prop/Set, disallow *)
-		  (* if Univ.is_small_univ l' || Univ.is_small_univ r' then *)
-		  (*   raise UniversesDiffer *)
-		  (* else *)
-		  if fo then 
-		    if not (Univ.check_eq univs l r) then 
+		else if not (Univ.check_eq univs l r) then
+		  (* Two rigid/global levels, none of them being local,
+		     one of them being Prop/Set, disallow *)
+		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
+		    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, []))
+		  else
+		    if fo then 
 		      raise UniversesDiffer
 	      in
 	        Univ.enforce_eq_level l' r' local
            | _, _ (* One of the two is algebraic or global *) -> 
 	     if Univ.check_eq univs l r then local
-	     else raise UniversesDiffer
+	     else 
+	       raise UniversesDiffer
   in
   let local = 
     Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 967583a2b..7250217d6 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -160,12 +160,17 @@ let eq_cs_pattern p1 p2 = match p1, p2 with
 | Default_cs, Default_cs -> true
 | _ -> false
 
+let rec assoc_pat a = function
+  | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs
+  | [] -> raise Not_found
+
+
 let object_table =
-  Summary.ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t)
+  Summary.ref (Refmap.empty : ((cs_pattern * constr) * obj_typ) list Refmap.t)
     ~name:"record-canonical-structs"
 
 let canonical_projections () =
-  Refmap.fold (fun x -> List.fold_right (fun (y,c) acc -> ((x,y),c)::acc))
+  Refmap.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
     !object_table []
 
 let keep_true_projections projs kinds =
@@ -212,7 +217,7 @@ let compute_canonical_projections (con,ind) =
 	       begin
 		 try
 		   let patt, n , args = cs_pattern_of_constr t in
-		     ((ConstRef proji_sp, patt, n, args) :: l)
+		     ((ConstRef proji_sp, patt, t, n, args) :: l)
 		 with Not_found ->
                    if Flags.is_verbose () then
                      (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
@@ -224,8 +229,8 @@ let compute_canonical_projections (con,ind) =
 	       end
 	   | _ -> l)
       [] lps in
-  List.map (fun (refi,c,inj,argj) ->
-    (refi,c),
+  List.map (fun (refi,c,t,inj,argj) ->
+    (refi,(c,t)),
     {o_DEF=v; o_CTX=ctx; o_INJ=inj; o_TABS=lt;
      o_TPARAMS=params; o_NPARAMS=List.length params; o_TCOMPS=argj})
     comp
@@ -236,16 +241,18 @@ let pr_cs_pattern = function
   | Default_cs -> str "_"
   | Sort_cs s -> Termops.pr_sort_family s
 
+let pr_pattern (p,c) = pr_cs_pattern p
+
 let open_canonical_structure i (_,o) =
   if Int.equal i 1 then
     let lo = compute_canonical_projections o in
-    List.iter (fun ((proj,cs_pat),s) ->
+    List.iter (fun ((proj,(cs_pat,_ as pat)),s) ->
       let l = try Refmap.find proj !object_table with Not_found -> [] in
-      let ocs = try Some (List.assoc_f eq_cs_pattern cs_pat l)
+      let ocs = try Some (assoc_pat cs_pat l)
       with Not_found -> None
       in match ocs with
-        | None -> object_table := Refmap.add proj ((cs_pat,s)::l) !object_table;
-        | Some cs ->
+        | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
+        | Some (c, cs) ->
             if Flags.is_verbose () then
               let old_can_s = (Termops.print_constr cs.o_DEF)
               and new_can_s = (Termops.print_constr s.o_DEF) in
@@ -309,7 +316,7 @@ let declare_canonical_structure ref =
   add_canonical_structure (check_and_decompose_canonical_structure ref)
 
 let lookup_canonical_conversion (proj,pat) =
-  List.assoc_f eq_cs_pattern pat (Refmap.find proj !object_table)
+  assoc_pat pat (Refmap.find proj !object_table)
 
   (* let cst, u' = destConst cs.o_DEF in *)
   (*   { cs with o_DEF = mkConstU (cst, u) } *)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index b1763a359..4a03d9bc5 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -66,7 +66,7 @@ type obj_typ = {
 val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
 val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 
-val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
+val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
 val declare_canonical_structure : global_reference -> unit
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> (constr * constr Reductionops.Stack.t) -> bool
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b64156649..7022946e5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1024,6 +1024,7 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
     | Reduction.CUMUL -> Reduction.trans_conv_leq_universes in
     try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true
     with Reduction.NotConvertible -> false
+    | Univ.UniverseInconsistency _ -> false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
 let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
@@ -1034,6 +1035,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
       let cstrs = f ~evars:(safe_evar_value sigma) ~ts env (Evd.universes sigma) x y in
 	Evd.add_constraints sigma cstrs, true
     with Reduction.NotConvertible -> sigma, false
+    | Univ.UniverseInconsistency _ -> sigma, false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
     
 (********************************************************************)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0ab886ca3..b1b2bc05b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -706,7 +706,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 
   and solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 (sigma,ms,es) =
-    let (ctx,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+    let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
       try Evarconv.check_conv_record f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
@@ -730,6 +730,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 			   substn params1 params in
       let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb b false) substn ts ts1 in
       let app = mkApp (c, Array.rev_of_list ks) in
+      (* let substn = unirec_rec curenvnb pb b false substn t cN in *)
 	unirec_rec curenvnb pb b false substn c1 app
       with Invalid_argument "Reductionops.Stack.fold2" ->
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 112402bca..6873bbb11 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -107,8 +107,11 @@ let fail_quick_unif_flags = {
 let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
   let env = pf_env gls in
   let evd = create_goal_evar_defs (project gls) in
-  let evd' = w_unify env evd CONV ~flags m n in
-  tclIDTAC {it = gls.it; sigma =  evd'; }
+    try 
+      let evd' = w_unify env evd CONV ~flags m n in
+	tclIDTAC {it = gls.it; sigma =  evd'; }
+    with e when Errors.noncritical e ->
+      tclFAIL 0 (Errors.print e) gls
 
 let unify ?(flags=fail_quick_unif_flags) m gls =
   let n = pf_concl gls in unifyTerms ~flags m n gls
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index ccce3bbe1..1ed2221cc 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -23,6 +23,7 @@ Function ftest (n m : nat) : nat :=
          end
   | S p => 0
   end.
+(* MS: FIXME: apparently can't define R_ftest_complete *)
 
 Lemma test1 : forall n m : nat, ftest n m <= 2.
 intros n m.