Bug 2733 : { } implicits and Fixpoints

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

2 files changed, 39 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v
new file mode 100644
index 0000000000..60c3719349
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2733.v
@@ -0,0 +1,24 @@
+Unset Asymmetric Patterns.
+
+Inductive ty := N | B.
+
+Inductive alt_list : ty -> ty -> Type :=
+  | nil {k} : alt_list k k
+  | Ncons {k} : nat -> alt_list B k -> alt_list N k
+  | Bcons {k} : bool -> alt_list N k -> alt_list B k.
+
+Definition trullynul k {k'} (l : alt_list k k') :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
+Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 ->
+alt_list t1 t3 :=
+  match l with
+  | nil => fun _ l2 => P l2
+  | Ncons n l1 => fun _ l2 => Ncons n (app (@P) l1 l2)
+  | Bcons b l1 => fun _ l2 => Bcons b (app (@P) l1 l2)
+  end.
+
+Check (fun {t t'} (l: alt_list t t') => app trullynul l nil).
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 13139557a5..9deaa270f5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -482,12 +482,12 @@ type structured_fixpoint_expr = {
 let interp_fix_context evdref env isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
   let impl_env, ((env', ctx), imps) = interp_context_evars evdref env before in
-  let _, ((env'', ctx'), imps') = interp_context_evars ~impl_env evdref env' after in
+  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env evdref env' after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
-    ((env'', ctx' @ ctx), imps @ imps', annot)
-      
-let interp_fix_ccl evdref (env,_) fix =
-  interp_type_evars evdref env fix.fix_type
+    ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
+
+let interp_fix_ccl evdref impls (env,_) fix =
+  interp_type_evars_impls ~impls ~evdref ~fail_evar:false env fix.fix_type
 
 let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
   Option.map (fun body ->
@@ -727,13 +727,17 @@ let interp_recursive isfix fixl notations =
 
   (* Interp arities allowing for unresolved types *)
   let evdref = ref Evd.empty in
-  let fixctxs, fiximps, fixannots =
+  let fixctxs, fiximppairs, fixannots =
     list_split3 (List.map (interp_fix_context evdref env isfix) fixl) in
-  let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
+  let fixctximpenvs, fixctximps = List.split fiximppairs in
+  let fixccls,fixcclimps = List.split (list_map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (nf_evar !evdref) fixtypes in
+  let fiximps = list_map3
+    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps))
+    fixctximps fixcclimps fixctxs in
   let rec_sign =
-    List.fold_left2 
+    List.fold_left2
       (fun env' id t ->
 	 if Flags.is_program_mode () then
 	   let sort = Retyping.get_type_of env !evdref t in
@@ -754,7 +758,9 @@ let interp_recursive isfix fixl notations =
   let fixdefs =
     Metasyntax.with_syntax_protection (fun () ->
       List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
-      list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
+      list_map4
+	(fun fixctximpenv -> interp_fix_body evdref env_rec (Idmap.fold Idmap.add fixctximpenv impls))
+	fixctximpenvs fixctxs fixl fixccls)
       () in
 
   (* Instantiate evars and check all are resolved *)