From 4c19fdbb973cc68fe8a0812e5a08ed518ce8c2a7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Sep 2022 21:39:52 -0700
Subject: [PATCH] fix: `normFVarImp` bug

---
 src/Lean/Compiler/LCNF/CompilerM.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/CompilerM.lean b/src/Lean/Compiler/LCNF/CompilerM.lean
index d3c5a82996..7b345ead46 100644
--- a/src/Lean/Compiler/LCNF/CompilerM.lean
+++ b/src/Lean/Compiler/LCNF/CompilerM.lean
@@ -124,9 +124,9 @@ where
     else
       e
 
-private def normFVarImp (s : FVarSubst) (fvarId : FVarId) : FVarId :=
+private partial def normFVarImp (s : FVarSubst) (fvarId : FVarId) : FVarId :=
   match s.find? fvarId with
-  | some (.fvar fvarId') => fvarId'
+  | some (.fvar fvarId') => normFVarImp s fvarId'
   | some _ => panic! "invalid LCNF substitution of free variable with expression"
   | none => fvarId