diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index 1b83ca4198..fb73ae1550 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -290,6 +290,12 @@ between e.g. `↑x + ↑y` and `↑(x + y)`.
 -/
 syntax:1024 (name := coeNotation) "↑" term:1024 : term
 
+/-- `⇑ t` coerces `t` to a function. -/
+syntax:1024 (name := coeFunNotation) "⇑" term:1024 : term
+
+/-- `↥ t` coerces `t` to a type. -/
+syntax:1024 (name := coeSortNotation) "↥" term:1024 : term
+
 /-! # Basic instances -/
 
 instance boolToProp : Coe Bool Prop where
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 08ba15eec8..87d783870f 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -485,6 +485,13 @@ existing code. It may be removed in a future version of the library.
 -/
 syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr
 
+/--
+The `@[coe]` attribute on a function (which should also appear in a
+`instance : Coe A B := ⟨myFn⟩` declaration) allows the delaborator to show
+applications of this function as `↑` when printing expressions.
+-/
+syntax (name := Attr.coe) "coe" : attr
+
 /--
 When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
 a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 582135b9af..08d7562c45 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -19,6 +19,20 @@ open Meta
     throwError "invalid coercion notation, expected type is not known"
   ensureHasType expectedType? e
 
+@[builtin_term_elab coeFunNotation] def elabCoeFunNotation : TermElab := fun stx _ => do
+  let x ← elabTerm stx none
+  if let some ty ← coerceToFunction? x then
+    return ty
+  else
+    throwError "cannot coerce to function{indentExpr x}"
+
+@[builtin_term_elab coeSortNotation] def elabCoeSortNotation : TermElab := fun stx _ => do
+  let x ← elabTerm stx none
+  if let some ty ← coerceToSort? x then
+    return ty
+  else
+    throwError "cannot coerce to sort{indentExpr x}"
+
 @[builtin_term_elab anonymousCtor] def elabAnonymousCtor : TermElab := fun stx expectedType? =>
   match stx with
   | `(⟨$args,*⟩) => do
diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean
index 0b70d2aca7..0a07f6bf5c 100644
--- a/src/Lean/Meta.lean
+++ b/src/Lean/Meta.lean
@@ -43,3 +43,4 @@ import Lean.Meta.CasesOn
 import Lean.Meta.ExprLens
 import Lean.Meta.ExprTraverse
 import Lean.Meta.Eval
+import Lean.Meta.CoeAttr
diff --git a/src/Lean/Meta/CoeAttr.lean b/src/Lean/Meta/CoeAttr.lean
new file mode 100644
index 0000000000..5a2449505b
--- /dev/null
+++ b/src/Lean/Meta/CoeAttr.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2022 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Mario Carneiro, Leonardo de Moura
+-/
+import Lean.Attributes
+import Lean.ScopedEnvExtension
+import Lean.Meta.FunInfo
+
+/-!
+# The `@[coe]` attribute, used to delaborate coercion functions as `↑`
+
+When writing a coercion, if the pattern
+```
+@[coe]
+def A.toB (a : A) : B := sorry
+
+instance : Coe A B where coe := A.toB
+```
+is used, then `A.toB a` will be pretty-printed as `↑a`.
+-/
+
+namespace Lean.Meta
+
+/-- The different types of coercions that are supported by the `coe` attribute. -/
+inductive CoeFnType
+  /-- The basic coercion `↑x`, see `CoeT.coe` -/
+  | coe
+  /-- The coercion to a function type, see `CoeFun.coe` -/
+  | coeFun
+  /-- The coercion to a type, see `CoeSort.coe` -/
+  | coeSort
+  deriving Inhabited, Repr, DecidableEq
+
+instance : ToExpr CoeFnType where
+  toTypeExpr := mkConst ``CoeFnType
+  toExpr := open CoeFnType in fun
+    | coe => mkConst ``coe
+    | coeFun => mkConst ``coeFun
+    | coeSort => mkConst ``coeSort
+
+/-- Information associated to a coercion function to enable sensible delaboration. -/
+structure CoeFnInfo where
+  /-- The number of arguments to the coercion function -/
+  numArgs : Nat
+  /-- The argument index that represents the value being coerced -/
+  coercee : Nat
+  /-- The type of coercion -/
+  type : CoeFnType
+  deriving Inhabited, Repr
+
+instance : ToExpr CoeFnInfo where
+  toTypeExpr := mkConst ``CoeFnInfo
+  toExpr | ⟨a, b, c⟩ => mkApp3 (mkConst ``CoeFnInfo.mk) (toExpr a) (toExpr b) (toExpr c)
+
+/-- The environment extension for tracking coercion functions for delaboration -/
+-- TODO: does it need to be a scoped extension
+initialize coeExt : SimpleScopedEnvExtension (Name × CoeFnInfo) (NameMap CoeFnInfo) ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun st (n, i) => st.insert n i
+    initial := {}
+  }
+
+/-- Lookup the coercion information for a given function -/
+def getCoeFnInfo? (fn : Name) : CoreM (Option CoeFnInfo) :=
+  return (coeExt.getState (← getEnv)).find? fn
+
+/-- Add `name` to the coercion extension and add a coercion delaborator for the function. -/
+def registerCoercion (name : Name) (info : Option CoeFnInfo := none) : MetaM Unit := do
+  let info ← match info with | some info => pure info | none => do
+    let fnInfo ← getFunInfo (← mkConstWithLevelParams name)
+    let some coercee := fnInfo.paramInfo.findIdx? (·.binderInfo.isExplicit)
+      | throwError "{name} has no explicit arguments"
+    pure { numArgs := coercee + 1, coercee, type := .coe }
+  modifyEnv fun env => coeExt.addEntry env (name, info)
+
+builtin_initialize registerBuiltinAttribute {
+  name := `coe
+  descr := "Adds a definition as a coercion"
+  add := fun decl _stx kind => MetaM.run' do
+    unless kind == .global do
+      throwError "cannot add local or scoped coe attribute"
+    registerCoercion decl
+}
+
+end Lean.Meta
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index c5c036cac7..52d03c05a2 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -1,13 +1,13 @@
 /-
 Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
+Authors: Sebastian Ullrich, Leonardo de Moura, Gabriel Ebner, Mario Carneiro
 -/
-
+import Lean.Parser
 import Lean.PrettyPrinter.Delaborator.Basic
 import Lean.PrettyPrinter.Delaborator.SubExpr
 import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
-import Lean.Parser
+import Lean.Meta.CoeAttr
 
 namespace Lean.PrettyPrinter.Delaborator
 open Lean.Meta
@@ -315,7 +315,8 @@ Default delaborator for applications.
 -/
 @[builtin_delab app]
 def delabApp : Delab := do
-  delabAppCore (← getExpr).getAppNumArgs delabAppFn
+  let e ← getExpr
+  delabAppCore e.getAppNumArgs delabAppFn
 
 /--
 The `withOverApp` combinator allows delaborators to handle "over-application" by using the core
@@ -340,6 +341,27 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
   else
     delabAppCore (n - arity) x
 
+/--
+This delaborator tries to elide functions which are known coercions.
+For example, `Int.ofNat` is a coercion, so instead of printing `ofNat n` we just print `↑n`,
+and when re-parsing this we can (usually) recover the specific coercion being used.
+-/
+@[builtin_delab app]
+def coeDelaborator : Delab := whenPPOption getPPCoercions do
+  let e ← getExpr
+  let .const declName _ := e.getAppFn | failure
+  let some info ← Meta.getCoeFnInfo? declName | failure
+  let n := e.getAppNumArgs
+  withOverApp info.numArgs do
+    match info.type with
+    | .coe => `(↑$(← withNaryArg info.coercee delab))
+    | .coeFun =>
+      if n = info.numArgs then
+        `(⇑$(← withNaryArg info.coercee delab))
+      else
+        withNaryArg info.coercee delab
+    | .coeSort => `(↥$(← withNaryArg info.coercee delab))
+
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where
   info        : MatcherInfo
diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out
index 59be053f7b..f3853cafdc 100644
--- a/tests/lean/1021.lean.expected.out
+++ b/tests/lean/1021.lean.expected.out
@@ -1,8 +1,8 @@
-some { range := { pos := { line := 175, column := 42 },
+some { range := { pos := { line := 189, column := 42 },
              charUtf16 := 42,
-             endPos := { line := 181, column := 31 },
+             endPos := { line := 195, column := 31 },
              endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 175, column := 46 },
+  selectionRange := { pos := { line := 189, column := 46 },
                       charUtf16 := 46,
-                      endPos := { line := 175, column := 58 },
+                      endPos := { line := 189, column := 58 },
                       endCharUtf16 := 58 } }
diff --git a/tests/lean/coeAttr1.lean b/tests/lean/coeAttr1.lean
new file mode 100644
index 0000000000..8c9171fd05
--- /dev/null
+++ b/tests/lean/coeAttr1.lean
@@ -0,0 +1,11 @@
+@[coe] def f (n : Nat) : String :=
+  toString n
+
+#check f 10
+
+instance : Coe Nat String where
+  coe := f
+
+def g (n : String) := n
+
+#check fun x : Nat => g x
diff --git a/tests/lean/coeAttr1.lean.expected.out b/tests/lean/coeAttr1.lean.expected.out
new file mode 100644
index 0000000000..f777fe6e6d
--- /dev/null
+++ b/tests/lean/coeAttr1.lean.expected.out
@@ -0,0 +1,2 @@
+↑10 : String
+fun x => g ↑x : Nat → String