fix: ensure inferForallType at LCNF handles universes like the kernel and MetaM

src/Lean/Compiler/LCNF/InferType.lean

@@ -263,10 +263,10 @@ mutual
         let e := e.instantiateRev fvars
         let some u ← getLevel? e | return anyTypeExpr
         let mut u := u
-        for x in fvars do
+        for x in fvars.reverse do
           let xType ← inferType x
           let some v ← getLevel? xType | return anyTypeExpr
-          u := .imax v u
+          u := mkLevelIMax' v u
         return .sort u.normalize
 
   partial def inferLambdaType (e : Expr) : InferTypeM Expr :=

tests/lean/run/inferForallTypeLCNF.lean

@@ -0,0 +1,7 @@
+import Lean
+
+variable {U V}
+
+def f : (U → V) → (U → U) := sorry
+
+#eval Lean.Compiler.compile #[``f]