From 5dc1bbb18891fcdf685a9775de82581624555213 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Nov 2019 09:19:06 -0800
Subject: [PATCH] chore: normalize universe level

---
 library/Init/Lean/Meta/InferType.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/Init/Lean/Meta/InferType.lean b/library/Init/Lean/Meta/InferType.lean
index 88a8722bff..cad10a7872 100644
--- a/library/Init/Lean/Meta/InferType.lean
+++ b/library/Init/Lean/Meta/InferType.lean
@@ -107,7 +107,7 @@ forallTelescope whnf e $ fun xs e => do
       xTypeLvl ← getLevel whnf inferType xType;
       pure $ Level.imax xTypeLvl lvl)
     lvl;
-  pure $ Expr.sort lvl
+  pure $ Expr.sort lvl.normalize
 
 /- Infer type of lambda and let expressions -/
 @[specialize] private def inferLambdaType