Fixing kernel bug in typing match with let-ins in the arity.

Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).

Fixing similar error in pretyping.

3 files changed, 26 insertions, 2 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 892557ac6c..939eeef5d5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -136,7 +136,7 @@ let betazeta_appvect n c v =
     if Int.equal n 0 then applist (substl env t, stack) else
     match kind_of_term t, stack with
         Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
-      | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+      | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
       | _ -> anomaly (Pp.str "Not enough lambda/let's") in
   stacklam n [] c (Array.to_list v)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 156c9a2772..bdd9ed81cf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1651,7 +1651,7 @@ let betazetaevar_applist sigma n c l =
     if Int.equal n 0 then applist (substl env t, stack) else
     match kind_of_term t, stack with
     | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
-    | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
     | Evar ev, _ ->
       (match safe_evar_value sigma ev with
       | Some body -> stacklam n env body stack
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index ce9050d421..8c8f02eccf 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -17,3 +17,27 @@ Definition foo (x : I') : bool :=
   match x with
   C' => true
   end.
+
+(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *)
+
+Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type :=
+  E2 : I2 A nat.
+
+Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with
+  E2 _ => (0,0,(0,0))
+  end.
+
+(* This used to succeed in 8.3, 8.4 and 8.5beta1 *)
+
+Inductive IND : forall X:Type, let Y:=X in Type :=
+  C : IND True.
+
+Definition F (x:IND True) (A:Type) :=
+  (* This failed in 8.5beta2 though it should have been accepted *)
+  match x in IND Y Z return Z with
+  C => I
+  end.
+
+Theorem paradox : False.
+  (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
+Fail Proof (F C False).