From cab5e98780deb1bb65dbeef5d558376f8e34bccc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 Dec 2017 11:24:59 +0100
Subject: Fix #5368: Canonical structure unification fails.

Universe instances were lost during constructions of the canonical instance.
---
 pretyping/evarconv.ml         | 2 ++
 test-suite/bugs/closed/5368.v | 6 ++++++
 2 files changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/5368.v

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cb88446236..f7a3789a21 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -218,6 +218,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   let t' = EConstr.of_constr t' in
   let t' = subst_univs_level_constr subst t' in
   let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in
+  let params = List.map (fun c -> subst_univs_level_constr subst c) params in
+  let us = List.map (fun c -> subst_univs_level_constr subst c) us in
   let h, _ = decompose_app_vect sigma t' in
     ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
     (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
diff --git a/test-suite/bugs/closed/5368.v b/test-suite/bugs/closed/5368.v
new file mode 100644
index 0000000000..410fe1707d
--- /dev/null
+++ b/test-suite/bugs/closed/5368.v
@@ -0,0 +1,6 @@
+Set Universe Polymorphism.
+
+Record cantype := {T:Type; op:T -> unit}.
+Canonical Structure test (P:Type) := {| T := P -> Type; op := fun _ => tt|}.
+
+Check (op _ ((fun (_:unit) => Set):_)).
-- 
cgit v1.2.3