Improved check is_open_canonical_projection

The check looks for 1 canonical projection applied to a meta/evar.
This fails to deal with telescopes that generate unification problems
containing something like "(pi_1 (pi_2 ?))" that is indeed a "stuck"
canonical projection but not of the form recognized by the previous
implementation. The same holds when pi_2 is a general function not
producing a constructor.

This patch checks if the argument of the canonical projection weak head
reduces to a constructor calling whd_betadeltaiota.

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

5 files changed, 23 insertions, 7 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 236bc1b43c..47822b22e0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -324,7 +324,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
              if the first argument is a beta-redex (expand a constant
              only if necessary) or the second argument is potentially
              usable as a canonical projection *)
-	  if isLambda flex1 or is_open_canonical_projection i appr2
+	  if isLambda flex1 or is_open_canonical_projection env i appr2
 	  then
 	    match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 994fe33d09..b3be7afd99 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -336,10 +336,14 @@ let declare_canonical_structure ref =
 let lookup_canonical_conversion (proj,pat) =
   List.assoc pat (Refmap.find proj !object_table)
 
-let is_open_canonical_projection sigma (c,args) =
+let is_open_canonical_projection env sigma (c,args) =
   try
-    let n = find_projection_nparams (global_of_constr c) in                                                           
-    try isEvar_or_Meta (whd_evar sigma (List.nth args n)) with Failure _ -> false
+    let n = find_projection_nparams (global_of_constr c) in
+    try
+      let arg = whd_betadeltaiota env sigma (List.nth args n) in
+      let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in
+      not (isConstruct hd) 
+    with Failure _ -> false
   with Not_found -> false
 
 let freeze () =
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index b4e76756bb..6165fac266 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -80,6 +80,6 @@ val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
 val declare_canonical_structure : global_reference -> unit
 val is_open_canonical_projection :
-  Evd.evar_map -> (constr * constr list) -> bool
+  Environ.env -> Evd.evar_map -> (constr * constr list) -> bool
 val canonical_projections : unit ->
   ((global_reference * cs_pattern) * obj_typ) list
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6fff81cfe6..693ea43957 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -560,7 +560,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
     let f1 () =
       if isApp cM then
 	let f1l1 = decompose_app cM in
-	  if is_open_canonical_projection sigma f1l1 then
+	  if is_open_canonical_projection env sigma f1l1 then
 	    let f2l2 = decompose_app cN in
 	      solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 substn
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -573,7 +573,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	try f1 () with e when precatchable_exception e ->
 	  if isApp cN then
 	    let f2l2 = decompose_app cN in
-	      if is_open_canonical_projection sigma f2l2 then
+	      if is_open_canonical_projection env sigma f2l2 then
 		let f1l1 = decompose_app cM in
 		  solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn
 	      else error_cannot_unify (fst curenvnb) sigma (cM,cN)
diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v
new file mode 100644
index 0000000000..8a607c936d
--- /dev/null
+++ b/test-suite/success/telescope_canonical.v
@@ -0,0 +1,12 @@
+Structure Inner := mkI { is :> Type }.
+Structure Outer := mkO { os :> Inner }.
+
+Canonical Structure natInner := mkI nat.
+Canonical Structure natOuter := mkO natInner.
+
+Definition hidden_nat := nat.
+
+Axiom P : forall S : Outer, is (os S) -> Prop.
+
+Lemma foo (n : hidden_nat) : P _ n.
+Admitted.