Univs: fix bug #4161.

Retypecheck abstracted infered predicate to register the right
universe constraints.

2 files changed, 43 insertions, 16 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 05e09b968..2a4be9f31 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1865,7 +1865,14 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
-let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
+let context_of_arsign l =
+  let (x, _) = List.fold_right
+    (fun c (x, n) ->
+       (lift_rel_context n c @ x, List.length c + n))
+    l ([], 0)
+  in x
+
+let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
   let subst, len =
     List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
@@ -1905,7 +1912,9 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
 	      mkRel (n + nar))
       | _ ->
 	  map_constr_with_binders succ predicate lift c
-  in predicate 0 c
+  in
+  let p = predicate 0 c in
+  fst (Typing.type_of (push_rel_context (context_of_arsign arsign) env) sigma p), p
 
 
 (* Builds the predicate. If the predicate is dependent, its context is
@@ -1927,11 +1936,11 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
 	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let pred1 =
-          prepare_predicate_from_arsign_tycon loc tomatchs arsign t in
+        let sigma1,pred1 =
+          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
-	[sigma, pred1; sigma2, pred2]
+	[sigma1, pred1; sigma2, pred2]
     | None, _ ->
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
@@ -2366,13 +2375,6 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
     assert(Int.equal slift 0); (* we must have folded over all elements of the arity signature *)
     arsign'', allnames, nar, eqs, neqs, refls
 
-let context_of_arsign l =
-  let (x, _) = List.fold_right
-    (fun c (x, n) ->
-       (lift_rel_context n c @ x, List.length c + n))
-    l ([], 0)
-  in x
-
 let compile_program_cases loc style (typing_function, evdref) tycon env
     (predopt, tomatchl, eqns) =
   let typing_fun tycon env = function
@@ -2404,10 +2406,8 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
     | Some t ->
 	let pred = 
 	  try
-	    let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in
-	      (* The tycon may be ill-typed after abstraction. *)
-	    let env' = push_rel_context (context_of_arsign sign) env in
-	      ignore(Typing.sort_of env' evdref pred); pred
+	    let evd, pred = prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t in
+	      evdref := evd; pred
 	  with e when Errors.noncritical e ->
 	    let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
 	      lift nar t
diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v
new file mode 100644
index 000000000..aa2b189b6
--- /dev/null
+++ b/test-suite/bugs/closed/4161.v
@@ -0,0 +1,27 @@
+
+    (* Inductive t : Type -> Type := *)
+    (* | Just : forall (A : Type), t A -> t A. *)
+
+    (* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *)
+    (*   match x in t A return t (A + unit) with *)
+    (*   | Just T x => @test T x *)
+    (*   end. *)
+
+
+    Definition Type1 := Type.
+Definition Type2 := Type.
+Definition cast (x:Type2) := x:Type1.
+Axiom f: Type2 -> Prop.
+Definition A :=
+ let T := fun A:Type1 => _ in
+ fun A':Type2 =>
+ eq_refl : T A' = f A' :> Prop.
+(* Type2 <= Type1... f A -> Type1 <= Type2 *)
+
+Inductive t : Type -> Type :=
+    | Just : forall (A : Type), t A -> t A.
+
+Fixpoint test {A : Type} (x : t A) : t (A + unit) :=
+  match x in t A with
+  | Just B x => @test B x
+  end.
\ No newline at end of file