From d9fcfd71d992e99108c8b419647d0478dadc6667 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Oct 2022 07:18:27 -0700 Subject: [PATCH] fix: missing test --- src/Lean/Compiler/LCNF/MonoTypes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/MonoTypes.lean b/src/Lean/Compiler/LCNF/MonoTypes.lean index e8f828858a..3d41428026 100644 --- a/src/Lean/Compiler/LCNF/MonoTypes.lean +++ b/src/Lean/Compiler/LCNF/MonoTypes.lean @@ -42,7 +42,7 @@ Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t. def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo) := do if isRuntimeBultinType declName then return none let .inductInfo info ← getConstInfo declName | return none - if info.isUnsafe then return none + if info.isUnsafe || info.isRec then return none let [ctorName] := info.ctors | return none let mask ← getRelevantCtorFields ctorName let mut result := none