Fix #11553: magicaly_constant_of_fixbody checks existence of made up constant

2 files changed, 52 insertions, 19 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4d4fe13983..d5beebe690 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -722,32 +722,31 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
     let open UnivProblem in
-    try
-      let (cst_mod,_) = Constant.repr2 reference in
-      let cst = Constant.make2 cst_mod (Label.of_id id) in
+    let (cst_mod,_) = Constant.repr2 reference in
+    let cst = Constant.make2 cst_mod (Label.of_id id) in
+    if not (Environ.mem_constant cst env) then bd
+    else
       let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
         let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
         begin match csts with
-        | Some csts ->
-          let subst = Set.fold (fun cst acc ->
-              let l, r = match cst with
-                | ULub (u, v) | UWeak (u, v) -> u, v
-                | UEq (u, v) | ULe (u, v) ->
-                  let get u = Option.get (Universe.level u) in
-                  get u, get v
-              in
-            Univ.LMap.add l r acc)
-            csts Univ.LMap.empty
-          in
-          let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
-          mkConstU (cst, EInstance.make inst)
-        | None -> bd
+          | Some csts ->
+            let subst = Set.fold (fun cst acc ->
+                let l, r = match cst with
+                  | ULub (u, v) | UWeak (u, v) -> u, v
+                  | UEq (u, v) | ULe (u, v) ->
+                    let get u = Option.get (Universe.level u) in
+                    get u, get v
+                in
+                Univ.LMap.add l r acc)
+                csts Univ.LMap.empty
+            in
+            let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
+            mkConstU (cst, EInstance.make inst)
+          | None -> bd
         end
-    with
-    | Not_found -> bd
 
 let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
diff --git a/test-suite/bugs/closed/bug_11553.v b/test-suite/bugs/closed/bug_11553.v
new file mode 100644
index 0000000000..a4a4353cd6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11553.v
@@ -0,0 +1,34 @@
+Definition var := nat.
+Module Import A.
+Class Rename (term : Type) := rename : (var -> var) -> term -> term.
+End A.
+
+Inductive tm : Type :=
+  (* | tv : vl_ -> tm *)
+ with vl_ : Type :=
+  | var_vl : var -> vl_.
+
+Definition vl := vl_.
+
+Fixpoint tm_rename (sb : var -> var) (t : tm) : tm :=
+  let b := vl_rename : Rename vl in
+  match t with
+  end
+with
+vl_rename (sb : var -> var) v : vl :=
+  let a := tm_rename : Rename tm in
+  let b := vl_rename : Rename vl in
+  match v with
+  | var_vl x => var_vl (sb x)
+  end.
+
+Instance rename_vl : Rename vl := vl_rename.
+
+Lemma foo ξ x: rename_vl ξ (var_vl x) = var_vl x.
+(* Succeeds *)
+cbn. Abort.
+
+Lemma foo ξ x: rename ξ (var_vl x) = var_vl x.
+(* Fails *)
+cbn.
+Abort.