From cdc2731401cc203e7e96a316d86f9ceef99f365d Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Tue, 1 Apr 2025 12:59:25 -0700
Subject: [PATCH] chore: derive more type classes for IR data structures
 (#7085)

---
 src/Lean/Compiler/IR/Basic.lean      | 3 ++-
 src/Lean/Compiler/IR/CtorLayout.lean | 1 +
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 2e35230020..fbce9ef632 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -180,7 +180,7 @@ structure CtorInfo where
   size : Nat
   usize : Nat
   ssize : Nat
-  deriving Repr
+  deriving Inhabited, Repr
 
 def CtorInfo.beq : CtorInfo → CtorInfo → Bool
   | ⟨n₁, cidx₁, size₁, usize₁, ssize₁⟩, ⟨n₂, cidx₂, size₂, usize₂, ssize₂⟩ =>
@@ -223,6 +223,7 @@ inductive Expr where
   | lit (v : LitVal)
   /-- Return `1 : uint8` Iff `RC(x) > 1` -/
   | isShared (x : VarId)
+  deriving Inhabited
 
 @[export lean_ir_mk_ctor_expr]  def mkCtorExpr (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Arg) : Expr :=
   Expr.ctor ⟨n, cidx, size, usize, ssize⟩ ys
diff --git a/src/Lean/Compiler/IR/CtorLayout.lean b/src/Lean/Compiler/IR/CtorLayout.lean
index 0b94b8516a..53b22376ca 100644
--- a/src/Lean/Compiler/IR/CtorLayout.lean
+++ b/src/Lean/Compiler/IR/CtorLayout.lean
@@ -15,6 +15,7 @@ inductive CtorFieldInfo where
   | object (i : Nat)
   | usize  (i : Nat)
   | scalar (sz : Nat) (offset : Nat) (type : IRType)
+  deriving Inhabited
 
 namespace CtorFieldInfo