From 7dbfaf9b751917a7fe020485bf57f41fdddcaafa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 7 Aug 2022 09:24:18 -0700
Subject: [PATCH] fix: bug at `mkSizeOfSpecLemmaInstance`

closes #1441
---
 src/Lean/Meta/SizeOf.lean | 6 ++++--
 tests/lean/run/1441.lean  | 2 ++
 2 files changed, 6 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1441.lean

diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index 9d5f136738..a709ef14c1 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -185,11 +185,13 @@ def mkSizeOfSpecLemmaName (ctorName : Name) : Name :=
 def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr :=
   matchConstCtor ctorApp.getAppFn (fun _ => throwError "failed to apply 'sizeOf' spec, constructor expected{indentExpr ctorApp}") fun ctorInfo _ => do
     let ctorArgs     := ctorApp.getAppArgs
-    let ctorFields   := ctorArgs[ctorArgs.size - ctorInfo.numFields:]
+    let ctorParams   := ctorArgs[:ctorInfo.numParams]
+    let ctorFields   := ctorArgs[ctorInfo.numParams:]
     let lemmaName  := mkSizeOfSpecLemmaName ctorInfo.name
     let lemmaInfo  ← getConstInfo lemmaName
     let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size
-    let lemmaArgMask := mkArray (lemmaArity - ctorInfo.numFields) (none (α := Expr))
+    let lemmaArgMask := ctorParams.toArray.map some
+    let lemmaArgMask := lemmaArgMask ++ mkArray (lemmaArity - ctorInfo.numParams - ctorInfo.numFields) (none (α := Expr))
     let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some
     mkAppOptM lemmaName lemmaArgMask
 
diff --git a/tests/lean/run/1441.lean b/tests/lean/run/1441.lean
new file mode 100644
index 0000000000..b50109323d
--- /dev/null
+++ b/tests/lean/run/1441.lean
@@ -0,0 +1,2 @@
+inductive MsgEmbed where
+  | trace : Sum (Array MsgEmbed) Unit → MsgEmbed