Merge PR #17853: Fix #17852 (universe issue with reverse coercions)

Reviewed-by: SkySkimmer Co-authored-by: gares <gares@users.noreply.github.com>
coq · Jul 15, 2023 · 9066520 · 9066520
2 parents 72e72dc + 03d078f
commit 9066520
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 0 deletions.
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
@@ -650,6 +650,12 @@ let add_reverse_coercion env sigma v'_ty v_ty v' v =
   match Coqlib.lib_ref_opt "core.coercion.reverse_coercion" with
   | None -> sigma, v'
   | Some reverse_coercion ->
+     let sigma, v'_ty =
+       Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible
+         (Some false) env sigma v'_ty in
+     let sigma, v_ty =
+       Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible
+         (Some false) env sigma v_ty in
      let sigma, reverse_coercion = Evd.fresh_global env sigma reverse_coercion in
      Typing.checked_appvect env sigma reverse_coercion [| v'_ty; v_ty; v'; v |]
 

diff --git a/test-suite/bugs/bug_17852.v b/test-suite/bugs/bug_17852.v
@@ -0,0 +1,26 @@
+Module Ex0.
+
+Record S : Type := Pack { sort :> Type }.
+
+Canonical SSet := Pack Set.
+
+Check Set : S.
+(* Error: Anomaly "Unable to handle arbitrary u+k <= v constraints." *)
+
+End Ex0.
+
+Module Ex1.
+
+Record type : Type := Pack { sort :> nat -> Type }.
+
+Definition set := fun _ : nat => Set.
+
+Canonical inst := Pack set.
+
+Set Printing All.
+Set Printing Universes.
+
+Check set : type.
+(* Error: Anomaly "Unable to handle arbitrary u+k <= v constraints." *)
+
+End Ex1.