Fix universe abstraction for const_relevance of opaques

Fix coq#18594
SkySkimmer · Jan 31, 2024 · 9badbc2 · 9badbc2
1 parent 18b537d
commit 9badbc2
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 1 deletion.
diff --git a/kernel/constant_typing.ml b/kernel/constant_typing.ml
@@ -243,7 +243,7 @@ let infer_opaque ~sec_univs env entry =
     const_type = typ;
     const_body_code = tps;
     const_universes = univs;
-    const_relevance = Sorts.relevance_of_sort typj.utj_type;
+    const_relevance = UVars.subst_sort_level_relevance usubst @@ Sorts.relevance_of_sort typj.utj_type;
     const_inline_code = false;
     const_typing_flags = Environ.typing_flags env;
   }, context

diff --git a/test-suite/bugs/bug_18594.v b/test-suite/bugs/bug_18594.v
@@ -0,0 +1,12 @@
+Set Universe Polymorphism.
+
+Lemma foo@{s| |} (A:Type@{s|Set}) (a:A) : A.
+Proof.
+  exact a.
+Qed.
+
+Definition bar : foo nat = foo (id nat) := eq_refl.
+
+Fail Definition baz x y : foo nat x = foo nat y := eq_refl.
+
+Definition baz' (A:SProp) (f:A->nat) x y : f (foo A x) = f (foo A y) := eq_refl.