diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 86dd59a674..6e5ad2c9c4 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -18,7 +18,7 @@ inductive Except (ε : Type u) (α : Type v)
 
 attribute [unbox] Except
 
-instance {ε α : Type} [Inhabited ε] : Inhabited (Except ε α) :=
+instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) :=
 ⟨Except.error (arbitrary ε)⟩
 
 section