diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean
index 015f9b38d..bda2e0bf7 100644
--- a/library/algebra/relation.lean
+++ b/library/algebra/relation.lean
@@ -23,10 +23,10 @@ mk : reflexive R → is_reflexive R
 
 namespace is_reflexive
 
-  definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_reflexive R) : reflexive R :=
+  definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_reflexive R) : reflexive R :=
   is_reflexive.rec (λu, u) C
 
-  definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_reflexive R} : reflexive R :=
+  definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_reflexive R} : reflexive R :=
   is_reflexive.rec (λu, u) C
 
 end is_reflexive
@@ -37,10 +37,10 @@ mk : symmetric R → is_symmetric R
 
 namespace is_symmetric
 
-  definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_symmetric R) : symmetric R :=
+  definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_symmetric R) : symmetric R :=
   is_symmetric.rec (λu, u) C
 
-  definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_symmetric R} : symmetric R :=
+  definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_symmetric R} : symmetric R :=
   is_symmetric.rec (λu, u) C
 
 end is_symmetric
@@ -51,10 +51,10 @@ mk : transitive R → is_transitive R
 
 namespace is_transitive
 
-  definition app ⦃T : Type⦄ {R : T → T → Type} (C : is_transitive R) : transitive R :=
+  definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_transitive R) : transitive R :=
   is_transitive.rec (λu, u) C
 
-  definition infer ⦃T : Type⦄ (R : T → T → Type) {C : is_transitive R} : transitive R :=
+  definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_transitive R} : transitive R :=
   is_transitive.rec (λu, u) C
 
 end is_transitive
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 61853a22a..a25786d8b 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1054,8 +1054,8 @@ std::tuple<expr, level_param_names> elaborator::operator()(list<expr> const & ct
     auto p  = solve(cs).pull();
     lean_assert(p);
     substitution s = p->first.first;
-    check_sort_assignments(s);
     auto result = apply(s, r);
+    check_sort_assignments(s);
     copy_info_to_manager(s);
     return result;
 }
@@ -1081,11 +1081,11 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(
     auto p  = solve(cs).pull();
     lean_assert(p);
     substitution s = p->first.first;
-    check_sort_assignments(s);
     name_set univ_params = collect_univ_params(r_v, collect_univ_params(r_t));
     buffer<name> new_params;
     expr new_r_t = apply(s, r_t, univ_params, new_params);
     expr new_r_v = apply(s, r_v, univ_params, new_params);
+    check_sort_assignments(s);
     copy_info_to_manager(s);
     return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end()));
 }