Do not rely on Reductionops to recognize canonical projections.

No need to call the whole whd_gen machinery when a simple matching over
a term would suffice.

Note that this changes a bit the semantics, but I suspect that the previous
code was buggy. Indeed, whd_nored also pushes cases and fixpoints on the
stack, so that an applied canonical projection inside such a context would
also match. But the caller in unification performs an approximate check where
the term needs to be an application or a projection, which would prevent
such complex situations most of the time, e.g. it would work with a dummy
commutative cut but not their corresponding vanilla match.

3 files changed, 22 insertions, 15 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b6e44265ae..aa862a912e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -323,23 +323,32 @@ let check_and_decompose_canonical_structure env sigma ref =
 let lookup_canonical_conversion env (proj,pat) =
   assoc_pat env pat (GlobRef.Map.find proj !object_table)
 
-let decompose_projection sigma c args =
+let rec get_nth n = function
+| [] -> raise Not_found
+| arg :: args ->
+  let len = Array.length arg in
+  if n < len then arg.(n)
+  else get_nth (n - len) args
+
+let rec decompose_projection sigma c args =
   match EConstr.kind sigma c with
+  | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args
+  | Cast (c, _, _) -> decompose_projection sigma c args
+  | App (c, arg) -> decompose_projection sigma c (arg :: args)
   | Const (c, u) ->
      let n = find_projection_nparams (GlobRef.ConstRef c) in
      (* Check if there is some canonical projection attached to this structure *)
      let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
-     let arg = Stack.nth args n in
-     arg
+     get_nth n args
   | Proj (p, c) ->
      let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in
      c
   | _ -> raise Not_found
 
-let is_open_canonical_projection env sigma (c,args) =
+let is_open_canonical_projection env sigma c =
   let open EConstr in
   try
-    let arg = decompose_projection sigma c args in
+    let arg = decompose_projection sigma c [] in
     try
       let arg = whd_all env sigma arg in
       let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5b8dc8184a..83927085e9 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -94,7 +94,7 @@ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
   cs -> unit
 val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
 val is_open_canonical_projection :
-  Environ.env -> Evd.evar_map -> Reductionops.state -> bool
+  Environ.env -> Evd.evar_map -> EConstr.t -> bool
 val canonical_projections : unit ->
   ((GlobRef.t * cs_pattern) * obj_typ) list
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1c24578a1c..3d3010d1a4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1070,10 +1070,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp_or_Proj sigma cM then
-        let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in
-          if is_open_canonical_projection curenv sigma f1l1 then
-            let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in
-              solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
+          if is_open_canonical_projection curenv sigma cM then
+            solve_canonical_projection curenvnb pb opt cM cN substn
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
@@ -1086,14 +1084,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       else
         try f1 () with e when precatchable_exception e ->
           if isApp_or_Proj sigma cN then
-            let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in
-              if is_open_canonical_projection curenv sigma f2l2 then
-                let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in
-                  solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
+              if is_open_canonical_projection curenv sigma cN then
+                solve_canonical_projection curenvnb pb opt cN cM substn
               else error_cannot_unify (fst curenvnb) sigma (cM,cN)
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 
-  and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
+  and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) =
+    let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in
+    let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in
     let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
       try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)