diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean
index 322231ff65..ddcd04417d 100644
--- a/src/Init/Control/Id.lean
+++ b/src/Init/Control/Id.lean
@@ -33,6 +33,9 @@ instance : Monad Id :=
 @[inline] protected def run {α : Type u} (x : Id α) : α :=
 x
 
+instance {α} [HasOfNat α] : HasOfNat (Id α) :=
+inferInstanceAs (HasOfNat α)
+
 instance : MonadRun id Id :=
 ⟨@Id.run⟩