Fix #13330: Kernel messes with polymorphic side-effects.

Polymorphic side-effects generated in monomorphic mode would be counted towards
trusted subcomponents. This would allow to make ill-typed terms pass as
legitimate by mimicking the shape of the inlining of monomorphic side-effects in
such a proof.

2 files changed, 22 insertions, 5 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index bf02ceb2c2..6abd283f6c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -671,7 +671,7 @@ let inline_side_effects env body side_eff =
   let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in
   let side_eff = List.rev side_eff in
   (** Most recent side-effects first in side_eff *)
-  if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs)
+  if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs, 0)
   else
     (** Second step: compute the lifts and substitutions to apply *)
     let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in
@@ -725,10 +725,10 @@ let inline_side_effects env body side_eff =
       else mkLetIn (na, b, ty, accu)
     in
     let body = List.fold_right fold_arg args body in
-    (body, ctx, sigs)
+    (body, ctx, sigs, len - 1)
 
 let inline_private_constants env ((body, ctx), side_eff) =
-  let body, ctx',_ = inline_side_effects env body side_eff in
+  let body, ctx', _, _ = inline_side_effects env body side_eff in
   let ctx' = Univ.ContextSet.union ctx ctx' in
   (body, ctx')
 
@@ -880,11 +880,11 @@ let add_constant l decl senv =
       match decl with
       | OpaqueEntry ce ->
         let handle env body eff =
-          let body, uctx, signatures = inline_side_effects env body eff in
+          let body, uctx, signatures, skip = inline_side_effects env body eff in
           let trusted = check_signatures senv signatures in
           let trusted, uctx = match trusted with
           | None -> 0, uctx
-          | Some univs -> List.length signatures, Univ.ContextSet.union univs uctx
+          | Some univs -> skip, Univ.ContextSet.union univs uctx
           in
           body, uctx, trusted
         in
diff --git a/test-suite/bugs/closed/bug_13330.v b/test-suite/bugs/closed/bug_13330.v
new file mode 100644
index 0000000000..d13de2e58d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13330.v
@@ -0,0 +1,17 @@
+Polymorphic Inductive path {A : Type} (x : A) : A -> Type :=
+  refl : path x x.
+
+Goal False.
+Proof.
+simple refine (let H : False := _ in _).
++ exact_no_check I.
++ assert (path true false -> path false true).
+  (** Create a dummy polymorphic side-effect *)
+  {
+    intro IHn.
+    rewrite IHn.
+    reflexivity.
+  }
+  exact H.
+Fail Qed.
+Abort.