From f8bf68a9afaa03457198b1d10bd33ca1bcc35658 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Oct 2019 13:10:54 -0700
Subject: [PATCH] chore: invoke `inferCtorSummaries` from IR compiler

---
 library/Init/Lean/Compiler/IR/Default.lean         | 2 ++
 library/Init/Lean/Compiler/IR/UnreachBranches.lean | 3 ++-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/library/Init/Lean/Compiler/IR/Default.lean b/library/Init/Lean/Compiler/IR/Default.lean
index 7cd3b19e5e..8c183cb254 100644
--- a/library/Init/Lean/Compiler/IR/Default.lean
+++ b/library/Init/Lean/Compiler/IR/Default.lean
@@ -18,6 +18,7 @@ import Init.Lean.Compiler.IR.Boxing
 import Init.Lean.Compiler.IR.RC
 import Init.Lean.Compiler.IR.ExpandResetReuse
 import Init.Lean.Compiler.IR.UnboxResult
+import Init.Lean.Compiler.IR.UnreachBranches
 import Init.Lean.Compiler.IR.EmitC
 
 namespace Lean
@@ -27,6 +28,7 @@ private def compileAux (decls : Array Decl) : CompilerM Unit :=
 do
 logDecls `init decls;
 checkDecls decls;
+inferCtorSummaries decls;
 let decls := decls.map Decl.pushProj;
 logDecls `push_proj decls;
 let decls := decls.map Decl.insertResetReuse;
diff --git a/library/Init/Lean/Compiler/IR/UnreachBranches.lean b/library/Init/Lean/Compiler/IR/UnreachBranches.lean
index 3c128d30a9..d62db15521 100644
--- a/library/Init/Lean/Compiler/IR/UnreachBranches.lean
+++ b/library/Init/Lean/Compiler/IR/UnreachBranches.lean
@@ -222,8 +222,9 @@ def inferStep : M Bool :=
 do ctx ← read;
    ctx.decls.size.mfold (fun idx modified => do
      match ctx.decls.get! idx with
-     | Decl.fdecl _ ys _ b => do
+     | Decl.fdecl fid ys _ b => do
        s ← get;
+       -- dbgTrace (">> " ++ toString fid) $ fun _ =>
        let currVals := s.funVals.get! idx;
        adaptReader (fun (ctx : InterpContext) => { currFnIdx := idx, .. ctx }) $ do
          ys.mfor $ fun y => updateVarAssignment y.x top;