diff --git a/library/Init/Lean/Meta/InferType.lean b/library/Init/Lean/Meta/InferType.lean
index f944a4dc8a..88a8722bff 100644
--- a/library/Init/Lean/Meta/InferType.lean
+++ b/library/Init/Lean/Meta/InferType.lean
@@ -100,8 +100,7 @@ do typeType ← inferType type;
     (inferType : Expr → MetaM Expr)
     (e : Expr) : MetaM Expr :=
 forallTelescope whnf e $ fun xs e => do
-  type ← inferType e;
-  lvl  ← getLevel whnf inferType type;
+  lvl  ← getLevel whnf inferType e;
   lvl  ← xs.foldrM
     (fun x lvl => do
       xType    ← inferType x;