diff --git a/library/init/core.lean b/library/init/core.lean
index a1c1528c58..ecbe11f678 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -105,7 +105,7 @@ a
 @[reducible] def out_param (α : Sort u) : Sort u := α
 
 /-- Auxiliary declaration used to implement the notation (a : α) -/
-@[reducible] def typed_expr (α : Type u) (a : α) : α := a
+@[reducible] def typed_expr (α : Sort u) (a : α) : α := a
 
 /-
   id_rhs is an auxiliary declaration used in the equation compiler to address performance
diff --git a/tests/lean/run/1954.lean b/tests/lean/run/1954.lean
new file mode 100644
index 0000000000..e9e000a563
--- /dev/null
+++ b/tests/lean/run/1954.lean
@@ -0,0 +1,2 @@
+def all (p : ℕ → Prop) : Prop := ∀x, p x
+example {p : ℕ → Prop} (h : all p) : p 0 := ‹all p› 0