From c0ac2138f7eda7cac7bfa3ad0698eef5ac02fdea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Sep 2022 16:38:16 -0700 Subject: [PATCH] fix: ensure `inferForallType` at LCNF handles universes like the kernel and `MetaM` --- src/Lean/Compiler/LCNF/InferType.lean | 4 ++-- tests/lean/run/inferForallTypeLCNF.lean | 7 +++++++ 2 files changed, 9 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/inferForallTypeLCNF.lean diff --git a/src/Lean/Compiler/LCNF/InferType.lean b/src/Lean/Compiler/LCNF/InferType.lean index d085062cdf..e3c64673ba 100644 --- a/src/Lean/Compiler/LCNF/InferType.lean +++ b/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 := diff --git a/tests/lean/run/inferForallTypeLCNF.lean b/tests/lean/run/inferForallTypeLCNF.lean new file mode 100644 index 0000000000..f2cf58879d --- /dev/null +++ b/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]