Fixing #4001 (missing type constraints when building return clause of match).

2 files changed, 22 insertions, 2 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fdb19d3780..7c3165fa8e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1644,7 +1644,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
   in
   aux (0,extenv,subst0) t0
 
-let build_tycon loc env tycon_env subst tycon extenv evdref t =
+let build_tycon loc env tycon_env s subst tycon extenv evdref t =
   let t,tt = match t with
     | None ->
 	(* This is the situation we are building a return predicate and
@@ -1659,6 +1659,8 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
         let evd,tt = Typing.e_type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
+  let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
+  if not b then anomaly (Pp.str "Build_tycon: should be a type");
   { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -1780,7 +1782,7 @@ let build_inversion_problem loc env sigma tms t =
       mat       = [eqn1;eqn2];
       caseloc   = loc;
       casestyle = RegularStyle;
-      typing_function = build_tycon loc env pb_env subst} in
+      typing_function = build_tycon loc env pb_env s subst} in
   let pred = (compile pb).uj_val in
   (!evdref,pred)
 
diff --git a/test-suite/bugs/closed/4001.v b/test-suite/bugs/closed/4001.v
new file mode 100644
index 0000000000..25d78f4b0e
--- /dev/null
+++ b/test-suite/bugs/closed/4001.v
@@ -0,0 +1,18 @@
+(* Computing the type constraints to be satisfied when building the
+   return clause of a match with a match *)
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+  
+Variable A : Type.
+Variable typ : A -> Type.
+
+Inductive t : list A -> Type :=
+| snil  : t nil
+| scons : forall (x : A) (e : typ x) (lx : list A) (le : t  lx), t (x::lx).
+
+Definition car (x:A) (lx : list A) (s: t (x::lx)) : typ x :=
+  match s in t l'  with
+  | snil => False
+  | scons _ e _ _ => e
+  end.