Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).

A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.

This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.

Thanks to Jason for helping in diagnosing the problem.

3 files changed, 48 insertions, 4 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6e4d72705b..ef3e53bf1f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -847,7 +847,7 @@ let subst_predicate (subst,copt) ccl tms =
     | Some c -> c::subst in
   substnl_predicate sigma 0 ccl tms
 
-let specialize_predicate_var (cur,typ,dep) tms ccl =
+let specialize_predicate_var (cur,typ,dep) env tms ccl =
   let c = match dep with
   | Anonymous -> None
   | Name _ -> Some cur
@@ -855,7 +855,9 @@ let specialize_predicate_var (cur,typ,dep) tms ccl =
   let l =
     match typ with
     | IsInd (_, IndType (_, _), []) -> []
-    | IsInd (_, IndType (_, realargs), names) -> realargs
+    | IsInd (_, IndType (indf, realargs), names) ->
+       let arsign,_ = get_arity env indf in
+       subst_of_rel_context_instance arsign realargs
     | NotInd _ -> [] in
   subst_predicate (l,c) ccl tms
 
@@ -1390,7 +1392,7 @@ and match_current pb (initial,tomatch) =
 and shift_problem ((current,t),_,na) pb =
   let ty = type_of_tomatch t in
   let tomatch = lift_tomatch_stack 1 pb.tomatch in
-  let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+  let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
   let pb =
     { pb with
        env = push_rel (LocalDef (na,current,ty)) pb.env;
@@ -1407,7 +1409,7 @@ and shift_problem ((current,t),_,na) pb =
    are already introduced in the context, we avoid creating aliases to
    themselves by treating this case specially. *)
 and pop_problem ((current,t),_,na) pb =
-  let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+  let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
   let pb =
     { pb with
        pred = pred;
diff --git a/test-suite/bugs/closed/5322.v b/test-suite/bugs/closed/5322.v
new file mode 100644
index 0000000000..01aec8f29b
--- /dev/null
+++ b/test-suite/bugs/closed/5322.v
@@ -0,0 +1,14 @@
+(* Regression in computing types of branches in "match" *)
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := a : op Unit Unit.
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2.
+  refine match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with
+         | _ => _
+         end.
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 3c696502cd..465b3eb8c0 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -41,6 +41,7 @@ Definition F (x:IND True) (A:Type) :=
 Theorem paradox : False.
   (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
 Fail Proof (F C False).
+Abort.
 
 (* Another bug found in November 2015 (a substitution was wrongly
    reversed at pretyping level) *)
@@ -61,3 +62,30 @@ Inductive Ind2 (b:=1) (c:nat) : Type :=
   Constr2 : Ind2 c.
 
 Eval vm_compute in Constr2 2.
+
+(* A bug introduced in ade2363 (similar to #5322 and #5324). This
+   commit started to see that some List.rev was wrong in the "var"
+   case of a pattern-matching problem but it failed to see that a
+   transformation from a list of arguments into a substitution was
+   still needed. *)
+
+(* The order of real arguments was made wrong by ade2363 in the "var"
+   case of the compilation of "match" *)
+
+Inductive IND2 : forall X Y:Type, Type :=
+  CONSTR2 : IND2 unit Empty_set.
+
+Check fun x:IND2 bool nat =>
+  match x in IND2 a b return a with
+  | y => _
+  end = true.
+
+(* From January 2017, using the proper function to turn arguments into
+   a substitution up to a context possibly containing let-ins, so that
+   the following, which was wrong also before ade2363, now works
+   correctly *)
+
+Check fun x:Ind bool nat =>
+  match x in Ind _ X Y Z return Z with
+  | y => (true,0)
+  end.