diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean
index 209967f59d..8be04fd32b 100644
--- a/src/Init/SizeOf.lean
+++ b/src/Init/SizeOf.lean
@@ -41,7 +41,11 @@ for every element of `α`.
 protected def default.sizeOf (α : Sort u) : α → Nat
   | _ => 0
 
-instance (priority := low) (α : Sort u) : SizeOf α where
+/--
+Every type `α` has a low priority default `SizeOf` instance that just returns `0`
+for every element of `α`.
+-/
+instance (priority := low) instSizeOfDefault (α : Sort u) : SizeOf α where
   sizeOf := default.sizeOf α
 
 @[simp] theorem sizeOf_default (n : α) : sizeOf n = 0 := rfl