diff --git a/library/Init/Lean/Meta/InferType.lean b/library/Init/Lean/Meta/InferType.lean
index dbdc6e3e25..e3cc4d98e8 100644
--- a/library/Init/Lean/Meta/InferType.lean
+++ b/library/Init/Lean/Meta/InferType.lean
@@ -37,9 +37,9 @@ do env ← getEnv;
    match env.find c with
    | some cinfo =>
      if cinfo.lparams.length == lvls.length then
-       throwEx $ Exception.incorrectNumOfLevels c lvls
-     else
        pure $ cinfo.instantiateTypeLevelParams lvls
+     else
+       throwEx $ Exception.incorrectNumOfLevels c lvls
    | none =>
      throwEx $ Exception.unknownConst c