fix: lambdaBoundedTelescope at Compiler/Check.lean

src/Lean/Compiler/Check.lean

@@ -21,7 +21,7 @@ def lambdaBoundedTelescope (e : Expr) (n : Nat) (k : Array Expr → Expr → Inf
 where
   go (e : Expr) (i : Nat) (xs : Array Expr) : InferTypeM α :=
     match i with
-    | 0 => k xs e
+    | 0 => k xs (e.instantiateRev xs)
     | i+1 => match e with
       | .lam n d b bi =>
         withLocalDecl n (d.instantiateRev xs) bi fun x => go b i (xs.push x)

tests/lean/run/lcnf1.lean

@@ -50,3 +50,14 @@ def Vec.head : Vec α (n+1) → α
 set_option profiler true
 set_option trace.Compiler.step true
 #eval Compiler.compile #[``Lean.Meta.isExprDefEqAuxImpl]
+
+def foo (a b : Nat) :=
+  let d := match a with
+  | .zero => b
+  | .succ c => c
+  let e := match b with
+  | .zero => a
+  | .succ f => f
+  Nat.add d e
+
+#eval Compiler.compile #[``foo]