diff --git a/library/system/IO.lean b/library/system/IO.lean
index 42a9020a21..8ce8090adb 100644
--- a/library/system/IO.lean
+++ b/library/system/IO.lean
@@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
 -/
-constant IO : Type → Type
+constant IO.{l} : Type.{l} → Type.{l}
 constant functorIO : functor IO
 constant monadIO : monad IO