From 0ca664107a1e60dfa47aa7536e30a348456efe44 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Nov 2020 21:36:51 +0100
Subject: 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.
---
 kernel/safe_typing.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3